Theorem axcclem 10449

Description: Lemma for axcc 10450. (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 9298	. . . . . . . 8 ⊢ (𝐴 ≺ ω → 𝐴 ∈ Fin)
2		axcclem.1	. . . . . . . . . 10 ⊢ 𝐴 = (𝑥 ∖ {∅})
3	2	eleq1i 2825	. . . . . . . . 9 ⊢ (𝐴 ∈ Fin ↔ (𝑥 ∖ {∅}) ∈ Fin)
4		undif1 4475	. . . . . . . . . . 11 ⊢ ((𝑥 ∖ {∅}) ∪ {∅}) = (𝑥 ∪ {∅})
5		snfi 9041	. . . . . . . . . . . 12 ⊢ {∅} ∈ Fin
6		unfi 9169	. . . . . . . . . . . 12 ⊢ (((𝑥 ∖ {∅}) ∈ Fin ∧ {∅} ∈ Fin) → ((𝑥 ∖ {∅}) ∪ {∅}) ∈ Fin)
7	5, 6	mpan2 690	. . . . . . . . . . 11 ⊢ ((𝑥 ∖ {∅}) ∈ Fin → ((𝑥 ∖ {∅}) ∪ {∅}) ∈ Fin)
8	4, 7	eqeltrrid 2839	. . . . . . . . . 10 ⊢ ((𝑥 ∖ {∅}) ∈ Fin → (𝑥 ∪ {∅}) ∈ Fin)
9		ssun1 4172	. . . . . . . . . 10 ⊢ 𝑥 ⊆ (𝑥 ∪ {∅})
10		ssfi 9170	. . . . . . . . . 10 ⊢ (((𝑥 ∪ {∅}) ∈ Fin ∧ 𝑥 ⊆ (𝑥 ∪ {∅})) → 𝑥 ∈ Fin)
11	8, 9, 10	sylancl 587	. . . . . . . . 9 ⊢ ((𝑥 ∖ {∅}) ∈ Fin → 𝑥 ∈ Fin)
12	3, 11	sylbi 216	. . . . . . . 8 ⊢ (𝐴 ∈ Fin → 𝑥 ∈ Fin)
13		dcomex 10439	. . . . . . . . . 10 ⊢ ω ∈ V
14		isfiniteg 9301	. . . . . . . . . 10 ⊢ (ω ∈ V → (𝑥 ∈ Fin ↔ 𝑥 ≺ ω))
15	13, 14	ax-mp 5	. . . . . . . . 9 ⊢ (𝑥 ∈ Fin ↔ 𝑥 ≺ ω)
16		sdomnen 8974	. . . . . . . . 9 ⊢ (𝑥 ≺ ω → ¬ 𝑥 ≈ ω)
17	15, 16	sylbi 216	. . . . . . . 8 ⊢ (𝑥 ∈ Fin → ¬ 𝑥 ≈ ω)
18	1, 12, 17	3syl 18	. . . . . . 7 ⊢ (𝐴 ≺ ω → ¬ 𝑥 ≈ ω)
19	18	con2i 139	. . . . . 6 ⊢ (𝑥 ≈ ω → ¬ 𝐴 ≺ ω)
20		sdomentr 9108	. . . . . . 7 ⊢ ((𝐴 ≺ 𝑥 ∧ 𝑥 ≈ ω) → 𝐴 ≺ ω)
21	20	expcom 415	. . . . . 6 ⊢ (𝑥 ≈ ω → (𝐴 ≺ 𝑥 → 𝐴 ≺ ω))
22	19, 21	mtod 197	. . . . 5 ⊢ (𝑥 ≈ ω → ¬ 𝐴 ≺ 𝑥)
23		vex 3479	. . . . . 6 ⊢ 𝑥 ∈ V
24		difss 4131	. . . . . . 7 ⊢ (𝑥 ∖ {∅}) ⊆ 𝑥
25	2, 24	eqsstri 4016	. . . . . 6 ⊢ 𝐴 ⊆ 𝑥
26		ssdomg 8993	. . . . . 6 ⊢ (𝑥 ∈ V → (𝐴 ⊆ 𝑥 → 𝐴 ≼ 𝑥))
27	23, 25, 26	mp2 9	. . . . 5 ⊢ 𝐴 ≼ 𝑥
28	22, 27	jctil 521	. . . 4 ⊢ (𝑥 ≈ ω → (𝐴 ≼ 𝑥 ∧ ¬ 𝐴 ≺ 𝑥))
29		bren2 8976	. . . 4 ⊢ (𝐴 ≈ 𝑥 ↔ (𝐴 ≼ 𝑥 ∧ ¬ 𝐴 ≺ 𝑥))
30	28, 29	sylibr 233	. . 3 ⊢ (𝑥 ≈ ω → 𝐴 ≈ 𝑥)
31		entr 8999	. . 3 ⊢ ((𝐴 ≈ 𝑥 ∧ 𝑥 ≈ ω) → 𝐴 ≈ ω)
32	30, 31	mpancom 687	. 2 ⊢ (𝑥 ≈ ω → 𝐴 ≈ ω)
33		ensym 8996	. 2 ⊢ (𝐴 ≈ ω → ω ≈ 𝐴)
34		bren 8946	. . 3 ⊢ (ω ≈ 𝐴 ↔ ∃𝑓 𝑓:ω–1-1-onto→𝐴)
35		f1of 6831	. . . . . . . 8 ⊢ (𝑓:ω–1-1-onto→𝐴 → 𝑓:ω⟶𝐴)
36		peano1 7876	. . . . . . . 8 ⊢ ∅ ∈ ω
37		ffvelcdm 7081	. . . . . . . 8 ⊢ ((𝑓:ω⟶𝐴 ∧ ∅ ∈ ω) → (𝑓‘∅) ∈ 𝐴)
38	35, 36, 37	sylancl 587	. . . . . . 7 ⊢ (𝑓:ω–1-1-onto→𝐴 → (𝑓‘∅) ∈ 𝐴)
39		eldifn 4127	. . . . . . . . 9 ⊢ ((𝑓‘∅) ∈ (𝑥 ∖ {∅}) → ¬ (𝑓‘∅) ∈ {∅})
40	39, 2	eleq2s 2852	. . . . . . . 8 ⊢ ((𝑓‘∅) ∈ 𝐴 → ¬ (𝑓‘∅) ∈ {∅})
41		fvex 6902	. . . . . . . . . . 11 ⊢ (𝑓‘∅) ∈ V
42	41	elsn 4643	. . . . . . . . . 10 ⊢ ((𝑓‘∅) ∈ {∅} ↔ (𝑓‘∅) = ∅)
43	42	notbii 320	. . . . . . . . 9 ⊢ (¬ (𝑓‘∅) ∈ {∅} ↔ ¬ (𝑓‘∅) = ∅)
44		neq0 4345	. . . . . . . . 9 ⊢ (¬ (𝑓‘∅) = ∅ ↔ ∃𝑐 𝑐 ∈ (𝑓‘∅))
45	43, 44	bitr2i 276	. . . . . . . 8 ⊢ (∃𝑐 𝑐 ∈ (𝑓‘∅) ↔ ¬ (𝑓‘∅) ∈ {∅})
46	40, 45	sylibr 233	. . . . . . 7 ⊢ ((𝑓‘∅) ∈ 𝐴 → ∃𝑐 𝑐 ∈ (𝑓‘∅))
47	38, 46	syl 17	. . . . . 6 ⊢ (𝑓:ω–1-1-onto→𝐴 → ∃𝑐 𝑐 ∈ (𝑓‘∅))
48		elunii 4913	. . . . . . . . . . 11 ⊢ ((𝑐 ∈ (𝑓‘∅) ∧ (𝑓‘∅) ∈ 𝐴) → 𝑐 ∈ ∪ 𝐴)
49	38, 48	sylan2 594	. . . . . . . . . 10 ⊢ ((𝑐 ∈ (𝑓‘∅) ∧ 𝑓:ω–1-1-onto→𝐴) → 𝑐 ∈ ∪ 𝐴)
50	35	ffvelcdmda 7084	. . . . . . . . . . . . . 14 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑛 ∈ ω) → (𝑓‘𝑛) ∈ 𝐴)
51		difabs 4293	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∖ {∅}) ∖ {∅}) = (𝑥 ∖ {∅})
52	2	difeq1i 4118	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∖ {∅}) = ((𝑥 ∖ {∅}) ∖ {∅})
53	51, 52, 2	3eqtr4i 2771	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∖ {∅}) = 𝐴
54		pwuni 4949	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐴 ⊆ 𝒫 ∪ 𝐴
55		ssdif 4139	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ⊆ 𝒫 ∪ 𝐴 → (𝐴 ∖ {∅}) ⊆ (𝒫 ∪ 𝐴 ∖ {∅}))
56	54, 55	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∖ {∅}) ⊆ (𝒫 ∪ 𝐴 ∖ {∅})
57	53, 56	eqsstrri 4017	. . . . . . . . . . . . . . . 16 ⊢ 𝐴 ⊆ (𝒫 ∪ 𝐴 ∖ {∅})
58	57	sseli 3978	. . . . . . . . . . . . . . 15 ⊢ ((𝑓‘𝑛) ∈ 𝐴 → (𝑓‘𝑛) ∈ (𝒫 ∪ 𝐴 ∖ {∅}))
59	58	ralrimivw 3151	. . . . . . . . . . . . . 14 ⊢ ((𝑓‘𝑛) ∈ 𝐴 → ∀𝑦 ∈ ∪ 𝐴(𝑓‘𝑛) ∈ (𝒫 ∪ 𝐴 ∖ {∅}))
60	50, 59	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑛 ∈ ω) → ∀𝑦 ∈ ∪ 𝐴(𝑓‘𝑛) ∈ (𝒫 ∪ 𝐴 ∖ {∅}))
61	60	ralrimiva 3147	. . . . . . . . . . . 12 ⊢ (𝑓:ω–1-1-onto→𝐴 → ∀𝑛 ∈ ω ∀𝑦 ∈ ∪ 𝐴(𝑓‘𝑛) ∈ (𝒫 ∪ 𝐴 ∖ {∅}))
62		axcclem.2	. . . . . . . . . . . . 13 ⊢ 𝐹 = (𝑛 ∈ ω, 𝑦 ∈ ∪ 𝐴 ↦ (𝑓‘𝑛))
63	62	fmpo 8051	. . . . . . . . . . . 12 ⊢ (∀𝑛 ∈ ω ∀𝑦 ∈ ∪ 𝐴(𝑓‘𝑛) ∈ (𝒫 ∪ 𝐴 ∖ {∅}) ↔ 𝐹:(ω × ∪ 𝐴)⟶(𝒫 ∪ 𝐴 ∖ {∅}))
64	61, 63	sylib 217	. . . . . . . . . . 11 ⊢ (𝑓:ω–1-1-onto→𝐴 → 𝐹:(ω × ∪ 𝐴)⟶(𝒫 ∪ 𝐴 ∖ {∅}))
65	64	adantl 483	. . . . . . . . . 10 ⊢ ((𝑐 ∈ (𝑓‘∅) ∧ 𝑓:ω–1-1-onto→𝐴) → 𝐹:(ω × ∪ 𝐴)⟶(𝒫 ∪ 𝐴 ∖ {∅}))
66	23	difexi 5328	. . . . . . . . . . . . 13 ⊢ (𝑥 ∖ {∅}) ∈ V
67	2, 66	eqeltri 2830	. . . . . . . . . . . 12 ⊢ 𝐴 ∈ V
68	67	uniex 7728	. . . . . . . . . . 11 ⊢ ∪ 𝐴 ∈ V
69	68	axdc4 10448	. . . . . . . . . 10 ⊢ ((𝑐 ∈ ∪ 𝐴 ∧ 𝐹:(ω × ∪ 𝐴)⟶(𝒫 ∪ 𝐴 ∖ {∅})) → ∃ℎ(ℎ:ω⟶∪ 𝐴 ∧ (ℎ‘∅) = 𝑐 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))))
70	49, 65, 69	syl2anc 585	. . . . . . . . 9 ⊢ ((𝑐 ∈ (𝑓‘∅) ∧ 𝑓:ω–1-1-onto→𝐴) → ∃ℎ(ℎ:ω⟶∪ 𝐴 ∧ (ℎ‘∅) = 𝑐 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))))
71		3simpb 1150	. . . . . . . . . 10 ⊢ ((ℎ:ω⟶∪ 𝐴 ∧ (ℎ‘∅) = 𝑐 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))) → (ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))))
72	71	eximi 1838	. . . . . . . . 9 ⊢ (∃ℎ(ℎ:ω⟶∪ 𝐴 ∧ (ℎ‘∅) = 𝑐 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))) → ∃ℎ(ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))))
73	70, 72	syl 17	. . . . . . . 8 ⊢ ((𝑐 ∈ (𝑓‘∅) ∧ 𝑓:ω–1-1-onto→𝐴) → ∃ℎ(ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))))
74	73	ex 414	. . . . . . 7 ⊢ (𝑐 ∈ (𝑓‘∅) → (𝑓:ω–1-1-onto→𝐴 → ∃ℎ(ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))))
75	74	exlimiv 1934	. . . . . 6 ⊢ (∃𝑐 𝑐 ∈ (𝑓‘∅) → (𝑓:ω–1-1-onto→𝐴 → ∃ℎ(ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))))
76	47, 75	mpcom 38	. . . . 5 ⊢ (𝑓:ω–1-1-onto→𝐴 → ∃ℎ(ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))))
77		velsn 4644	. . . . . . . . . . 11 ⊢ (𝑧 ∈ {∅} ↔ 𝑧 = ∅)
78	77	necon3bbii 2989	. . . . . . . . . 10 ⊢ (¬ 𝑧 ∈ {∅} ↔ 𝑧 ≠ ∅)
79	2	eleq2i 2826	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝐴 ↔ 𝑧 ∈ (𝑥 ∖ {∅}))
80		eldif 3958	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (𝑥 ∖ {∅}) ↔ (𝑧 ∈ 𝑥 ∧ ¬ 𝑧 ∈ {∅}))
81	79, 80	sylbbr 235	. . . . . . . . . 10 ⊢ ((𝑧 ∈ 𝑥 ∧ ¬ 𝑧 ∈ {∅}) → 𝑧 ∈ 𝐴)
82	78, 81	sylan2br 596	. . . . . . . . 9 ⊢ ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → 𝑧 ∈ 𝐴)
83		simpl 484	. . . . . . . . . . . 12 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑧 ∈ 𝐴) → 𝑓:ω–1-1-onto→𝐴)
84		f1ofo 6838	. . . . . . . . . . . . . 14 ⊢ (𝑓:ω–1-1-onto→𝐴 → 𝑓:ω–onto→𝐴)
85		foelrn 7105	. . . . . . . . . . . . . 14 ⊢ ((𝑓:ω–onto→𝐴 ∧ 𝑧 ∈ 𝐴) → ∃𝑖 ∈ ω 𝑧 = (𝑓‘𝑖))
86	84, 85	sylan 581	. . . . . . . . . . . . 13 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑧 ∈ 𝐴) → ∃𝑖 ∈ ω 𝑧 = (𝑓‘𝑖))
87		suceq 6428	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 = 𝑖 → suc 𝑘 = suc 𝑖)
88	87	fveq2d 6893	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 = 𝑖 → (ℎ‘suc 𝑘) = (ℎ‘suc 𝑖))
89		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 = 𝑖 → 𝑘 = 𝑖)
90		fveq2 6889	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 = 𝑖 → (ℎ‘𝑘) = (ℎ‘𝑖))
91	89, 90	oveq12d 7424	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 = 𝑖 → (𝑘𝐹(ℎ‘𝑘)) = (𝑖𝐹(ℎ‘𝑖)))
92	88, 91	eleq12d 2828	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 𝑖 → ((ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ↔ (ℎ‘suc 𝑖) ∈ (𝑖𝐹(ℎ‘𝑖))))
93	92	rspcv 3609	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 ∈ ω → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (ℎ‘suc 𝑖) ∈ (𝑖𝐹(ℎ‘𝑖))))
94	93	3ad2ant3 1136	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (ℎ‘suc 𝑖) ∈ (𝑖𝐹(ℎ‘𝑖))))
95	94	imp 408	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))) → (ℎ‘suc 𝑖) ∈ (𝑖𝐹(ℎ‘𝑖)))
96	95	3adant3 1133	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (ℎ‘suc 𝑖) ∈ (𝑖𝐹(ℎ‘𝑖)))
97		eqcom 2740	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 = (𝑓‘𝑖) ↔ (𝑓‘𝑖) = 𝑧)
98		f1ocnvfv 7273	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → ((𝑓‘𝑖) = 𝑧 → (◡𝑓‘𝑧) = 𝑖))
99	97, 98	biimtrid 241	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (𝑧 = (𝑓‘𝑖) → (◡𝑓‘𝑧) = 𝑖))
100	99	3adant1 1131	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (𝑧 = (𝑓‘𝑖) → (◡𝑓‘𝑧) = 𝑖))
101	100	imp 408	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ 𝑧 = (𝑓‘𝑖)) → (◡𝑓‘𝑧) = 𝑖)
102	101	eqcomd 2739	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ 𝑧 = (𝑓‘𝑖)) → 𝑖 = (◡𝑓‘𝑧))
103	102	3adant2 1132	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → 𝑖 = (◡𝑓‘𝑧))
104		suceq 6428	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = (◡𝑓‘𝑧) → suc 𝑖 = suc (◡𝑓‘𝑧))
105	103, 104	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → suc 𝑖 = suc (◡𝑓‘𝑧))
106	105	fveq2d 6893	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (ℎ‘suc 𝑖) = (ℎ‘suc (◡𝑓‘𝑧)))
107		simpr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ℎ:ω⟶∪ 𝐴 ∧ 𝑖 ∈ ω) → 𝑖 ∈ ω)
108		ffvelcdm 7081	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ℎ:ω⟶∪ 𝐴 ∧ 𝑖 ∈ ω) → (ℎ‘𝑖) ∈ ∪ 𝐴)
109		fveq2 6889	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑖 → (𝑓‘𝑛) = (𝑓‘𝑖))
110		eqidd 2734	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = (ℎ‘𝑖) → (𝑓‘𝑖) = (𝑓‘𝑖))
111		fvex 6902	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓‘𝑖) ∈ V
112	109, 110, 62, 111	ovmpo 7565	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑖 ∈ ω ∧ (ℎ‘𝑖) ∈ ∪ 𝐴) → (𝑖𝐹(ℎ‘𝑖)) = (𝑓‘𝑖))
113	107, 108, 112	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℎ:ω⟶∪ 𝐴 ∧ 𝑖 ∈ ω) → (𝑖𝐹(ℎ‘𝑖)) = (𝑓‘𝑖))
114	113	3adant2 1132	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (𝑖𝐹(ℎ‘𝑖)) = (𝑓‘𝑖))
115	114	3ad2ant1 1134	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (𝑖𝐹(ℎ‘𝑖)) = (𝑓‘𝑖))
116	96, 106, 115	3eltr3d 2848	. . . . . . . . . . . . . . . . . . 19 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (ℎ‘suc (◡𝑓‘𝑧)) ∈ (𝑓‘𝑖))
117	35	ffvelcdmda 7084	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (𝑓‘𝑖) ∈ 𝐴)
118	117	3adant1 1131	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (𝑓‘𝑖) ∈ 𝐴)
119	118	3ad2ant1 1134	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (𝑓‘𝑖) ∈ 𝐴)
120		eleq1 2822	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = (𝑓‘𝑖) → (𝑧 ∈ 𝐴 ↔ (𝑓‘𝑖) ∈ 𝐴))
121	120	3ad2ant3 1136	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (𝑧 ∈ 𝐴 ↔ (𝑓‘𝑖) ∈ 𝐴))
122	119, 121	mpbird 257	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → 𝑧 ∈ 𝐴)
123		fveq2 6889	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑧 → (◡𝑓‘𝑤) = (◡𝑓‘𝑧))
124		suceq 6428	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((◡𝑓‘𝑤) = (◡𝑓‘𝑧) → suc (◡𝑓‘𝑤) = suc (◡𝑓‘𝑧))
125	123, 124	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = 𝑧 → suc (◡𝑓‘𝑤) = suc (◡𝑓‘𝑧))
126	125	fveq2d 6893	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑧 → (ℎ‘suc (◡𝑓‘𝑤)) = (ℎ‘suc (◡𝑓‘𝑧)))
127		axcclem.3	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐺 = (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤)))
128		fvex 6902	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℎ‘suc (◡𝑓‘𝑧)) ∈ V
129	126, 127, 128	fvmpt 6996	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ 𝐴 → (𝐺‘𝑧) = (ℎ‘suc (◡𝑓‘𝑧)))
130	122, 129	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (𝐺‘𝑧) = (ℎ‘suc (◡𝑓‘𝑧)))
131		simp3 1139	. . . . . . . . . . . . . . . . . . 19 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → 𝑧 = (𝑓‘𝑖))
132	116, 130, 131	3eltr4d 2849	. . . . . . . . . . . . . . . . . 18 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (𝐺‘𝑧) ∈ 𝑧)
133	132	3exp 1120	. . . . . . . . . . . . . . . . 17 ⊢ ((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (𝑧 = (𝑓‘𝑖) → (𝐺‘𝑧) ∈ 𝑧)))
134	133	com3r 87	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝑓‘𝑖) → ((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (𝐺‘𝑧) ∈ 𝑧)))
135	134	3expd 1354	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝑓‘𝑖) → (ℎ:ω⟶∪ 𝐴 → (𝑓:ω–1-1-onto→𝐴 → (𝑖 ∈ ω → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (𝐺‘𝑧) ∈ 𝑧)))))
136	135	com4r 94	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ ω → (𝑧 = (𝑓‘𝑖) → (ℎ:ω⟶∪ 𝐴 → (𝑓:ω–1-1-onto→𝐴 → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (𝐺‘𝑧) ∈ 𝑧)))))
137	136	rexlimiv 3149	. . . . . . . . . . . . 13 ⊢ (∃𝑖 ∈ ω 𝑧 = (𝑓‘𝑖) → (ℎ:ω⟶∪ 𝐴 → (𝑓:ω–1-1-onto→𝐴 → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (𝐺‘𝑧) ∈ 𝑧))))
138	86, 137	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑧 ∈ 𝐴) → (ℎ:ω⟶∪ 𝐴 → (𝑓:ω–1-1-onto→𝐴 → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (𝐺‘𝑧) ∈ 𝑧))))
139	83, 138	mpid 44	. . . . . . . . . . 11 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑧 ∈ 𝐴) → (ℎ:ω⟶∪ 𝐴 → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (𝐺‘𝑧) ∈ 𝑧)))
140	139	impd 412	. . . . . . . . . 10 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑧 ∈ 𝐴) → ((ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))) → (𝐺‘𝑧) ∈ 𝑧))
141	140	impancom 453	. . . . . . . . 9 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ (ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))) → (𝑧 ∈ 𝐴 → (𝐺‘𝑧) ∈ 𝑧))
142	82, 141	syl5 34	. . . . . . . 8 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ (ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))) → ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → (𝐺‘𝑧) ∈ 𝑧))
143	142	expd 417	. . . . . . 7 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ (ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))) → (𝑧 ∈ 𝑥 → (𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧)))
144	143	ralrimiv 3146	. . . . . 6 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ (ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))) → ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧))
145		fvrn0 6919	. . . . . . . . . . 11 ⊢ (ℎ‘suc (◡𝑓‘𝑤)) ∈ (ran ℎ ∪ {∅})
146	145	rgenw 3066	. . . . . . . . . 10 ⊢ ∀𝑤 ∈ 𝐴 (ℎ‘suc (◡𝑓‘𝑤)) ∈ (ran ℎ ∪ {∅})
147		eqid 2733	. . . . . . . . . . 11 ⊢ (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤))) = (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤)))
148	147	fmpt 7107	. . . . . . . . . 10 ⊢ (∀𝑤 ∈ 𝐴 (ℎ‘suc (◡𝑓‘𝑤)) ∈ (ran ℎ ∪ {∅}) ↔ (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤))):𝐴⟶(ran ℎ ∪ {∅}))
149	146, 148	mpbi 229	. . . . . . . . 9 ⊢ (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤))):𝐴⟶(ran ℎ ∪ {∅})
150		vex 3479	. . . . . . . . . . 11 ⊢ ℎ ∈ V
151	150	rnex 7900	. . . . . . . . . 10 ⊢ ran ℎ ∈ V
152		p0ex 5382	. . . . . . . . . 10 ⊢ {∅} ∈ V
153	151, 152	unex 7730	. . . . . . . . 9 ⊢ (ran ℎ ∪ {∅}) ∈ V
154		fex2 7921	. . . . . . . . 9 ⊢ (((𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤))):𝐴⟶(ran ℎ ∪ {∅}) ∧ 𝐴 ∈ V ∧ (ran ℎ ∪ {∅}) ∈ V) → (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤))) ∈ V)
155	149, 67, 153, 154	mp3an 1462	. . . . . . . 8 ⊢ (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤))) ∈ V
156	127, 155	eqeltri 2830	. . . . . . 7 ⊢ 𝐺 ∈ V
157		fveq1 6888	. . . . . . . . . 10 ⊢ (𝑔 = 𝐺 → (𝑔‘𝑧) = (𝐺‘𝑧))
158	157	eleq1d 2819	. . . . . . . . 9 ⊢ (𝑔 = 𝐺 → ((𝑔‘𝑧) ∈ 𝑧 ↔ (𝐺‘𝑧) ∈ 𝑧))
159	158	imbi2d 341	. . . . . . . 8 ⊢ (𝑔 = 𝐺 → ((𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧) ↔ (𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧)))
160	159	ralbidv 3178	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧) ↔ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧)))
161	156, 160	spcev 3597	. . . . . 6 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧) → ∃𝑔∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧))
162	144, 161	syl 17	. . . . 5 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ (ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))) → ∃𝑔∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧))
163	76, 162	exlimddv 1939	. . . 4 ⊢ (𝑓:ω–1-1-onto→𝐴 → ∃𝑔∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧))
164	163	exlimiv 1934	. . 3 ⊢ (∃𝑓 𝑓:ω–1-1-onto→𝐴 → ∃𝑔∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧))
165	34, 164	sylbi 216	. 2 ⊢ (ω ≈ 𝐴 → ∃𝑔∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧))
166	32, 33, 165	3syl 18	1 ⊢ (𝑥 ≈ ω → ∃𝑔∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542  ∃wex 1782   ∈ wcel 2107   ≠ wne 2941  ∀wral 3062  ∃wrex 3071  Vcvv 3475   ∖ cdif 3945   ∪ cun 3946   ⊆ wss 3948  ∅c0 4322  𝒫 cpw 4602  {csn 4628  ∪ cuni 4908   class class class wbr 5148   ↦ cmpt 5231   × cxp 5674  ^◡ccnv 5675  ran crn 5677  suc csuc 6364  ⟶wf 6537  –onto→wfo 6539  –1-1-onto→wf1o 6540  ‘cfv 6541  (class class class)co 7406   ∈ cmpo 7408  ωcom 7852   ≈ cen 8933   ≼ cdom 8934   ≺ csdm 8935  Fincfn 8936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-dc 10438

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6298  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-ov 7409  df-oprab 7410  df-mpo 7411  df-om 7853  df-1st 7972  df-2nd 7973  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-1o 8463  df-er 8700  df-en 8937  df-dom 8938  df-sdom 8939  df-fin 8940

This theorem is referenced by:  axcc  10450