Theorem axdc4lem 9160

Description: Lemma for axdc4 9161. (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 6977	. . . 4 ⊢ ∅ ∈ ω
2		opelxpi 5072	. . . 4 ⊢ ((∅ ∈ ω ∧ 𝐶 ∈ 𝐴) → ⟨∅, 𝐶⟩ ∈ (ω × 𝐴))
3	1, 2	mpan 702	. . 3 ⊢ (𝐶 ∈ 𝐴 → ⟨∅, 𝐶⟩ ∈ (ω × 𝐴))
4		simp2 1055	. . . . . . . 8 ⊢ ((𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑛 ∈ ω ∧ 𝑥 ∈ 𝐴) → 𝑛 ∈ ω)
5		fovrn 6702	. . . . . . . 8 ⊢ ((𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑛 ∈ ω ∧ 𝑥 ∈ 𝐴) → (𝑛𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅}))
6		peano2 6978	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ω → suc 𝑛 ∈ ω)
7	6	snssd 4281	. . . . . . . . . 10 ⊢ (𝑛 ∈ ω → {suc 𝑛} ⊆ ω)
8		eldifi 3694	. . . . . . . . . 10 ⊢ ((𝑛𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → (𝑛𝐹𝑥) ∈ 𝒫 𝐴)
9		axdc4lem.1	. . . . . . . . . . . 12 ⊢ 𝐴 ∈ V
10	9	elpw2 4755	. . . . . . . . . . 11 ⊢ ((𝑛𝐹𝑥) ∈ 𝒫 𝐴 ↔ (𝑛𝐹𝑥) ⊆ 𝐴)
11		xpss12 5148	. . . . . . . . . . 11 ⊢ (({suc 𝑛} ⊆ ω ∧ (𝑛𝐹𝑥) ⊆ 𝐴) → ({suc 𝑛} × (𝑛𝐹𝑥)) ⊆ (ω × 𝐴))
12	10, 11	sylan2b 491	. . . . . . . . . 10 ⊢ (({suc 𝑛} ⊆ ω ∧ (𝑛𝐹𝑥) ∈ 𝒫 𝐴) → ({suc 𝑛} × (𝑛𝐹𝑥)) ⊆ (ω × 𝐴))
13	7, 8, 12	syl2an 493	. . . . . . . . 9 ⊢ ((𝑛 ∈ ω ∧ (𝑛𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅})) → ({suc 𝑛} × (𝑛𝐹𝑥)) ⊆ (ω × 𝐴))
14		snex 4835	. . . . . . . . . . 11 ⊢ {suc 𝑛} ∈ V
15		ovex 6577	. . . . . . . . . . 11 ⊢ (𝑛𝐹𝑥) ∈ V
16	14, 15	xpex 6860	. . . . . . . . . 10 ⊢ ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ V
17	16	elpw 4114	. . . . . . . . 9 ⊢ (({suc 𝑛} × (𝑛𝐹𝑥)) ∈ 𝒫 (ω × 𝐴) ↔ ({suc 𝑛} × (𝑛𝐹𝑥)) ⊆ (ω × 𝐴))
18	13, 17	sylibr 223	. . . . . . . 8 ⊢ ((𝑛 ∈ ω ∧ (𝑛𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅})) → ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ 𝒫 (ω × 𝐴))
19	4, 5, 18	syl2anc 691	. . . . . . 7 ⊢ ((𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑛 ∈ ω ∧ 𝑥 ∈ 𝐴) → ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ 𝒫 (ω × 𝐴))
20		eldifn 3695	. . . . . . . 8 ⊢ ((𝑛𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → ¬ (𝑛𝐹𝑥) ∈ {∅})
21	15	elsn 4140	. . . . . . . . . . 11 ⊢ ((𝑛𝐹𝑥) ∈ {∅} ↔ (𝑛𝐹𝑥) = ∅)
22	21	necon3bbii 2829	. . . . . . . . . 10 ⊢ (¬ (𝑛𝐹𝑥) ∈ {∅} ↔ (𝑛𝐹𝑥) ≠ ∅)
23		vex 3176	. . . . . . . . . . . . 13 ⊢ 𝑛 ∈ V
24	23	sucex 6903	. . . . . . . . . . . 12 ⊢ suc 𝑛 ∈ V
25	24	snnz 4252	. . . . . . . . . . 11 ⊢ {suc 𝑛} ≠ ∅
26		xpnz 5472	. . . . . . . . . . . 12 ⊢ (({suc 𝑛} ≠ ∅ ∧ (𝑛𝐹𝑥) ≠ ∅) ↔ ({suc 𝑛} × (𝑛𝐹𝑥)) ≠ ∅)
27	26	biimpi 205	. . . . . . . . . . 11 ⊢ (({suc 𝑛} ≠ ∅ ∧ (𝑛𝐹𝑥) ≠ ∅) → ({suc 𝑛} × (𝑛𝐹𝑥)) ≠ ∅)
28	25, 27	mpan 702	. . . . . . . . . 10 ⊢ ((𝑛𝐹𝑥) ≠ ∅ → ({suc 𝑛} × (𝑛𝐹𝑥)) ≠ ∅)
29	22, 28	sylbi 206	. . . . . . . . 9 ⊢ (¬ (𝑛𝐹𝑥) ∈ {∅} → ({suc 𝑛} × (𝑛𝐹𝑥)) ≠ ∅)
30	16	elsn 4140	. . . . . . . . . 10 ⊢ (({suc 𝑛} × (𝑛𝐹𝑥)) ∈ {∅} ↔ ({suc 𝑛} × (𝑛𝐹𝑥)) = ∅)
31	30	necon3bbii 2829	. . . . . . . . 9 ⊢ (¬ ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ {∅} ↔ ({suc 𝑛} × (𝑛𝐹𝑥)) ≠ ∅)
32	29, 31	sylibr 223	. . . . . . . 8 ⊢ (¬ (𝑛𝐹𝑥) ∈ {∅} → ¬ ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ {∅})
33	5, 20, 32	3syl 18	. . . . . . 7 ⊢ ((𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑛 ∈ ω ∧ 𝑥 ∈ 𝐴) → ¬ ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ {∅})
34	19, 33	eldifd 3551	. . . . . 6 ⊢ ((𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑛 ∈ ω ∧ 𝑥 ∈ 𝐴) → ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ (𝒫 (ω × 𝐴) ∖ {∅}))
35	34	3expib 1260	. . . . 5 ⊢ (𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) → ((𝑛 ∈ ω ∧ 𝑥 ∈ 𝐴) → ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ (𝒫 (ω × 𝐴) ∖ {∅})))
36	35	ralrimivv 2953	. . . 4 ⊢ (𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) → ∀𝑛 ∈ ω ∀𝑥 ∈ 𝐴 ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ (𝒫 (ω × 𝐴) ∖ {∅}))
37		axdc4lem.2	. . . . 5 ⊢ 𝐺 = (𝑛 ∈ ω, 𝑥 ∈ 𝐴 ↦ ({suc 𝑛} × (𝑛𝐹𝑥)))
38	37	fmpt2 7126	. . . 4 ⊢ (∀𝑛 ∈ ω ∀𝑥 ∈ 𝐴 ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ (𝒫 (ω × 𝐴) ∖ {∅}) ↔ 𝐺:(ω × 𝐴)⟶(𝒫 (ω × 𝐴) ∖ {∅}))
39	36, 38	sylib 207	. . 3 ⊢ (𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) → 𝐺:(ω × 𝐴)⟶(𝒫 (ω × 𝐴) ∖ {∅}))
40		dcomex 9152	. . . . 5 ⊢ ω ∈ V
41	40, 9	xpex 6860	. . . 4 ⊢ (ω × 𝐴) ∈ V
42	41	axdc3 9159	. . 3 ⊢ ((⟨∅, 𝐶⟩ ∈ (ω × 𝐴) ∧ 𝐺:(ω × 𝐴)⟶(𝒫 (ω × 𝐴) ∖ {∅})) → ∃ℎ(ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))))
43	3, 39, 42	syl2an 493	. 2 ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅})) → ∃ℎ(ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))))
44		2ndcof 7088	. . . . . . . . 9 ⊢ (ℎ:ω⟶(ω × 𝐴) → (2nd ∘ ℎ):ω⟶𝐴)
45	44	3ad2ant1 1075	. . . . . . . 8 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (2nd ∘ ℎ):ω⟶𝐴)
46	45	adantl 481	. . . . . . 7 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (2nd ∘ ℎ):ω⟶𝐴)
47		fex2 7014	. . . . . . . 8 ⊢ (((2nd ∘ ℎ):ω⟶𝐴 ∧ ω ∈ V ∧ 𝐴 ∈ V) → (2nd ∘ ℎ) ∈ V)
48	40, 9, 47	mp3an23 1408	. . . . . . 7 ⊢ ((2nd ∘ ℎ):ω⟶𝐴 → (2nd ∘ ℎ) ∈ V)
49	46, 48	syl 17	. . . . . 6 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (2nd ∘ ℎ) ∈ V)
50		fvco3 6185	. . . . . . . . . . 11 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ ∅ ∈ ω) → ((2nd ∘ ℎ)‘∅) = (2nd ‘(ℎ‘∅)))
51	1, 50	mpan2 703	. . . . . . . . . 10 ⊢ (ℎ:ω⟶(ω × 𝐴) → ((2nd ∘ ℎ)‘∅) = (2nd ‘(ℎ‘∅)))
52	51	3ad2ant1 1075	. . . . . . . . 9 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ((2nd ∘ ℎ)‘∅) = (2nd ‘(ℎ‘∅)))
53		fveq2 6103	. . . . . . . . . 10 ⊢ ((ℎ‘∅) = ⟨∅, 𝐶⟩ → (2nd ‘(ℎ‘∅)) = (2nd ‘⟨∅, 𝐶⟩))
54	53	3ad2ant2 1076	. . . . . . . . 9 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (2nd ‘(ℎ‘∅)) = (2nd ‘⟨∅, 𝐶⟩))
55	52, 54	eqtrd 2644	. . . . . . . 8 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ((2nd ∘ ℎ)‘∅) = (2nd ‘⟨∅, 𝐶⟩))
56		op2ndg 7072	. . . . . . . . 9 ⊢ ((∅ ∈ ω ∧ 𝐶 ∈ 𝐴) → (2nd ‘⟨∅, 𝐶⟩) = 𝐶)
57	1, 56	mpan 702	. . . . . . . 8 ⊢ (𝐶 ∈ 𝐴 → (2nd ‘⟨∅, 𝐶⟩) = 𝐶)
58	55, 57	sylan9eqr 2666	. . . . . . 7 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ((2nd ∘ ℎ)‘∅) = 𝐶)
59		nfv 1830	. . . . . . . . 9 ⊢ Ⅎ𝑘 𝐶 ∈ 𝐴
60		nfv 1830	. . . . . . . . . 10 ⊢ Ⅎ𝑘 ℎ:ω⟶(ω × 𝐴)
61		nfv 1830	. . . . . . . . . 10 ⊢ Ⅎ𝑘(ℎ‘∅) = ⟨∅, 𝐶⟩
62		nfra1 2925	. . . . . . . . . 10 ⊢ Ⅎ𝑘∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))
63	60, 61, 62	nf3an 1819	. . . . . . . . 9 ⊢ Ⅎ𝑘(ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))
64	59, 63	nfan 1816	. . . . . . . 8 ⊢ Ⅎ𝑘(𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))))
65		fveq2 6103	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = ∅ → (ℎ‘𝑚) = (ℎ‘∅))
66		opeq1 4340	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = ∅ → ⟨𝑚, 𝑧⟩ = ⟨∅, 𝑧⟩)
67	65, 66	eqeq12d 2625	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = ∅ → ((ℎ‘𝑚) = ⟨𝑚, 𝑧⟩ ↔ (ℎ‘∅) = ⟨∅, 𝑧⟩))
68	67	exbidv 1837	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = ∅ → (∃𝑧(ℎ‘𝑚) = ⟨𝑚, 𝑧⟩ ↔ ∃𝑧(ℎ‘∅) = ⟨∅, 𝑧⟩))
69		fveq2 6103	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑖 → (ℎ‘𝑚) = (ℎ‘𝑖))
70		opeq1 4340	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑖 → ⟨𝑚, 𝑧⟩ = ⟨𝑖, 𝑧⟩)
71	69, 70	eqeq12d 2625	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑖 → ((ℎ‘𝑚) = ⟨𝑚, 𝑧⟩ ↔ (ℎ‘𝑖) = ⟨𝑖, 𝑧⟩))
72	71	exbidv 1837	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑖 → (∃𝑧(ℎ‘𝑚) = ⟨𝑚, 𝑧⟩ ↔ ∃𝑧(ℎ‘𝑖) = ⟨𝑖, 𝑧⟩))
73		fveq2 6103	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = suc 𝑖 → (ℎ‘𝑚) = (ℎ‘suc 𝑖))
74		opeq1 4340	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = suc 𝑖 → ⟨𝑚, 𝑧⟩ = ⟨suc 𝑖, 𝑧⟩)
75	73, 74	eqeq12d 2625	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = suc 𝑖 → ((ℎ‘𝑚) = ⟨𝑚, 𝑧⟩ ↔ (ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩))
76	75	exbidv 1837	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = suc 𝑖 → (∃𝑧(ℎ‘𝑚) = ⟨𝑚, 𝑧⟩ ↔ ∃𝑧(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩))
77		opeq2 4341	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝐶 → ⟨∅, 𝑧⟩ = ⟨∅, 𝐶⟩)
78	77	eqeq2d 2620	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝐶 → ((ℎ‘∅) = ⟨∅, 𝑧⟩ ↔ (ℎ‘∅) = ⟨∅, 𝐶⟩))
79	78	spcegv 3267	. . . . . . . . . . . . . . . . 17 ⊢ (𝐶 ∈ 𝐴 → ((ℎ‘∅) = ⟨∅, 𝐶⟩ → ∃𝑧(ℎ‘∅) = ⟨∅, 𝑧⟩))
80	79	imp 444	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩) → ∃𝑧(ℎ‘∅) = ⟨∅, 𝑧⟩)
81	80	3ad2antr2 1220	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ∃𝑧(ℎ‘∅) = ⟨∅, 𝑧⟩)
82		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → (𝐺‘(ℎ‘𝑖)) = (𝐺‘⟨𝑖, 𝑧⟩))
83		df-ov 6552	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑖𝐺𝑧) = (𝐺‘⟨𝑖, 𝑧⟩)
84	82, 83	syl6eqr 2662	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → (𝐺‘(ℎ‘𝑖)) = (𝑖𝐺𝑧))
85	84	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) ∧ (ℎ‘𝑖) = ⟨𝑖, 𝑧⟩) → (𝐺‘(ℎ‘𝑖)) = (𝑖𝐺𝑧))
86		simplr 788	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) ∧ (ℎ‘𝑖) = ⟨𝑖, 𝑧⟩) → 𝑖 ∈ ω)
87		ffvelrn 6265	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) → (ℎ‘𝑖) ∈ (ω × 𝐴))
88		eleq1 2676	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ((ℎ‘𝑖) ∈ (ω × 𝐴) ↔ ⟨𝑖, 𝑧⟩ ∈ (ω × 𝐴)))
89		opelxp2 5075	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (⟨𝑖, 𝑧⟩ ∈ (ω × 𝐴) → 𝑧 ∈ 𝐴)
90	88, 89	syl6bi 242	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ((ℎ‘𝑖) ∈ (ω × 𝐴) → 𝑧 ∈ 𝐴))
91	87, 90	mpan9 485	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) ∧ (ℎ‘𝑖) = ⟨𝑖, 𝑧⟩) → 𝑧 ∈ 𝐴)
92		suceq 5707	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑛 = 𝑖 → suc 𝑛 = suc 𝑖)
93	92	sneqd 4137	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑛 = 𝑖 → {suc 𝑛} = {suc 𝑖})
94		oveq1 6556	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑛 = 𝑖 → (𝑛𝐹𝑥) = (𝑖𝐹𝑥))
95	93, 94	xpeq12d 5064	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑛 = 𝑖 → ({suc 𝑛} × (𝑛𝐹𝑥)) = ({suc 𝑖} × (𝑖𝐹𝑥)))
96		oveq2 6557	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 = 𝑧 → (𝑖𝐹𝑥) = (𝑖𝐹𝑧))
97	96	xpeq2d 5063	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = 𝑧 → ({suc 𝑖} × (𝑖𝐹𝑥)) = ({suc 𝑖} × (𝑖𝐹𝑧)))
98		snex 4835	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ {suc 𝑖} ∈ V
99		ovex 6577	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑖𝐹𝑧) ∈ V
100	98, 99	xpex 6860	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ({suc 𝑖} × (𝑖𝐹𝑧)) ∈ V
101	95, 97, 37, 100	ovmpt2 6694	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑖 ∈ ω ∧ 𝑧 ∈ 𝐴) → (𝑖𝐺𝑧) = ({suc 𝑖} × (𝑖𝐹𝑧)))
102	86, 91, 101	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) ∧ (ℎ‘𝑖) = ⟨𝑖, 𝑧⟩) → (𝑖𝐺𝑧) = ({suc 𝑖} × (𝑖𝐹𝑧)))
103	85, 102	eqtrd 2644	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) ∧ (ℎ‘𝑖) = ⟨𝑖, 𝑧⟩) → (𝐺‘(ℎ‘𝑖)) = ({suc 𝑖} × (𝑖𝐹𝑧)))
104		suceq 5707	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑘 = 𝑖 → suc 𝑘 = suc 𝑖)
105	104	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 = 𝑖 → (ℎ‘suc 𝑘) = (ℎ‘suc 𝑖))
106		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑘 = 𝑖 → (ℎ‘𝑘) = (ℎ‘𝑖))
107	106	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 = 𝑖 → (𝐺‘(ℎ‘𝑘)) = (𝐺‘(ℎ‘𝑖)))
108	105, 107	eleq12d 2682	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 = 𝑖 → ((ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) ↔ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))))
109	108	rspcv 3278	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 ∈ ω → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))))
110	109	ad2antlr 759	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) ∧ (ℎ‘𝑖) = ⟨𝑖, 𝑧⟩) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))))
111		eleq2 2677	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐺‘(ℎ‘𝑖)) = ({suc 𝑖} × (𝑖𝐹𝑧)) → ((ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖)) ↔ (ℎ‘suc 𝑖) ∈ ({suc 𝑖} × (𝑖𝐹𝑧))))
112		elxp 5055	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((ℎ‘suc 𝑖) ∈ ({suc 𝑖} × (𝑖𝐹𝑧)) ↔ ∃𝑠∃𝑡((ℎ‘suc 𝑖) = ⟨𝑠, 𝑡⟩ ∧ (𝑠 ∈ {suc 𝑖} ∧ 𝑡 ∈ (𝑖𝐹𝑧))))
113		velsn 4141	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑠 ∈ {suc 𝑖} ↔ 𝑠 = suc 𝑖)
114		opeq1 4340	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑠 = suc 𝑖 → ⟨𝑠, 𝑡⟩ = ⟨suc 𝑖, 𝑡⟩)
115	113, 114	sylbi 206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑠 ∈ {suc 𝑖} → ⟨𝑠, 𝑡⟩ = ⟨suc 𝑖, 𝑡⟩)
116	115	eqeq2d 2620	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑠 ∈ {suc 𝑖} → ((ℎ‘suc 𝑖) = ⟨𝑠, 𝑡⟩ ↔ (ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩))
117	116	biimpac 502	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((ℎ‘suc 𝑖) = ⟨𝑠, 𝑡⟩ ∧ 𝑠 ∈ {suc 𝑖}) → (ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩)
118	117	adantrr 749	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((ℎ‘suc 𝑖) = ⟨𝑠, 𝑡⟩ ∧ (𝑠 ∈ {suc 𝑖} ∧ 𝑡 ∈ (𝑖𝐹𝑧))) → (ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩)
119	118	eximi 1752	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∃𝑡((ℎ‘suc 𝑖) = ⟨𝑠, 𝑡⟩ ∧ (𝑠 ∈ {suc 𝑖} ∧ 𝑡 ∈ (𝑖𝐹𝑧))) → ∃𝑡(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩)
120	119	exlimiv 1845	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∃𝑠∃𝑡((ℎ‘suc 𝑖) = ⟨𝑠, 𝑡⟩ ∧ (𝑠 ∈ {suc 𝑖} ∧ 𝑡 ∈ (𝑖𝐹𝑧))) → ∃𝑡(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩)
121	112, 120	sylbi 206	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((ℎ‘suc 𝑖) ∈ ({suc 𝑖} × (𝑖𝐹𝑧)) → ∃𝑡(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩)
122	111, 121	syl6bi 242	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐺‘(ℎ‘𝑖)) = ({suc 𝑖} × (𝑖𝐹𝑧)) → ((ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖)) → ∃𝑡(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩))
123	103, 110, 122	sylsyld 59	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) ∧ (ℎ‘𝑖) = ⟨𝑖, 𝑧⟩) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → ∃𝑡(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩))
124	123	expcom 450	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → ∃𝑡(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩)))
125	124	exlimiv 1845	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑧(ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → ∃𝑡(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩)))
126	125	com3l 87	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → (∃𝑧(ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ∃𝑡(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩)))
127		opeq2 4341	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 = 𝑧 → ⟨suc 𝑖, 𝑡⟩ = ⟨suc 𝑖, 𝑧⟩)
128	127	eqeq2d 2620	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 = 𝑧 → ((ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩ ↔ (ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩))
129	128	cbvexv 2263	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑡(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩ ↔ ∃𝑧(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩)
130	126, 129	syl8ib 245	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → (∃𝑧(ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ∃𝑧(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩)))
131	130	impancom 455	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑖 ∈ ω → (∃𝑧(ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ∃𝑧(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩)))
132	131	3adant2 1073	. . . . . . . . . . . . . . . . 17 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑖 ∈ ω → (∃𝑧(ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ∃𝑧(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩)))
133	132	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (𝑖 ∈ ω → (∃𝑧(ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ∃𝑧(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩)))
134	133	com12 32	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ ω → ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (∃𝑧(ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ∃𝑧(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩)))
135	68, 72, 76, 81, 134	finds2 6986	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ω → ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ∃𝑧(ℎ‘𝑚) = ⟨𝑚, 𝑧⟩))
136	135	com12 32	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (𝑚 ∈ ω → ∃𝑧(ℎ‘𝑚) = ⟨𝑚, 𝑧⟩))
137	136	ralrimiv 2948	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ∀𝑚 ∈ ω ∃𝑧(ℎ‘𝑚) = ⟨𝑚, 𝑧⟩)
138		fveq2 6103	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑘 → (ℎ‘𝑚) = (ℎ‘𝑘))
139		opeq1 4340	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑘 → ⟨𝑚, 𝑧⟩ = ⟨𝑘, 𝑧⟩)
140	138, 139	eqeq12d 2625	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑘 → ((ℎ‘𝑚) = ⟨𝑚, 𝑧⟩ ↔ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩))
141	140	exbidv 1837	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑘 → (∃𝑧(ℎ‘𝑚) = ⟨𝑚, 𝑧⟩ ↔ ∃𝑧(ℎ‘𝑘) = ⟨𝑘, 𝑧⟩))
142	141	rspccv 3279	. . . . . . . . . . . 12 ⊢ (∀𝑚 ∈ ω ∃𝑧(ℎ‘𝑚) = ⟨𝑚, 𝑧⟩ → (𝑘 ∈ ω → ∃𝑧(ℎ‘𝑘) = ⟨𝑘, 𝑧⟩))
143	137, 142	syl 17	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (𝑘 ∈ ω → ∃𝑧(ℎ‘𝑘) = ⟨𝑘, 𝑧⟩))
144	143	3impia 1253	. . . . . . . . . 10 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → ∃𝑧(ℎ‘𝑘) = ⟨𝑘, 𝑧⟩)
145		simp21 1087	. . . . . . . . . 10 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → ℎ:ω⟶(ω × 𝐴))
146		simp3 1056	. . . . . . . . . 10 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → 𝑘 ∈ ω)
147		rspa 2914	. . . . . . . . . . . 12 ⊢ ((∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) ∧ 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))
148	147	3ad2antl3 1218	. . . . . . . . . . 11 ⊢ (((ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))
149	148	3adant1 1072	. . . . . . . . . 10 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))
150		simpl 472	. . . . . . . . . . . . . . . . 17 ⊢ (((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩)
151	150	fveq2d 6107	. . . . . . . . . . . . . . . 16 ⊢ (((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (𝐺‘(ℎ‘𝑘)) = (𝐺‘⟨𝑘, 𝑧⟩))
152		simprr 792	. . . . . . . . . . . . . . . . 17 ⊢ (((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → 𝑘 ∈ ω)
153		ffvelrn 6265	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → (ℎ‘𝑘) ∈ (ω × 𝐴))
154		eleq1 2676	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ → ((ℎ‘𝑘) ∈ (ω × 𝐴) ↔ ⟨𝑘, 𝑧⟩ ∈ (ω × 𝐴)))
155		opelxp2 5075	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑘, 𝑧⟩ ∈ (ω × 𝐴) → 𝑧 ∈ 𝐴)
156	154, 155	syl6bi 242	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ → ((ℎ‘𝑘) ∈ (ω × 𝐴) → 𝑧 ∈ 𝐴))
157	153, 156	syl5 33	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → 𝑧 ∈ 𝐴))
158	157	imp 444	. . . . . . . . . . . . . . . . 17 ⊢ (((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → 𝑧 ∈ 𝐴)
159		df-ov 6552	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘𝐺𝑧) = (𝐺‘⟨𝑘, 𝑧⟩)
160		suceq 5707	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑘 → suc 𝑛 = suc 𝑘)
161	160	sneqd 4137	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑘 → {suc 𝑛} = {suc 𝑘})
162		oveq1 6556	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑘 → (𝑛𝐹𝑥) = (𝑘𝐹𝑥))
163	161, 162	xpeq12d 5064	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑘 → ({suc 𝑛} × (𝑛𝐹𝑥)) = ({suc 𝑘} × (𝑘𝐹𝑥)))
164		oveq2 6557	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑧 → (𝑘𝐹𝑥) = (𝑘𝐹𝑧))
165	164	xpeq2d 5063	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑧 → ({suc 𝑘} × (𝑘𝐹𝑥)) = ({suc 𝑘} × (𝑘𝐹𝑧)))
166		snex 4835	. . . . . . . . . . . . . . . . . . . 20 ⊢ {suc 𝑘} ∈ V
167		ovex 6577	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘𝐹𝑧) ∈ V
168	166, 167	xpex 6860	. . . . . . . . . . . . . . . . . . 19 ⊢ ({suc 𝑘} × (𝑘𝐹𝑧)) ∈ V
169	163, 165, 37, 168	ovmpt2 6694	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ω ∧ 𝑧 ∈ 𝐴) → (𝑘𝐺𝑧) = ({suc 𝑘} × (𝑘𝐹𝑧)))
170	159, 169	syl5eqr 2658	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ω ∧ 𝑧 ∈ 𝐴) → (𝐺‘⟨𝑘, 𝑧⟩) = ({suc 𝑘} × (𝑘𝐹𝑧)))
171	152, 158, 170	syl2anc 691	. . . . . . . . . . . . . . . 16 ⊢ (((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (𝐺‘⟨𝑘, 𝑧⟩) = ({suc 𝑘} × (𝑘𝐹𝑧)))
172	151, 171	eqtrd 2644	. . . . . . . . . . . . . . 15 ⊢ (((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (𝐺‘(ℎ‘𝑘)) = ({suc 𝑘} × (𝑘𝐹𝑧)))
173	172	eleq2d 2673	. . . . . . . . . . . . . 14 ⊢ (((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) ↔ (ℎ‘suc 𝑘) ∈ ({suc 𝑘} × (𝑘𝐹𝑧))))
174		elxp 5055	. . . . . . . . . . . . . . . . 17 ⊢ ((ℎ‘suc 𝑘) ∈ ({suc 𝑘} × (𝑘𝐹𝑧)) ↔ ∃𝑠∃𝑡((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (𝑠 ∈ {suc 𝑘} ∧ 𝑡 ∈ (𝑘𝐹𝑧))))
175		peano2 6978	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 ∈ ω → suc 𝑘 ∈ ω)
176		fvco3 6185	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ suc 𝑘 ∈ ω) → ((2nd ∘ ℎ)‘suc 𝑘) = (2nd ‘(ℎ‘suc 𝑘)))
177	175, 176	sylan2 490	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((2nd ∘ ℎ)‘suc 𝑘) = (2nd ‘(ℎ‘suc 𝑘)))
178	177	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd ∘ ℎ)‘suc 𝑘) = (2nd ‘(ℎ‘suc 𝑘)))
179		simpll 786	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩)
180	179	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (2nd ‘(ℎ‘suc 𝑘)) = (2nd ‘⟨𝑠, 𝑡⟩))
181	178, 180	eqtrd 2644	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd ∘ ℎ)‘suc 𝑘) = (2nd ‘⟨𝑠, 𝑡⟩))
182		vex 3176	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑠 ∈ V
183		vex 3176	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑡 ∈ V
184	182, 183	op2nd 7068	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (2nd ‘⟨𝑠, 𝑡⟩) = 𝑡
185	181, 184	syl6eq 2660	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd ∘ ℎ)‘suc 𝑘) = 𝑡)
186		fvco3 6185	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((2nd ∘ ℎ)‘𝑘) = (2nd ‘(ℎ‘𝑘)))
187	186	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd ∘ ℎ)‘𝑘) = (2nd ‘(ℎ‘𝑘)))
188		simplr 788	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩)
189	188	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (2nd ‘(ℎ‘𝑘)) = (2nd ‘⟨𝑘, 𝑧⟩))
190	187, 189	eqtrd 2644	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd ∘ ℎ)‘𝑘) = (2nd ‘⟨𝑘, 𝑧⟩))
191		vex 3176	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑘 ∈ V
192		vex 3176	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑧 ∈ V
193	191, 192	op2nd 7068	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (2nd ‘⟨𝑘, 𝑧⟩) = 𝑧
194	190, 193	syl6eq 2660	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd ∘ ℎ)‘𝑘) = 𝑧)
195	194	oveq2d 6565	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (𝑘𝐹((2nd ∘ ℎ)‘𝑘)) = (𝑘𝐹𝑧))
196	185, 195	eleq12d 2682	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)) ↔ 𝑡 ∈ (𝑘𝐹𝑧)))
197	196	biimprcd 239	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 ∈ (𝑘𝐹𝑧) → ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))
198	197	exp4c 634	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ∈ (𝑘𝐹𝑧) → ((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ → ((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))))
199	198	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑠 ∈ {suc 𝑘} ∧ 𝑡 ∈ (𝑘𝐹𝑧)) → ((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ → ((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))))
200	199	impcom 445	. . . . . . . . . . . . . . . . . 18 ⊢ (((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (𝑠 ∈ {suc 𝑘} ∧ 𝑡 ∈ (𝑘𝐹𝑧))) → ((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))))
201	200	exlimivv 1847	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑠∃𝑡((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (𝑠 ∈ {suc 𝑘} ∧ 𝑡 ∈ (𝑘𝐹𝑧))) → ((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))))
202	174, 201	sylbi 206	. . . . . . . . . . . . . . . 16 ⊢ ((ℎ‘suc 𝑘) ∈ ({suc 𝑘} × (𝑘𝐹𝑧)) → ((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))))
203	202	com3l 87	. . . . . . . . . . . . . . 15 ⊢ ((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((ℎ‘suc 𝑘) ∈ ({suc 𝑘} × (𝑘𝐹𝑧)) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))))
204	203	imp 444	. . . . . . . . . . . . . 14 ⊢ (((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((ℎ‘suc 𝑘) ∈ ({suc 𝑘} × (𝑘𝐹𝑧)) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))
205	173, 204	sylbid 229	. . . . . . . . . . . . 13 ⊢ (((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))
206	205	ex 449	. . . . . . . . . . . 12 ⊢ ((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))))
207	206	exlimiv 1845	. . . . . . . . . . 11 ⊢ (∃𝑧(ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))))
208	207	3imp 1249	. . . . . . . . . 10 ⊢ ((∃𝑧(ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) ∧ (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))
209	144, 145, 146, 149, 208	syl121anc 1323	. . . . . . . . 9 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))
210	209	3expia 1259	. . . . . . . 8 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (𝑘 ∈ ω → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))
211	64, 210	ralrimi 2940	. . . . . . 7 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ∀𝑘 ∈ ω ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))
212	46, 58, 211	3jca 1235	. . . . . 6 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ((2nd ∘ ℎ):ω⟶𝐴 ∧ ((2nd ∘ ℎ)‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))
213		feq1 5939	. . . . . . . 8 ⊢ (𝑔 = (2nd ∘ ℎ) → (𝑔:ω⟶𝐴 ↔ (2nd ∘ ℎ):ω⟶𝐴))
214		fveq1 6102	. . . . . . . . 9 ⊢ (𝑔 = (2nd ∘ ℎ) → (𝑔‘∅) = ((2nd ∘ ℎ)‘∅))
215	214	eqeq1d 2612	. . . . . . . 8 ⊢ (𝑔 = (2nd ∘ ℎ) → ((𝑔‘∅) = 𝐶 ↔ ((2nd ∘ ℎ)‘∅) = 𝐶))
216		fveq1 6102	. . . . . . . . . 10 ⊢ (𝑔 = (2nd ∘ ℎ) → (𝑔‘suc 𝑘) = ((2nd ∘ ℎ)‘suc 𝑘))
217		fveq1 6102	. . . . . . . . . . 11 ⊢ (𝑔 = (2nd ∘ ℎ) → (𝑔‘𝑘) = ((2nd ∘ ℎ)‘𝑘))
218	217	oveq2d 6565	. . . . . . . . . 10 ⊢ (𝑔 = (2nd ∘ ℎ) → (𝑘𝐹(𝑔‘𝑘)) = (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))
219	216, 218	eleq12d 2682	. . . . . . . . 9 ⊢ (𝑔 = (2nd ∘ ℎ) → ((𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘)) ↔ ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))
220	219	ralbidv 2969	. . . . . . . 8 ⊢ (𝑔 = (2nd ∘ ℎ) → (∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘)) ↔ ∀𝑘 ∈ ω ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))
221	213, 215, 220	3anbi123d 1391	. . . . . . 7 ⊢ (𝑔 = (2nd ∘ ℎ) → ((𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘))) ↔ ((2nd ∘ ℎ):ω⟶𝐴 ∧ ((2nd ∘ ℎ)‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))))
222	221	spcegv 3267	. . . . . 6 ⊢ ((2nd ∘ ℎ) ∈ V → (((2nd ∘ ℎ):ω⟶𝐴 ∧ ((2nd ∘ ℎ)‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘)))))
223	49, 212, 222	sylc 63	. . . . 5 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘))))
224	223	ex 449	. . . 4 ⊢ (𝐶 ∈ 𝐴 → ((ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘)))))
225	224	exlimdv 1848	. . 3 ⊢ (𝐶 ∈ 𝐴 → (∃ℎ(ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘)))))
226	225	adantr 480	. 2 ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅})) → (∃ℎ(ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘)))))
227	43, 226	mpd 15	1 ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘))))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   ∧ w3a 1031   = wceq 1475  ∃wex 1695   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  Vcvv 3173   ∖ cdif 3537   ⊆ wss 3540  ∅c0 3874  𝒫 cpw 4108  {csn 4125  ⟨cop 4131   × cxp 5036   ∘ ccom 5042  suc csuc 5642  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549   ↦ cmpt2 6551  ωcom 6957  2^nd c2nd 7058

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-pow 4769  ax-pr 4833  ax-un 6847  ax-dc 9151

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-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  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-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-1o 7447

This theorem is referenced by:  axdc4  9161