Theorem axcclem 10447

Description: Lemma for axcc 10448. (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 9256	. . . . . . . 8 ⊢ (𝐴 ≺ ω → 𝐴 ∈ Fin)
2		axcclem.1	. . . . . . . . . 10 ⊢ 𝐴 = (𝑥 ∖ {∅})
3	2	eleq1i 2853	. . . . . . . . 9 ⊢ (𝐴 ∈ Fin ↔ (𝑥 ∖ {∅}) ∈ Fin)
4		undif1 4436	. . . . . . . . . . 11 ⊢ ((𝑥 ∖ {∅}) ∪ {∅}) = (𝑥 ∪ {∅})
5		snfi 9038	. . . . . . . . . . . 12 ⊢ {∅} ∈ Fin
6		unfi 9153	. . . . . . . . . . . 12 ⊢ (((𝑥 ∖ {∅}) ∈ Fin ∧ {∅} ∈ Fin) → ((𝑥 ∖ {∅}) ∪ {∅}) ∈ Fin)
7	5, 6	mpan2 703	. . . . . . . . . . 11 ⊢ ((𝑥 ∖ {∅}) ∈ Fin → ((𝑥 ∖ {∅}) ∪ {∅}) ∈ Fin)
8	4, 7	eqeltrrid 2867	. . . . . . . . . 10 ⊢ ((𝑥 ∖ {∅}) ∈ Fin → (𝑥 ∪ {∅}) ∈ Fin)
9		ssun1 4130	. . . . . . . . . 10 ⊢ 𝑥 ⊆ (𝑥 ∪ {∅})
10		ssfi 9155	. . . . . . . . . 10 ⊢ (((𝑥 ∪ {∅}) ∈ Fin ∧ 𝑥 ⊆ (𝑥 ∪ {∅})) → 𝑥 ∈ Fin)
11	8, 9, 10	sylancl 597	. . . . . . . . 9 ⊢ ((𝑥 ∖ {∅}) ∈ Fin → 𝑥 ∈ Fin)
12	3, 11	sylbi 220	. . . . . . . 8 ⊢ (𝐴 ∈ Fin → 𝑥 ∈ Fin)
13		dcomex 10437	. . . . . . . . . 10 ⊢ ω ∈ V
14		isfiniteg 9258	. . . . . . . . . 10 ⊢ (ω ∈ V → (𝑥 ∈ Fin ↔ 𝑥 ≺ ω))
15	13, 14	ax-mp 5	. . . . . . . . 9 ⊢ (𝑥 ∈ Fin ↔ 𝑥 ≺ ω)
16		sdomnen 8976	. . . . . . . . 9 ⊢ (𝑥 ≺ ω → ¬ 𝑥 ≈ ω)
17	15, 16	sylbi 220	. . . . . . . 8 ⊢ (𝑥 ∈ Fin → ¬ 𝑥 ≈ ω)
18	1, 12, 17	3syl 19	. . . . . . 7 ⊢ (𝐴 ≺ ω → ¬ 𝑥 ≈ ω)
19	18	con2i 140	. . . . . 6 ⊢ (𝑥 ≈ ω → ¬ 𝐴 ≺ ω)
20		sdomentr 9097	. . . . . . 7 ⊢ ((𝐴 ≺ 𝑥 ∧ 𝑥 ≈ ω) → 𝐴 ≺ ω)
21	20	expcom 418	. . . . . 6 ⊢ (𝑥 ≈ ω → (𝐴 ≺ 𝑥 → 𝐴 ≺ ω))
22	19, 21	mtod 201	. . . . 5 ⊢ (𝑥 ≈ ω → ¬ 𝐴 ≺ 𝑥)
23		vex 3458	. . . . . 6 ⊢ 𝑥 ∈ V
24		difss 4089	. . . . . . 7 ⊢ (𝑥 ∖ {∅}) ⊆ 𝑥
25	2, 24	eqsstri 3982	. . . . . 6 ⊢ 𝐴 ⊆ 𝑥
26		ssdomg 8995	. . . . . 6 ⊢ (𝑥 ∈ V → (𝐴 ⊆ 𝑥 → 𝐴 ≼ 𝑥))
27	23, 25, 26	mp2 9	. . . . 5 ⊢ 𝐴 ≼ 𝑥
28	22, 27	jctil 528	. . . 4 ⊢ (𝑥 ≈ ω → (𝐴 ≼ 𝑥 ∧ ¬ 𝐴 ≺ 𝑥))
29		bren2 8978	. . . 4 ⊢ (𝐴 ≈ 𝑥 ↔ (𝐴 ≼ 𝑥 ∧ ¬ 𝐴 ≺ 𝑥))
30	28, 29	sylibr 237	. . 3 ⊢ (𝑥 ≈ ω → 𝐴 ≈ 𝑥)
31		entr 9001	. . 3 ⊢ ((𝐴 ≈ 𝑥 ∧ 𝑥 ≈ ω) → 𝐴 ≈ ω)
32	30, 31	mpancom 700	. 2 ⊢ (𝑥 ≈ ω → 𝐴 ≈ ω)
33		ensym 8998	. 2 ⊢ (𝐴 ≈ ω → ω ≈ 𝐴)
34		bren 8951	. . 3 ⊢ (ω ≈ 𝐴 ↔ ∃𝑓 𝑓:ω–1-1-onto→𝐴)
35		f1of 6820	. . . . . . . 8 ⊢ (𝑓:ω–1-1-onto→𝐴 → 𝑓:ω⟶𝐴)
36		peano1 7883	. . . . . . . 8 ⊢ ∅ ∈ ω
37		ffvelcdm 7076	. . . . . . . 8 ⊢ ((𝑓:ω⟶𝐴 ∧ ∅ ∈ ω) → (𝑓‘∅) ∈ 𝐴)
38	35, 36, 37	sylancl 597	. . . . . . 7 ⊢ (𝑓:ω–1-1-onto→𝐴 → (𝑓‘∅) ∈ 𝐴)
39		eldifn 4085	. . . . . . . . 9 ⊢ ((𝑓‘∅) ∈ (𝑥 ∖ {∅}) → ¬ (𝑓‘∅) ∈ {∅})
40	39, 2	eleq2s 2880	. . . . . . . 8 ⊢ ((𝑓‘∅) ∈ 𝐴 → ¬ (𝑓‘∅) ∈ {∅})
41		fvex 6894	. . . . . . . . . . 11 ⊢ (𝑓‘∅) ∈ V
42	41	elsn 4603	. . . . . . . . . 10 ⊢ ((𝑓‘∅) ∈ {∅} ↔ (𝑓‘∅) = ∅)
43	42	notbii 323	. . . . . . . . 9 ⊢ (¬ (𝑓‘∅) ∈ {∅} ↔ ¬ (𝑓‘∅) = ∅)
44		neq0 4305	. . . . . . . . 9 ⊢ (¬ (𝑓‘∅) = ∅ ↔ ∃𝑐 𝑐 ∈ (𝑓‘∅))
45	43, 44	bitr2i 279	. . . . . . . 8 ⊢ (∃𝑐 𝑐 ∈ (𝑓‘∅) ↔ ¬ (𝑓‘∅) ∈ {∅})
46	40, 45	sylibr 237	. . . . . . 7 ⊢ ((𝑓‘∅) ∈ 𝐴 → ∃𝑐 𝑐 ∈ (𝑓‘∅))
47	38, 46	syl 18	. . . . . 6 ⊢ (𝑓:ω–1-1-onto→𝐴 → ∃𝑐 𝑐 ∈ (𝑓‘∅))
48		elunii 4876	. . . . . . . . . . 11 ⊢ ((𝑐 ∈ (𝑓‘∅) ∧ (𝑓‘∅) ∈ 𝐴) → 𝑐 ∈ ∪ 𝐴)
49	38, 48	sylan2 604	. . . . . . . . . 10 ⊢ ((𝑐 ∈ (𝑓‘∅) ∧ 𝑓:ω–1-1-onto→𝐴) → 𝑐 ∈ ∪ 𝐴)
50	35	ffvelcdmda 7079	. . . . . . . . . . . . . 14 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑛 ∈ ω) → (𝑓‘𝑛) ∈ 𝐴)
51		difabs 4255	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∖ {∅}) ∖ {∅}) = (𝑥 ∖ {∅})
52	2	difeq1i 4076	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∖ {∅}) = ((𝑥 ∖ {∅}) ∖ {∅})
53	51, 52, 2	3eqtr4i 2795	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∖ {∅}) = 𝐴
54		pwuni 4910	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐴 ⊆ 𝒫 ∪ 𝐴
55		ssdif 4097	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ⊆ 𝒫 ∪ 𝐴 → (𝐴 ∖ {∅}) ⊆ (𝒫 ∪ 𝐴 ∖ {∅}))
56	54, 55	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∖ {∅}) ⊆ (𝒫 ∪ 𝐴 ∖ {∅})
57	53, 56	eqsstrri 3983	. . . . . . . . . . . . . . . 16 ⊢ 𝐴 ⊆ (𝒫 ∪ 𝐴 ∖ {∅})
58	57	sseli 3932	. . . . . . . . . . . . . . 15 ⊢ ((𝑓‘𝑛) ∈ 𝐴 → (𝑓‘𝑛) ∈ (𝒫 ∪ 𝐴 ∖ {∅}))
59	58	ralrimivw 3160	. . . . . . . . . . . . . 14 ⊢ ((𝑓‘𝑛) ∈ 𝐴 → ∀𝑦 ∈ ∪ 𝐴(𝑓‘𝑛) ∈ (𝒫 ∪ 𝐴 ∖ {∅}))
60	50, 59	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑛 ∈ ω) → ∀𝑦 ∈ ∪ 𝐴(𝑓‘𝑛) ∈ (𝒫 ∪ 𝐴 ∖ {∅}))
61	60	ralrimiva 3156	. . . . . . . . . . . 12 ⊢ (𝑓:ω–1-1-onto→𝐴 → ∀𝑛 ∈ ω ∀𝑦 ∈ ∪ 𝐴(𝑓‘𝑛) ∈ (𝒫 ∪ 𝐴 ∖ {∅}))
62		axcclem.2	. . . . . . . . . . . . 13 ⊢ 𝐹 = (𝑛 ∈ ω, 𝑦 ∈ ∪ 𝐴 ↦ (𝑓‘𝑛))
63	62	fmpo 8063	. . . . . . . . . . . 12 ⊢ (∀𝑛 ∈ ω ∀𝑦 ∈ ∪ 𝐴(𝑓‘𝑛) ∈ (𝒫 ∪ 𝐴 ∖ {∅}) ↔ 𝐹:(ω × ∪ 𝐴)⟶(𝒫 ∪ 𝐴 ∖ {∅}))
64	61, 63	sylib 221	. . . . . . . . . . 11 ⊢ (𝑓:ω–1-1-onto→𝐴 → 𝐹:(ω × ∪ 𝐴)⟶(𝒫 ∪ 𝐴 ∖ {∅}))
65	64	adantl 486	. . . . . . . . . 10 ⊢ ((𝑐 ∈ (𝑓‘∅) ∧ 𝑓:ω–1-1-onto→𝐴) → 𝐹:(ω × ∪ 𝐴)⟶(𝒫 ∪ 𝐴 ∖ {∅}))
66	23	difexi 5300	. . . . . . . . . . . . 13 ⊢ (𝑥 ∖ {∅}) ∈ V
67	2, 66	eqeltri 2858	. . . . . . . . . . . 12 ⊢ 𝐴 ∈ V
68	67	uniex 7741	. . . . . . . . . . 11 ⊢ ∪ 𝐴 ∈ V
69	68	axdc4 10446	. . . . . . . . . 10 ⊢ ((𝑐 ∈ ∪ 𝐴 ∧ 𝐹:(ω × ∪ 𝐴)⟶(𝒫 ∪ 𝐴 ∖ {∅})) → ∃ℎ(ℎ:ω⟶∪ 𝐴 ∧ (ℎ‘∅) = 𝑐 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))))
70	49, 65, 69	syl2anc 595	. . . . . . . . 9 ⊢ ((𝑐 ∈ (𝑓‘∅) ∧ 𝑓:ω–1-1-onto→𝐴) → ∃ℎ(ℎ:ω⟶∪ 𝐴 ∧ (ℎ‘∅) = 𝑐 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))))
71		3simpb 1166	. . . . . . . . . 10 ⊢ ((ℎ:ω⟶∪ 𝐴 ∧ (ℎ‘∅) = 𝑐 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))) → (ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))))
72	71	eximi 1864	. . . . . . . . 9 ⊢ (∃ℎ(ℎ:ω⟶∪ 𝐴 ∧ (ℎ‘∅) = 𝑐 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))) → ∃ℎ(ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))))
73	70, 72	syl 18	. . . . . . . 8 ⊢ ((𝑐 ∈ (𝑓‘∅) ∧ 𝑓:ω–1-1-onto→𝐴) → ∃ℎ(ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))))
74	73	ex 417	. . . . . . 7 ⊢ (𝑐 ∈ (𝑓‘∅) → (𝑓:ω–1-1-onto→𝐴 → ∃ℎ(ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))))
75	74	exlimiv 1959	. . . . . 6 ⊢ (∃𝑐 𝑐 ∈ (𝑓‘∅) → (𝑓:ω–1-1-onto→𝐴 → ∃ℎ(ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))))
76	47, 75	mpcom 39	. . . . 5 ⊢ (𝑓:ω–1-1-onto→𝐴 → ∃ℎ(ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))))
77		velsn 4604	. . . . . . . . . . 11 ⊢ (𝑧 ∈ {∅} ↔ 𝑧 = ∅)
78	77	necon3bbii 3004	. . . . . . . . . 10 ⊢ (¬ 𝑧 ∈ {∅} ↔ 𝑧 ≠ ∅)
79	2	eleq2i 2854	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝐴 ↔ 𝑧 ∈ (𝑥 ∖ {∅}))
80		eldif 3914	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (𝑥 ∖ {∅}) ↔ (𝑧 ∈ 𝑥 ∧ ¬ 𝑧 ∈ {∅}))
81	79, 80	sylbbr 239	. . . . . . . . . 10 ⊢ ((𝑧 ∈ 𝑥 ∧ ¬ 𝑧 ∈ {∅}) → 𝑧 ∈ 𝐴)
82	78, 81	sylan2br 606	. . . . . . . . 9 ⊢ ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → 𝑧 ∈ 𝐴)
83		simpl 487	. . . . . . . . . . . 12 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑧 ∈ 𝐴) → 𝑓:ω–1-1-onto→𝐴)
84		f1ofo 6828	. . . . . . . . . . . . . 14 ⊢ (𝑓:ω–1-1-onto→𝐴 → 𝑓:ω–onto→𝐴)
85		foelrn 7102	. . . . . . . . . . . . . 14 ⊢ ((𝑓:ω–onto→𝐴 ∧ 𝑧 ∈ 𝐴) → ∃𝑖 ∈ ω 𝑧 = (𝑓‘𝑖))
86	84, 85	sylan 591	. . . . . . . . . . . . 13 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑧 ∈ 𝐴) → ∃𝑖 ∈ ω 𝑧 = (𝑓‘𝑖))
87		suceq 6429	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 = 𝑖 → suc 𝑘 = suc 𝑖)
88	87	fveq2d 6885	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 = 𝑖 → (ℎ‘suc 𝑘) = (ℎ‘suc 𝑖))
89		id 23	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 = 𝑖 → 𝑘 = 𝑖)
90		fveq2 6881	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 = 𝑖 → (ℎ‘𝑘) = (ℎ‘𝑖))
91	89, 90	oveq12d 7430	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 = 𝑖 → (𝑘𝐹(ℎ‘𝑘)) = (𝑖𝐹(ℎ‘𝑖)))
92	88, 91	eleq12d 2856	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 𝑖 → ((ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ↔ (ℎ‘suc 𝑖) ∈ (𝑖𝐹(ℎ‘𝑖))))
93	92	rspcv 3576	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 ∈ ω → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (ℎ‘suc 𝑖) ∈ (𝑖𝐹(ℎ‘𝑖))))
94	93	3ad2ant3 1152	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (ℎ‘suc 𝑖) ∈ (𝑖𝐹(ℎ‘𝑖))))
95	94	imp 411	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))) → (ℎ‘suc 𝑖) ∈ (𝑖𝐹(ℎ‘𝑖)))
96	95	3adant3 1149	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (ℎ‘suc 𝑖) ∈ (𝑖𝐹(ℎ‘𝑖)))
97		eqcom 2769	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 = (𝑓‘𝑖) ↔ (𝑓‘𝑖) = 𝑧)
98		f1ocnvfv 7276	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → ((𝑓‘𝑖) = 𝑧 → (◡𝑓‘𝑧) = 𝑖))
99	97, 98	biimtrid 245	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (𝑧 = (𝑓‘𝑖) → (◡𝑓‘𝑧) = 𝑖))
100	99	3adant1 1147	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (𝑧 = (𝑓‘𝑖) → (◡𝑓‘𝑧) = 𝑖))
101	100	imp 411	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ 𝑧 = (𝑓‘𝑖)) → (◡𝑓‘𝑧) = 𝑖)
102	101	eqcomd 2768	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ 𝑧 = (𝑓‘𝑖)) → 𝑖 = (◡𝑓‘𝑧))
103	102	3adant2 1148	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → 𝑖 = (◡𝑓‘𝑧))
104		suceq 6429	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = (◡𝑓‘𝑧) → suc 𝑖 = suc (◡𝑓‘𝑧))
105	103, 104	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → suc 𝑖 = suc (◡𝑓‘𝑧))
106	105	fveq2d 6885	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (ℎ‘suc 𝑖) = (ℎ‘suc (◡𝑓‘𝑧)))
107		simpr 489	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ℎ:ω⟶∪ 𝐴 ∧ 𝑖 ∈ ω) → 𝑖 ∈ ω)
108		ffvelcdm 7076	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ℎ:ω⟶∪ 𝐴 ∧ 𝑖 ∈ ω) → (ℎ‘𝑖) ∈ ∪ 𝐴)
109		fveq2 6881	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑖 → (𝑓‘𝑛) = (𝑓‘𝑖))
110		eqidd 2763	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = (ℎ‘𝑖) → (𝑓‘𝑖) = (𝑓‘𝑖))
111		fvex 6894	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓‘𝑖) ∈ V
112	109, 110, 62, 111	ovmpo 7572	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑖 ∈ ω ∧ (ℎ‘𝑖) ∈ ∪ 𝐴) → (𝑖𝐹(ℎ‘𝑖)) = (𝑓‘𝑖))
113	107, 108, 112	syl2anc 595	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℎ:ω⟶∪ 𝐴 ∧ 𝑖 ∈ ω) → (𝑖𝐹(ℎ‘𝑖)) = (𝑓‘𝑖))
114	113	3adant2 1148	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (𝑖𝐹(ℎ‘𝑖)) = (𝑓‘𝑖))
115	114	3ad2ant1 1150	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (𝑖𝐹(ℎ‘𝑖)) = (𝑓‘𝑖))
116	96, 106, 115	3eltr3d 2876	. . . . . . . . . . . . . . . . . . 19 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (ℎ‘suc (◡𝑓‘𝑧)) ∈ (𝑓‘𝑖))
117	35	ffvelcdmda 7079	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (𝑓‘𝑖) ∈ 𝐴)
118	117	3adant1 1147	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (𝑓‘𝑖) ∈ 𝐴)
119	118	3ad2ant1 1150	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (𝑓‘𝑖) ∈ 𝐴)
120		eleq1 2850	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = (𝑓‘𝑖) → (𝑧 ∈ 𝐴 ↔ (𝑓‘𝑖) ∈ 𝐴))
121	120	3ad2ant3 1152	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (𝑧 ∈ 𝐴 ↔ (𝑓‘𝑖) ∈ 𝐴))
122	119, 121	mpbird 260	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → 𝑧 ∈ 𝐴)
123		fveq2 6881	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑧 → (◡𝑓‘𝑤) = (◡𝑓‘𝑧))
124		suceq 6429	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((◡𝑓‘𝑤) = (◡𝑓‘𝑧) → suc (◡𝑓‘𝑤) = suc (◡𝑓‘𝑧))
125	123, 124	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = 𝑧 → suc (◡𝑓‘𝑤) = suc (◡𝑓‘𝑧))
126	125	fveq2d 6885	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑧 → (ℎ‘suc (◡𝑓‘𝑤)) = (ℎ‘suc (◡𝑓‘𝑧)))
127		axcclem.3	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐺 = (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤)))
128		fvex 6894	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℎ‘suc (◡𝑓‘𝑧)) ∈ V
129	126, 127, 128	fvmpt 6989	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ 𝐴 → (𝐺‘𝑧) = (ℎ‘suc (◡𝑓‘𝑧)))
130	122, 129	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (𝐺‘𝑧) = (ℎ‘suc (◡𝑓‘𝑧)))
131		simp3 1155	. . . . . . . . . . . . . . . . . . 19 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → 𝑧 = (𝑓‘𝑖))
132	116, 130, 131	3eltr4d 2877	. . . . . . . . . . . . . . . . . 18 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (𝐺‘𝑧) ∈ 𝑧)
133	132	3exp 1136	. . . . . . . . . . . . . . . . 17 ⊢ ((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (𝑧 = (𝑓‘𝑖) → (𝐺‘𝑧) ∈ 𝑧)))
134	133	com3r 88	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝑓‘𝑖) → ((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (𝐺‘𝑧) ∈ 𝑧)))
135	134	3expd 1371	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝑓‘𝑖) → (ℎ:ω⟶∪ 𝐴 → (𝑓:ω–1-1-onto→𝐴 → (𝑖 ∈ ω → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (𝐺‘𝑧) ∈ 𝑧)))))
136	135	com4r 95	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ ω → (𝑧 = (𝑓‘𝑖) → (ℎ:ω⟶∪ 𝐴 → (𝑓:ω–1-1-onto→𝐴 → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (𝐺‘𝑧) ∈ 𝑧)))))
137	136	rexlimiv 3158	. . . . . . . . . . . . 13 ⊢ (∃𝑖 ∈ ω 𝑧 = (𝑓‘𝑖) → (ℎ:ω⟶∪ 𝐴 → (𝑓:ω–1-1-onto→𝐴 → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (𝐺‘𝑧) ∈ 𝑧))))
138	86, 137	syl 18	. . . . . . . . . . . 12 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑧 ∈ 𝐴) → (ℎ:ω⟶∪ 𝐴 → (𝑓:ω–1-1-onto→𝐴 → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (𝐺‘𝑧) ∈ 𝑧))))
139	83, 138	mpid 45	. . . . . . . . . . 11 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑧 ∈ 𝐴) → (ℎ:ω⟶∪ 𝐴 → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (𝐺‘𝑧) ∈ 𝑧)))
140	139	impd 415	. . . . . . . . . 10 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑧 ∈ 𝐴) → ((ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))) → (𝐺‘𝑧) ∈ 𝑧))
141	140	impancom 456	. . . . . . . . 9 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ (ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))) → (𝑧 ∈ 𝐴 → (𝐺‘𝑧) ∈ 𝑧))
142	82, 141	syl5 35	. . . . . . . 8 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ (ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))) → ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → (𝐺‘𝑧) ∈ 𝑧))
143	142	expd 420	. . . . . . 7 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ (ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))) → (𝑧 ∈ 𝑥 → (𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧)))
144	143	ralrimiv 3155	. . . . . 6 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ (ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))) → ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧))
145		fvrn0 6909	. . . . . . . . . . 11 ⊢ (ℎ‘suc (◡𝑓‘𝑤)) ∈ (ran ℎ ∪ {∅})
146	145	rgenw 3082	. . . . . . . . . 10 ⊢ ∀𝑤 ∈ 𝐴 (ℎ‘suc (◡𝑓‘𝑤)) ∈ (ran ℎ ∪ {∅})
147		eqid 2762	. . . . . . . . . . 11 ⊢ (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤))) = (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤)))
148	147	fmpt 7105	. . . . . . . . . 10 ⊢ (∀𝑤 ∈ 𝐴 (ℎ‘suc (◡𝑓‘𝑤)) ∈ (ran ℎ ∪ {∅}) ↔ (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤))):𝐴⟶(ran ℎ ∪ {∅}))
149	146, 148	mpbi 233	. . . . . . . . 9 ⊢ (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤))):𝐴⟶(ran ℎ ∪ {∅})
150		vex 3458	. . . . . . . . . . 11 ⊢ ℎ ∈ V
151	150	rnex 7905	. . . . . . . . . 10 ⊢ ran ℎ ∈ V
152		p0ex 5354	. . . . . . . . . 10 ⊢ {∅} ∈ V
153	151, 152	unex 7744	. . . . . . . . 9 ⊢ (ran ℎ ∪ {∅}) ∈ V
154		fex2 7931	. . . . . . . . 9 ⊢ (((𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤))):𝐴⟶(ran ℎ ∪ {∅}) ∧ 𝐴 ∈ V ∧ (ran ℎ ∪ {∅}) ∈ V) → (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤))) ∈ V)
155	149, 67, 153, 154	mp3an 1489	. . . . . . . 8 ⊢ (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤))) ∈ V
156	127, 155	eqeltri 2858	. . . . . . 7 ⊢ 𝐺 ∈ V
157		fveq1 6880	. . . . . . . . . 10 ⊢ (𝑔 = 𝐺 → (𝑔‘𝑧) = (𝐺‘𝑧))
158	157	eleq1d 2847	. . . . . . . . 9 ⊢ (𝑔 = 𝐺 → ((𝑔‘𝑧) ∈ 𝑧 ↔ (𝐺‘𝑧) ∈ 𝑧))
159	158	imbi2d 343	. . . . . . . 8 ⊢ (𝑔 = 𝐺 → ((𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧) ↔ (𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧)))
160	159	ralbidv 3187	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧) ↔ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧)))
161	156, 160	spcev 3564	. . . . . 6 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧) → ∃𝑔∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧))
162	144, 161	syl 18	. . . . 5 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ (ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))) → ∃𝑔∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧))
163	76, 162	exlimddv 1964	. . . 4 ⊢ (𝑓:ω–1-1-onto→𝐴 → ∃𝑔∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧))
164	163	exlimiv 1959	. . 3 ⊢ (∃𝑓 𝑓:ω–1-1-onto→𝐴 → ∃𝑔∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧))
165	34, 164	sylbi 220	. 2 ⊢ (ω ≈ 𝐴 → ∃𝑔∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧))
166	32, 33, 165	3syl 19	1 ⊢ (𝑥 ≈ ω → ∃𝑔∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1102   = wceq 1569  ∃wex 1808   ∈ wcel 2142   ≠ wne 2957  ∀wral 3078  ∃wrex 3088  Vcvv 3454   ∖ cdif 3901   ∪ cun 3902   ⊆ wss 3904  ∅c0 4285  𝒫 cpw 4561  {csn 4588  ∪ cuni 4871   class class class wbr 5108   ↦ cmpt 5191   × cxp 5658  ^◡ccnv 5659  ran crn 5661  suc csuc 6362  ⟶wf 6532  –onto→wfo 6534  –1-1-onto→wf1o 6535  ‘cfv 6536  (class class class)co 7412   ∈ cmpo 7414  ωcom 7860   ≈ cen 8938   ≼ cdom 8939   ≺ csdm 8940  Fincfn 8941

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5256  ax-nul 5268  ax-pow 5335  ax-pr 5403  ax-un 7734  ax-dc 10436

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1103  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-reu 3369  df-rab 3416  df-v 3456  df-sbc 3744  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-int 4912  df-iun 4957  df-br 5109  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5555  df-eprel 5560  df-po 5568  df-so 5569  df-fr 5613  df-we 5615  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-res 5672  df-ima 5673  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7861  df-1st 7984  df-2nd 7985  df-frecs 8276  df-wrecs 8307  df-recs 8356  df-rdg 8395  df-1o 8451  df-er 8692  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945

This theorem is used by:  axcc  10448