Theorem axdc4lem 10452

Description: Lemma for axdc4 10453. (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 7881	. . . 4 ⊢ ∅ ∈ ω
2		opelxpi 5712	. . . 4 ⊢ ((∅ ∈ ω ∧ 𝐶 ∈ 𝐴) → ⟨∅, 𝐶⟩ ∈ (ω × 𝐴))
3	1, 2	mpan 686	. . 3 ⊢ (𝐶 ∈ 𝐴 → ⟨∅, 𝐶⟩ ∈ (ω × 𝐴))
4		simp2 1135	. . . . . . . 8 ⊢ ((𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑛 ∈ ω ∧ 𝑥 ∈ 𝐴) → 𝑛 ∈ ω)
5		fovcdm 7579	. . . . . . . 8 ⊢ ((𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑛 ∈ ω ∧ 𝑥 ∈ 𝐴) → (𝑛𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅}))
6		peano2 7883	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ω → suc 𝑛 ∈ ω)
7	6	snssd 4811	. . . . . . . . . 10 ⊢ (𝑛 ∈ ω → {suc 𝑛} ⊆ ω)
8		eldifi 4125	. . . . . . . . . 10 ⊢ ((𝑛𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → (𝑛𝐹𝑥) ∈ 𝒫 𝐴)
9		axdc4lem.1	. . . . . . . . . . . 12 ⊢ 𝐴 ∈ V
10	9	elpw2 5344	. . . . . . . . . . 11 ⊢ ((𝑛𝐹𝑥) ∈ 𝒫 𝐴 ↔ (𝑛𝐹𝑥) ⊆ 𝐴)
11		xpss12 5690	. . . . . . . . . . 11 ⊢ (({suc 𝑛} ⊆ ω ∧ (𝑛𝐹𝑥) ⊆ 𝐴) → ({suc 𝑛} × (𝑛𝐹𝑥)) ⊆ (ω × 𝐴))
12	10, 11	sylan2b 592	. . . . . . . . . 10 ⊢ (({suc 𝑛} ⊆ ω ∧ (𝑛𝐹𝑥) ∈ 𝒫 𝐴) → ({suc 𝑛} × (𝑛𝐹𝑥)) ⊆ (ω × 𝐴))
13	7, 8, 12	syl2an 594	. . . . . . . . 9 ⊢ ((𝑛 ∈ ω ∧ (𝑛𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅})) → ({suc 𝑛} × (𝑛𝐹𝑥)) ⊆ (ω × 𝐴))
14		snex 5430	. . . . . . . . . . 11 ⊢ {suc 𝑛} ∈ V
15		ovex 7444	. . . . . . . . . . 11 ⊢ (𝑛𝐹𝑥) ∈ V
16	14, 15	xpex 7742	. . . . . . . . . 10 ⊢ ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ V
17	16	elpw 4605	. . . . . . . . 9 ⊢ (({suc 𝑛} × (𝑛𝐹𝑥)) ∈ 𝒫 (ω × 𝐴) ↔ ({suc 𝑛} × (𝑛𝐹𝑥)) ⊆ (ω × 𝐴))
18	13, 17	sylibr 233	. . . . . . . 8 ⊢ ((𝑛 ∈ ω ∧ (𝑛𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅})) → ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ 𝒫 (ω × 𝐴))
19	4, 5, 18	syl2anc 582	. . . . . . 7 ⊢ ((𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑛 ∈ ω ∧ 𝑥 ∈ 𝐴) → ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ 𝒫 (ω × 𝐴))
20		eldifn 4126	. . . . . . . 8 ⊢ ((𝑛𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → ¬ (𝑛𝐹𝑥) ∈ {∅})
21	15	elsn 4642	. . . . . . . . . . 11 ⊢ ((𝑛𝐹𝑥) ∈ {∅} ↔ (𝑛𝐹𝑥) = ∅)
22	21	necon3bbii 2986	. . . . . . . . . 10 ⊢ (¬ (𝑛𝐹𝑥) ∈ {∅} ↔ (𝑛𝐹𝑥) ≠ ∅)
23		vex 3476	. . . . . . . . . . . . 13 ⊢ 𝑛 ∈ V
24	23	sucex 7796	. . . . . . . . . . . 12 ⊢ suc 𝑛 ∈ V
25	24	snnz 4779	. . . . . . . . . . 11 ⊢ {suc 𝑛} ≠ ∅
26		xpnz 6157	. . . . . . . . . . . 12 ⊢ (({suc 𝑛} ≠ ∅ ∧ (𝑛𝐹𝑥) ≠ ∅) ↔ ({suc 𝑛} × (𝑛𝐹𝑥)) ≠ ∅)
27	26	biimpi 215	. . . . . . . . . . 11 ⊢ (({suc 𝑛} ≠ ∅ ∧ (𝑛𝐹𝑥) ≠ ∅) → ({suc 𝑛} × (𝑛𝐹𝑥)) ≠ ∅)
28	25, 27	mpan 686	. . . . . . . . . 10 ⊢ ((𝑛𝐹𝑥) ≠ ∅ → ({suc 𝑛} × (𝑛𝐹𝑥)) ≠ ∅)
29	22, 28	sylbi 216	. . . . . . . . 9 ⊢ (¬ (𝑛𝐹𝑥) ∈ {∅} → ({suc 𝑛} × (𝑛𝐹𝑥)) ≠ ∅)
30	16	elsn 4642	. . . . . . . . . 10 ⊢ (({suc 𝑛} × (𝑛𝐹𝑥)) ∈ {∅} ↔ ({suc 𝑛} × (𝑛𝐹𝑥)) = ∅)
31	30	necon3bbii 2986	. . . . . . . . 9 ⊢ (¬ ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ {∅} ↔ ({suc 𝑛} × (𝑛𝐹𝑥)) ≠ ∅)
32	29, 31	sylibr 233	. . . . . . . 8 ⊢ (¬ (𝑛𝐹𝑥) ∈ {∅} → ¬ ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ {∅})
33	5, 20, 32	3syl 18	. . . . . . 7 ⊢ ((𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑛 ∈ ω ∧ 𝑥 ∈ 𝐴) → ¬ ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ {∅})
34	19, 33	eldifd 3958	. . . . . 6 ⊢ ((𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑛 ∈ ω ∧ 𝑥 ∈ 𝐴) → ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ (𝒫 (ω × 𝐴) ∖ {∅}))
35	34	3expib 1120	. . . . 5 ⊢ (𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) → ((𝑛 ∈ ω ∧ 𝑥 ∈ 𝐴) → ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ (𝒫 (ω × 𝐴) ∖ {∅})))
36	35	ralrimivv 3196	. . . 4 ⊢ (𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) → ∀𝑛 ∈ ω ∀𝑥 ∈ 𝐴 ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ (𝒫 (ω × 𝐴) ∖ {∅}))
37		axdc4lem.2	. . . . 5 ⊢ 𝐺 = (𝑛 ∈ ω, 𝑥 ∈ 𝐴 ↦ ({suc 𝑛} × (𝑛𝐹𝑥)))
38	37	fmpo 8056	. . . 4 ⊢ (∀𝑛 ∈ ω ∀𝑥 ∈ 𝐴 ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ (𝒫 (ω × 𝐴) ∖ {∅}) ↔ 𝐺:(ω × 𝐴)⟶(𝒫 (ω × 𝐴) ∖ {∅}))
39	36, 38	sylib 217	. . 3 ⊢ (𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) → 𝐺:(ω × 𝐴)⟶(𝒫 (ω × 𝐴) ∖ {∅}))
40		dcomex 10444	. . . . 5 ⊢ ω ∈ V
41	40, 9	xpex 7742	. . . 4 ⊢ (ω × 𝐴) ∈ V
42	41	axdc3 10451	. . 3 ⊢ ((⟨∅, 𝐶⟩ ∈ (ω × 𝐴) ∧ 𝐺:(ω × 𝐴)⟶(𝒫 (ω × 𝐴) ∖ {∅})) → ∃ℎ(ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))))
43	3, 39, 42	syl2an 594	. 2 ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅})) → ∃ℎ(ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))))
44		2ndcof 8008	. . . . . . . . 9 ⊢ (ℎ:ω⟶(ω × 𝐴) → (2nd ∘ ℎ):ω⟶𝐴)
45	44	3ad2ant1 1131	. . . . . . . 8 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (2nd ∘ ℎ):ω⟶𝐴)
46	45	adantl 480	. . . . . . 7 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (2nd ∘ ℎ):ω⟶𝐴)
47		fex2 7926	. . . . . . . 8 ⊢ (((2nd ∘ ℎ):ω⟶𝐴 ∧ ω ∈ V ∧ 𝐴 ∈ V) → (2nd ∘ ℎ) ∈ V)
48	40, 9, 47	mp3an23 1451	. . . . . . 7 ⊢ ((2nd ∘ ℎ):ω⟶𝐴 → (2nd ∘ ℎ) ∈ V)
49	46, 48	syl 17	. . . . . 6 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (2nd ∘ ℎ) ∈ V)
50		fvco3 6989	. . . . . . . . . . 11 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ ∅ ∈ ω) → ((2nd ∘ ℎ)‘∅) = (2nd ‘(ℎ‘∅)))
51	1, 50	mpan2 687	. . . . . . . . . 10 ⊢ (ℎ:ω⟶(ω × 𝐴) → ((2nd ∘ ℎ)‘∅) = (2nd ‘(ℎ‘∅)))
52	51	3ad2ant1 1131	. . . . . . . . 9 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ((2nd ∘ ℎ)‘∅) = (2nd ‘(ℎ‘∅)))
53		fveq2 6890	. . . . . . . . . 10 ⊢ ((ℎ‘∅) = ⟨∅, 𝐶⟩ → (2nd ‘(ℎ‘∅)) = (2nd ‘⟨∅, 𝐶⟩))
54	53	3ad2ant2 1132	. . . . . . . . 9 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (2nd ‘(ℎ‘∅)) = (2nd ‘⟨∅, 𝐶⟩))
55	52, 54	eqtrd 2770	. . . . . . . 8 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ((2nd ∘ ℎ)‘∅) = (2nd ‘⟨∅, 𝐶⟩))
56		op2ndg 7990	. . . . . . . . 9 ⊢ ((∅ ∈ ω ∧ 𝐶 ∈ 𝐴) → (2nd ‘⟨∅, 𝐶⟩) = 𝐶)
57	1, 56	mpan 686	. . . . . . . 8 ⊢ (𝐶 ∈ 𝐴 → (2nd ‘⟨∅, 𝐶⟩) = 𝐶)
58	55, 57	sylan9eqr 2792	. . . . . . 7 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ((2nd ∘ ℎ)‘∅) = 𝐶)
59		nfv 1915	. . . . . . . . 9 ⊢ Ⅎ𝑘 𝐶 ∈ 𝐴
60		nfv 1915	. . . . . . . . . 10 ⊢ Ⅎ𝑘 ℎ:ω⟶(ω × 𝐴)
61		nfv 1915	. . . . . . . . . 10 ⊢ Ⅎ𝑘(ℎ‘∅) = ⟨∅, 𝐶⟩
62		nfra1 3279	. . . . . . . . . 10 ⊢ Ⅎ𝑘∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))
63	60, 61, 62	nf3an 1902	. . . . . . . . 9 ⊢ Ⅎ𝑘(ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))
64	59, 63	nfan 1900	. . . . . . . 8 ⊢ Ⅎ𝑘(𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))))
65		fveq2 6890	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = ∅ → (ℎ‘𝑚) = (ℎ‘∅))
66		opeq1 4872	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = ∅ → ⟨𝑚, 𝑧⟩ = ⟨∅, 𝑧⟩)
67	65, 66	eqeq12d 2746	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = ∅ → ((ℎ‘𝑚) = ⟨𝑚, 𝑧⟩ ↔ (ℎ‘∅) = ⟨∅, 𝑧⟩))
68	67	exbidv 1922	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = ∅ → (∃𝑧(ℎ‘𝑚) = ⟨𝑚, 𝑧⟩ ↔ ∃𝑧(ℎ‘∅) = ⟨∅, 𝑧⟩))
69		fveq2 6890	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑖 → (ℎ‘𝑚) = (ℎ‘𝑖))
70		opeq1 4872	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑖 → ⟨𝑚, 𝑧⟩ = ⟨𝑖, 𝑧⟩)
71	69, 70	eqeq12d 2746	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑖 → ((ℎ‘𝑚) = ⟨𝑚, 𝑧⟩ ↔ (ℎ‘𝑖) = ⟨𝑖, 𝑧⟩))
72	71	exbidv 1922	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑖 → (∃𝑧(ℎ‘𝑚) = ⟨𝑚, 𝑧⟩ ↔ ∃𝑧(ℎ‘𝑖) = ⟨𝑖, 𝑧⟩))
73		fveq2 6890	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = suc 𝑖 → (ℎ‘𝑚) = (ℎ‘suc 𝑖))
74		opeq1 4872	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = suc 𝑖 → ⟨𝑚, 𝑧⟩ = ⟨suc 𝑖, 𝑧⟩)
75	73, 74	eqeq12d 2746	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = suc 𝑖 → ((ℎ‘𝑚) = ⟨𝑚, 𝑧⟩ ↔ (ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩))
76	75	exbidv 1922	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = suc 𝑖 → (∃𝑧(ℎ‘𝑚) = ⟨𝑚, 𝑧⟩ ↔ ∃𝑧(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩))
77		opeq2 4873	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝐶 → ⟨∅, 𝑧⟩ = ⟨∅, 𝐶⟩)
78	77	eqeq2d 2741	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝐶 → ((ℎ‘∅) = ⟨∅, 𝑧⟩ ↔ (ℎ‘∅) = ⟨∅, 𝐶⟩))
79	78	spcegv 3586	. . . . . . . . . . . . . . . . 17 ⊢ (𝐶 ∈ 𝐴 → ((ℎ‘∅) = ⟨∅, 𝐶⟩ → ∃𝑧(ℎ‘∅) = ⟨∅, 𝑧⟩))
80	79	imp 405	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩) → ∃𝑧(ℎ‘∅) = ⟨∅, 𝑧⟩)
81	80	3ad2antr2 1187	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ∃𝑧(ℎ‘∅) = ⟨∅, 𝑧⟩)
82		fveq2 6890	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → (𝐺‘(ℎ‘𝑖)) = (𝐺‘⟨𝑖, 𝑧⟩))
83		df-ov 7414	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑖𝐺𝑧) = (𝐺‘⟨𝑖, 𝑧⟩)
84	82, 83	eqtr4di 2788	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → (𝐺‘(ℎ‘𝑖)) = (𝑖𝐺𝑧))
85	84	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) ∧ (ℎ‘𝑖) = ⟨𝑖, 𝑧⟩) → (𝐺‘(ℎ‘𝑖)) = (𝑖𝐺𝑧))
86		simplr 765	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) ∧ (ℎ‘𝑖) = ⟨𝑖, 𝑧⟩) → 𝑖 ∈ ω)
87		ffvelcdm 7082	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) → (ℎ‘𝑖) ∈ (ω × 𝐴))
88		eleq1 2819	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ((ℎ‘𝑖) ∈ (ω × 𝐴) ↔ ⟨𝑖, 𝑧⟩ ∈ (ω × 𝐴)))
89		opelxp2 5718	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (⟨𝑖, 𝑧⟩ ∈ (ω × 𝐴) → 𝑧 ∈ 𝐴)
90	88, 89	syl6bi 252	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ((ℎ‘𝑖) ∈ (ω × 𝐴) → 𝑧 ∈ 𝐴))
91	87, 90	mpan9 505	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) ∧ (ℎ‘𝑖) = ⟨𝑖, 𝑧⟩) → 𝑧 ∈ 𝐴)
92		suceq 6429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑛 = 𝑖 → suc 𝑛 = suc 𝑖)
93	92	sneqd 4639	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑛 = 𝑖 → {suc 𝑛} = {suc 𝑖})
94		oveq1 7418	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑛 = 𝑖 → (𝑛𝐹𝑥) = (𝑖𝐹𝑥))
95	93, 94	xpeq12d 5706	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑛 = 𝑖 → ({suc 𝑛} × (𝑛𝐹𝑥)) = ({suc 𝑖} × (𝑖𝐹𝑥)))
96		oveq2 7419	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 = 𝑧 → (𝑖𝐹𝑥) = (𝑖𝐹𝑧))
97	96	xpeq2d 5705	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = 𝑧 → ({suc 𝑖} × (𝑖𝐹𝑥)) = ({suc 𝑖} × (𝑖𝐹𝑧)))
98		snex 5430	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ {suc 𝑖} ∈ V
99		ovex 7444	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑖𝐹𝑧) ∈ V
100	98, 99	xpex 7742	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ({suc 𝑖} × (𝑖𝐹𝑧)) ∈ V
101	95, 97, 37, 100	ovmpo 7570	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑖 ∈ ω ∧ 𝑧 ∈ 𝐴) → (𝑖𝐺𝑧) = ({suc 𝑖} × (𝑖𝐹𝑧)))
102	86, 91, 101	syl2anc 582	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) ∧ (ℎ‘𝑖) = ⟨𝑖, 𝑧⟩) → (𝑖𝐺𝑧) = ({suc 𝑖} × (𝑖𝐹𝑧)))
103	85, 102	eqtrd 2770	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) ∧ (ℎ‘𝑖) = ⟨𝑖, 𝑧⟩) → (𝐺‘(ℎ‘𝑖)) = ({suc 𝑖} × (𝑖𝐹𝑧)))
104		suceq 6429	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑘 = 𝑖 → suc 𝑘 = suc 𝑖)
105	104	fveq2d 6894	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 = 𝑖 → (ℎ‘suc 𝑘) = (ℎ‘suc 𝑖))
106		2fveq3 6895	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 = 𝑖 → (𝐺‘(ℎ‘𝑘)) = (𝐺‘(ℎ‘𝑖)))
107	105, 106	eleq12d 2825	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 = 𝑖 → ((ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) ↔ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))))
108	107	rspcv 3607	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 ∈ ω → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))))
109	108	ad2antlr 723	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) ∧ (ℎ‘𝑖) = ⟨𝑖, 𝑧⟩) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))))
110		eleq2 2820	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐺‘(ℎ‘𝑖)) = ({suc 𝑖} × (𝑖𝐹𝑧)) → ((ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖)) ↔ (ℎ‘suc 𝑖) ∈ ({suc 𝑖} × (𝑖𝐹𝑧))))
111		elxp 5698	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((ℎ‘suc 𝑖) ∈ ({suc 𝑖} × (𝑖𝐹𝑧)) ↔ ∃𝑠∃𝑡((ℎ‘suc 𝑖) = ⟨𝑠, 𝑡⟩ ∧ (𝑠 ∈ {suc 𝑖} ∧ 𝑡 ∈ (𝑖𝐹𝑧))))
112		velsn 4643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑠 ∈ {suc 𝑖} ↔ 𝑠 = suc 𝑖)
113		opeq1 4872	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑠 = suc 𝑖 → ⟨𝑠, 𝑡⟩ = ⟨suc 𝑖, 𝑡⟩)
114	112, 113	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑠 ∈ {suc 𝑖} → ⟨𝑠, 𝑡⟩ = ⟨suc 𝑖, 𝑡⟩)
115	114	eqeq2d 2741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑠 ∈ {suc 𝑖} → ((ℎ‘suc 𝑖) = ⟨𝑠, 𝑡⟩ ↔ (ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩))
116	115	biimpac 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((ℎ‘suc 𝑖) = ⟨𝑠, 𝑡⟩ ∧ 𝑠 ∈ {suc 𝑖}) → (ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩)
117	116	adantrr 713	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((ℎ‘suc 𝑖) = ⟨𝑠, 𝑡⟩ ∧ (𝑠 ∈ {suc 𝑖} ∧ 𝑡 ∈ (𝑖𝐹𝑧))) → (ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩)
118	117	eximi 1835	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∃𝑡((ℎ‘suc 𝑖) = ⟨𝑠, 𝑡⟩ ∧ (𝑠 ∈ {suc 𝑖} ∧ 𝑡 ∈ (𝑖𝐹𝑧))) → ∃𝑡(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩)
119	118	exlimiv 1931	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∃𝑠∃𝑡((ℎ‘suc 𝑖) = ⟨𝑠, 𝑡⟩ ∧ (𝑠 ∈ {suc 𝑖} ∧ 𝑡 ∈ (𝑖𝐹𝑧))) → ∃𝑡(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩)
120	111, 119	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((ℎ‘suc 𝑖) ∈ ({suc 𝑖} × (𝑖𝐹𝑧)) → ∃𝑡(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩)
121	110, 120	syl6bi 252	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐺‘(ℎ‘𝑖)) = ({suc 𝑖} × (𝑖𝐹𝑧)) → ((ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖)) → ∃𝑡(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩))
122	103, 109, 121	sylsyld 61	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) ∧ (ℎ‘𝑖) = ⟨𝑖, 𝑧⟩) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → ∃𝑡(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩))
123	122	expcom 412	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → ∃𝑡(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩)))
124	123	exlimiv 1931	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑧(ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → ∃𝑡(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩)))
125	124	com3l 89	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → (∃𝑧(ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ∃𝑡(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩)))
126		opeq2 4873	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 = 𝑧 → ⟨suc 𝑖, 𝑡⟩ = ⟨suc 𝑖, 𝑧⟩)
127	126	eqeq2d 2741	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 = 𝑧 → ((ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩ ↔ (ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩))
128	127	cbvexvw 2038	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑡(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩ ↔ ∃𝑧(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩)
129	125, 128	syl8ib 255	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → (∃𝑧(ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ∃𝑧(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩)))
130	129	impancom 450	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑖 ∈ ω → (∃𝑧(ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ∃𝑧(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩)))
131	130	3adant2 1129	. . . . . . . . . . . . . . . . 17 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑖 ∈ ω → (∃𝑧(ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ∃𝑧(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩)))
132	131	adantl 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (𝑖 ∈ ω → (∃𝑧(ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ∃𝑧(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩)))
133	132	com12 32	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ ω → ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (∃𝑧(ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ∃𝑧(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩)))
134	68, 72, 76, 81, 133	finds2 7893	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ω → ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ∃𝑧(ℎ‘𝑚) = ⟨𝑚, 𝑧⟩))
135	134	com12 32	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (𝑚 ∈ ω → ∃𝑧(ℎ‘𝑚) = ⟨𝑚, 𝑧⟩))
136	135	ralrimiv 3143	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ∀𝑚 ∈ ω ∃𝑧(ℎ‘𝑚) = ⟨𝑚, 𝑧⟩)
137		fveq2 6890	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑘 → (ℎ‘𝑚) = (ℎ‘𝑘))
138		opeq1 4872	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑘 → ⟨𝑚, 𝑧⟩ = ⟨𝑘, 𝑧⟩)
139	137, 138	eqeq12d 2746	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑘 → ((ℎ‘𝑚) = ⟨𝑚, 𝑧⟩ ↔ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩))
140	139	exbidv 1922	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑘 → (∃𝑧(ℎ‘𝑚) = ⟨𝑚, 𝑧⟩ ↔ ∃𝑧(ℎ‘𝑘) = ⟨𝑘, 𝑧⟩))
141	140	rspccv 3608	. . . . . . . . . . . 12 ⊢ (∀𝑚 ∈ ω ∃𝑧(ℎ‘𝑚) = ⟨𝑚, 𝑧⟩ → (𝑘 ∈ ω → ∃𝑧(ℎ‘𝑘) = ⟨𝑘, 𝑧⟩))
142	136, 141	syl 17	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (𝑘 ∈ ω → ∃𝑧(ℎ‘𝑘) = ⟨𝑘, 𝑧⟩))
143	142	3impia 1115	. . . . . . . . . 10 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → ∃𝑧(ℎ‘𝑘) = ⟨𝑘, 𝑧⟩)
144		simp21 1204	. . . . . . . . . 10 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → ℎ:ω⟶(ω × 𝐴))
145		simp3 1136	. . . . . . . . . 10 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → 𝑘 ∈ ω)
146		rspa 3243	. . . . . . . . . . . 12 ⊢ ((∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) ∧ 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))
147	146	3ad2antl3 1185	. . . . . . . . . . 11 ⊢ (((ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))
148	147	3adant1 1128	. . . . . . . . . 10 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))
149		simpl 481	. . . . . . . . . . . . . . . . 17 ⊢ (((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩)
150	149	fveq2d 6894	. . . . . . . . . . . . . . . 16 ⊢ (((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (𝐺‘(ℎ‘𝑘)) = (𝐺‘⟨𝑘, 𝑧⟩))
151		simprr 769	. . . . . . . . . . . . . . . . 17 ⊢ (((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → 𝑘 ∈ ω)
152		eleq1 2819	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ → ((ℎ‘𝑘) ∈ (ω × 𝐴) ↔ ⟨𝑘, 𝑧⟩ ∈ (ω × 𝐴)))
153		opelxp2 5718	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨𝑘, 𝑧⟩ ∈ (ω × 𝐴) → 𝑧 ∈ 𝐴)
154	152, 153	syl6bi 252	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ → ((ℎ‘𝑘) ∈ (ω × 𝐴) → 𝑧 ∈ 𝐴))
155		ffvelcdm 7082	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → (ℎ‘𝑘) ∈ (ω × 𝐴))
156	154, 155	impel 504	. . . . . . . . . . . . . . . . 17 ⊢ (((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → 𝑧 ∈ 𝐴)
157		df-ov 7414	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘𝐺𝑧) = (𝐺‘⟨𝑘, 𝑧⟩)
158		suceq 6429	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑘 → suc 𝑛 = suc 𝑘)
159	158	sneqd 4639	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑘 → {suc 𝑛} = {suc 𝑘})
160		oveq1 7418	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑘 → (𝑛𝐹𝑥) = (𝑘𝐹𝑥))
161	159, 160	xpeq12d 5706	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑘 → ({suc 𝑛} × (𝑛𝐹𝑥)) = ({suc 𝑘} × (𝑘𝐹𝑥)))
162		oveq2 7419	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑧 → (𝑘𝐹𝑥) = (𝑘𝐹𝑧))
163	162	xpeq2d 5705	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑧 → ({suc 𝑘} × (𝑘𝐹𝑥)) = ({suc 𝑘} × (𝑘𝐹𝑧)))
164		snex 5430	. . . . . . . . . . . . . . . . . . . 20 ⊢ {suc 𝑘} ∈ V
165		ovex 7444	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘𝐹𝑧) ∈ V
166	164, 165	xpex 7742	. . . . . . . . . . . . . . . . . . 19 ⊢ ({suc 𝑘} × (𝑘𝐹𝑧)) ∈ V
167	161, 163, 37, 166	ovmpo 7570	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ω ∧ 𝑧 ∈ 𝐴) → (𝑘𝐺𝑧) = ({suc 𝑘} × (𝑘𝐹𝑧)))
168	157, 167	eqtr3id 2784	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ω ∧ 𝑧 ∈ 𝐴) → (𝐺‘⟨𝑘, 𝑧⟩) = ({suc 𝑘} × (𝑘𝐹𝑧)))
169	151, 156, 168	syl2anc 582	. . . . . . . . . . . . . . . 16 ⊢ (((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (𝐺‘⟨𝑘, 𝑧⟩) = ({suc 𝑘} × (𝑘𝐹𝑧)))
170	150, 169	eqtrd 2770	. . . . . . . . . . . . . . 15 ⊢ (((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (𝐺‘(ℎ‘𝑘)) = ({suc 𝑘} × (𝑘𝐹𝑧)))
171	170	eleq2d 2817	. . . . . . . . . . . . . 14 ⊢ (((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) ↔ (ℎ‘suc 𝑘) ∈ ({suc 𝑘} × (𝑘𝐹𝑧))))
172		elxp 5698	. . . . . . . . . . . . . . . . 17 ⊢ ((ℎ‘suc 𝑘) ∈ ({suc 𝑘} × (𝑘𝐹𝑧)) ↔ ∃𝑠∃𝑡((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (𝑠 ∈ {suc 𝑘} ∧ 𝑡 ∈ (𝑘𝐹𝑧))))
173		peano2 7883	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 ∈ ω → suc 𝑘 ∈ ω)
174		fvco3 6989	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ suc 𝑘 ∈ ω) → ((2nd ∘ ℎ)‘suc 𝑘) = (2nd ‘(ℎ‘suc 𝑘)))
175	173, 174	sylan2 591	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((2nd ∘ ℎ)‘suc 𝑘) = (2nd ‘(ℎ‘suc 𝑘)))
176	175	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd ∘ ℎ)‘suc 𝑘) = (2nd ‘(ℎ‘suc 𝑘)))
177		simpll 763	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩)
178	177	fveq2d 6894	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (2nd ‘(ℎ‘suc 𝑘)) = (2nd ‘⟨𝑠, 𝑡⟩))
179	176, 178	eqtrd 2770	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd ∘ ℎ)‘suc 𝑘) = (2nd ‘⟨𝑠, 𝑡⟩))
180		vex 3476	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑠 ∈ V
181		vex 3476	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑡 ∈ V
182	180, 181	op2nd 7986	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (2nd ‘⟨𝑠, 𝑡⟩) = 𝑡
183	179, 182	eqtrdi 2786	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd ∘ ℎ)‘suc 𝑘) = 𝑡)
184		fvco3 6989	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((2nd ∘ ℎ)‘𝑘) = (2nd ‘(ℎ‘𝑘)))
185	184	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd ∘ ℎ)‘𝑘) = (2nd ‘(ℎ‘𝑘)))
186		simplr 765	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩)
187	186	fveq2d 6894	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (2nd ‘(ℎ‘𝑘)) = (2nd ‘⟨𝑘, 𝑧⟩))
188	185, 187	eqtrd 2770	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd ∘ ℎ)‘𝑘) = (2nd ‘⟨𝑘, 𝑧⟩))
189		vex 3476	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑘 ∈ V
190		vex 3476	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑧 ∈ V
191	189, 190	op2nd 7986	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (2nd ‘⟨𝑘, 𝑧⟩) = 𝑧
192	188, 191	eqtrdi 2786	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd ∘ ℎ)‘𝑘) = 𝑧)
193	192	oveq2d 7427	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (𝑘𝐹((2nd ∘ ℎ)‘𝑘)) = (𝑘𝐹𝑧))
194	183, 193	eleq12d 2825	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)) ↔ 𝑡 ∈ (𝑘𝐹𝑧)))
195	194	biimprcd 249	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 ∈ (𝑘𝐹𝑧) → ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))
196	195	exp4c 431	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ∈ (𝑘𝐹𝑧) → ((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ → ((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))))
197	196	adantl 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑠 ∈ {suc 𝑘} ∧ 𝑡 ∈ (𝑘𝐹𝑧)) → ((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ → ((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))))
198	197	impcom 406	. . . . . . . . . . . . . . . . . 18 ⊢ (((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (𝑠 ∈ {suc 𝑘} ∧ 𝑡 ∈ (𝑘𝐹𝑧))) → ((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))))
199	198	exlimivv 1933	. . . . . . . . . . . . . . . . 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 405	. . . . . . . . . . . . . 14 ⊢ (((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((ℎ‘suc 𝑘) ∈ ({suc 𝑘} × (𝑘𝐹𝑧)) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))
203	171, 202	sylbid 239	. . . . . . . . . . . . 13 ⊢ (((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))
204	203	ex 411	. . . . . . . . . . . 12 ⊢ ((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))))
205	204	exlimiv 1931	. . . . . . . . . . 11 ⊢ (∃𝑧(ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))))
206	205	3imp 1109	. . . . . . . . . 10 ⊢ ((∃𝑧(ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) ∧ (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))
207	143, 144, 145, 148, 206	syl121anc 1373	. . . . . . . . 9 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))
208	207	3expia 1119	. . . . . . . 8 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (𝑘 ∈ ω → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))
209	64, 208	ralrimi 3252	. . . . . . 7 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ∀𝑘 ∈ ω ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))
210	46, 58, 209	3jca 1126	. . . . . 6 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ((2nd ∘ ℎ):ω⟶𝐴 ∧ ((2nd ∘ ℎ)‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))
211		feq1 6697	. . . . . . 7 ⊢ (𝑔 = (2nd ∘ ℎ) → (𝑔:ω⟶𝐴 ↔ (2nd ∘ ℎ):ω⟶𝐴))
212		fveq1 6889	. . . . . . . 8 ⊢ (𝑔 = (2nd ∘ ℎ) → (𝑔‘∅) = ((2nd ∘ ℎ)‘∅))
213	212	eqeq1d 2732	. . . . . . 7 ⊢ (𝑔 = (2nd ∘ ℎ) → ((𝑔‘∅) = 𝐶 ↔ ((2nd ∘ ℎ)‘∅) = 𝐶))
214		fveq1 6889	. . . . . . . . 9 ⊢ (𝑔 = (2nd ∘ ℎ) → (𝑔‘suc 𝑘) = ((2nd ∘ ℎ)‘suc 𝑘))
215		fveq1 6889	. . . . . . . . . 10 ⊢ (𝑔 = (2nd ∘ ℎ) → (𝑔‘𝑘) = ((2nd ∘ ℎ)‘𝑘))
216	215	oveq2d 7427	. . . . . . . . 9 ⊢ (𝑔 = (2nd ∘ ℎ) → (𝑘𝐹(𝑔‘𝑘)) = (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))
217	214, 216	eleq12d 2825	. . . . . . . 8 ⊢ (𝑔 = (2nd ∘ ℎ) → ((𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘)) ↔ ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))
218	217	ralbidv 3175	. . . . . . 7 ⊢ (𝑔 = (2nd ∘ ℎ) → (∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘)) ↔ ∀𝑘 ∈ ω ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))
219	211, 213, 218	3anbi123d 1434	. . . . . 6 ⊢ (𝑔 = (2nd ∘ ℎ) → ((𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘))) ↔ ((2nd ∘ ℎ):ω⟶𝐴 ∧ ((2nd ∘ ℎ)‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))))
220	49, 210, 219	spcedv 3587	. . . . 5 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘))))
221	220	ex 411	. . . 4 ⊢ (𝐶 ∈ 𝐴 → ((ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘)))))
222	221	exlimdv 1934	. . 3 ⊢ (𝐶 ∈ 𝐴 → (∃ℎ(ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘)))))
223	222	adantr 479	. 2 ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅})) → (∃ℎ(ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘)))))
224	43, 223	mpd 15	1 ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘))))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 394   ∧ w3a 1085   = wceq 1539  ∃wex 1779   ∈ wcel 2104   ≠ wne 2938  ∀wral 3059  Vcvv 3472   ∖ cdif 3944   ⊆ wss 3947  ∅c0 4321  𝒫 cpw 4601  {csn 4627  ⟨cop 4633   × cxp 5673   ∘ ccom 5679  suc csuc 6365  ⟶wf 6538  ‘cfv 6542  (class class class)co 7411   ∈ cmpo 7413  ωcom 7857  2^nd c2nd 7976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-dc 10443

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-1o 8468

This theorem is referenced by:  axdc4  10453