Theorem axdc4lem 9871

Description: Lemma for axdc4 9872. (Contributed by Mario Carneiro, 31-Jan-2013.) (Revised by Mario Carneiro, 16-Nov-2013.)

Hypotheses

Ref	Expression
axdc4lem.1	⊢ 𝐴 ∈ V
axdc4lem.2	⊢ 𝐺 = (𝑛 ∈ ω, 𝑥 ∈ 𝐴 ↦ ({suc 𝑛} × (𝑛𝐹𝑥)))

Assertion

Ref	Expression
axdc4lem	⊢ ((𝐶 ∈ 𝐴 ∧ 𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘))))

Distinct variable groups:   𝑔,𝑘,𝑛,𝑥,𝐴   𝐶,𝑔,𝑘   𝑔,𝐹,𝑛,𝑥   𝑘,𝐺

Allowed substitution hints:   𝐶(𝑥,𝑛)   𝐹(𝑘)   𝐺(𝑥,𝑔,𝑛)

Proof of Theorem axdc4lem

Dummy variables ℎ 𝑖 𝑚 𝑠 𝑡 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		peano1 7595	. . . 4 ⊢ ∅ ∈ ω
2		opelxpi 5586	. . . 4 ⊢ ((∅ ∈ ω ∧ 𝐶 ∈ 𝐴) → ⟨∅, 𝐶⟩ ∈ (ω × 𝐴))
3	1, 2	mpan 688	. . 3 ⊢ (𝐶 ∈ 𝐴 → ⟨∅, 𝐶⟩ ∈ (ω × 𝐴))
4		simp2 1133	. . . . . . . 8 ⊢ ((𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑛 ∈ ω ∧ 𝑥 ∈ 𝐴) → 𝑛 ∈ ω)
5		fovrn 7312	. . . . . . . 8 ⊢ ((𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑛 ∈ ω ∧ 𝑥 ∈ 𝐴) → (𝑛𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅}))
6		peano2 7596	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ω → suc 𝑛 ∈ ω)
7	6	snssd 4735	. . . . . . . . . 10 ⊢ (𝑛 ∈ ω → {suc 𝑛} ⊆ ω)
8		eldifi 4102	. . . . . . . . . 10 ⊢ ((𝑛𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → (𝑛𝐹𝑥) ∈ 𝒫 𝐴)
9		axdc4lem.1	. . . . . . . . . . . 12 ⊢ 𝐴 ∈ V
10	9	elpw2 5240	. . . . . . . . . . 11 ⊢ ((𝑛𝐹𝑥) ∈ 𝒫 𝐴 ↔ (𝑛𝐹𝑥) ⊆ 𝐴)
11		xpss12 5564	. . . . . . . . . . 11 ⊢ (({suc 𝑛} ⊆ ω ∧ (𝑛𝐹𝑥) ⊆ 𝐴) → ({suc 𝑛} × (𝑛𝐹𝑥)) ⊆ (ω × 𝐴))
12	10, 11	sylan2b 595	. . . . . . . . . 10 ⊢ (({suc 𝑛} ⊆ ω ∧ (𝑛𝐹𝑥) ∈ 𝒫 𝐴) → ({suc 𝑛} × (𝑛𝐹𝑥)) ⊆ (ω × 𝐴))
13	7, 8, 12	syl2an 597	. . . . . . . . 9 ⊢ ((𝑛 ∈ ω ∧ (𝑛𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅})) → ({suc 𝑛} × (𝑛𝐹𝑥)) ⊆ (ω × 𝐴))
14		snex 5323	. . . . . . . . . . 11 ⊢ {suc 𝑛} ∈ V
15		ovex 7183	. . . . . . . . . . 11 ⊢ (𝑛𝐹𝑥) ∈ V
16	14, 15	xpex 7470	. . . . . . . . . 10 ⊢ ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ V
17	16	elpw 4545	. . . . . . . . 9 ⊢ (({suc 𝑛} × (𝑛𝐹𝑥)) ∈ 𝒫 (ω × 𝐴) ↔ ({suc 𝑛} × (𝑛𝐹𝑥)) ⊆ (ω × 𝐴))
18	13, 17	sylibr 236	. . . . . . . 8 ⊢ ((𝑛 ∈ ω ∧ (𝑛𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅})) → ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ 𝒫 (ω × 𝐴))
19	4, 5, 18	syl2anc 586	. . . . . . 7 ⊢ ((𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑛 ∈ ω ∧ 𝑥 ∈ 𝐴) → ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ 𝒫 (ω × 𝐴))
20		eldifn 4103	. . . . . . . 8 ⊢ ((𝑛𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → ¬ (𝑛𝐹𝑥) ∈ {∅})
21	15	elsn 4575	. . . . . . . . . . 11 ⊢ ((𝑛𝐹𝑥) ∈ {∅} ↔ (𝑛𝐹𝑥) = ∅)
22	21	necon3bbii 3063	. . . . . . . . . 10 ⊢ (¬ (𝑛𝐹𝑥) ∈ {∅} ↔ (𝑛𝐹𝑥) ≠ ∅)
23		vex 3497	. . . . . . . . . . . . 13 ⊢ 𝑛 ∈ V
24	23	sucex 7520	. . . . . . . . . . . 12 ⊢ suc 𝑛 ∈ V
25	24	snnz 4704	. . . . . . . . . . 11 ⊢ {suc 𝑛} ≠ ∅
26		xpnz 6010	. . . . . . . . . . . 12 ⊢ (({suc 𝑛} ≠ ∅ ∧ (𝑛𝐹𝑥) ≠ ∅) ↔ ({suc 𝑛} × (𝑛𝐹𝑥)) ≠ ∅)
27	26	biimpi 218	. . . . . . . . . . 11 ⊢ (({suc 𝑛} ≠ ∅ ∧ (𝑛𝐹𝑥) ≠ ∅) → ({suc 𝑛} × (𝑛𝐹𝑥)) ≠ ∅)
28	25, 27	mpan 688	. . . . . . . . . 10 ⊢ ((𝑛𝐹𝑥) ≠ ∅ → ({suc 𝑛} × (𝑛𝐹𝑥)) ≠ ∅)
29	22, 28	sylbi 219	. . . . . . . . 9 ⊢ (¬ (𝑛𝐹𝑥) ∈ {∅} → ({suc 𝑛} × (𝑛𝐹𝑥)) ≠ ∅)
30	16	elsn 4575	. . . . . . . . . 10 ⊢ (({suc 𝑛} × (𝑛𝐹𝑥)) ∈ {∅} ↔ ({suc 𝑛} × (𝑛𝐹𝑥)) = ∅)
31	30	necon3bbii 3063	. . . . . . . . 9 ⊢ (¬ ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ {∅} ↔ ({suc 𝑛} × (𝑛𝐹𝑥)) ≠ ∅)
32	29, 31	sylibr 236	. . . . . . . 8 ⊢ (¬ (𝑛𝐹𝑥) ∈ {∅} → ¬ ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ {∅})
33	5, 20, 32	3syl 18	. . . . . . 7 ⊢ ((𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑛 ∈ ω ∧ 𝑥 ∈ 𝐴) → ¬ ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ {∅})
34	19, 33	eldifd 3946	. . . . . 6 ⊢ ((𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑛 ∈ ω ∧ 𝑥 ∈ 𝐴) → ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ (𝒫 (ω × 𝐴) ∖ {∅}))
35	34	3expib 1118	. . . . 5 ⊢ (𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) → ((𝑛 ∈ ω ∧ 𝑥 ∈ 𝐴) → ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ (𝒫 (ω × 𝐴) ∖ {∅})))
36	35	ralrimivv 3190	. . . 4 ⊢ (𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) → ∀𝑛 ∈ ω ∀𝑥 ∈ 𝐴 ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ (𝒫 (ω × 𝐴) ∖ {∅}))
37		axdc4lem.2	. . . . 5 ⊢ 𝐺 = (𝑛 ∈ ω, 𝑥 ∈ 𝐴 ↦ ({suc 𝑛} × (𝑛𝐹𝑥)))
38	37	fmpo 7760	. . . 4 ⊢ (∀𝑛 ∈ ω ∀𝑥 ∈ 𝐴 ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ (𝒫 (ω × 𝐴) ∖ {∅}) ↔ 𝐺:(ω × 𝐴)⟶(𝒫 (ω × 𝐴) ∖ {∅}))
39	36, 38	sylib 220	. . 3 ⊢ (𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) → 𝐺:(ω × 𝐴)⟶(𝒫 (ω × 𝐴) ∖ {∅}))
40		dcomex 9863	. . . . 5 ⊢ ω ∈ V
41	40, 9	xpex 7470	. . . 4 ⊢ (ω × 𝐴) ∈ V
42	41	axdc3 9870	. . 3 ⊢ ((⟨∅, 𝐶⟩ ∈ (ω × 𝐴) ∧ 𝐺:(ω × 𝐴)⟶(𝒫 (ω × 𝐴) ∖ {∅})) → ∃ℎ(ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))))
43	3, 39, 42	syl2an 597	. 2 ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅})) → ∃ℎ(ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))))
44		2ndcof 7714	. . . . . . . . 9 ⊢ (ℎ:ω⟶(ω × 𝐴) → (2nd ∘ ℎ):ω⟶𝐴)
45	44	3ad2ant1 1129	. . . . . . . 8 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (2nd ∘ ℎ):ω⟶𝐴)
46	45	adantl 484	. . . . . . 7 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (2nd ∘ ℎ):ω⟶𝐴)
47		fex2 7632	. . . . . . . 8 ⊢ (((2nd ∘ ℎ):ω⟶𝐴 ∧ ω ∈ V ∧ 𝐴 ∈ V) → (2nd ∘ ℎ) ∈ V)
48	40, 9, 47	mp3an23 1449	. . . . . . 7 ⊢ ((2nd ∘ ℎ):ω⟶𝐴 → (2nd ∘ ℎ) ∈ V)
49	46, 48	syl 17	. . . . . 6 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (2nd ∘ ℎ) ∈ V)
50		fvco3 6754	. . . . . . . . . . 11 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ ∅ ∈ ω) → ((2nd ∘ ℎ)‘∅) = (2nd ‘(ℎ‘∅)))
51	1, 50	mpan2 689	. . . . . . . . . 10 ⊢ (ℎ:ω⟶(ω × 𝐴) → ((2nd ∘ ℎ)‘∅) = (2nd ‘(ℎ‘∅)))
52	51	3ad2ant1 1129	. . . . . . . . 9 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ((2nd ∘ ℎ)‘∅) = (2nd ‘(ℎ‘∅)))
53		fveq2 6664	. . . . . . . . . 10 ⊢ ((ℎ‘∅) = ⟨∅, 𝐶⟩ → (2nd ‘(ℎ‘∅)) = (2nd ‘⟨∅, 𝐶⟩))
54	53	3ad2ant2 1130	. . . . . . . . 9 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (2nd ‘(ℎ‘∅)) = (2nd ‘⟨∅, 𝐶⟩))
55	52, 54	eqtrd 2856	. . . . . . . 8 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ((2nd ∘ ℎ)‘∅) = (2nd ‘⟨∅, 𝐶⟩))
56		op2ndg 7696	. . . . . . . . 9 ⊢ ((∅ ∈ ω ∧ 𝐶 ∈ 𝐴) → (2nd ‘⟨∅, 𝐶⟩) = 𝐶)
57	1, 56	mpan 688	. . . . . . . 8 ⊢ (𝐶 ∈ 𝐴 → (2nd ‘⟨∅, 𝐶⟩) = 𝐶)
58	55, 57	sylan9eqr 2878	. . . . . . 7 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ((2nd ∘ ℎ)‘∅) = 𝐶)
59		nfv 1911	. . . . . . . . 9 ⊢ Ⅎ𝑘 𝐶 ∈ 𝐴
60		nfv 1911	. . . . . . . . . 10 ⊢ Ⅎ𝑘 ℎ:ω⟶(ω × 𝐴)
61		nfv 1911	. . . . . . . . . 10 ⊢ Ⅎ𝑘(ℎ‘∅) = ⟨∅, 𝐶⟩
62		nfra1 3219	. . . . . . . . . 10 ⊢ Ⅎ𝑘∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))
63	60, 61, 62	nf3an 1898	. . . . . . . . 9 ⊢ Ⅎ𝑘(ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))
64	59, 63	nfan 1896	. . . . . . . 8 ⊢ Ⅎ𝑘(𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))))
65		fveq2 6664	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = ∅ → (ℎ‘𝑚) = (ℎ‘∅))
66		opeq1 4796	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = ∅ → ⟨𝑚, 𝑧⟩ = ⟨∅, 𝑧⟩)
67	65, 66	eqeq12d 2837	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = ∅ → ((ℎ‘𝑚) = ⟨𝑚, 𝑧⟩ ↔ (ℎ‘∅) = ⟨∅, 𝑧⟩))
68	67	exbidv 1918	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = ∅ → (∃𝑧(ℎ‘𝑚) = ⟨𝑚, 𝑧⟩ ↔ ∃𝑧(ℎ‘∅) = ⟨∅, 𝑧⟩))
69		fveq2 6664	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑖 → (ℎ‘𝑚) = (ℎ‘𝑖))
70		opeq1 4796	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑖 → ⟨𝑚, 𝑧⟩ = ⟨𝑖, 𝑧⟩)
71	69, 70	eqeq12d 2837	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑖 → ((ℎ‘𝑚) = ⟨𝑚, 𝑧⟩ ↔ (ℎ‘𝑖) = ⟨𝑖, 𝑧⟩))
72	71	exbidv 1918	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑖 → (∃𝑧(ℎ‘𝑚) = ⟨𝑚, 𝑧⟩ ↔ ∃𝑧(ℎ‘𝑖) = ⟨𝑖, 𝑧⟩))
73		fveq2 6664	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = suc 𝑖 → (ℎ‘𝑚) = (ℎ‘suc 𝑖))
74		opeq1 4796	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = suc 𝑖 → ⟨𝑚, 𝑧⟩ = ⟨suc 𝑖, 𝑧⟩)
75	73, 74	eqeq12d 2837	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = suc 𝑖 → ((ℎ‘𝑚) = ⟨𝑚, 𝑧⟩ ↔ (ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩))
76	75	exbidv 1918	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = suc 𝑖 → (∃𝑧(ℎ‘𝑚) = ⟨𝑚, 𝑧⟩ ↔ ∃𝑧(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩))
77		opeq2 4797	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝐶 → ⟨∅, 𝑧⟩ = ⟨∅, 𝐶⟩)
78	77	eqeq2d 2832	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝐶 → ((ℎ‘∅) = ⟨∅, 𝑧⟩ ↔ (ℎ‘∅) = ⟨∅, 𝐶⟩))
79	78	spcegv 3596	. . . . . . . . . . . . . . . . 17 ⊢ (𝐶 ∈ 𝐴 → ((ℎ‘∅) = ⟨∅, 𝐶⟩ → ∃𝑧(ℎ‘∅) = ⟨∅, 𝑧⟩))
80	79	imp 409	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩) → ∃𝑧(ℎ‘∅) = ⟨∅, 𝑧⟩)
81	80	3ad2antr2 1185	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ∃𝑧(ℎ‘∅) = ⟨∅, 𝑧⟩)
82		fveq2 6664	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → (𝐺‘(ℎ‘𝑖)) = (𝐺‘⟨𝑖, 𝑧⟩))
83		df-ov 7153	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑖𝐺𝑧) = (𝐺‘⟨𝑖, 𝑧⟩)
84	82, 83	syl6eqr 2874	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → (𝐺‘(ℎ‘𝑖)) = (𝑖𝐺𝑧))
85	84	adantl 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) ∧ (ℎ‘𝑖) = ⟨𝑖, 𝑧⟩) → (𝐺‘(ℎ‘𝑖)) = (𝑖𝐺𝑧))
86		simplr 767	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) ∧ (ℎ‘𝑖) = ⟨𝑖, 𝑧⟩) → 𝑖 ∈ ω)
87		ffvelrn 6843	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) → (ℎ‘𝑖) ∈ (ω × 𝐴))
88		eleq1 2900	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ((ℎ‘𝑖) ∈ (ω × 𝐴) ↔ ⟨𝑖, 𝑧⟩ ∈ (ω × 𝐴)))
89		opelxp2 5591	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (⟨𝑖, 𝑧⟩ ∈ (ω × 𝐴) → 𝑧 ∈ 𝐴)
90	88, 89	syl6bi 255	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ((ℎ‘𝑖) ∈ (ω × 𝐴) → 𝑧 ∈ 𝐴))
91	87, 90	mpan9 509	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) ∧ (ℎ‘𝑖) = ⟨𝑖, 𝑧⟩) → 𝑧 ∈ 𝐴)
92		suceq 6250	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑛 = 𝑖 → suc 𝑛 = suc 𝑖)
93	92	sneqd 4572	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑛 = 𝑖 → {suc 𝑛} = {suc 𝑖})
94		oveq1 7157	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑛 = 𝑖 → (𝑛𝐹𝑥) = (𝑖𝐹𝑥))
95	93, 94	xpeq12d 5580	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑛 = 𝑖 → ({suc 𝑛} × (𝑛𝐹𝑥)) = ({suc 𝑖} × (𝑖𝐹𝑥)))
96		oveq2 7158	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 = 𝑧 → (𝑖𝐹𝑥) = (𝑖𝐹𝑧))
97	96	xpeq2d 5579	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = 𝑧 → ({suc 𝑖} × (𝑖𝐹𝑥)) = ({suc 𝑖} × (𝑖𝐹𝑧)))
98		snex 5323	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ {suc 𝑖} ∈ V
99		ovex 7183	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑖𝐹𝑧) ∈ V
100	98, 99	xpex 7470	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ({suc 𝑖} × (𝑖𝐹𝑧)) ∈ V
101	95, 97, 37, 100	ovmpo 7304	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑖 ∈ ω ∧ 𝑧 ∈ 𝐴) → (𝑖𝐺𝑧) = ({suc 𝑖} × (𝑖𝐹𝑧)))
102	86, 91, 101	syl2anc 586	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) ∧ (ℎ‘𝑖) = ⟨𝑖, 𝑧⟩) → (𝑖𝐺𝑧) = ({suc 𝑖} × (𝑖𝐹𝑧)))
103	85, 102	eqtrd 2856	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) ∧ (ℎ‘𝑖) = ⟨𝑖, 𝑧⟩) → (𝐺‘(ℎ‘𝑖)) = ({suc 𝑖} × (𝑖𝐹𝑧)))
104		suceq 6250	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑘 = 𝑖 → suc 𝑘 = suc 𝑖)
105	104	fveq2d 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 = 𝑖 → (ℎ‘suc 𝑘) = (ℎ‘suc 𝑖))
106		2fveq3 6669	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 = 𝑖 → (𝐺‘(ℎ‘𝑘)) = (𝐺‘(ℎ‘𝑖)))
107	105, 106	eleq12d 2907	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 = 𝑖 → ((ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) ↔ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))))
108	107	rspcv 3617	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 ∈ ω → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))))
109	108	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) ∧ (ℎ‘𝑖) = ⟨𝑖, 𝑧⟩) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))))
110		eleq2 2901	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐺‘(ℎ‘𝑖)) = ({suc 𝑖} × (𝑖𝐹𝑧)) → ((ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖)) ↔ (ℎ‘suc 𝑖) ∈ ({suc 𝑖} × (𝑖𝐹𝑧))))
111		elxp 5572	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((ℎ‘suc 𝑖) ∈ ({suc 𝑖} × (𝑖𝐹𝑧)) ↔ ∃𝑠∃𝑡((ℎ‘suc 𝑖) = ⟨𝑠, 𝑡⟩ ∧ (𝑠 ∈ {suc 𝑖} ∧ 𝑡 ∈ (𝑖𝐹𝑧))))
112		velsn 4576	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑠 ∈ {suc 𝑖} ↔ 𝑠 = suc 𝑖)
113		opeq1 4796	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑠 = suc 𝑖 → ⟨𝑠, 𝑡⟩ = ⟨suc 𝑖, 𝑡⟩)
114	112, 113	sylbi 219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑠 ∈ {suc 𝑖} → ⟨𝑠, 𝑡⟩ = ⟨suc 𝑖, 𝑡⟩)
115	114	eqeq2d 2832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑠 ∈ {suc 𝑖} → ((ℎ‘suc 𝑖) = ⟨𝑠, 𝑡⟩ ↔ (ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩))
116	115	biimpac 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((ℎ‘suc 𝑖) = ⟨𝑠, 𝑡⟩ ∧ 𝑠 ∈ {suc 𝑖}) → (ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩)
117	116	adantrr 715	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((ℎ‘suc 𝑖) = ⟨𝑠, 𝑡⟩ ∧ (𝑠 ∈ {suc 𝑖} ∧ 𝑡 ∈ (𝑖𝐹𝑧))) → (ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩)
118	117	eximi 1831	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∃𝑡((ℎ‘suc 𝑖) = ⟨𝑠, 𝑡⟩ ∧ (𝑠 ∈ {suc 𝑖} ∧ 𝑡 ∈ (𝑖𝐹𝑧))) → ∃𝑡(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩)
119	118	exlimiv 1927	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∃𝑠∃𝑡((ℎ‘suc 𝑖) = ⟨𝑠, 𝑡⟩ ∧ (𝑠 ∈ {suc 𝑖} ∧ 𝑡 ∈ (𝑖𝐹𝑧))) → ∃𝑡(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩)
120	111, 119	sylbi 219	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((ℎ‘suc 𝑖) ∈ ({suc 𝑖} × (𝑖𝐹𝑧)) → ∃𝑡(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩)
121	110, 120	syl6bi 255	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐺‘(ℎ‘𝑖)) = ({suc 𝑖} × (𝑖𝐹𝑧)) → ((ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖)) → ∃𝑡(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩))
122	103, 109, 121	sylsyld 61	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) ∧ (ℎ‘𝑖) = ⟨𝑖, 𝑧⟩) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → ∃𝑡(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩))
123	122	expcom 416	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → ∃𝑡(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩)))
124	123	exlimiv 1927	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑧(ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → ∃𝑡(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩)))
125	124	com3l 89	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → (∃𝑧(ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ∃𝑡(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩)))
126		opeq2 4797	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 = 𝑧 → ⟨suc 𝑖, 𝑡⟩ = ⟨suc 𝑖, 𝑧⟩)
127	126	eqeq2d 2832	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 = 𝑧 → ((ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩ ↔ (ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩))
128	127	cbvexvw 2040	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑡(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩ ↔ ∃𝑧(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩)
129	125, 128	syl8ib 258	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → (∃𝑧(ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ∃𝑧(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩)))
130	129	impancom 454	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑖 ∈ ω → (∃𝑧(ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ∃𝑧(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩)))
131	130	3adant2 1127	. . . . . . . . . . . . . . . . 17 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑖 ∈ ω → (∃𝑧(ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ∃𝑧(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩)))
132	131	adantl 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (𝑖 ∈ ω → (∃𝑧(ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ∃𝑧(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩)))
133	132	com12 32	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ ω → ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (∃𝑧(ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ∃𝑧(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩)))
134	68, 72, 76, 81, 133	finds2 7604	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ω → ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ∃𝑧(ℎ‘𝑚) = ⟨𝑚, 𝑧⟩))
135	134	com12 32	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (𝑚 ∈ ω → ∃𝑧(ℎ‘𝑚) = ⟨𝑚, 𝑧⟩))
136	135	ralrimiv 3181	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ∀𝑚 ∈ ω ∃𝑧(ℎ‘𝑚) = ⟨𝑚, 𝑧⟩)
137		fveq2 6664	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑘 → (ℎ‘𝑚) = (ℎ‘𝑘))
138		opeq1 4796	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑘 → ⟨𝑚, 𝑧⟩ = ⟨𝑘, 𝑧⟩)
139	137, 138	eqeq12d 2837	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑘 → ((ℎ‘𝑚) = ⟨𝑚, 𝑧⟩ ↔ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩))
140	139	exbidv 1918	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑘 → (∃𝑧(ℎ‘𝑚) = ⟨𝑚, 𝑧⟩ ↔ ∃𝑧(ℎ‘𝑘) = ⟨𝑘, 𝑧⟩))
141	140	rspccv 3619	. . . . . . . . . . . 12 ⊢ (∀𝑚 ∈ ω ∃𝑧(ℎ‘𝑚) = ⟨𝑚, 𝑧⟩ → (𝑘 ∈ ω → ∃𝑧(ℎ‘𝑘) = ⟨𝑘, 𝑧⟩))
142	136, 141	syl 17	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (𝑘 ∈ ω → ∃𝑧(ℎ‘𝑘) = ⟨𝑘, 𝑧⟩))
143	142	3impia 1113	. . . . . . . . . 10 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → ∃𝑧(ℎ‘𝑘) = ⟨𝑘, 𝑧⟩)
144		simp21 1202	. . . . . . . . . 10 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → ℎ:ω⟶(ω × 𝐴))
145		simp3 1134	. . . . . . . . . 10 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → 𝑘 ∈ ω)
146		rspa 3206	. . . . . . . . . . . 12 ⊢ ((∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) ∧ 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))
147	146	3ad2antl3 1183	. . . . . . . . . . 11 ⊢ (((ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))
148	147	3adant1 1126	. . . . . . . . . 10 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))
149		simpl 485	. . . . . . . . . . . . . . . . 17 ⊢ (((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩)
150	149	fveq2d 6668	. . . . . . . . . . . . . . . 16 ⊢ (((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (𝐺‘(ℎ‘𝑘)) = (𝐺‘⟨𝑘, 𝑧⟩))
151		simprr 771	. . . . . . . . . . . . . . . . 17 ⊢ (((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → 𝑘 ∈ ω)
152		eleq1 2900	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ → ((ℎ‘𝑘) ∈ (ω × 𝐴) ↔ ⟨𝑘, 𝑧⟩ ∈ (ω × 𝐴)))
153		opelxp2 5591	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨𝑘, 𝑧⟩ ∈ (ω × 𝐴) → 𝑧 ∈ 𝐴)
154	152, 153	syl6bi 255	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ → ((ℎ‘𝑘) ∈ (ω × 𝐴) → 𝑧 ∈ 𝐴))
155		ffvelrn 6843	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → (ℎ‘𝑘) ∈ (ω × 𝐴))
156	154, 155	impel 508	. . . . . . . . . . . . . . . . 17 ⊢ (((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → 𝑧 ∈ 𝐴)
157		df-ov 7153	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘𝐺𝑧) = (𝐺‘⟨𝑘, 𝑧⟩)
158		suceq 6250	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑘 → suc 𝑛 = suc 𝑘)
159	158	sneqd 4572	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑘 → {suc 𝑛} = {suc 𝑘})
160		oveq1 7157	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑘 → (𝑛𝐹𝑥) = (𝑘𝐹𝑥))
161	159, 160	xpeq12d 5580	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑘 → ({suc 𝑛} × (𝑛𝐹𝑥)) = ({suc 𝑘} × (𝑘𝐹𝑥)))
162		oveq2 7158	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑧 → (𝑘𝐹𝑥) = (𝑘𝐹𝑧))
163	162	xpeq2d 5579	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑧 → ({suc 𝑘} × (𝑘𝐹𝑥)) = ({suc 𝑘} × (𝑘𝐹𝑧)))
164		snex 5323	. . . . . . . . . . . . . . . . . . . 20 ⊢ {suc 𝑘} ∈ V
165		ovex 7183	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘𝐹𝑧) ∈ V
166	164, 165	xpex 7470	. . . . . . . . . . . . . . . . . . 19 ⊢ ({suc 𝑘} × (𝑘𝐹𝑧)) ∈ V
167	161, 163, 37, 166	ovmpo 7304	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ω ∧ 𝑧 ∈ 𝐴) → (𝑘𝐺𝑧) = ({suc 𝑘} × (𝑘𝐹𝑧)))
168	157, 167	syl5eqr 2870	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ω ∧ 𝑧 ∈ 𝐴) → (𝐺‘⟨𝑘, 𝑧⟩) = ({suc 𝑘} × (𝑘𝐹𝑧)))
169	151, 156, 168	syl2anc 586	. . . . . . . . . . . . . . . 16 ⊢ (((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (𝐺‘⟨𝑘, 𝑧⟩) = ({suc 𝑘} × (𝑘𝐹𝑧)))
170	150, 169	eqtrd 2856	. . . . . . . . . . . . . . 15 ⊢ (((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (𝐺‘(ℎ‘𝑘)) = ({suc 𝑘} × (𝑘𝐹𝑧)))
171	170	eleq2d 2898	. . . . . . . . . . . . . 14 ⊢ (((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) ↔ (ℎ‘suc 𝑘) ∈ ({suc 𝑘} × (𝑘𝐹𝑧))))
172		elxp 5572	. . . . . . . . . . . . . . . . 17 ⊢ ((ℎ‘suc 𝑘) ∈ ({suc 𝑘} × (𝑘𝐹𝑧)) ↔ ∃𝑠∃𝑡((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (𝑠 ∈ {suc 𝑘} ∧ 𝑡 ∈ (𝑘𝐹𝑧))))
173		peano2 7596	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 ∈ ω → suc 𝑘 ∈ ω)
174		fvco3 6754	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ suc 𝑘 ∈ ω) → ((2nd ∘ ℎ)‘suc 𝑘) = (2nd ‘(ℎ‘suc 𝑘)))
175	173, 174	sylan2 594	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((2nd ∘ ℎ)‘suc 𝑘) = (2nd ‘(ℎ‘suc 𝑘)))
176	175	adantl 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd ∘ ℎ)‘suc 𝑘) = (2nd ‘(ℎ‘suc 𝑘)))
177		simpll 765	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩)
178	177	fveq2d 6668	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (2nd ‘(ℎ‘suc 𝑘)) = (2nd ‘⟨𝑠, 𝑡⟩))
179	176, 178	eqtrd 2856	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd ∘ ℎ)‘suc 𝑘) = (2nd ‘⟨𝑠, 𝑡⟩))
180		vex 3497	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑠 ∈ V
181		vex 3497	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑡 ∈ V
182	180, 181	op2nd 7692	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (2nd ‘⟨𝑠, 𝑡⟩) = 𝑡
183	179, 182	syl6eq 2872	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd ∘ ℎ)‘suc 𝑘) = 𝑡)
184		fvco3 6754	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((2nd ∘ ℎ)‘𝑘) = (2nd ‘(ℎ‘𝑘)))
185	184	adantl 484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd ∘ ℎ)‘𝑘) = (2nd ‘(ℎ‘𝑘)))
186		simplr 767	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩)
187	186	fveq2d 6668	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (2nd ‘(ℎ‘𝑘)) = (2nd ‘⟨𝑘, 𝑧⟩))
188	185, 187	eqtrd 2856	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd ∘ ℎ)‘𝑘) = (2nd ‘⟨𝑘, 𝑧⟩))
189		vex 3497	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑘 ∈ V
190		vex 3497	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑧 ∈ V
191	189, 190	op2nd 7692	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (2nd ‘⟨𝑘, 𝑧⟩) = 𝑧
192	188, 191	syl6eq 2872	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd ∘ ℎ)‘𝑘) = 𝑧)
193	192	oveq2d 7166	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (𝑘𝐹((2nd ∘ ℎ)‘𝑘)) = (𝑘𝐹𝑧))
194	183, 193	eleq12d 2907	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)) ↔ 𝑡 ∈ (𝑘𝐹𝑧)))
195	194	biimprcd 252	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 ∈ (𝑘𝐹𝑧) → ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))
196	195	exp4c 435	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ∈ (𝑘𝐹𝑧) → ((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ → ((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))))
197	196	adantl 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑠 ∈ {suc 𝑘} ∧ 𝑡 ∈ (𝑘𝐹𝑧)) → ((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ → ((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))))
198	197	impcom 410	. . . . . . . . . . . . . . . . . 18 ⊢ (((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (𝑠 ∈ {suc 𝑘} ∧ 𝑡 ∈ (𝑘𝐹𝑧))) → ((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))))
199	198	exlimivv 1929	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑠∃𝑡((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (𝑠 ∈ {suc 𝑘} ∧ 𝑡 ∈ (𝑘𝐹𝑧))) → ((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))))
200	172, 199	sylbi 219	. . . . . . . . . . . . . . . 16 ⊢ ((ℎ‘suc 𝑘) ∈ ({suc 𝑘} × (𝑘𝐹𝑧)) → ((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))))
201	200	com3l 89	. . . . . . . . . . . . . . 15 ⊢ ((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((ℎ‘suc 𝑘) ∈ ({suc 𝑘} × (𝑘𝐹𝑧)) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))))
202	201	imp 409	. . . . . . . . . . . . . 14 ⊢ (((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((ℎ‘suc 𝑘) ∈ ({suc 𝑘} × (𝑘𝐹𝑧)) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))
203	171, 202	sylbid 242	. . . . . . . . . . . . 13 ⊢ (((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))
204	203	ex 415	. . . . . . . . . . . 12 ⊢ ((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))))
205	204	exlimiv 1927	. . . . . . . . . . 11 ⊢ (∃𝑧(ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))))
206	205	3imp 1107	. . . . . . . . . 10 ⊢ ((∃𝑧(ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) ∧ (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))
207	143, 144, 145, 148, 206	syl121anc 1371	. . . . . . . . 9 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))
208	207	3expia 1117	. . . . . . . 8 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (𝑘 ∈ ω → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))
209	64, 208	ralrimi 3216	. . . . . . 7 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ∀𝑘 ∈ ω ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))
210	46, 58, 209	3jca 1124	. . . . . 6 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ((2nd ∘ ℎ):ω⟶𝐴 ∧ ((2nd ∘ ℎ)‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))
211		feq1 6489	. . . . . . 7 ⊢ (𝑔 = (2nd ∘ ℎ) → (𝑔:ω⟶𝐴 ↔ (2nd ∘ ℎ):ω⟶𝐴))
212		fveq1 6663	. . . . . . . 8 ⊢ (𝑔 = (2nd ∘ ℎ) → (𝑔‘∅) = ((2nd ∘ ℎ)‘∅))
213	212	eqeq1d 2823	. . . . . . 7 ⊢ (𝑔 = (2nd ∘ ℎ) → ((𝑔‘∅) = 𝐶 ↔ ((2nd ∘ ℎ)‘∅) = 𝐶))
214		fveq1 6663	. . . . . . . . 9 ⊢ (𝑔 = (2nd ∘ ℎ) → (𝑔‘suc 𝑘) = ((2nd ∘ ℎ)‘suc 𝑘))
215		fveq1 6663	. . . . . . . . . 10 ⊢ (𝑔 = (2nd ∘ ℎ) → (𝑔‘𝑘) = ((2nd ∘ ℎ)‘𝑘))
216	215	oveq2d 7166	. . . . . . . . 9 ⊢ (𝑔 = (2nd ∘ ℎ) → (𝑘𝐹(𝑔‘𝑘)) = (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))
217	214, 216	eleq12d 2907	. . . . . . . 8 ⊢ (𝑔 = (2nd ∘ ℎ) → ((𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘)) ↔ ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))
218	217	ralbidv 3197	. . . . . . 7 ⊢ (𝑔 = (2nd ∘ ℎ) → (∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘)) ↔ ∀𝑘 ∈ ω ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))
219	211, 213, 218	3anbi123d 1432	. . . . . 6 ⊢ (𝑔 = (2nd ∘ ℎ) → ((𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘))) ↔ ((2nd ∘ ℎ):ω⟶𝐴 ∧ ((2nd ∘ ℎ)‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))))
220	49, 210, 219	spcedv 3598	. . . . 5 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘))))
221	220	ex 415	. . . 4 ⊢ (𝐶 ∈ 𝐴 → ((ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘)))))
222	221	exlimdv 1930	. . 3 ⊢ (𝐶 ∈ 𝐴 → (∃ℎ(ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘)))))
223	222	adantr 483	. 2 ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅})) → (∃ℎ(ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘)))))
224	43, 223	mpd 15	1 ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘))))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 398   ∧ w3a 1083   = wceq 1533  ∃wex 1776   ∈ wcel 2110   ≠ wne 3016  ∀wral 3138  Vcvv 3494   ∖ cdif 3932   ⊆ wss 3935  ∅c0 4290  𝒫 cpw 4538  {csn 4560  ⟨cop 4566   × cxp 5547   ∘ ccom 5553  suc csuc 6187  ⟶wf 6345  ‘cfv 6349  (class class class)co 7150   ∈ cmpo 7152  ωcom 7574  2^nd c2nd 7682

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7455  ax-dc 9862

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4561  df-pr 4563  df-tp 4565  df-op 4567  df-uni 4832  df-iun 4913  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7575  df-1st 7683  df-2nd 7684  df-1o 8096

This theorem is referenced by:  axdc4  9872