Theorem bnj594 30236

Description: Technical lemma for bnj852 30245. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)

Hypotheses

Ref	Expression
bnj594.1	⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))
bnj594.2	⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))
bnj594.3	⊢ (𝜒 ↔ (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))
bnj594.7	⊢ 𝐷 = (ω ∖ {∅})
bnj594.9	⊢ (𝜑′ ↔ (𝑔‘∅) = pred(𝑥, 𝐴, 𝑅))
bnj594.10	⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑔‘suc 𝑖) = ∪ 𝑦 ∈ (𝑔‘𝑖) pred(𝑦, 𝐴, 𝑅)))
bnj594.11	⊢ (𝜒′ ↔ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))
bnj594.15	⊢ (𝜃 ↔ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗)))
bnj594.16	⊢ ([𝑘 / 𝑗]𝜃 ↔ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑘) = (𝑔‘𝑘)))
bnj594.17	⊢ (𝜏 ↔ ∀𝑘 ∈ 𝑛 (𝑘 E 𝑗 → [𝑘 / 𝑗]𝜃))

Assertion

Ref	Expression
bnj594	⊢ ((𝑗 ∈ 𝑛 ∧ 𝜏) → 𝜃)

Distinct variable groups:   𝐴,𝑖,𝑘   𝐷,𝑘   𝑅,𝑖,𝑘   𝜒,𝑘   𝑘,𝜒′   𝑓,𝑖,𝑘,𝑦   𝑔,𝑖,𝑘,𝑦   𝑖,𝑛,𝑘   𝑗,𝑘

Allowed substitution hints:   𝜑(𝑥,𝑦,𝑓,𝑔,𝑖,𝑗,𝑘,𝑛)   𝜓(𝑥,𝑦,𝑓,𝑔,𝑖,𝑗,𝑘,𝑛)   𝜒(𝑥,𝑦,𝑓,𝑔,𝑖,𝑗,𝑛)   𝜃(𝑥,𝑦,𝑓,𝑔,𝑖,𝑗,𝑘,𝑛)   𝜏(𝑥,𝑦,𝑓,𝑔,𝑖,𝑗,𝑘,𝑛)   𝐴(𝑥,𝑦,𝑓,𝑔,𝑗,𝑛)   𝐷(𝑥,𝑦,𝑓,𝑔,𝑖,𝑗,𝑛)   𝑅(𝑥,𝑦,𝑓,𝑔,𝑗,𝑛)   𝜑′(𝑥,𝑦,𝑓,𝑔,𝑖,𝑗,𝑘,𝑛)   𝜓′(𝑥,𝑦,𝑓,𝑔,𝑖,𝑗,𝑘,𝑛)   𝜒′(𝑥,𝑦,𝑓,𝑔,𝑖,𝑗,𝑛)

Proof of Theorem bnj594

