Theorem axdc4lem 10069

Description: Lemma for axdc4 10070. (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 7667	. . . 4 ⊢ ∅ ∈ ω
2		opelxpi 5588	. . . 4 ⊢ ((∅ ∈ ω ∧ 𝐶 ∈ 𝐴) → ⟨∅, 𝐶⟩ ∈ (ω × 𝐴))
3	1, 2	mpan 690	. . 3 ⊢ (𝐶 ∈ 𝐴 → ⟨∅, 𝐶⟩ ∈ (ω × 𝐴))
4		simp2 1139	. . . . . . . 8 ⊢ ((𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑛 ∈ ω ∧ 𝑥 ∈ 𝐴) → 𝑛 ∈ ω)
5		fovrn 7378	. . . . . . . 8 ⊢ ((𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑛 ∈ ω ∧ 𝑥 ∈ 𝐴) → (𝑛𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅}))
6		peano2 7668	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ω → suc 𝑛 ∈ ω)
7	6	snssd 4722	. . . . . . . . . 10 ⊢ (𝑛 ∈ ω → {suc 𝑛} ⊆ ω)
8		eldifi 4041	. . . . . . . . . 10 ⊢ ((𝑛𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → (𝑛𝐹𝑥) ∈ 𝒫 𝐴)
9		axdc4lem.1	. . . . . . . . . . . 12 ⊢ 𝐴 ∈ V
10	9	elpw2 5238	. . . . . . . . . . 11 ⊢ ((𝑛𝐹𝑥) ∈ 𝒫 𝐴 ↔ (𝑛𝐹𝑥) ⊆ 𝐴)
11		xpss12 5566	. . . . . . . . . . 11 ⊢ (({suc 𝑛} ⊆ ω ∧ (𝑛𝐹𝑥) ⊆ 𝐴) → ({suc 𝑛} × (𝑛𝐹𝑥)) ⊆ (ω × 𝐴))
12	10, 11	sylan2b 597	. . . . . . . . . 10 ⊢ (({suc 𝑛} ⊆ ω ∧ (𝑛𝐹𝑥) ∈ 𝒫 𝐴) → ({suc 𝑛} × (𝑛𝐹𝑥)) ⊆ (ω × 𝐴))
13	7, 8, 12	syl2an 599	. . . . . . . . 9 ⊢ ((𝑛 ∈ ω ∧ (𝑛𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅})) → ({suc 𝑛} × (𝑛𝐹𝑥)) ⊆ (ω × 𝐴))
14		snex 5324	. . . . . . . . . . 11 ⊢ {suc 𝑛} ∈ V
15		ovex 7246	. . . . . . . . . . 11 ⊢ (𝑛𝐹𝑥) ∈ V
16	14, 15	xpex 7538	. . . . . . . . . 10 ⊢ ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ V
17	16	elpw 4517	. . . . . . . . 9 ⊢ (({suc 𝑛} × (𝑛𝐹𝑥)) ∈ 𝒫 (ω × 𝐴) ↔ ({suc 𝑛} × (𝑛𝐹𝑥)) ⊆ (ω × 𝐴))
18	13, 17	sylibr 237	. . . . . . . 8 ⊢ ((𝑛 ∈ ω ∧ (𝑛𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅})) → ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ 𝒫 (ω × 𝐴))
19	4, 5, 18	syl2anc 587	. . . . . . 7 ⊢ ((𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑛 ∈ ω ∧ 𝑥 ∈ 𝐴) → ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ 𝒫 (ω × 𝐴))
20		eldifn 4042	. . . . . . . 8 ⊢ ((𝑛𝐹𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → ¬ (𝑛𝐹𝑥) ∈ {∅})
21	15	elsn 4556	. . . . . . . . . . 11 ⊢ ((𝑛𝐹𝑥) ∈ {∅} ↔ (𝑛𝐹𝑥) = ∅)
22	21	necon3bbii 2988	. . . . . . . . . 10 ⊢ (¬ (𝑛𝐹𝑥) ∈ {∅} ↔ (𝑛𝐹𝑥) ≠ ∅)
23		vex 3412	. . . . . . . . . . . . 13 ⊢ 𝑛 ∈ V
24	23	sucex 7590	. . . . . . . . . . . 12 ⊢ suc 𝑛 ∈ V
25	24	snnz 4692	. . . . . . . . . . 11 ⊢ {suc 𝑛} ≠ ∅
26		xpnz 6022	. . . . . . . . . . . 12 ⊢ (({suc 𝑛} ≠ ∅ ∧ (𝑛𝐹𝑥) ≠ ∅) ↔ ({suc 𝑛} × (𝑛𝐹𝑥)) ≠ ∅)
27	26	biimpi 219	. . . . . . . . . . 11 ⊢ (({suc 𝑛} ≠ ∅ ∧ (𝑛𝐹𝑥) ≠ ∅) → ({suc 𝑛} × (𝑛𝐹𝑥)) ≠ ∅)
28	25, 27	mpan 690	. . . . . . . . . 10 ⊢ ((𝑛𝐹𝑥) ≠ ∅ → ({suc 𝑛} × (𝑛𝐹𝑥)) ≠ ∅)
29	22, 28	sylbi 220	. . . . . . . . 9 ⊢ (¬ (𝑛𝐹𝑥) ∈ {∅} → ({suc 𝑛} × (𝑛𝐹𝑥)) ≠ ∅)
30	16	elsn 4556	. . . . . . . . . 10 ⊢ (({suc 𝑛} × (𝑛𝐹𝑥)) ∈ {∅} ↔ ({suc 𝑛} × (𝑛𝐹𝑥)) = ∅)
31	30	necon3bbii 2988	. . . . . . . . 9 ⊢ (¬ ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ {∅} ↔ ({suc 𝑛} × (𝑛𝐹𝑥)) ≠ ∅)
32	29, 31	sylibr 237	. . . . . . . 8 ⊢ (¬ (𝑛𝐹𝑥) ∈ {∅} → ¬ ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ {∅})
33	5, 20, 32	3syl 18	. . . . . . 7 ⊢ ((𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑛 ∈ ω ∧ 𝑥 ∈ 𝐴) → ¬ ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ {∅})
34	19, 33	eldifd 3877	. . . . . 6 ⊢ ((𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑛 ∈ ω ∧ 𝑥 ∈ 𝐴) → ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ (𝒫 (ω × 𝐴) ∖ {∅}))
35	34	3expib 1124	. . . . 5 ⊢ (𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) → ((𝑛 ∈ ω ∧ 𝑥 ∈ 𝐴) → ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ (𝒫 (ω × 𝐴) ∖ {∅})))
36	35	ralrimivv 3111	. . . 4 ⊢ (𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) → ∀𝑛 ∈ ω ∀𝑥 ∈ 𝐴 ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ (𝒫 (ω × 𝐴) ∖ {∅}))
37		axdc4lem.2	. . . . 5 ⊢ 𝐺 = (𝑛 ∈ ω, 𝑥 ∈ 𝐴 ↦ ({suc 𝑛} × (𝑛𝐹𝑥)))
38	37	fmpo 7838	. . . 4 ⊢ (∀𝑛 ∈ ω ∀𝑥 ∈ 𝐴 ({suc 𝑛} × (𝑛𝐹𝑥)) ∈ (𝒫 (ω × 𝐴) ∖ {∅}) ↔ 𝐺:(ω × 𝐴)⟶(𝒫 (ω × 𝐴) ∖ {∅}))
39	36, 38	sylib 221	. . 3 ⊢ (𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}) → 𝐺:(ω × 𝐴)⟶(𝒫 (ω × 𝐴) ∖ {∅}))
40		dcomex 10061	. . . . 5 ⊢ ω ∈ V
41	40, 9	xpex 7538	. . . 4 ⊢ (ω × 𝐴) ∈ V
42	41	axdc3 10068	. . 3 ⊢ ((⟨∅, 𝐶⟩ ∈ (ω × 𝐴) ∧ 𝐺:(ω × 𝐴)⟶(𝒫 (ω × 𝐴) ∖ {∅})) → ∃ℎ(ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))))
43	3, 39, 42	syl2an 599	. 2 ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅})) → ∃ℎ(ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))))
44		2ndcof 7792	. . . . . . . . 9 ⊢ (ℎ:ω⟶(ω × 𝐴) → (2nd ∘ ℎ):ω⟶𝐴)
45	44	3ad2ant1 1135	. . . . . . . 8 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (2nd ∘ ℎ):ω⟶𝐴)
46	45	adantl 485	. . . . . . 7 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (2nd ∘ ℎ):ω⟶𝐴)
47		fex2 7711	. . . . . . . 8 ⊢ (((2nd ∘ ℎ):ω⟶𝐴 ∧ ω ∈ V ∧ 𝐴 ∈ V) → (2nd ∘ ℎ) ∈ V)
48	40, 9, 47	mp3an23 1455	. . . . . . 7 ⊢ ((2nd ∘ ℎ):ω⟶𝐴 → (2nd ∘ ℎ) ∈ V)
49	46, 48	syl 17	. . . . . 6 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (2nd ∘ ℎ) ∈ V)
50		fvco3 6810	. . . . . . . . . . 11 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ ∅ ∈ ω) → ((2nd ∘ ℎ)‘∅) = (2nd ‘(ℎ‘∅)))
51	1, 50	mpan2 691	. . . . . . . . . 10 ⊢ (ℎ:ω⟶(ω × 𝐴) → ((2nd ∘ ℎ)‘∅) = (2nd ‘(ℎ‘∅)))
52	51	3ad2ant1 1135	. . . . . . . . 9 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ((2nd ∘ ℎ)‘∅) = (2nd ‘(ℎ‘∅)))
53		fveq2 6717	. . . . . . . . . 10 ⊢ ((ℎ‘∅) = ⟨∅, 𝐶⟩ → (2nd ‘(ℎ‘∅)) = (2nd ‘⟨∅, 𝐶⟩))
54	53	3ad2ant2 1136	. . . . . . . . 9 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (2nd ‘(ℎ‘∅)) = (2nd ‘⟨∅, 𝐶⟩))
55	52, 54	eqtrd 2777	. . . . . . . 8 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ((2nd ∘ ℎ)‘∅) = (2nd ‘⟨∅, 𝐶⟩))
56		op2ndg 7774	. . . . . . . . 9 ⊢ ((∅ ∈ ω ∧ 𝐶 ∈ 𝐴) → (2nd ‘⟨∅, 𝐶⟩) = 𝐶)
57	1, 56	mpan 690	. . . . . . . 8 ⊢ (𝐶 ∈ 𝐴 → (2nd ‘⟨∅, 𝐶⟩) = 𝐶)
58	55, 57	sylan9eqr 2800	. . . . . . 7 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ((2nd ∘ ℎ)‘∅) = 𝐶)
59		nfv 1922	. . . . . . . . 9 ⊢ Ⅎ𝑘 𝐶 ∈ 𝐴
60		nfv 1922	. . . . . . . . . 10 ⊢ Ⅎ𝑘 ℎ:ω⟶(ω × 𝐴)
61		nfv 1922	. . . . . . . . . 10 ⊢ Ⅎ𝑘(ℎ‘∅) = ⟨∅, 𝐶⟩
62		nfra1 3140	. . . . . . . . . 10 ⊢ Ⅎ𝑘∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))
63	60, 61, 62	nf3an 1909	. . . . . . . . 9 ⊢ Ⅎ𝑘(ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))
64	59, 63	nfan 1907	. . . . . . . 8 ⊢ Ⅎ𝑘(𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))))
65		fveq2 6717	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = ∅ → (ℎ‘𝑚) = (ℎ‘∅))
66		opeq1 4784	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = ∅ → ⟨𝑚, 𝑧⟩ = ⟨∅, 𝑧⟩)
67	65, 66	eqeq12d 2753	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = ∅ → ((ℎ‘𝑚) = ⟨𝑚, 𝑧⟩ ↔ (ℎ‘∅) = ⟨∅, 𝑧⟩))
68	67	exbidv 1929	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = ∅ → (∃𝑧(ℎ‘𝑚) = ⟨𝑚, 𝑧⟩ ↔ ∃𝑧(ℎ‘∅) = ⟨∅, 𝑧⟩))
69		fveq2 6717	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑖 → (ℎ‘𝑚) = (ℎ‘𝑖))
70		opeq1 4784	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑖 → ⟨𝑚, 𝑧⟩ = ⟨𝑖, 𝑧⟩)
71	69, 70	eqeq12d 2753	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑖 → ((ℎ‘𝑚) = ⟨𝑚, 𝑧⟩ ↔ (ℎ‘𝑖) = ⟨𝑖, 𝑧⟩))
72	71	exbidv 1929	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑖 → (∃𝑧(ℎ‘𝑚) = ⟨𝑚, 𝑧⟩ ↔ ∃𝑧(ℎ‘𝑖) = ⟨𝑖, 𝑧⟩))
73		fveq2 6717	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = suc 𝑖 → (ℎ‘𝑚) = (ℎ‘suc 𝑖))
74		opeq1 4784	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = suc 𝑖 → ⟨𝑚, 𝑧⟩ = ⟨suc 𝑖, 𝑧⟩)
75	73, 74	eqeq12d 2753	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = suc 𝑖 → ((ℎ‘𝑚) = ⟨𝑚, 𝑧⟩ ↔ (ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩))
76	75	exbidv 1929	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = suc 𝑖 → (∃𝑧(ℎ‘𝑚) = ⟨𝑚, 𝑧⟩ ↔ ∃𝑧(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩))
77		opeq2 4785	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝐶 → ⟨∅, 𝑧⟩ = ⟨∅, 𝐶⟩)
78	77	eqeq2d 2748	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝐶 → ((ℎ‘∅) = ⟨∅, 𝑧⟩ ↔ (ℎ‘∅) = ⟨∅, 𝐶⟩))
79	78	spcegv 3512	. . . . . . . . . . . . . . . . 17 ⊢ (𝐶 ∈ 𝐴 → ((ℎ‘∅) = ⟨∅, 𝐶⟩ → ∃𝑧(ℎ‘∅) = ⟨∅, 𝑧⟩))
80	79	imp 410	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩) → ∃𝑧(ℎ‘∅) = ⟨∅, 𝑧⟩)
81	80	3ad2antr2 1191	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ∃𝑧(ℎ‘∅) = ⟨∅, 𝑧⟩)
82		fveq2 6717	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → (𝐺‘(ℎ‘𝑖)) = (𝐺‘⟨𝑖, 𝑧⟩))
83		df-ov 7216	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑖𝐺𝑧) = (𝐺‘⟨𝑖, 𝑧⟩)
84	82, 83	eqtr4di 2796	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → (𝐺‘(ℎ‘𝑖)) = (𝑖𝐺𝑧))
85	84	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) ∧ (ℎ‘𝑖) = ⟨𝑖, 𝑧⟩) → (𝐺‘(ℎ‘𝑖)) = (𝑖𝐺𝑧))
86		simplr 769	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) ∧ (ℎ‘𝑖) = ⟨𝑖, 𝑧⟩) → 𝑖 ∈ ω)
87		ffvelrn 6902	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) → (ℎ‘𝑖) ∈ (ω × 𝐴))
88		eleq1 2825	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ((ℎ‘𝑖) ∈ (ω × 𝐴) ↔ ⟨𝑖, 𝑧⟩ ∈ (ω × 𝐴)))
89		opelxp2 5593	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (⟨𝑖, 𝑧⟩ ∈ (ω × 𝐴) → 𝑧 ∈ 𝐴)
90	88, 89	syl6bi 256	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ((ℎ‘𝑖) ∈ (ω × 𝐴) → 𝑧 ∈ 𝐴))
91	87, 90	mpan9 510	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) ∧ (ℎ‘𝑖) = ⟨𝑖, 𝑧⟩) → 𝑧 ∈ 𝐴)
92		suceq 6278	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑛 = 𝑖 → suc 𝑛 = suc 𝑖)
93	92	sneqd 4553	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑛 = 𝑖 → {suc 𝑛} = {suc 𝑖})
94		oveq1 7220	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑛 = 𝑖 → (𝑛𝐹𝑥) = (𝑖𝐹𝑥))
95	93, 94	xpeq12d 5582	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑛 = 𝑖 → ({suc 𝑛} × (𝑛𝐹𝑥)) = ({suc 𝑖} × (𝑖𝐹𝑥)))
96		oveq2 7221	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 = 𝑧 → (𝑖𝐹𝑥) = (𝑖𝐹𝑧))
97	96	xpeq2d 5581	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = 𝑧 → ({suc 𝑖} × (𝑖𝐹𝑥)) = ({suc 𝑖} × (𝑖𝐹𝑧)))
98		snex 5324	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ {suc 𝑖} ∈ V
99		ovex 7246	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑖𝐹𝑧) ∈ V
100	98, 99	xpex 7538	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ({suc 𝑖} × (𝑖𝐹𝑧)) ∈ V
101	95, 97, 37, 100	ovmpo 7369	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑖 ∈ ω ∧ 𝑧 ∈ 𝐴) → (𝑖𝐺𝑧) = ({suc 𝑖} × (𝑖𝐹𝑧)))
102	86, 91, 101	syl2anc 587	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) ∧ (ℎ‘𝑖) = ⟨𝑖, 𝑧⟩) → (𝑖𝐺𝑧) = ({suc 𝑖} × (𝑖𝐹𝑧)))
103	85, 102	eqtrd 2777	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) ∧ (ℎ‘𝑖) = ⟨𝑖, 𝑧⟩) → (𝐺‘(ℎ‘𝑖)) = ({suc 𝑖} × (𝑖𝐹𝑧)))
104		suceq 6278	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑘 = 𝑖 → suc 𝑘 = suc 𝑖)
105	104	fveq2d 6721	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 = 𝑖 → (ℎ‘suc 𝑘) = (ℎ‘suc 𝑖))
106		2fveq3 6722	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 = 𝑖 → (𝐺‘(ℎ‘𝑘)) = (𝐺‘(ℎ‘𝑖)))
107	105, 106	eleq12d 2832	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 = 𝑖 → ((ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) ↔ (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))))
108	107	rspcv 3532	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 ∈ ω → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))))
109	108	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) ∧ (ℎ‘𝑖) = ⟨𝑖, 𝑧⟩) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → (ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖))))
110		eleq2 2826	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐺‘(ℎ‘𝑖)) = ({suc 𝑖} × (𝑖𝐹𝑧)) → ((ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖)) ↔ (ℎ‘suc 𝑖) ∈ ({suc 𝑖} × (𝑖𝐹𝑧))))
111		elxp 5574	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((ℎ‘suc 𝑖) ∈ ({suc 𝑖} × (𝑖𝐹𝑧)) ↔ ∃𝑠∃𝑡((ℎ‘suc 𝑖) = ⟨𝑠, 𝑡⟩ ∧ (𝑠 ∈ {suc 𝑖} ∧ 𝑡 ∈ (𝑖𝐹𝑧))))
112		velsn 4557	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑠 ∈ {suc 𝑖} ↔ 𝑠 = suc 𝑖)
113		opeq1 4784	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑠 = suc 𝑖 → ⟨𝑠, 𝑡⟩ = ⟨suc 𝑖, 𝑡⟩)
114	112, 113	sylbi 220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑠 ∈ {suc 𝑖} → ⟨𝑠, 𝑡⟩ = ⟨suc 𝑖, 𝑡⟩)
115	114	eqeq2d 2748	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑠 ∈ {suc 𝑖} → ((ℎ‘suc 𝑖) = ⟨𝑠, 𝑡⟩ ↔ (ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩))
116	115	biimpac 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((ℎ‘suc 𝑖) = ⟨𝑠, 𝑡⟩ ∧ 𝑠 ∈ {suc 𝑖}) → (ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩)
117	116	adantrr 717	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((ℎ‘suc 𝑖) = ⟨𝑠, 𝑡⟩ ∧ (𝑠 ∈ {suc 𝑖} ∧ 𝑡 ∈ (𝑖𝐹𝑧))) → (ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩)
118	117	eximi 1842	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∃𝑡((ℎ‘suc 𝑖) = ⟨𝑠, 𝑡⟩ ∧ (𝑠 ∈ {suc 𝑖} ∧ 𝑡 ∈ (𝑖𝐹𝑧))) → ∃𝑡(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩)
119	118	exlimiv 1938	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∃𝑠∃𝑡((ℎ‘suc 𝑖) = ⟨𝑠, 𝑡⟩ ∧ (𝑠 ∈ {suc 𝑖} ∧ 𝑡 ∈ (𝑖𝐹𝑧))) → ∃𝑡(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩)
120	111, 119	sylbi 220	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((ℎ‘suc 𝑖) ∈ ({suc 𝑖} × (𝑖𝐹𝑧)) → ∃𝑡(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩)
121	110, 120	syl6bi 256	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐺‘(ℎ‘𝑖)) = ({suc 𝑖} × (𝑖𝐹𝑧)) → ((ℎ‘suc 𝑖) ∈ (𝐺‘(ℎ‘𝑖)) → ∃𝑡(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩))
122	103, 109, 121	sylsyld 61	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) ∧ (ℎ‘𝑖) = ⟨𝑖, 𝑧⟩) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → ∃𝑡(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩))
123	122	expcom 417	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → ∃𝑡(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩)))
124	123	exlimiv 1938	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑧(ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → ∃𝑡(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩)))
125	124	com3l 89	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → (∃𝑧(ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ∃𝑡(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩)))
126		opeq2 4785	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 = 𝑧 → ⟨suc 𝑖, 𝑡⟩ = ⟨suc 𝑖, 𝑧⟩)
127	126	eqeq2d 2748	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 = 𝑧 → ((ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩ ↔ (ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩))
128	127	cbvexvw 2045	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑡(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑡⟩ ↔ ∃𝑧(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩)
129	125, 128	syl8ib 259	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑖 ∈ ω) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → (∃𝑧(ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ∃𝑧(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩)))
130	129	impancom 455	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑖 ∈ ω → (∃𝑧(ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ∃𝑧(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩)))
131	130	3adant2 1133	. . . . . . . . . . . . . . . . 17 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → (𝑖 ∈ ω → (∃𝑧(ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ∃𝑧(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩)))
132	131	adantl 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (𝑖 ∈ ω → (∃𝑧(ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ∃𝑧(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩)))
133	132	com12 32	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ ω → ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (∃𝑧(ℎ‘𝑖) = ⟨𝑖, 𝑧⟩ → ∃𝑧(ℎ‘suc 𝑖) = ⟨suc 𝑖, 𝑧⟩)))
134	68, 72, 76, 81, 133	finds2 7678	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ω → ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ∃𝑧(ℎ‘𝑚) = ⟨𝑚, 𝑧⟩))
135	134	com12 32	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (𝑚 ∈ ω → ∃𝑧(ℎ‘𝑚) = ⟨𝑚, 𝑧⟩))
136	135	ralrimiv 3104	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ∀𝑚 ∈ ω ∃𝑧(ℎ‘𝑚) = ⟨𝑚, 𝑧⟩)
137		fveq2 6717	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑘 → (ℎ‘𝑚) = (ℎ‘𝑘))
138		opeq1 4784	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑘 → ⟨𝑚, 𝑧⟩ = ⟨𝑘, 𝑧⟩)
139	137, 138	eqeq12d 2753	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑘 → ((ℎ‘𝑚) = ⟨𝑚, 𝑧⟩ ↔ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩))
140	139	exbidv 1929	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑘 → (∃𝑧(ℎ‘𝑚) = ⟨𝑚, 𝑧⟩ ↔ ∃𝑧(ℎ‘𝑘) = ⟨𝑘, 𝑧⟩))
141	140	rspccv 3534	. . . . . . . . . . . 12 ⊢ (∀𝑚 ∈ ω ∃𝑧(ℎ‘𝑚) = ⟨𝑚, 𝑧⟩ → (𝑘 ∈ ω → ∃𝑧(ℎ‘𝑘) = ⟨𝑘, 𝑧⟩))
142	136, 141	syl 17	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (𝑘 ∈ ω → ∃𝑧(ℎ‘𝑘) = ⟨𝑘, 𝑧⟩))
143	142	3impia 1119	. . . . . . . . . 10 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → ∃𝑧(ℎ‘𝑘) = ⟨𝑘, 𝑧⟩)
144		simp21 1208	. . . . . . . . . 10 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → ℎ:ω⟶(ω × 𝐴))
145		simp3 1140	. . . . . . . . . 10 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → 𝑘 ∈ ω)
146		rspa 3128	. . . . . . . . . . . 12 ⊢ ((∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) ∧ 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))
147	146	3ad2antl3 1189	. . . . . . . . . . 11 ⊢ (((ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))
148	147	3adant1 1132	. . . . . . . . . 10 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))
149		simpl 486	. . . . . . . . . . . . . . . . 17 ⊢ (((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩)
150	149	fveq2d 6721	. . . . . . . . . . . . . . . 16 ⊢ (((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (𝐺‘(ℎ‘𝑘)) = (𝐺‘⟨𝑘, 𝑧⟩))
151		simprr 773	. . . . . . . . . . . . . . . . 17 ⊢ (((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → 𝑘 ∈ ω)
152		eleq1 2825	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ → ((ℎ‘𝑘) ∈ (ω × 𝐴) ↔ ⟨𝑘, 𝑧⟩ ∈ (ω × 𝐴)))
153		opelxp2 5593	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨𝑘, 𝑧⟩ ∈ (ω × 𝐴) → 𝑧 ∈ 𝐴)
154	152, 153	syl6bi 256	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ → ((ℎ‘𝑘) ∈ (ω × 𝐴) → 𝑧 ∈ 𝐴))
155		ffvelrn 6902	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → (ℎ‘𝑘) ∈ (ω × 𝐴))
156	154, 155	impel 509	. . . . . . . . . . . . . . . . 17 ⊢ (((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → 𝑧 ∈ 𝐴)
157		df-ov 7216	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘𝐺𝑧) = (𝐺‘⟨𝑘, 𝑧⟩)
158		suceq 6278	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑘 → suc 𝑛 = suc 𝑘)
159	158	sneqd 4553	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑘 → {suc 𝑛} = {suc 𝑘})
160		oveq1 7220	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑘 → (𝑛𝐹𝑥) = (𝑘𝐹𝑥))
161	159, 160	xpeq12d 5582	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑘 → ({suc 𝑛} × (𝑛𝐹𝑥)) = ({suc 𝑘} × (𝑘𝐹𝑥)))
162		oveq2 7221	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑧 → (𝑘𝐹𝑥) = (𝑘𝐹𝑧))
163	162	xpeq2d 5581	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑧 → ({suc 𝑘} × (𝑘𝐹𝑥)) = ({suc 𝑘} × (𝑘𝐹𝑧)))
164		snex 5324	. . . . . . . . . . . . . . . . . . . 20 ⊢ {suc 𝑘} ∈ V
165		ovex 7246	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘𝐹𝑧) ∈ V
166	164, 165	xpex 7538	. . . . . . . . . . . . . . . . . . 19 ⊢ ({suc 𝑘} × (𝑘𝐹𝑧)) ∈ V
167	161, 163, 37, 166	ovmpo 7369	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ω ∧ 𝑧 ∈ 𝐴) → (𝑘𝐺𝑧) = ({suc 𝑘} × (𝑘𝐹𝑧)))
168	157, 167	eqtr3id 2792	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ω ∧ 𝑧 ∈ 𝐴) → (𝐺‘⟨𝑘, 𝑧⟩) = ({suc 𝑘} × (𝑘𝐹𝑧)))
169	151, 156, 168	syl2anc 587	. . . . . . . . . . . . . . . 16 ⊢ (((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (𝐺‘⟨𝑘, 𝑧⟩) = ({suc 𝑘} × (𝑘𝐹𝑧)))
170	150, 169	eqtrd 2777	. . . . . . . . . . . . . . 15 ⊢ (((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (𝐺‘(ℎ‘𝑘)) = ({suc 𝑘} × (𝑘𝐹𝑧)))
171	170	eleq2d 2823	. . . . . . . . . . . . . 14 ⊢ (((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) ↔ (ℎ‘suc 𝑘) ∈ ({suc 𝑘} × (𝑘𝐹𝑧))))
172		elxp 5574	. . . . . . . . . . . . . . . . 17 ⊢ ((ℎ‘suc 𝑘) ∈ ({suc 𝑘} × (𝑘𝐹𝑧)) ↔ ∃𝑠∃𝑡((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (𝑠 ∈ {suc 𝑘} ∧ 𝑡 ∈ (𝑘𝐹𝑧))))
173		peano2 7668	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 ∈ ω → suc 𝑘 ∈ ω)
174		fvco3 6810	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ suc 𝑘 ∈ ω) → ((2nd ∘ ℎ)‘suc 𝑘) = (2nd ‘(ℎ‘suc 𝑘)))
175	173, 174	sylan2 596	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((2nd ∘ ℎ)‘suc 𝑘) = (2nd ‘(ℎ‘suc 𝑘)))
176	175	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd ∘ ℎ)‘suc 𝑘) = (2nd ‘(ℎ‘suc 𝑘)))
177		simpll 767	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩)
178	177	fveq2d 6721	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (2nd ‘(ℎ‘suc 𝑘)) = (2nd ‘⟨𝑠, 𝑡⟩))
179	176, 178	eqtrd 2777	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd ∘ ℎ)‘suc 𝑘) = (2nd ‘⟨𝑠, 𝑡⟩))
180		vex 3412	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑠 ∈ V
181		vex 3412	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑡 ∈ V
182	180, 181	op2nd 7770	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (2nd ‘⟨𝑠, 𝑡⟩) = 𝑡
183	179, 182	eqtrdi 2794	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd ∘ ℎ)‘suc 𝑘) = 𝑡)
184		fvco3 6810	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((2nd ∘ ℎ)‘𝑘) = (2nd ‘(ℎ‘𝑘)))
185	184	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd ∘ ℎ)‘𝑘) = (2nd ‘(ℎ‘𝑘)))
186		simplr 769	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩)
187	186	fveq2d 6721	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (2nd ‘(ℎ‘𝑘)) = (2nd ‘⟨𝑘, 𝑧⟩))
188	185, 187	eqtrd 2777	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd ∘ ℎ)‘𝑘) = (2nd ‘⟨𝑘, 𝑧⟩))
189		vex 3412	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑘 ∈ V
190		vex 3412	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑧 ∈ V
191	189, 190	op2nd 7770	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (2nd ‘⟨𝑘, 𝑧⟩) = 𝑧
192	188, 191	eqtrdi 2794	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd ∘ ℎ)‘𝑘) = 𝑧)
193	192	oveq2d 7229	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (𝑘𝐹((2nd ∘ ℎ)‘𝑘)) = (𝑘𝐹𝑧))
194	183, 193	eleq12d 2832	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → (((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)) ↔ 𝑡 ∈ (𝑘𝐹𝑧)))
195	194	biimprcd 253	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 ∈ (𝑘𝐹𝑧) → ((((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (ℎ‘𝑘) = ⟨𝑘, 𝑧⟩) ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))
196	195	exp4c 436	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ∈ (𝑘𝐹𝑧) → ((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ → ((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))))
197	196	adantl 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑠 ∈ {suc 𝑘} ∧ 𝑡 ∈ (𝑘𝐹𝑧)) → ((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ → ((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))))
198	197	impcom 411	. . . . . . . . . . . . . . . . . 18 ⊢ (((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (𝑠 ∈ {suc 𝑘} ∧ 𝑡 ∈ (𝑘𝐹𝑧))) → ((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))))
199	198	exlimivv 1940	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑠∃𝑡((ℎ‘suc 𝑘) = ⟨𝑠, 𝑡⟩ ∧ (𝑠 ∈ {suc 𝑘} ∧ 𝑡 ∈ (𝑘𝐹𝑧))) → ((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))))
200	172, 199	sylbi 220	. . . . . . . . . . . . . . . 16 ⊢ ((ℎ‘suc 𝑘) ∈ ({suc 𝑘} × (𝑘𝐹𝑧)) → ((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))))
201	200	com3l 89	. . . . . . . . . . . . . . 15 ⊢ ((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((ℎ‘suc 𝑘) ∈ ({suc 𝑘} × (𝑘𝐹𝑧)) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))))
202	201	imp 410	. . . . . . . . . . . . . 14 ⊢ (((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((ℎ‘suc 𝑘) ∈ ({suc 𝑘} × (𝑘𝐹𝑧)) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))
203	171, 202	sylbid 243	. . . . . . . . . . . . 13 ⊢ (((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω)) → ((ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))
204	203	ex 416	. . . . . . . . . . . 12 ⊢ ((ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))))
205	204	exlimiv 1938	. . . . . . . . . . 11 ⊢ (∃𝑧(ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ → ((ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) → ((ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))))
206	205	3imp 1113	. . . . . . . . . 10 ⊢ ((∃𝑧(ℎ‘𝑘) = ⟨𝑘, 𝑧⟩ ∧ (ℎ:ω⟶(ω × 𝐴) ∧ 𝑘 ∈ ω) ∧ (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))
207	143, 144, 145, 148, 206	syl121anc 1377	. . . . . . . . 9 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) ∧ 𝑘 ∈ ω) → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))
208	207	3expia 1123	. . . . . . . 8 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → (𝑘 ∈ ω → ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))
209	64, 208	ralrimi 3137	. . . . . . 7 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ∀𝑘 ∈ ω ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))
210	46, 58, 209	3jca 1130	. . . . . 6 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ((2nd ∘ ℎ):ω⟶𝐴 ∧ ((2nd ∘ ℎ)‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))
211		feq1 6526	. . . . . . 7 ⊢ (𝑔 = (2nd ∘ ℎ) → (𝑔:ω⟶𝐴 ↔ (2nd ∘ ℎ):ω⟶𝐴))
212		fveq1 6716	. . . . . . . 8 ⊢ (𝑔 = (2nd ∘ ℎ) → (𝑔‘∅) = ((2nd ∘ ℎ)‘∅))
213	212	eqeq1d 2739	. . . . . . 7 ⊢ (𝑔 = (2nd ∘ ℎ) → ((𝑔‘∅) = 𝐶 ↔ ((2nd ∘ ℎ)‘∅) = 𝐶))
214		fveq1 6716	. . . . . . . . 9 ⊢ (𝑔 = (2nd ∘ ℎ) → (𝑔‘suc 𝑘) = ((2nd ∘ ℎ)‘suc 𝑘))
215		fveq1 6716	. . . . . . . . . 10 ⊢ (𝑔 = (2nd ∘ ℎ) → (𝑔‘𝑘) = ((2nd ∘ ℎ)‘𝑘))
216	215	oveq2d 7229	. . . . . . . . 9 ⊢ (𝑔 = (2nd ∘ ℎ) → (𝑘𝐹(𝑔‘𝑘)) = (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))
217	214, 216	eleq12d 2832	. . . . . . . 8 ⊢ (𝑔 = (2nd ∘ ℎ) → ((𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘)) ↔ ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))
218	217	ralbidv 3118	. . . . . . 7 ⊢ (𝑔 = (2nd ∘ ℎ) → (∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘)) ↔ ∀𝑘 ∈ ω ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘))))
219	211, 213, 218	3anbi123d 1438	. . . . . 6 ⊢ (𝑔 = (2nd ∘ ℎ) → ((𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘))) ↔ ((2nd ∘ ℎ):ω⟶𝐴 ∧ ((2nd ∘ ℎ)‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω ((2nd ∘ ℎ)‘suc 𝑘) ∈ (𝑘𝐹((2nd ∘ ℎ)‘𝑘)))))
220	49, 210, 219	spcedv 3513	. . . . 5 ⊢ ((𝐶 ∈ 𝐴 ∧ (ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘)))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘))))
221	220	ex 416	. . . 4 ⊢ (𝐶 ∈ 𝐴 → ((ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘)))))
222	221	exlimdv 1941	. . 3 ⊢ (𝐶 ∈ 𝐴 → (∃ℎ(ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘)))))
223	222	adantr 484	. 2 ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅})) → (∃ℎ(ℎ:ω⟶(ω × 𝐴) ∧ (ℎ‘∅) = ⟨∅, 𝐶⟩ ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝐺‘(ℎ‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘)))))
224	43, 223	mpd 15	1 ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝑘𝐹(𝑔‘𝑘))))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∧ w3a 1089   = wceq 1543  ∃wex 1787   ∈ wcel 2110   ≠ wne 2940  ∀wral 3061  Vcvv 3408   ∖ cdif 3863   ⊆ wss 3866  ∅c0 4237  𝒫 cpw 4513  {csn 4541  ⟨cop 4547   × cxp 5549   ∘ ccom 5555  suc csuc 6215  ⟶wf 6376  ‘cfv 6380  (class class class)co 7213   ∈ cmpo 7215  ωcom 7644  2^nd c2nd 7760

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523  ax-dc 10060

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-pss 3885  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-tp 4546  df-op 4548  df-uni 4820  df-iun 4906  df-br 5054  df-opab 5116  df-mpt 5136  df-tr 5162  df-id 5455  df-eprel 5460  df-po 5468  df-so 5469  df-fr 5509  df-we 5511  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-ord 6216  df-on 6217  df-lim 6218  df-suc 6219  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-ov 7216  df-oprab 7217  df-mpo 7218  df-om 7645  df-1st 7761  df-2nd 7762  df-1o 8202

This theorem is referenced by:  axdc4  10070