Theorem axdc4lem 10454

Description: Lemma for axdc4 10455. (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 7883	. . . 4 ⊢ ∅ ∈ ω
2		opelxpi 5713	. . . 4 ⊢ ((∅ ∈ ω ∧ 𝐶 ∈ 𝐴) → ⟨∅, 𝐶⟩ ∈ (ω × 𝐴))
3	1, 2	mpan 687	. . 3 ⊢ (𝐶 ∈ 𝐴 → ⟨∅, 𝐶⟩ ∈ (ω × 𝐴))
4		simp2 1136	. . . . . . . 8 ⊢ ((𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑛 ∈ ω ∧ 𝑥 ∈ 𝐴) → 𝑛 ∈ ω)
5		fovcdm 7581	. . . . . . . 8 ⊢ ((𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑛 ∈ ω ∧ 𝑥 ∈ 𝐴) → (𝑛𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅}))
6		peano2 7885	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ω → suc 𝑛 ∈ ω)
7	6	snssd 4812	. . . . . . . . . 10 ⊢ (𝑛 ∈ ω → {suc 𝑛} ⊆ ω)
8		eldifi 4126	. . . . . . . . . 10 ⊢ ((𝑛𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → (𝑛𝐹𝑥) ∈ 𝒫 𝐴)
9		axdc4lem.1	. . . . . . . . . . . 12 ⊢ 𝐴 ∈ V
10	9	elpw2 5345	. . . . . . . . . . 11 ⊢ ((𝑛𝐹𝑥) ∈ 𝒫 𝐴 ↔ (𝑛𝐹𝑥) ⊆ 𝐴)
11		xpss12 5691	. . . . . . . . . . 11 ⊢ (({suc 𝑛} ⊆ ω ∧ (𝑛𝐹𝑥) ⊆ 𝐴) → ({suc 𝑛} × (𝑛𝐹𝑥)) ⊆ (ω × 𝐴))
12	10, 11	sylan2b 593	. . . . . . . . . 10 ⊢ (({suc 𝑛} ⊆ ω ∧ (𝑛𝐹𝑥) ∈ 𝒫 𝐴) → ({suc 𝑛} × (𝑛𝐹𝑥)) ⊆ (ω × 𝐴))
13	7, 8, 12	syl2an 595	. . . . . . . . 9 ⊢ ((𝑛 ∈ ω ∧ (𝑛𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅})) → ({suc 𝑛} × (𝑛𝐹𝑥)) ⊆ (ω × 𝐴))
14		snex 5431	. . . . . . . . . . 11 ⊢ {suc 𝑛} ∈ V
15		ovex 7445	. . . . . . . . . . 11 ⊢ (𝑛𝐹𝑥) ∈ V
16	14, 15	xpex 7744	. . . . . . . . . 10 ⊢ ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ V
17	16	elpw 4606	. . . . . . . . 9 ⊢ (({suc 𝑛} × (𝑛𝐹𝑥)) ∈ 𝒫 (ω × 𝐴) ↔ ({suc 𝑛} × (𝑛𝐹𝑥)) ⊆ (ω × 𝐴))
18	13, 17	sylibr 233	. . . . . . . 8 ⊢ ((𝑛 ∈ ω ∧ (𝑛𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅})) → ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ 𝒫 (ω × 𝐴))
19	4, 5, 18	syl2anc 583	. . . . . . 7 ⊢ ((𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑛 ∈ ω ∧ 𝑥 ∈ 𝐴) → ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ 𝒫 (ω × 𝐴))
20		eldifn 4127	. . . . . . . 8 ⊢ ((𝑛𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → ¬ (𝑛𝐹𝑥) ∈ {∅})
21	15	elsn 4643	. . . . . . . . . . 11 ⊢ ((𝑛𝐹𝑥) ∈ {∅} ↔ (𝑛𝐹𝑥) = ∅)
22	21	necon3bbii 2987	. . . . . . . . . 10 ⊢ (¬ (𝑛𝐹𝑥) ∈ {∅} ↔ (𝑛𝐹𝑥) ≠ ∅)
23		vex 3477	. . . . . . . . . . . . 13 ⊢ 𝑛 ∈ V
24	23	sucex 7798	. . . . . . . . . . . 12 ⊢ suc 𝑛 ∈ V
25	24	snnz 4780	. . . . . . . . . . 11 ⊢ {suc 𝑛} ≠ ∅
26		xpnz 6158	. . . . . . . . . . . 12 ⊢ (({suc 𝑛} ≠ ∅ ∧ (𝑛𝐹𝑥) ≠ ∅) ↔ ({suc 𝑛} × (𝑛𝐹𝑥)) ≠ ∅)
27	26	biimpi 215	. . . . . . . . . . 11 ⊢ (({suc 𝑛} ≠ ∅ ∧ (𝑛𝐹𝑥) ≠ ∅) → ({suc 𝑛} × (𝑛𝐹𝑥)) ≠ ∅)
28	25, 27	mpan 687	. . . . . . . . . 10 ⊢ ((𝑛𝐹𝑥) ≠ ∅ → ({suc 𝑛} × (𝑛𝐹𝑥)) ≠ ∅)
29	22, 28	sylbi 216	. . . . . . . . 9 ⊢ (¬ (𝑛𝐹𝑥) ∈ {∅} → ({suc 𝑛} × (𝑛𝐹𝑥)) ≠ ∅)
30	16	elsn 4643	. . . . . . . . . 10 ⊢ (({suc 𝑛} × (𝑛𝐹𝑥)) ∈ {∅} ↔ ({suc 𝑛} × (𝑛𝐹𝑥)) = ∅)
31	30	necon3bbii 2987	. . . . . . . . 9 ⊢ (¬ ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ {∅} ↔ ({suc 𝑛} × (𝑛𝐹𝑥)) ≠ ∅)
32	29, 31	sylibr 233	. . . . . . . 8 ⊢ (¬ (𝑛𝐹𝑥) ∈ {∅} → ¬ ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ {∅})
33	5, 20, 32	3syl 18	. . . . . . 7 ⊢ ((𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑛 ∈ ω ∧ 𝑥 ∈ 𝐴) → ¬ ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ {∅})
34	19, 33	eldifd 3959	. . . . . 6 ⊢ ((𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑛 ∈ ω ∧ 𝑥 ∈ 𝐴) → ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ (𝒫 (ω × 𝐴) ∖ {∅}))
35	34	3expib 1121	. . . . 5 ⊢ (𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) → ((𝑛 ∈ ω ∧ 𝑥 ∈ 𝐴) → ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ (𝒫 (ω × 𝐴) ∖ {∅})))
36	35	ralrimivv 3197	. . . 4 ⊢ (𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) → ∀𝑛 ∈ ω ∀𝑥 ∈ 𝐴 ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ (𝒫 (ω × 𝐴) ∖ {∅}))
37		axdc4lem.2	. . . . 5 ⊢ 𝐺 = (𝑛 ∈ ω, 𝑥 ∈ 𝐴 ↦ ({suc 𝑛} × (𝑛𝐹𝑥)))
38	37	fmpo 8058	. . . 4 ⊢ (∀𝑛 ∈ ω ∀𝑥 ∈ 𝐴 ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ (𝒫 (ω × 𝐴) ∖ {∅}) ↔ 𝐺:(ω × 𝐴)⟶(𝒫 (ω × 𝐴) ∖ {∅}))
39	36, 38	sylib 217	. . 3 ⊢ (𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) → 𝐺:(ω × 𝐴)⟶(𝒫 (ω × 𝐴) ∖ {∅}))
40		dcomex 10446	. . . . 5 ⊢ ω ∈ V
41	40, 9	xpex 7744	. . . 4 ⊢ (ω × 𝐴) ∈ V
42	41	axdc3 10453	. . 3 ⊢ ((⟨∅, 𝐶⟩ ∈ (ω × 𝐴) ∧ 𝐺:(ω × 𝐴)⟶(𝒫 (ω × 𝐴) ∖ {∅})) → ∃ℎ(ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))))
43	3, 39, 42	syl2an 595	. 2 ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅})) → ∃ℎ(ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))))
44		2ndcof 8010	. . . . . . . . 9 ⊢ (ℎ:ω⟶(ω × 𝐴) → (2nd ∘ ℎ):ω⟶𝐴)
45	44	3ad2ant1 1132	. . . . . . . 8 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (2nd ∘ ℎ):ω⟶𝐴)
46	45	adantl 481	. . . . . . 7 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (2nd ∘ ℎ):ω⟶𝐴)
47		fex2 7928	. . . . . . . 8 ⊢ (((2nd ∘ ℎ):ω⟶𝐴 ∧ ω ∈ V ∧ 𝐴 ∈ V) → (2nd ∘ ℎ) ∈ V)
48	40, 9, 47	mp3an23 1452	. . . . . . 7 ⊢ ((2nd ∘ ℎ):ω⟶𝐴 → (2nd ∘ ℎ) ∈ V)
49	46, 48	syl 17	. . . . . 6 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (2nd ∘ ℎ) ∈ V)
50		fvco3 6990	. . . . . . . . . . 11 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ ∅ ∈ ω) → ((2nd ∘ ℎ)‘∅) = (2nd ‘(ℎ‘∅)))
51	1, 50	mpan2 688	. . . . . . . . . 10 ⊢ (ℎ:ω⟶(ω × 𝐴) → ((2nd ∘ ℎ)‘∅) = (2nd ‘(ℎ‘∅)))
52	51	3ad2ant1 1132	. . . . . . . . 9 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ((2nd ∘ ℎ)‘∅) = (2nd ‘(ℎ‘∅)))
53		fveq2 6891	. . . . . . . . . 10 ⊢ ((ℎ‘∅) = ⟨∅, 𝐶⟩ → (2nd ‘(ℎ‘∅)) = (2nd ‘⟨∅, 𝐶⟩))
54	53	3ad2ant2 1133	. . . . . . . . 9 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (2nd ‘(ℎ‘∅)) = (2nd ‘⟨∅, 𝐶⟩))
55	52, 54	eqtrd 2771	. . . . . . . 8 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ((2nd ∘ ℎ)‘∅) = (2nd ‘⟨∅, 𝐶⟩))
56		op2ndg 7992	. . . . . . . . 9 ⊢ ((∅ ∈ ω ∧ 𝐶 ∈ 𝐴) → (2nd ‘⟨∅, 𝐶⟩) = 𝐶)
57	1, 56	mpan 687	. . . . . . . 8 ⊢ (𝐶 ∈ 𝐴 → (2nd ‘⟨∅, 𝐶⟩) = 𝐶)
58	55, 57	sylan9eqr 2793	. . . . . . 7 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ((2nd ∘ ℎ)‘∅) = 𝐶)
59		nfv 1916	. . . . . . . . 9 ⊢ Ⅎ𝑘 𝐶 ∈ 𝐴
60		nfv 1916	. . . . . . . . . 10 ⊢ Ⅎ𝑘 ℎ:ω⟶(ω × 𝐴)
61		nfv 1916	. . . . . . . . . 10 ⊢ Ⅎ𝑘(ℎ‘∅) = ⟨∅, 𝐶⟩
62		nfra1 3280	. . . . . . . . . 10 ⊢ Ⅎ𝑘∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))
63	60, 61, 62	nf3an 1903	. . . . . . . . 9 ⊢ Ⅎ𝑘(ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))
64	59, 63	nfan 1901	. . . . . . . 8 ⊢ Ⅎ𝑘(𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))))
65		fveq2 6891	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = ∅ → (ℎ‘𝑚) = (ℎ‘∅))
66		opeq1 4873	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = ∅ → ⟨𝑚, 𝑧⟩ = ⟨∅, 𝑧⟩)
67	65, 66	eqeq12d 2747	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = ∅ → ((ℎ‘𝑚) = ⟨𝑚, 𝑧⟩ ↔ (ℎ‘∅) = ⟨∅, 𝑧⟩))
68	67	exbidv 1923	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = ∅ → (∃𝑧(ℎ‘𝑚) = ⟨𝑚, 𝑧⟩ ↔ ∃𝑧(ℎ‘∅) = ⟨∅, 𝑧⟩))
69		fveq2 6891	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑖 → (ℎ‘𝑚) = (ℎ‘𝑖))
70		opeq1 4873	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑖 → ⟨𝑚, 𝑧⟩ = ⟨𝑖, 𝑧⟩)
71	69, 70	eqeq12d 2747	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑖 → ((ℎ‘𝑚) = ⟨𝑚, 𝑧⟩ ↔ (ℎ‘𝑖) = ⟨𝑖, 𝑧⟩))
72	71	exbidv 1923	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑖 → (∃𝑧(ℎ‘𝑚) = ⟨𝑚, 𝑧⟩ ↔ ∃𝑧(ℎ‘𝑖) = ⟨𝑖, 𝑧⟩))
73		fveq2 6891	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = suc 𝑖 → (ℎ‘𝑚) = (ℎ‘suc 𝑖))
74		opeq1 4873	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = suc 𝑖 → ⟨𝑚, 𝑧⟩ = ⟨suc 𝑖, 𝑧⟩)
75	73, 74	eqeq12d 2747	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = suc 𝑖 → ((ℎ‘𝑚) = ⟨𝑚, 𝑧⟩ ↔ (ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩))
76	75	exbidv 1923	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = suc 𝑖 → (∃𝑧(ℎ‘𝑚) = ⟨𝑚, 𝑧⟩ ↔ ∃𝑧(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩))
77		opeq2 4874	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝐶 → ⟨∅, 𝑧⟩ = ⟨∅, 𝐶⟩)
78	77	eqeq2d 2742	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝐶 → ((ℎ‘∅) = ⟨∅, 𝑧⟩ ↔ (ℎ‘∅) = ⟨∅, 𝐶⟩))
79	78	spcegv 3587	. . . . . . . . . . . . . . . . 17 ⊢ (𝐶 ∈ 𝐴 → ((ℎ‘∅) = ⟨∅, 𝐶⟩ → ∃𝑧(ℎ‘∅) = ⟨∅, 𝑧⟩))
80	79	imp 406	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩) → ∃𝑧(ℎ‘∅) = ⟨∅, 𝑧⟩)
81	80	3ad2antr2 1188	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ∃𝑧(ℎ‘∅) = ⟨∅, 𝑧⟩)
82		fveq2 6891	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → (𝐺‘(ℎ‘𝑖)) = (𝐺‘⟨𝑖, 𝑧⟩))
83		df-ov 7415	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑖𝐺𝑧) = (𝐺‘⟨𝑖, 𝑧⟩)
84	82, 83	eqtr4di 2789	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → (𝐺‘(ℎ‘𝑖)) = (𝑖𝐺𝑧))
85	84	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) ∧ (ℎ‘𝑖) = ⟨𝑖, 𝑧⟩) → (𝐺‘(ℎ‘𝑖)) = (𝑖𝐺𝑧))
86		simplr 766	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) ∧ (ℎ‘𝑖) = ⟨𝑖, 𝑧⟩) → 𝑖 ∈ ω)
87		ffvelcdm 7083	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) → (ℎ‘𝑖) ∈ (ω × 𝐴))
88		eleq1 2820	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ((ℎ‘𝑖) ∈ (ω × 𝐴) ↔ ⟨𝑖, 𝑧⟩ ∈ (ω × 𝐴)))
89		opelxp2 5719	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (⟨𝑖, 𝑧⟩ ∈ (ω × 𝐴) → 𝑧 ∈ 𝐴)
90	88, 89	syl6bi 253	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ((ℎ‘𝑖) ∈ (ω × 𝐴) → 𝑧 ∈ 𝐴))
91	87, 90	mpan9 506	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) ∧ (ℎ‘𝑖) = ⟨𝑖, 𝑧⟩) → 𝑧 ∈ 𝐴)
92		suceq 6430	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑛 = 𝑖 → suc 𝑛 = suc 𝑖)
93	92	sneqd 4640	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑛 = 𝑖 → {suc 𝑛} = {suc 𝑖})
94		oveq1 7419	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑛 = 𝑖 → (𝑛𝐹𝑥) = (𝑖𝐹𝑥))
95	93, 94	xpeq12d 5707	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑛 = 𝑖 → ({suc 𝑛} × (𝑛𝐹𝑥)) = ({suc 𝑖} × (𝑖𝐹𝑥)))
96		oveq2 7420	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 = 𝑧 → (𝑖𝐹𝑥) = (𝑖𝐹𝑧))
97	96	xpeq2d 5706	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = 𝑧 → ({suc 𝑖} × (𝑖𝐹𝑥)) = ({suc 𝑖} × (𝑖𝐹𝑧)))
98		snex 5431	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ {suc 𝑖} ∈ V
99		ovex 7445	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑖𝐹𝑧) ∈ V
100	98, 99	xpex 7744	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ({suc 𝑖} × (𝑖𝐹𝑧)) ∈ V
101	95, 97, 37, 100	ovmpo 7571	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑖 ∈ ω ∧ 𝑧 ∈ 𝐴) → (𝑖𝐺𝑧) = ({suc 𝑖} × (𝑖𝐹𝑧)))
102	86, 91, 101	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) ∧ (ℎ‘𝑖) = ⟨𝑖, 𝑧⟩) → (𝑖𝐺𝑧) = ({suc 𝑖} × (𝑖𝐹𝑧)))
103	85, 102	eqtrd 2771	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) ∧ (ℎ‘𝑖) = ⟨𝑖, 𝑧⟩) → (𝐺‘(ℎ‘𝑖)) = ({suc 𝑖} × (𝑖𝐹𝑧)))
104		suceq 6430	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑘 = 𝑖 → suc 𝑘 = suc 𝑖)
105	104	fveq2d 6895	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 = 𝑖 → (ℎ‘suc 𝑘) = (ℎ‘suc 𝑖))
106		2fveq3 6896	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 = 𝑖 → (𝐺‘(ℎ‘𝑘)) = (𝐺‘(ℎ‘𝑖)))
107	105, 106	eleq12d 2826	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 = 𝑖 → ((ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) ↔ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))))
108	107	rspcv 3608	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 ∈ ω → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))))
109	108	ad2antlr 724	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) ∧ (ℎ‘𝑖) = ⟨𝑖, 𝑧⟩) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))))
110		eleq2 2821	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐺‘(ℎ‘𝑖)) = ({suc 𝑖} × (𝑖𝐹𝑧)) → ((ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖)) ↔ (ℎ‘suc 𝑖) ∈ ({suc 𝑖} × (𝑖𝐹𝑧))))
111		elxp 5699	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((ℎ‘suc 𝑖) ∈ ({suc 𝑖} × (𝑖𝐹𝑧)) ↔ ∃𝑠∃𝑡((ℎ‘suc 𝑖) = ⟨𝑠, 𝑡⟩ ∧ (𝑠 ∈ {suc 𝑖} ∧ 𝑡 ∈ (𝑖𝐹𝑧))))
112		velsn 4644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑠 ∈ {suc 𝑖} ↔ 𝑠 = suc 𝑖)
113		opeq1 4873	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑠 = suc 𝑖 → ⟨𝑠, 𝑡⟩ = ⟨suc 𝑖, 𝑡⟩)
114	112, 113	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑠 ∈ {suc 𝑖} → ⟨𝑠, 𝑡⟩ = ⟨suc 𝑖, 𝑡⟩)
115	114	eqeq2d 2742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑠 ∈ {suc 𝑖} → ((ℎ‘suc 𝑖) = ⟨𝑠, 𝑡⟩ ↔ (ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩))
116	115	biimpac 478	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((ℎ‘suc 𝑖) = ⟨𝑠, 𝑡⟩ ∧ 𝑠 ∈ {suc 𝑖}) → (ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩)
117	116	adantrr 714	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((ℎ‘suc 𝑖) = ⟨𝑠, 𝑡⟩ ∧ (𝑠 ∈ {suc 𝑖} ∧ 𝑡 ∈ (𝑖𝐹𝑧))) → (ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩)
118	117	eximi 1836	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∃𝑡((ℎ‘suc 𝑖) = ⟨𝑠, 𝑡⟩ ∧ (𝑠 ∈ {suc 𝑖} ∧ 𝑡 ∈ (𝑖𝐹𝑧))) → ∃𝑡(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩)
119	118	exlimiv 1932	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∃𝑠∃𝑡((ℎ‘suc 𝑖) = ⟨𝑠, 𝑡⟩ ∧ (𝑠 ∈ {suc 𝑖} ∧ 𝑡 ∈ (𝑖𝐹𝑧))) → ∃𝑡(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩)
120	111, 119	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((ℎ‘suc 𝑖) ∈ ({suc 𝑖} × (𝑖𝐹𝑧)) → ∃𝑡(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩)
121	110, 120	syl6bi 253	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐺‘(ℎ‘𝑖)) = ({suc 𝑖} × (𝑖𝐹𝑧)) → ((ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖)) → ∃𝑡(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩))
122	103, 109, 121	sylsyld 61	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) ∧ (ℎ‘𝑖) = ⟨𝑖, 𝑧⟩) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → ∃𝑡(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩))
123	122	expcom 413	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → ∃𝑡(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩)))
124	123	exlimiv 1932	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑧(ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → ∃𝑡(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩)))
125	124	com3l 89	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → (∃𝑧(ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ∃𝑡(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩)))
126		opeq2 4874	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 = 𝑧 → ⟨suc 𝑖, 𝑡⟩ = ⟨suc 𝑖, 𝑧⟩)
127	126	eqeq2d 2742	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 = 𝑧 → ((ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩ ↔ (ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩))
128	127	cbvexvw 2039	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑡(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩ ↔ ∃𝑧(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩)
129	125, 128	syl8ib 256	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → (∃𝑧(ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ∃𝑧(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩)))
130	129	impancom 451	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑖 ∈ ω → (∃𝑧(ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ∃𝑧(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩)))
131	130	3adant2 1130	. . . . . . . . . . . . . . . . 17 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑖 ∈ ω → (∃𝑧(ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ∃𝑧(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩)))
132	131	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (𝑖 ∈ ω → (∃𝑧(ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ∃𝑧(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩)))
133	132	com12 32	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ ω → ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (∃𝑧(ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ∃𝑧(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩)))
134	68, 72, 76, 81, 133	finds2 7895	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ω → ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ∃𝑧(ℎ‘𝑚) = ⟨𝑚, 𝑧⟩))
135	134	com12 32	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (𝑚 ∈ ω → ∃𝑧(ℎ‘𝑚) = ⟨𝑚, 𝑧⟩))
136	135	ralrimiv 3144	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ∀𝑚 ∈ ω ∃𝑧(ℎ‘𝑚) = ⟨𝑚, 𝑧⟩)
137		fveq2 6891	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑘 → (ℎ‘𝑚) = (ℎ‘𝑘))
138		opeq1 4873	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑘 → ⟨𝑚, 𝑧⟩ = ⟨𝑘, 𝑧⟩)
139	137, 138	eqeq12d 2747	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑘 → ((ℎ‘𝑚) = ⟨𝑚, 𝑧⟩ ↔ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩))
140	139	exbidv 1923	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑘 → (∃𝑧(ℎ‘𝑚) = ⟨𝑚, 𝑧⟩ ↔ ∃𝑧(ℎ‘𝑘) = ⟨𝑘, 𝑧⟩))
141	140	rspccv 3609	. . . . . . . . . . . 12 ⊢ (∀𝑚 ∈ ω ∃𝑧(ℎ‘𝑚) = ⟨𝑚, 𝑧⟩ → (𝑘 ∈ ω → ∃𝑧(ℎ‘𝑘) = ⟨𝑘, 𝑧⟩))
142	136, 141	syl 17	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (𝑘 ∈ ω → ∃𝑧(ℎ‘𝑘) = ⟨𝑘, 𝑧⟩))
143	142	3impia 1116	. . . . . . . . . 10 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → ∃𝑧(ℎ‘𝑘) = ⟨𝑘, 𝑧⟩)
144		simp21 1205	. . . . . . . . . 10 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → ℎ:ω⟶(ω × 𝐴))
145		simp3 1137	. . . . . . . . . 10 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → 𝑘 ∈ ω)
146		rspa 3244	. . . . . . . . . . . 12 ⊢ ((∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) ∧ 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))
147	146	3ad2antl3 1186	. . . . . . . . . . 11 ⊢ (((ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))
148	147	3adant1 1129	. . . . . . . . . 10 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))
149		simpl 482	. . . . . . . . . . . . . . . . 17 ⊢ (((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩)
150	149	fveq2d 6895	. . . . . . . . . . . . . . . 16 ⊢ (((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (𝐺‘(ℎ‘𝑘)) = (𝐺‘⟨𝑘, 𝑧⟩))
151		simprr 770	. . . . . . . . . . . . . . . . 17 ⊢ (((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → 𝑘 ∈ ω)
152		eleq1 2820	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ → ((ℎ‘𝑘) ∈ (ω × 𝐴) ↔ ⟨𝑘, 𝑧⟩ ∈ (ω × 𝐴)))
153		opelxp2 5719	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨𝑘, 𝑧⟩ ∈ (ω × 𝐴) → 𝑧 ∈ 𝐴)
154	152, 153	syl6bi 253	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ → ((ℎ‘𝑘) ∈ (ω × 𝐴) → 𝑧 ∈ 𝐴))
155		ffvelcdm 7083	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → (ℎ‘𝑘) ∈ (ω × 𝐴))
156	154, 155	impel 505	. . . . . . . . . . . . . . . . 17 ⊢ (((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → 𝑧 ∈ 𝐴)
157		df-ov 7415	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘𝐺𝑧) = (𝐺‘⟨𝑘, 𝑧⟩)
158		suceq 6430	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑘 → suc 𝑛 = suc 𝑘)
159	158	sneqd 4640	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑘 → {suc 𝑛} = {suc 𝑘})
160		oveq1 7419	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑘 → (𝑛𝐹𝑥) = (𝑘𝐹𝑥))
161	159, 160	xpeq12d 5707	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑘 → ({suc 𝑛} × (𝑛𝐹𝑥)) = ({suc 𝑘} × (𝑘𝐹𝑥)))
162		oveq2 7420	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑧 → (𝑘𝐹𝑥) = (𝑘𝐹𝑧))
163	162	xpeq2d 5706	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑧 → ({suc 𝑘} × (𝑘𝐹𝑥)) = ({suc 𝑘} × (𝑘𝐹𝑧)))
164		snex 5431	. . . . . . . . . . . . . . . . . . . 20 ⊢ {suc 𝑘} ∈ V
165		ovex 7445	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘𝐹𝑧) ∈ V
166	164, 165	xpex 7744	. . . . . . . . . . . . . . . . . . 19 ⊢ ({suc 𝑘} × (𝑘𝐹𝑧)) ∈ V
167	161, 163, 37, 166	ovmpo 7571	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ω ∧ 𝑧 ∈ 𝐴) → (𝑘𝐺𝑧) = ({suc 𝑘} × (𝑘𝐹𝑧)))
168	157, 167	eqtr3id 2785	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ω ∧ 𝑧 ∈ 𝐴) → (𝐺‘⟨𝑘, 𝑧⟩) = ({suc 𝑘} × (𝑘𝐹𝑧)))
169	151, 156, 168	syl2anc 583	. . . . . . . . . . . . . . . 16 ⊢ (((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (𝐺‘⟨𝑘, 𝑧⟩) = ({suc 𝑘} × (𝑘𝐹𝑧)))
170	150, 169	eqtrd 2771	. . . . . . . . . . . . . . 15 ⊢ (((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (𝐺‘(ℎ‘𝑘)) = ({suc 𝑘} × (𝑘𝐹𝑧)))
171	170	eleq2d 2818	. . . . . . . . . . . . . 14 ⊢ (((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) ↔ (ℎ‘suc 𝑘) ∈ ({suc 𝑘} × (𝑘𝐹𝑧))))
172		elxp 5699	. . . . . . . . . . . . . . . . 17 ⊢ ((ℎ‘suc 𝑘) ∈ ({suc 𝑘} × (𝑘𝐹𝑧)) ↔ ∃𝑠∃𝑡((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (𝑠 ∈ {suc 𝑘} ∧ 𝑡 ∈ (𝑘𝐹𝑧))))
173		peano2 7885	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 ∈ ω → suc 𝑘 ∈ ω)
174		fvco3 6990	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ suc 𝑘 ∈ ω) → ((2nd ∘ ℎ)‘suc 𝑘) = (2nd ‘(ℎ‘suc 𝑘)))
175	173, 174	sylan2 592	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((2nd ∘ ℎ)‘suc 𝑘) = (2nd ‘(ℎ‘suc 𝑘)))
176	175	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd ∘ ℎ)‘suc 𝑘) = (2nd ‘(ℎ‘suc 𝑘)))
177		simpll 764	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩)
178	177	fveq2d 6895	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (2nd ‘(ℎ‘suc 𝑘)) = (2nd ‘⟨𝑠, 𝑡⟩))
179	176, 178	eqtrd 2771	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd ∘ ℎ)‘suc 𝑘) = (2nd ‘⟨𝑠, 𝑡⟩))
180		vex 3477	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑠 ∈ V
181		vex 3477	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑡 ∈ V
182	180, 181	op2nd 7988	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (2nd ‘⟨𝑠, 𝑡⟩) = 𝑡
183	179, 182	eqtrdi 2787	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd ∘ ℎ)‘suc 𝑘) = 𝑡)
184		fvco3 6990	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((2nd ∘ ℎ)‘𝑘) = (2nd ‘(ℎ‘𝑘)))
185	184	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd ∘ ℎ)‘𝑘) = (2nd ‘(ℎ‘𝑘)))
186		simplr 766	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩)
187	186	fveq2d 6895	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (2nd ‘(ℎ‘𝑘)) = (2nd ‘⟨𝑘, 𝑧⟩))
188	185, 187	eqtrd 2771	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd ∘ ℎ)‘𝑘) = (2nd ‘⟨𝑘, 𝑧⟩))
189		vex 3477	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑘 ∈ V
190		vex 3477	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑧 ∈ V
191	189, 190	op2nd 7988	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (2nd ‘⟨𝑘, 𝑧⟩) = 𝑧
192	188, 191	eqtrdi 2787	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd ∘ ℎ)‘𝑘) = 𝑧)
193	192	oveq2d 7428	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (𝑘𝐹((2nd ∘ ℎ)‘𝑘)) = (𝑘𝐹𝑧))
194	183, 193	eleq12d 2826	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)) ↔ 𝑡 ∈ (𝑘𝐹𝑧)))
195	194	biimprcd 249	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 ∈ (𝑘𝐹𝑧) → ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))
196	195	exp4c 432	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ∈ (𝑘𝐹𝑧) → ((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ → ((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))))
197	196	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑠 ∈ {suc 𝑘} ∧ 𝑡 ∈ (𝑘𝐹𝑧)) → ((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ → ((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))))
198	197	impcom 407	. . . . . . . . . . . . . . . . . 18 ⊢ (((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (𝑠 ∈ {suc 𝑘} ∧ 𝑡 ∈ (𝑘𝐹𝑧))) → ((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))))
199	198	exlimivv 1934	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑠∃𝑡((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (𝑠 ∈ {suc 𝑘} ∧ 𝑡 ∈ (𝑘𝐹𝑧))) → ((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))))
200	172, 199	sylbi 216	. . . . . . . . . . . . . . . 16 ⊢ ((ℎ‘suc 𝑘) ∈ ({suc 𝑘} × (𝑘𝐹𝑧)) → ((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))))
201	200	com3l 89	. . . . . . . . . . . . . . 15 ⊢ ((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((ℎ‘suc 𝑘) ∈ ({suc 𝑘} × (𝑘𝐹𝑧)) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))))
202	201	imp 406	. . . . . . . . . . . . . 14 ⊢ (((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((ℎ‘suc 𝑘) ∈ ({suc 𝑘} × (𝑘𝐹𝑧)) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))
203	171, 202	sylbid 239	. . . . . . . . . . . . 13 ⊢ (((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))
204	203	ex 412	. . . . . . . . . . . 12 ⊢ ((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))))
205	204	exlimiv 1932	. . . . . . . . . . 11 ⊢ (∃𝑧(ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))))
206	205	3imp 1110	. . . . . . . . . 10 ⊢ ((∃𝑧(ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) ∧ (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))
207	143, 144, 145, 148, 206	syl121anc 1374	. . . . . . . . 9 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))
208	207	3expia 1120	. . . . . . . 8 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (𝑘 ∈ ω → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))
209	64, 208	ralrimi 3253	. . . . . . 7 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ∀𝑘 ∈ ω ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))
210	46, 58, 209	3jca 1127	. . . . . 6 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ((2nd ∘ ℎ):ω⟶𝐴 ∧ ((2nd ∘ ℎ)‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))
211		feq1 6698	. . . . . . 7 ⊢ (𝑔 = (2nd ∘ ℎ) → (𝑔:ω⟶𝐴 ↔ (2nd ∘ ℎ):ω⟶𝐴))
212		fveq1 6890	. . . . . . . 8 ⊢ (𝑔 = (2nd ∘ ℎ) → (𝑔‘∅) = ((2nd ∘ ℎ)‘∅))
213	212	eqeq1d 2733	. . . . . . 7 ⊢ (𝑔 = (2nd ∘ ℎ) → ((𝑔‘∅) = 𝐶 ↔ ((2nd ∘ ℎ)‘∅) = 𝐶))
214		fveq1 6890	. . . . . . . . 9 ⊢ (𝑔 = (2nd ∘ ℎ) → (𝑔‘suc 𝑘) = ((2nd ∘ ℎ)‘suc 𝑘))
215		fveq1 6890	. . . . . . . . . 10 ⊢ (𝑔 = (2nd ∘ ℎ) → (𝑔‘𝑘) = ((2nd ∘ ℎ)‘𝑘))
216	215	oveq2d 7428	. . . . . . . . 9 ⊢ (𝑔 = (2nd ∘ ℎ) → (𝑘𝐹(𝑔‘𝑘)) = (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))
217	214, 216	eleq12d 2826	. . . . . . . 8 ⊢ (𝑔 = (2nd ∘ ℎ) → ((𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘)) ↔ ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))
218	217	ralbidv 3176	. . . . . . 7 ⊢ (𝑔 = (2nd ∘ ℎ) → (∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘)) ↔ ∀𝑘 ∈ ω ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))
219	211, 213, 218	3anbi123d 1435	. . . . . 6 ⊢ (𝑔 = (2nd ∘ ℎ) → ((𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘))) ↔ ((2nd ∘ ℎ):ω⟶𝐴 ∧ ((2nd ∘ ℎ)‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))))
220	49, 210, 219	spcedv 3588	. . . . 5 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘))))
221	220	ex 412	. . . 4 ⊢ (𝐶 ∈ 𝐴 → ((ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘)))))
222	221	exlimdv 1935	. . 3 ⊢ (𝐶 ∈ 𝐴 → (∃ℎ(ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘)))))
223	222	adantr 480	. 2 ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅})) → (∃ℎ(ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘)))))
224	43, 223	mpd 15	1 ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘))))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1540  ∃wex 1780   ∈ wcel 2105   ≠ wne 2939  ∀wral 3060  Vcvv 3473   ∖ cdif 3945   ⊆ wss 3948  ∅c0 4322  𝒫 cpw 4602  {csn 4628  ⟨cop 4634   × cxp 5674   ∘ ccom 5680  suc csuc 6366  ⟶wf 6539  ‘cfv 6543  (class class class)co 7412   ∈ cmpo 7414  ωcom 7859  2^nd c2nd 7978

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729  ax-dc 10445

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7860  df-1st 7979  df-2nd 7980  df-1o 8470

This theorem is referenced by:  axdc4  10455