Theorem axcclem 9162

Description: Lemma for axcc 9163. (Contributed by Mario Carneiro, 2-Feb-2013.) (Revised by Mario Carneiro, 16-Nov-2013.)

Hypotheses

Ref	Expression
axcclem.1	⊢ 𝐴 = (𝑥 ∖ {∅})
axcclem.2	⊢ 𝐹 = (𝑛 ∈ ω, 𝑦 ∈ ∪ 𝐴 ↦ (𝑓‘𝑛))
axcclem.3	⊢ 𝐺 = (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤)))

Assertion

Ref	Expression
axcclem	⊢ (𝑥 ≈ ω → ∃𝑔∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧))

Distinct variable groups:   𝐴,𝑓,ℎ,𝑛,𝑦   𝑤,𝐴,𝑧,𝑓,ℎ   ℎ,𝐹,𝑧   𝑔,𝐺,𝑧   𝑓,𝑔,𝑥,ℎ

Allowed substitution hints:   𝐴(𝑥,𝑔)   𝐹(𝑥,𝑦,𝑤,𝑓,𝑔,𝑛)   𝐺(𝑥,𝑦,𝑤,𝑓,ℎ,𝑛)

Proof of Theorem axcclem

Dummy variables 𝑐 𝑖 𝑘 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		isfinite2 8103	. . . . . . . 8 ⊢ (𝐴 ≺ ω → 𝐴 ∈ Fin)
2		axcclem.1	. . . . . . . . . 10 ⊢ 𝐴 = (𝑥 ∖ {∅})
3	2	eleq1i 2679	. . . . . . . . 9 ⊢ (𝐴 ∈ Fin ↔ (𝑥 ∖ {∅}) ∈ Fin)
4		undif1 3995	. . . . . . . . . . 11 ⊢ ((𝑥 ∖ {∅}) ∪ {∅}) = (𝑥 ∪ {∅})
5		snfi 7923	. . . . . . . . . . . 12 ⊢ {∅} ∈ Fin
6		unfi 8112	. . . . . . . . . . . 12 ⊢ (((𝑥 ∖ {∅}) ∈ Fin ∧ {∅} ∈ Fin) → ((𝑥 ∖ {∅}) ∪ {∅}) ∈ Fin)
7	5, 6	mpan2 703	. . . . . . . . . . 11 ⊢ ((𝑥 ∖ {∅}) ∈ Fin → ((𝑥 ∖ {∅}) ∪ {∅}) ∈ Fin)
8	4, 7	syl5eqelr 2693	. . . . . . . . . 10 ⊢ ((𝑥 ∖ {∅}) ∈ Fin → (𝑥 ∪ {∅}) ∈ Fin)
9		ssun1 3738	. . . . . . . . . 10 ⊢ 𝑥 ⊆ (𝑥 ∪ {∅})
10		ssfi 8065	. . . . . . . . . 10 ⊢ (((𝑥 ∪ {∅}) ∈ Fin ∧ 𝑥 ⊆ (𝑥 ∪ {∅})) → 𝑥 ∈ Fin)
11	8, 9, 10	sylancl 693	. . . . . . . . 9 ⊢ ((𝑥 ∖ {∅}) ∈ Fin → 𝑥 ∈ Fin)
12	3, 11	sylbi 206	. . . . . . . 8 ⊢ (𝐴 ∈ Fin → 𝑥 ∈ Fin)
13		dcomex 9152	. . . . . . . . . 10 ⊢ ω ∈ V
14		isfiniteg 8105	. . . . . . . . . 10 ⊢ (ω ∈ V → (𝑥 ∈ Fin ↔ 𝑥 ≺ ω))
15	13, 14	ax-mp 5	. . . . . . . . 9 ⊢ (𝑥 ∈ Fin ↔ 𝑥 ≺ ω)
16		sdomnen 7870	. . . . . . . . 9 ⊢ (𝑥 ≺ ω → ¬ 𝑥 ≈ ω)
17	15, 16	sylbi 206	. . . . . . . 8 ⊢ (𝑥 ∈ Fin → ¬ 𝑥 ≈ ω)
18	1, 12, 17	3syl 18	. . . . . . 7 ⊢ (𝐴 ≺ ω → ¬ 𝑥 ≈ ω)
19	18	con2i 133	. . . . . 6 ⊢ (𝑥 ≈ ω → ¬ 𝐴 ≺ ω)
20		sdomentr 7979	. . . . . . 7 ⊢ ((𝐴 ≺ 𝑥 ∧ 𝑥 ≈ ω) → 𝐴 ≺ ω)
21	20	expcom 450	. . . . . 6 ⊢ (𝑥 ≈ ω → (𝐴 ≺ 𝑥 → 𝐴 ≺ ω))
22	19, 21	mtod 188	. . . . 5 ⊢ (𝑥 ≈ ω → ¬ 𝐴 ≺ 𝑥)
23		vex 3176	. . . . . 6 ⊢ 𝑥 ∈ V
24		difss 3699	. . . . . . 7 ⊢ (𝑥 ∖ {∅}) ⊆ 𝑥
25	2, 24	eqsstri 3598	. . . . . 6 ⊢ 𝐴 ⊆ 𝑥
26		ssdomg 7887	. . . . . 6 ⊢ (𝑥 ∈ V → (𝐴 ⊆ 𝑥 → 𝐴 ≼ 𝑥))
27	23, 25, 26	mp2 9	. . . . 5 ⊢ 𝐴 ≼ 𝑥
28	22, 27	jctil 558	. . . 4 ⊢ (𝑥 ≈ ω → (𝐴 ≼ 𝑥 ∧ ¬ 𝐴 ≺ 𝑥))
29		bren2 7872	. . . 4 ⊢ (𝐴 ≈ 𝑥 ↔ (𝐴 ≼ 𝑥 ∧ ¬ 𝐴 ≺ 𝑥))
30	28, 29	sylibr 223	. . 3 ⊢ (𝑥 ≈ ω → 𝐴 ≈ 𝑥)
31		entr 7894	. . 3 ⊢ ((𝐴 ≈ 𝑥 ∧ 𝑥 ≈ ω) → 𝐴 ≈ ω)
32	30, 31	mpancom 700	. 2 ⊢ (𝑥 ≈ ω → 𝐴 ≈ ω)
33		ensym 7891	. 2 ⊢ (𝐴 ≈ ω → ω ≈ 𝐴)
34		bren 7850	. . 3 ⊢ (ω ≈ 𝐴 ↔ ∃𝑓 𝑓:ω–1-1-onto→𝐴)
35		f1of 6050	. . . . . . . 8 ⊢ (𝑓:ω–1-1-onto→𝐴 → 𝑓:ω⟶𝐴)
36		peano1 6977	. . . . . . . 8 ⊢ ∅ ∈ ω
37		ffvelrn 6265	. . . . . . . 8 ⊢ ((𝑓:ω⟶𝐴 ∧ ∅ ∈ ω) → (𝑓‘∅) ∈ 𝐴)
38	35, 36, 37	sylancl 693	. . . . . . 7 ⊢ (𝑓:ω–1-1-onto→𝐴 → (𝑓‘∅) ∈ 𝐴)
39		eldifn 3695	. . . . . . . . 9 ⊢ ((𝑓‘∅) ∈ (𝑥 ∖ {∅}) → ¬ (𝑓‘∅) ∈ {∅})
40	39, 2	eleq2s 2706	. . . . . . . 8 ⊢ ((𝑓‘∅) ∈ 𝐴 → ¬ (𝑓‘∅) ∈ {∅})
41		fvex 6113	. . . . . . . . . . 11 ⊢ (𝑓‘∅) ∈ V
42	41	elsn 4140	. . . . . . . . . 10 ⊢ ((𝑓‘∅) ∈ {∅} ↔ (𝑓‘∅) = ∅)
43	42	notbii 309	. . . . . . . . 9 ⊢ (¬ (𝑓‘∅) ∈ {∅} ↔ ¬ (𝑓‘∅) = ∅)
44		neq0 3889	. . . . . . . . 9 ⊢ (¬ (𝑓‘∅) = ∅ ↔ ∃𝑐 𝑐 ∈ (𝑓‘∅))
45	43, 44	bitr2i 264	. . . . . . . 8 ⊢ (∃𝑐 𝑐 ∈ (𝑓‘∅) ↔ ¬ (𝑓‘∅) ∈ {∅})
46	40, 45	sylibr 223	. . . . . . 7 ⊢ ((𝑓‘∅) ∈ 𝐴 → ∃𝑐 𝑐 ∈ (𝑓‘∅))
47	38, 46	syl 17	. . . . . 6 ⊢ (𝑓:ω–1-1-onto→𝐴 → ∃𝑐 𝑐 ∈ (𝑓‘∅))
48		elunii 4377	. . . . . . . . . . 11 ⊢ ((𝑐 ∈ (𝑓‘∅) ∧ (𝑓‘∅) ∈ 𝐴) → 𝑐 ∈ ∪ 𝐴)
49	38, 48	sylan2 490	. . . . . . . . . 10 ⊢ ((𝑐 ∈ (𝑓‘∅) ∧ 𝑓:ω–1-1-onto→𝐴) → 𝑐 ∈ ∪ 𝐴)
50	35	ffvelrnda 6267	. . . . . . . . . . . . . 14 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑛 ∈ ω) → (𝑓‘𝑛) ∈ 𝐴)
51		difabs 3851	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∖ {∅}) ∖ {∅}) = (𝑥 ∖ {∅})
52	2	difeq1i 3686	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∖ {∅}) = ((𝑥 ∖ {∅}) ∖ {∅})
53	51, 52, 2	3eqtr4i 2642	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∖ {∅}) = 𝐴
54		pwuni 4825	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐴 ⊆ 𝒫 ∪ 𝐴
55		ssdif 3707	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ⊆ 𝒫 ∪ 𝐴 → (𝐴 ∖ {∅}) ⊆ (𝒫 ∪ 𝐴 ∖ {∅}))
56	54, 55	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∖ {∅}) ⊆ (𝒫 ∪ 𝐴 ∖ {∅})
57	53, 56	eqsstr3i 3599	. . . . . . . . . . . . . . . 16 ⊢ 𝐴 ⊆ (𝒫 ∪ 𝐴 ∖ {∅})
58	57	sseli 3564	. . . . . . . . . . . . . . 15 ⊢ ((𝑓‘𝑛) ∈ 𝐴 → (𝑓‘𝑛) ∈ (𝒫 ∪ 𝐴 ∖ {∅}))
59	58	ralrimivw 2950	. . . . . . . . . . . . . 14 ⊢ ((𝑓‘𝑛) ∈ 𝐴 → ∀𝑦 ∈ ∪ 𝐴(𝑓‘𝑛) ∈ (𝒫 ∪ 𝐴 ∖ {∅}))
60	50, 59	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑛 ∈ ω) → ∀𝑦 ∈ ∪ 𝐴(𝑓‘𝑛) ∈ (𝒫 ∪ 𝐴 ∖ {∅}))
61	60	ralrimiva 2949	. . . . . . . . . . . 12 ⊢ (𝑓:ω–1-1-onto→𝐴 → ∀𝑛 ∈ ω ∀𝑦 ∈ ∪ 𝐴(𝑓‘𝑛) ∈ (𝒫 ∪ 𝐴 ∖ {∅}))
62		axcclem.2	. . . . . . . . . . . . 13 ⊢ 𝐹 = (𝑛 ∈ ω, 𝑦 ∈ ∪ 𝐴 ↦ (𝑓‘𝑛))
63	62	fmpt2 7126	. . . . . . . . . . . 12 ⊢ (∀𝑛 ∈ ω ∀𝑦 ∈ ∪ 𝐴(𝑓‘𝑛) ∈ (𝒫 ∪ 𝐴 ∖ {∅}) ↔ 𝐹:(ω × ∪ 𝐴)⟶(𝒫 ∪ 𝐴 ∖ {∅}))
64	61, 63	sylib 207	. . . . . . . . . . 11 ⊢ (𝑓:ω–1-1-onto→𝐴 → 𝐹:(ω × ∪ 𝐴)⟶(𝒫 ∪ 𝐴 ∖ {∅}))
65	64	adantl 481	. . . . . . . . . 10 ⊢ ((𝑐 ∈ (𝑓‘∅) ∧ 𝑓:ω–1-1-onto→𝐴) → 𝐹:(ω × ∪ 𝐴)⟶(𝒫 ∪ 𝐴 ∖ {∅}))
66		difexg 4735	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ V → (𝑥 ∖ {∅}) ∈ V)
67	23, 66	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (𝑥 ∖ {∅}) ∈ V
68	2, 67	eqeltri 2684	. . . . . . . . . . . 12 ⊢ 𝐴 ∈ V
69	68	uniex 6851	. . . . . . . . . . 11 ⊢ ∪ 𝐴 ∈ V
70	69	axdc4 9161	. . . . . . . . . 10 ⊢ ((𝑐 ∈ ∪ 𝐴 ∧ 𝐹:(ω × ∪ 𝐴)⟶(𝒫 ∪ 𝐴 ∖ {∅})) → ∃ℎ(ℎ:ω⟶∪ 𝐴 ∧ (ℎ‘∅) = 𝑐 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))))
71	49, 65, 70	syl2anc 691	. . . . . . . . 9 ⊢ ((𝑐 ∈ (𝑓‘∅) ∧ 𝑓:ω–1-1-onto→𝐴) → ∃ℎ(ℎ:ω⟶∪ 𝐴 ∧ (ℎ‘∅) = 𝑐 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))))
72		3simpb 1052	. . . . . . . . . 10 ⊢ ((ℎ:ω⟶∪ 𝐴 ∧ (ℎ‘∅) = 𝑐 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))) → (ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))))
73	72	eximi 1752	. . . . . . . . 9 ⊢ (∃ℎ(ℎ:ω⟶∪ 𝐴 ∧ (ℎ‘∅) = 𝑐 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))) → ∃ℎ(ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))))
74	71, 73	syl 17	. . . . . . . 8 ⊢ ((𝑐 ∈ (𝑓‘∅) ∧ 𝑓:ω–1-1-onto→𝐴) → ∃ℎ(ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))))
75	74	ex 449	. . . . . . 7 ⊢ (𝑐 ∈ (𝑓‘∅) → (𝑓:ω–1-1-onto→𝐴 → ∃ℎ(ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))))
76	75	exlimiv 1845	. . . . . 6 ⊢ (∃𝑐 𝑐 ∈ (𝑓‘∅) → (𝑓:ω–1-1-onto→𝐴 → ∃ℎ(ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))))
77	47, 76	mpcom 37	. . . . 5 ⊢ (𝑓:ω–1-1-onto→𝐴 → ∃ℎ(ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))))
78		velsn 4141	. . . . . . . . . . 11 ⊢ (𝑧 ∈ {∅} ↔ 𝑧 = ∅)
79	78	necon3bbii 2829	. . . . . . . . . 10 ⊢ (¬ 𝑧 ∈ {∅} ↔ 𝑧 ≠ ∅)
80	2	eleq2i 2680	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝐴 ↔ 𝑧 ∈ (𝑥 ∖ {∅}))
81		eldif 3550	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (𝑥 ∖ {∅}) ↔ (𝑧 ∈ 𝑥 ∧ ¬ 𝑧 ∈ {∅}))
82	80, 81	sylbbr 225	. . . . . . . . . 10 ⊢ ((𝑧 ∈ 𝑥 ∧ ¬ 𝑧 ∈ {∅}) → 𝑧 ∈ 𝐴)
83	79, 82	sylan2br 492	. . . . . . . . 9 ⊢ ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → 𝑧 ∈ 𝐴)
84		simpl 472	. . . . . . . . . . . 12 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑧 ∈ 𝐴) → 𝑓:ω–1-1-onto→𝐴)
85		f1ofo 6057	. . . . . . . . . . . . . 14 ⊢ (𝑓:ω–1-1-onto→𝐴 → 𝑓:ω–onto→𝐴)
86		foelrn 6286	. . . . . . . . . . . . . 14 ⊢ ((𝑓:ω–onto→𝐴 ∧ 𝑧 ∈ 𝐴) → ∃𝑖 ∈ ω 𝑧 = (𝑓‘𝑖))
87	85, 86	sylan 487	. . . . . . . . . . . . 13 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑧 ∈ 𝐴) → ∃𝑖 ∈ ω 𝑧 = (𝑓‘𝑖))
88		suceq 5707	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 = 𝑖 → suc 𝑘 = suc 𝑖)
89	88	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 = 𝑖 → (ℎ‘suc 𝑘) = (ℎ‘suc 𝑖))
90		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 = 𝑖 → 𝑘 = 𝑖)
91		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 = 𝑖 → (ℎ‘𝑘) = (ℎ‘𝑖))
92	90, 91	oveq12d 6567	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 = 𝑖 → (𝑘𝐹(ℎ‘𝑘)) = (𝑖𝐹(ℎ‘𝑖)))
93	89, 92	eleq12d 2682	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 𝑖 → ((ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ↔ (ℎ‘suc 𝑖) ∈ (𝑖𝐹(ℎ‘𝑖))))
94	93	rspcv 3278	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 ∈ ω → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (ℎ‘suc 𝑖) ∈ (𝑖𝐹(ℎ‘𝑖))))
95	94	3ad2ant3 1077	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (ℎ‘suc 𝑖) ∈ (𝑖𝐹(ℎ‘𝑖))))
96	95	imp 444	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))) → (ℎ‘suc 𝑖) ∈ (𝑖𝐹(ℎ‘𝑖)))
97	96	3adant3 1074	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (ℎ‘suc 𝑖) ∈ (𝑖𝐹(ℎ‘𝑖)))
98		eqcom 2617	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 = (𝑓‘𝑖) ↔ (𝑓‘𝑖) = 𝑧)
99		f1ocnvfv 6434	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → ((𝑓‘𝑖) = 𝑧 → (◡𝑓‘𝑧) = 𝑖))
100	98, 99	syl5bi 231	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (𝑧 = (𝑓‘𝑖) → (◡𝑓‘𝑧) = 𝑖))
101	100	3adant1 1072	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (𝑧 = (𝑓‘𝑖) → (◡𝑓‘𝑧) = 𝑖))
102	101	imp 444	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ 𝑧 = (𝑓‘𝑖)) → (◡𝑓‘𝑧) = 𝑖)
103	102	eqcomd 2616	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ 𝑧 = (𝑓‘𝑖)) → 𝑖 = (◡𝑓‘𝑧))
104	103	3adant2 1073	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → 𝑖 = (◡𝑓‘𝑧))
105		suceq 5707	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = (◡𝑓‘𝑧) → suc 𝑖 = suc (◡𝑓‘𝑧))
106	104, 105	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → suc 𝑖 = suc (◡𝑓‘𝑧))
107	106	fveq2d 6107	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (ℎ‘suc 𝑖) = (ℎ‘suc (◡𝑓‘𝑧)))
108		simpr 476	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ℎ:ω⟶∪ 𝐴 ∧ 𝑖 ∈ ω) → 𝑖 ∈ ω)
109		ffvelrn 6265	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ℎ:ω⟶∪ 𝐴 ∧ 𝑖 ∈ ω) → (ℎ‘𝑖) ∈ ∪ 𝐴)
110		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑖 → (𝑓‘𝑛) = (𝑓‘𝑖))
111		eqidd 2611	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = (ℎ‘𝑖) → (𝑓‘𝑖) = (𝑓‘𝑖))
112		fvex 6113	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓‘𝑖) ∈ V
113	110, 111, 62, 112	ovmpt2 6694	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑖 ∈ ω ∧ (ℎ‘𝑖) ∈ ∪ 𝐴) → (𝑖𝐹(ℎ‘𝑖)) = (𝑓‘𝑖))
114	108, 109, 113	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℎ:ω⟶∪ 𝐴 ∧ 𝑖 ∈ ω) → (𝑖𝐹(ℎ‘𝑖)) = (𝑓‘𝑖))
115	114	3adant2 1073	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (𝑖𝐹(ℎ‘𝑖)) = (𝑓‘𝑖))
116	115	3ad2ant1 1075	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (𝑖𝐹(ℎ‘𝑖)) = (𝑓‘𝑖))
117	97, 107, 116	3eltr3d 2702	. . . . . . . . . . . . . . . . . . 19 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (ℎ‘suc (◡𝑓‘𝑧)) ∈ (𝑓‘𝑖))
118	35	ffvelrnda 6267	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (𝑓‘𝑖) ∈ 𝐴)
119	118	3adant1 1072	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (𝑓‘𝑖) ∈ 𝐴)
120	119	3ad2ant1 1075	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (𝑓‘𝑖) ∈ 𝐴)
121		eleq1 2676	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = (𝑓‘𝑖) → (𝑧 ∈ 𝐴 ↔ (𝑓‘𝑖) ∈ 𝐴))
122	121	3ad2ant3 1077	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (𝑧 ∈ 𝐴 ↔ (𝑓‘𝑖) ∈ 𝐴))
123	120, 122	mpbird 246	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → 𝑧 ∈ 𝐴)
124		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑧 → (◡𝑓‘𝑤) = (◡𝑓‘𝑧))
125		suceq 5707	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((◡𝑓‘𝑤) = (◡𝑓‘𝑧) → suc (◡𝑓‘𝑤) = suc (◡𝑓‘𝑧))
126	124, 125	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = 𝑧 → suc (◡𝑓‘𝑤) = suc (◡𝑓‘𝑧))
127	126	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑧 → (ℎ‘suc (◡𝑓‘𝑤)) = (ℎ‘suc (◡𝑓‘𝑧)))
128		axcclem.3	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐺 = (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤)))
129		fvex 6113	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℎ‘suc (◡𝑓‘𝑧)) ∈ V
130	127, 128, 129	fvmpt 6191	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ 𝐴 → (𝐺‘𝑧) = (ℎ‘suc (◡𝑓‘𝑧)))
131	123, 130	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (𝐺‘𝑧) = (ℎ‘suc (◡𝑓‘𝑧)))
132		simp3 1056	. . . . . . . . . . . . . . . . . . 19 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → 𝑧 = (𝑓‘𝑖))
133	117, 131, 132	3eltr4d 2703	. . . . . . . . . . . . . . . . . 18 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (𝐺‘𝑧) ∈ 𝑧)
134	133	3exp 1256	. . . . . . . . . . . . . . . . 17 ⊢ ((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (𝑧 = (𝑓‘𝑖) → (𝐺‘𝑧) ∈ 𝑧)))
135	134	com3r 85	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝑓‘𝑖) → ((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (𝐺‘𝑧) ∈ 𝑧)))
136	135	3expd 1276	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝑓‘𝑖) → (ℎ:ω⟶∪ 𝐴 → (𝑓:ω–1-1-onto→𝐴 → (𝑖 ∈ ω → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (𝐺‘𝑧) ∈ 𝑧)))))
137	136	com4r 92	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ ω → (𝑧 = (𝑓‘𝑖) → (ℎ:ω⟶∪ 𝐴 → (𝑓:ω–1-1-onto→𝐴 → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (𝐺‘𝑧) ∈ 𝑧)))))
138	137	rexlimiv 3009	. . . . . . . . . . . . 13 ⊢ (∃𝑖 ∈ ω 𝑧 = (𝑓‘𝑖) → (ℎ:ω⟶∪ 𝐴 → (𝑓:ω–1-1-onto→𝐴 → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (𝐺‘𝑧) ∈ 𝑧))))
139	87, 138	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑧 ∈ 𝐴) → (ℎ:ω⟶∪ 𝐴 → (𝑓:ω–1-1-onto→𝐴 → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (𝐺‘𝑧) ∈ 𝑧))))
140	84, 139	mpid 43	. . . . . . . . . . 11 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑧 ∈ 𝐴) → (ℎ:ω⟶∪ 𝐴 → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (𝐺‘𝑧) ∈ 𝑧)))
141	140	impd 446	. . . . . . . . . 10 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑧 ∈ 𝐴) → ((ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))) → (𝐺‘𝑧) ∈ 𝑧))
142	141	impancom 455	. . . . . . . . 9 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ (ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))) → (𝑧 ∈ 𝐴 → (𝐺‘𝑧) ∈ 𝑧))
143	83, 142	syl5 33	. . . . . . . 8 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ (ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))) → ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → (𝐺‘𝑧) ∈ 𝑧))
144	143	expd 451	. . . . . . 7 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ (ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))) → (𝑧 ∈ 𝑥 → (𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧)))
145	144	ralrimiv 2948	. . . . . 6 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ (ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))) → ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧))
146		fvrn0 6126	. . . . . . . . . . 11 ⊢ (ℎ‘suc (◡𝑓‘𝑤)) ∈ (ran ℎ ∪ {∅})
147	146	rgenw 2908	. . . . . . . . . 10 ⊢ ∀𝑤 ∈ 𝐴 (ℎ‘suc (◡𝑓‘𝑤)) ∈ (ran ℎ ∪ {∅})
148		eqid 2610	. . . . . . . . . . 11 ⊢ (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤))) = (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤)))
149	148	fmpt 6289	. . . . . . . . . 10 ⊢ (∀𝑤 ∈ 𝐴 (ℎ‘suc (◡𝑓‘𝑤)) ∈ (ran ℎ ∪ {∅}) ↔ (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤))):𝐴⟶(ran ℎ ∪ {∅}))
150	147, 149	mpbi 219	. . . . . . . . 9 ⊢ (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤))):𝐴⟶(ran ℎ ∪ {∅})
151		vex 3176	. . . . . . . . . . 11 ⊢ ℎ ∈ V
152	151	rnex 6992	. . . . . . . . . 10 ⊢ ran ℎ ∈ V
153		p0ex 4779	. . . . . . . . . 10 ⊢ {∅} ∈ V
154	152, 153	unex 6854	. . . . . . . . 9 ⊢ (ran ℎ ∪ {∅}) ∈ V
155		fex2 7014	. . . . . . . . 9 ⊢ (((𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤))):𝐴⟶(ran ℎ ∪ {∅}) ∧ 𝐴 ∈ V ∧ (ran ℎ ∪ {∅}) ∈ V) → (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤))) ∈ V)
156	150, 68, 154, 155	mp3an 1416	. . . . . . . 8 ⊢ (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤))) ∈ V
157	128, 156	eqeltri 2684	. . . . . . 7 ⊢ 𝐺 ∈ V
158		fveq1 6102	. . . . . . . . . 10 ⊢ (𝑔 = 𝐺 → (𝑔‘𝑧) = (𝐺‘𝑧))
159	158	eleq1d 2672	. . . . . . . . 9 ⊢ (𝑔 = 𝐺 → ((𝑔‘𝑧) ∈ 𝑧 ↔ (𝐺‘𝑧) ∈ 𝑧))
160	159	imbi2d 329	. . . . . . . 8 ⊢ (𝑔 = 𝐺 → ((𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧) ↔ (𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧)))
161	160	ralbidv 2969	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧) ↔ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧)))
162	157, 161	spcev 3273	. . . . . 6 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧) → ∃𝑔∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧))
163	145, 162	syl 17	. . . . 5 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ (ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))) → ∃𝑔∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧))
164	77, 163	exlimddv 1850	. . . 4 ⊢ (𝑓:ω–1-1-onto→𝐴 → ∃𝑔∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧))
165	164	exlimiv 1845	. . 3 ⊢ (∃𝑓 𝑓:ω–1-1-onto→𝐴 → ∃𝑔∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧))
166	34, 165	sylbi 206	. 2 ⊢ (ω ≈ 𝐴 → ∃𝑔∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧))
167	32, 33, 166	3syl 18	1 ⊢ (𝑥 ≈ ω → ∃𝑔∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475  ∃wex 1695   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  Vcvv 3173   ∖ cdif 3537   ∪ cun 3538   ⊆ wss 3540  ∅c0 3874  𝒫 cpw 4108  {csn 4125  ∪ cuni 4372   class class class wbr 4583   ↦ cmpt 4643   × cxp 5036  ^◡ccnv 5037  ran crn 5039  suc csuc 5642  ⟶wf 5800  –onto→wfo 5802  –1-1-onto→wf1o 5803  ‘cfv 5804  (class class class)co 6549   ↦ cmpt2 6551  ωcom 6957   ≈ cen 7838   ≼ cdom 7839   ≺ csdm 7840  Fincfn 7841

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-int 4411  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-pred 5597  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-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845

This theorem is referenced by:  axcc  9163