Step	Hyp	Ref	Expression
1		bnj594.3	. . . . . . . . 9 ⊢ (𝜒 ↔ (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))
2	1	simp2bi 1070	. . . . . . . 8 ⊢ (𝜒 → 𝜑)
3		bnj594.1	. . . . . . . 8 ⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))
4	2, 3	sylib 207	. . . . . . 7 ⊢ (𝜒 → (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))
5		bnj594.11	. . . . . . . . 9 ⊢ (𝜒′ ↔ (𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′))
6	5	simp2bi 1070	. . . . . . . 8 ⊢ (𝜒′ → 𝜑′)
7		bnj594.9	. . . . . . . 8 ⊢ (𝜑′ ↔ (𝑔‘∅) = pred(𝑥, 𝐴, 𝑅))
8	6, 7	sylib 207	. . . . . . 7 ⊢ (𝜒′ → (𝑔‘∅) = pred(𝑥, 𝐴, 𝑅))
9		eqtr3 2631	. . . . . . 7 ⊢ (((𝑓‘∅) = pred(𝑥, 𝐴, 𝑅) ∧ (𝑔‘∅) = pred(𝑥, 𝐴, 𝑅)) → (𝑓‘∅) = (𝑔‘∅))
10	4, 8, 9	syl2an 493	. . . . . 6 ⊢ ((𝜒 ∧ 𝜒′) → (𝑓‘∅) = (𝑔‘∅))
11	10	3adant1 1072	. . . . 5 ⊢ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘∅) = (𝑔‘∅))
12		fveq2 6103	. . . . . 6 ⊢ (𝑗 = ∅ → (𝑓‘𝑗) = (𝑓‘∅))
13		fveq2 6103	. . . . . 6 ⊢ (𝑗 = ∅ → (𝑔‘𝑗) = (𝑔‘∅))
14	12, 13	eqeq12d 2625	. . . . 5 ⊢ (𝑗 = ∅ → ((𝑓‘𝑗) = (𝑔‘𝑗) ↔ (𝑓‘∅) = (𝑔‘∅)))
15	11, 14	syl5ibr 235	. . . 4 ⊢ (𝑗 = ∅ → ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗)))
16		bnj594.15	. . . 4 ⊢ (𝜃 ↔ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗)))
17	15, 16	sylibr 223	. . 3 ⊢ (𝑗 = ∅ → 𝜃)
18	17	a1d 25	. 2 ⊢ (𝑗 = ∅ → ((𝑗 ∈ 𝑛 ∧ 𝜏) → 𝜃))
19		bnj253 30023	. . . . . 6 ⊢ ((𝑛 ∈ 𝐷 ∧ 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) ↔ ((𝑛 ∈ 𝐷 ∧ 𝑛 ∈ 𝐷) ∧ 𝜒 ∧ 𝜒′))
20		bnj252 30022	. . . . . 6 ⊢ ((𝑛 ∈ 𝐷 ∧ 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) ↔ (𝑛 ∈ 𝐷 ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)))
21		anidm 674	. . . . . . 7 ⊢ ((𝑛 ∈ 𝐷 ∧ 𝑛 ∈ 𝐷) ↔ 𝑛 ∈ 𝐷)
22	21	3anbi1i 1246	. . . . . 6 ⊢ (((𝑛 ∈ 𝐷 ∧ 𝑛 ∈ 𝐷) ∧ 𝜒 ∧ 𝜒′) ↔ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′))
23	19, 20, 22	3bitr3i 289	. . . . 5 ⊢ ((𝑛 ∈ 𝐷 ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) ↔ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′))
24		df-bnj17 30006	. . . . . . . . . 10 ⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) ↔ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) ∧ 𝜏))
25		bnj594.17	. . . . . . . . . . . 12 ⊢ (𝜏 ↔ ∀𝑘 ∈ 𝑛 (𝑘 E 𝑗 → [𝑘 / 𝑗]𝜃))
26	25	bnj1095 30106	. . . . . . . . . . 11 ⊢ (𝜏 → ∀𝑘𝜏)
27	26	bnj1352 30152	. . . . . . . . . 10 ⊢ (((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) ∧ 𝜏) → ∀𝑘((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) ∧ 𝜏))
28	24, 27	hbxfrbi 1742	. . . . . . . . 9 ⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) → ∀𝑘(𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏))
29		bnj170 30017	. . . . . . . . . . . 12 ⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) ↔ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) ∧ 𝑗 ≠ ∅))
30		bnj594.7	. . . . . . . . . . . . . . 15 ⊢ 𝐷 = (ω ∖ {∅})
31	30	bnj923 30092	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ 𝐷 → 𝑛 ∈ ω)
32		elnn 6967	. . . . . . . . . . . . . 14 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ ω) → 𝑗 ∈ ω)
33	31, 32	sylan2 490	. . . . . . . . . . . . 13 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) → 𝑗 ∈ ω)
34	33	anim1i 590	. . . . . . . . . . . 12 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) ∧ 𝑗 ≠ ∅) → (𝑗 ∈ ω ∧ 𝑗 ≠ ∅))
35	29, 34	sylbi 206	. . . . . . . . . . 11 ⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) → (𝑗 ∈ ω ∧ 𝑗 ≠ ∅))
36		nnsuc 6974	. . . . . . . . . . 11 ⊢ ((𝑗 ∈ ω ∧ 𝑗 ≠ ∅) → ∃𝑘 ∈ ω 𝑗 = suc 𝑘)
37		rexex 2985	. . . . . . . . . . 11 ⊢ (∃𝑘 ∈ ω 𝑗 = suc 𝑘 → ∃𝑘 𝑗 = suc 𝑘)
38	35, 36, 37	3syl 18	. . . . . . . . . 10 ⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) → ∃𝑘 𝑗 = suc 𝑘)
39	38	bnj721 30081	. . . . . . . . 9 ⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) → ∃𝑘 𝑗 = suc 𝑘)
40	28, 39	bnj596 30070	. . . . . . . 8 ⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) → ∃𝑘((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) ∧ 𝑗 = suc 𝑘))
41		bnj667 30076	. . . . . . . . . . 11 ⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) → (𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏))
42	41	anim1i 590	. . . . . . . . . 10 ⊢ (((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) ∧ 𝑗 = suc 𝑘) → ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) ∧ 𝑗 = suc 𝑘))
43		bnj258 30027	. . . . . . . . . 10 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) ↔ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) ∧ 𝑗 = suc 𝑘))
44	42, 43	sylibr 223	. . . . . . . . 9 ⊢ (((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) ∧ 𝑗 = suc 𝑘) → (𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏))
45		df-bnj17 30006	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) ↔ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜏))
46		bnj219 30055	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = suc 𝑘 → 𝑘 E 𝑗)
47	46	3ad2ant3 1077	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) → 𝑘 E 𝑗)
48	47	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜏) → 𝑘 E 𝑗)
49		vex 3176	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑘 ∈ V
50	49	bnj216 30054	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = suc 𝑘 → 𝑘 ∈ 𝑗)
51		df-3an 1033	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) ↔ ((𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛) ∧ 𝑛 ∈ 𝐷))
52		3anrot 1036	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) ↔ (𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑘 ∈ 𝑗))
53		ancom 465	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛) ∧ 𝑛 ∈ 𝐷) ↔ (𝑛 ∈ 𝐷 ∧ (𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛)))
54	51, 52, 53	3bitr3i 289	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑘 ∈ 𝑗) ↔ (𝑛 ∈ 𝐷 ∧ (𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛)))
55		eldifi 3694	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ (ω ∖ {∅}) → 𝑛 ∈ ω)
56	55, 30	eleq2s 2706	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ 𝐷 → 𝑛 ∈ ω)
57		nnord 6965	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ ω → Ord 𝑛)
58		ordtr1 5684	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Ord 𝑛 → ((𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛) → 𝑘 ∈ 𝑛))
59	56, 57, 58	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ 𝐷 → ((𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛) → 𝑘 ∈ 𝑛))
60	59	imp 444	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ 𝐷 ∧ (𝑘 ∈ 𝑗 ∧ 𝑗 ∈ 𝑛)) → 𝑘 ∈ 𝑛)
61	54, 60	sylbi 206	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑘 ∈ 𝑗) → 𝑘 ∈ 𝑛)
62	50, 61	syl3an3 1353	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) → 𝑘 ∈ 𝑛)
63		rsp 2913	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑘 ∈ 𝑛 (𝑘 E 𝑗 → [𝑘 / 𝑗]𝜃) → (𝑘 ∈ 𝑛 → (𝑘 E 𝑗 → [𝑘 / 𝑗]𝜃)))
64	25, 63	sylbi 206	. . . . . . . . . . . . . . . . 17 ⊢ (𝜏 → (𝑘 ∈ 𝑛 → (𝑘 E 𝑗 → [𝑘 / 𝑗]𝜃)))
65	62, 64	mpan9 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜏) → (𝑘 E 𝑗 → [𝑘 / 𝑗]𝜃))
66	48, 65	mpd 15	. . . . . . . . . . . . . . 15 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜏) → [𝑘 / 𝑗]𝜃)
67	45, 66	sylbi 206	. . . . . . . . . . . . . 14 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) → [𝑘 / 𝑗]𝜃)
68	67	anim1i 590	. . . . . . . . . . . . 13 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) → ([𝑘 / 𝑗]𝜃 ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)))
69		bnj252 30022	. . . . . . . . . . . . 13 ⊢ (([𝑘 / 𝑗]𝜃 ∧ 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) ↔ ([𝑘 / 𝑗]𝜃 ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)))
70	68, 69	sylibr 223	. . . . . . . . . . . 12 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) → ([𝑘 / 𝑗]𝜃 ∧ 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′))
71		bnj446 30036	. . . . . . . . . . . . 13 ⊢ (([𝑘 / 𝑗]𝜃 ∧ 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) ↔ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) ∧ [𝑘 / 𝑗]𝜃))
72		bnj594.16	. . . . . . . . . . . . . 14 ⊢ ([𝑘 / 𝑗]𝜃 ↔ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑘) = (𝑔‘𝑘)))
73		pm3.35 609	. . . . . . . . . . . . . 14 ⊢ (((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) ∧ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑘) = (𝑔‘𝑘))) → (𝑓‘𝑘) = (𝑔‘𝑘))
74	72, 73	sylan2b 491	. . . . . . . . . . . . 13 ⊢ (((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) ∧ [𝑘 / 𝑗]𝜃) → (𝑓‘𝑘) = (𝑔‘𝑘))
75	71, 74	sylbi 206	. . . . . . . . . . . 12 ⊢ (([𝑘 / 𝑗]𝜃 ∧ 𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑘) = (𝑔‘𝑘))
76		iuneq1 4470	. . . . . . . . . . . 12 ⊢ ((𝑓‘𝑘) = (𝑔‘𝑘) → ∪ 𝑦 ∈ (𝑓‘𝑘) pred(𝑦, 𝐴, 𝑅) = ∪ 𝑦 ∈ (𝑔‘𝑘) pred(𝑦, 𝐴, 𝑅))
77	70, 75, 76	3syl 18	. . . . . . . . . . 11 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) → ∪ 𝑦 ∈ (𝑓‘𝑘) pred(𝑦, 𝐴, 𝑅) = ∪ 𝑦 ∈ (𝑔‘𝑘) pred(𝑦, 𝐴, 𝑅))
78		bnj658 30075	. . . . . . . . . . . . 13 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) → (𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘))
79	1	simp3bi 1071	. . . . . . . . . . . . . 14 ⊢ (𝜒 → 𝜓)
80	5	simp3bi 1071	. . . . . . . . . . . . . 14 ⊢ (𝜒′ → 𝜓′)
81	79, 80	bnj240 30018	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝜓 ∧ 𝜓′))
82	78, 81	anim12i 588	. . . . . . . . . . . 12 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) → ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ (𝜓 ∧ 𝜓′)))
83		simpl 472	. . . . . . . . . . . . 13 ⊢ ((𝜓 ∧ 𝜓′) → 𝜓)
84	83	anim2i 591	. . . . . . . . . . . 12 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ (𝜓 ∧ 𝜓′)) → ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜓))
85		simp3 1056	. . . . . . . . . . . . . 14 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) → 𝑗 = suc 𝑘)
86	85	anim1i 590	. . . . . . . . . . . . 13 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜓) → (𝑗 = suc 𝑘 ∧ 𝜓))
87		simpl1 1057	. . . . . . . . . . . . . 14 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘 ∧ 𝜓)) → 𝑗 ∈ 𝑛)
88		df-3an 1033	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ↔ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) ∧ 𝑗 = suc 𝑘))
89		ancom 465	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) ∧ 𝑗 = suc 𝑘) ↔ (𝑗 = suc 𝑘 ∧ (𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷)))
90	88, 89	bitri 263	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ↔ (𝑗 = suc 𝑘 ∧ (𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷)))
91		elnn 6967	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ 𝑗 ∧ 𝑗 ∈ ω) → 𝑘 ∈ ω)
92	50, 33, 91	syl2an 493	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 = suc 𝑘 ∧ (𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷)) → 𝑘 ∈ ω)
93	90, 92	sylbi 206	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) → 𝑘 ∈ ω)
94		bnj594.2	. . . . . . . . . . . . . . . . 17 ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))
95	94	bnj589 30233	. . . . . . . . . . . . . . . 16 ⊢ (𝜓 ↔ ∀𝑘 ∈ ω (suc 𝑘 ∈ 𝑛 → (𝑓‘suc 𝑘) = ∪ 𝑦 ∈ (𝑓‘𝑘) pred(𝑦, 𝐴, 𝑅)))
96	95	bnj590 30234	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 = suc 𝑘 ∧ 𝜓) → (𝑘 ∈ ω → (𝑗 ∈ 𝑛 → (𝑓‘𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑘) pred(𝑦, 𝐴, 𝑅))))
97	93, 96	mpan9 485	. . . . . . . . . . . . . 14 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘 ∧ 𝜓)) → (𝑗 ∈ 𝑛 → (𝑓‘𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑘) pred(𝑦, 𝐴, 𝑅)))
98	87, 97	mpd 15	. . . . . . . . . . . . 13 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘 ∧ 𝜓)) → (𝑓‘𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑘) pred(𝑦, 𝐴, 𝑅))
99	86, 98	syldan 486	. . . . . . . . . . . 12 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜓) → (𝑓‘𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑘) pred(𝑦, 𝐴, 𝑅))
100	82, 84, 99	3syl 18	. . . . . . . . . . 11 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) → (𝑓‘𝑗) = ∪ 𝑦 ∈ (𝑓‘𝑘) pred(𝑦, 𝐴, 𝑅))
101		simpr 476	. . . . . . . . . . . . 13 ⊢ ((𝜓 ∧ 𝜓′) → 𝜓′)
102	101	anim2i 591	. . . . . . . . . . . 12 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ (𝜓 ∧ 𝜓′)) → ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜓′))
103	85	anim1i 590	. . . . . . . . . . . . 13 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜓′) → (𝑗 = suc 𝑘 ∧ 𝜓′))
104		simpl1 1057	. . . . . . . . . . . . . 14 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘 ∧ 𝜓′)) → 𝑗 ∈ 𝑛)
105		bnj594.10	. . . . . . . . . . . . . . . . 17 ⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑔‘suc 𝑖) = ∪ 𝑦 ∈ (𝑔‘𝑖) pred(𝑦, 𝐴, 𝑅)))
106	105	bnj589 30233	. . . . . . . . . . . . . . . 16 ⊢ (𝜓′ ↔ ∀𝑘 ∈ ω (suc 𝑘 ∈ 𝑛 → (𝑔‘suc 𝑘) = ∪ 𝑦 ∈ (𝑔‘𝑘) pred(𝑦, 𝐴, 𝑅)))
107	106	bnj590 30234	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 = suc 𝑘 ∧ 𝜓′) → (𝑘 ∈ ω → (𝑗 ∈ 𝑛 → (𝑔‘𝑗) = ∪ 𝑦 ∈ (𝑔‘𝑘) pred(𝑦, 𝐴, 𝑅))))
108	93, 107	mpan9 485	. . . . . . . . . . . . . 14 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘 ∧ 𝜓′)) → (𝑗 ∈ 𝑛 → (𝑔‘𝑗) = ∪ 𝑦 ∈ (𝑔‘𝑘) pred(𝑦, 𝐴, 𝑅)))
109	104, 108	mpd 15	. . . . . . . . . . . . 13 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ (𝑗 = suc 𝑘 ∧ 𝜓′)) → (𝑔‘𝑗) = ∪ 𝑦 ∈ (𝑔‘𝑘) pred(𝑦, 𝐴, 𝑅))
110	103, 109	syldan 486	. . . . . . . . . . . 12 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘) ∧ 𝜓′) → (𝑔‘𝑗) = ∪ 𝑦 ∈ (𝑔‘𝑘) pred(𝑦, 𝐴, 𝑅))
111	82, 102, 110	3syl 18	. . . . . . . . . . 11 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) → (𝑔‘𝑗) = ∪ 𝑦 ∈ (𝑔‘𝑘) pred(𝑦, 𝐴, 𝑅))
112	77, 100, 111	3eqtr4d 2654	. . . . . . . . . 10 ⊢ (((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) → (𝑓‘𝑗) = (𝑔‘𝑗))
113	112	ex 449	. . . . . . . . 9 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝑗 = suc 𝑘 ∧ 𝜏) → ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗)))
114	44, 113	syl 17	. . . . . . . 8 ⊢ (((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) ∧ 𝑗 = suc 𝑘) → ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗)))
115	40, 114	bnj593 30069	. . . . . . 7 ⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) → ∃𝑘((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗)))
116		bnj258 30027	. . . . . . 7 ⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ∧ 𝜏) ↔ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝜏) ∧ 𝑛 ∈ 𝐷))
117		19.9v 1883	. . . . . . 7 ⊢ (∃𝑘((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗)) ↔ ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗)))
118	115, 116, 117	3imtr3i 279	. . . . . 6 ⊢ (((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝜏) ∧ 𝑛 ∈ 𝐷) → ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗)))
119	118	expimpd 627	. . . . 5 ⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝜏) → ((𝑛 ∈ 𝐷 ∧ (𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′)) → (𝑓‘𝑗) = (𝑔‘𝑗)))
120	23, 119	syl5bir 232	. . . 4 ⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝜏) → ((𝑛 ∈ 𝐷 ∧ 𝜒 ∧ 𝜒′) → (𝑓‘𝑗) = (𝑔‘𝑗)))
121	120, 16	sylibr 223	. . 3 ⊢ ((𝑗 ≠ ∅ ∧ 𝑗 ∈ 𝑛 ∧ 𝜏) → 𝜃)
122	121	3expib 1260	. 2 ⊢ (𝑗 ≠ ∅ → ((𝑗 ∈ 𝑛 ∧ 𝜏) → 𝜃))
123	18, 122	pm2.61ine 2865	1 ⊢ ((𝑗 ∈ 𝑛 ∧ 𝜏) → 𝜃)

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475  ∃wex 1695   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  [wsbc 3402   ∖ cdif 3537  ∅c0 3874  {csn 4125  ∪ ciun 4455   class class class wbr 4583   E cep 4947  Ord word 5639  suc csuc 5642   Fn wfn 5799  ‘cfv 5804  ωcom 6957   ∧ w-bnj17 30005   predc-bnj14 30007

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-tr 4681  df-eprel 4949  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fv 5812  df-om 6958  df-bnj17 30006

This theorem is referenced by:  bnj580  30237