Theorem axcclem 10340

Description: Lemma for axcc 10341. (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 9177	. . . . . . . 8 ⊢ (𝐴 ≺ ω → 𝐴 ∈ Fin)
2		axcclem.1	. . . . . . . . . 10 ⊢ 𝐴 = (𝑥 ∖ {∅})
3	2	eleq1i 2820	. . . . . . . . 9 ⊢ (𝐴 ∈ Fin ↔ (𝑥 ∖ {∅}) ∈ Fin)
4		undif1 4424	. . . . . . . . . . 11 ⊢ ((𝑥 ∖ {∅}) ∪ {∅}) = (𝑥 ∪ {∅})
5		snfi 8960	. . . . . . . . . . . 12 ⊢ {∅} ∈ Fin
6		unfi 9075	. . . . . . . . . . . 12 ⊢ (((𝑥 ∖ {∅}) ∈ Fin ∧ {∅} ∈ Fin) → ((𝑥 ∖ {∅}) ∪ {∅}) ∈ Fin)
7	5, 6	mpan2 691	. . . . . . . . . . 11 ⊢ ((𝑥 ∖ {∅}) ∈ Fin → ((𝑥 ∖ {∅}) ∪ {∅}) ∈ Fin)
8	4, 7	eqeltrrid 2834	. . . . . . . . . 10 ⊢ ((𝑥 ∖ {∅}) ∈ Fin → (𝑥 ∪ {∅}) ∈ Fin)
9		ssun1 4126	. . . . . . . . . 10 ⊢ 𝑥 ⊆ (𝑥 ∪ {∅})
10		ssfi 9077	. . . . . . . . . 10 ⊢ (((𝑥 ∪ {∅}) ∈ Fin ∧ 𝑥 ⊆ (𝑥 ∪ {∅})) → 𝑥 ∈ Fin)
11	8, 9, 10	sylancl 586	. . . . . . . . 9 ⊢ ((𝑥 ∖ {∅}) ∈ Fin → 𝑥 ∈ Fin)
12	3, 11	sylbi 217	. . . . . . . 8 ⊢ (𝐴 ∈ Fin → 𝑥 ∈ Fin)
13		dcomex 10330	. . . . . . . . . 10 ⊢ ω ∈ V
14		isfiniteg 9179	. . . . . . . . . 10 ⊢ (ω ∈ V → (𝑥 ∈ Fin ↔ 𝑥 ≺ ω))
15	13, 14	ax-mp 5	. . . . . . . . 9 ⊢ (𝑥 ∈ Fin ↔ 𝑥 ≺ ω)
16		sdomnen 8898	. . . . . . . . 9 ⊢ (𝑥 ≺ ω → ¬ 𝑥 ≈ ω)
17	15, 16	sylbi 217	. . . . . . . 8 ⊢ (𝑥 ∈ Fin → ¬ 𝑥 ≈ ω)
18	1, 12, 17	3syl 18	. . . . . . 7 ⊢ (𝐴 ≺ ω → ¬ 𝑥 ≈ ω)
19	18	con2i 139	. . . . . 6 ⊢ (𝑥 ≈ ω → ¬ 𝐴 ≺ ω)
20		sdomentr 9019	. . . . . . 7 ⊢ ((𝐴 ≺ 𝑥 ∧ 𝑥 ≈ ω) → 𝐴 ≺ ω)
21	20	expcom 413	. . . . . 6 ⊢ (𝑥 ≈ ω → (𝐴 ≺ 𝑥 → 𝐴 ≺ ω))
22	19, 21	mtod 198	. . . . 5 ⊢ (𝑥 ≈ ω → ¬ 𝐴 ≺ 𝑥)
23		vex 3438	. . . . . 6 ⊢ 𝑥 ∈ V
24		difss 4084	. . . . . . 7 ⊢ (𝑥 ∖ {∅}) ⊆ 𝑥
25	2, 24	eqsstri 3979	. . . . . 6 ⊢ 𝐴 ⊆ 𝑥
26		ssdomg 8917	. . . . . 6 ⊢ (𝑥 ∈ V → (𝐴 ⊆ 𝑥 → 𝐴 ≼ 𝑥))
27	23, 25, 26	mp2 9	. . . . 5 ⊢ 𝐴 ≼ 𝑥
28	22, 27	jctil 519	. . . 4 ⊢ (𝑥 ≈ ω → (𝐴 ≼ 𝑥 ∧ ¬ 𝐴 ≺ 𝑥))
29		bren2 8900	. . . 4 ⊢ (𝐴 ≈ 𝑥 ↔ (𝐴 ≼ 𝑥 ∧ ¬ 𝐴 ≺ 𝑥))
30	28, 29	sylibr 234	. . 3 ⊢ (𝑥 ≈ ω → 𝐴 ≈ 𝑥)
31		entr 8923	. . 3 ⊢ ((𝐴 ≈ 𝑥 ∧ 𝑥 ≈ ω) → 𝐴 ≈ ω)
32	30, 31	mpancom 688	. 2 ⊢ (𝑥 ≈ ω → 𝐴 ≈ ω)
33		ensym 8920	. 2 ⊢ (𝐴 ≈ ω → ω ≈ 𝐴)
34		bren 8874	. . 3 ⊢ (ω ≈ 𝐴 ↔ ∃𝑓 𝑓:ω–1-1-onto→𝐴)
35		f1of 6759	. . . . . . . 8 ⊢ (𝑓:ω–1-1-onto→𝐴 → 𝑓:ω⟶𝐴)
36		peano1 7814	. . . . . . . 8 ⊢ ∅ ∈ ω
37		ffvelcdm 7009	. . . . . . . 8 ⊢ ((𝑓:ω⟶𝐴 ∧ ∅ ∈ ω) → (𝑓‘∅) ∈ 𝐴)
38	35, 36, 37	sylancl 586	. . . . . . 7 ⊢ (𝑓:ω–1-1-onto→𝐴 → (𝑓‘∅) ∈ 𝐴)
39		eldifn 4080	. . . . . . . . 9 ⊢ ((𝑓‘∅) ∈ (𝑥 ∖ {∅}) → ¬ (𝑓‘∅) ∈ {∅})
40	39, 2	eleq2s 2847	. . . . . . . 8 ⊢ ((𝑓‘∅) ∈ 𝐴 → ¬ (𝑓‘∅) ∈ {∅})
41		fvex 6830	. . . . . . . . . . 11 ⊢ (𝑓‘∅) ∈ V
42	41	elsn 4589	. . . . . . . . . 10 ⊢ ((𝑓‘∅) ∈ {∅} ↔ (𝑓‘∅) = ∅)
43	42	notbii 320	. . . . . . . . 9 ⊢ (¬ (𝑓‘∅) ∈ {∅} ↔ ¬ (𝑓‘∅) = ∅)
44		neq0 4300	. . . . . . . . 9 ⊢ (¬ (𝑓‘∅) = ∅ ↔ ∃𝑐 𝑐 ∈ (𝑓‘∅))
45	43, 44	bitr2i 276	. . . . . . . 8 ⊢ (∃𝑐 𝑐 ∈ (𝑓‘∅) ↔ ¬ (𝑓‘∅) ∈ {∅})
46	40, 45	sylibr 234	. . . . . . 7 ⊢ ((𝑓‘∅) ∈ 𝐴 → ∃𝑐 𝑐 ∈ (𝑓‘∅))
47	38, 46	syl 17	. . . . . 6 ⊢ (𝑓:ω–1-1-onto→𝐴 → ∃𝑐 𝑐 ∈ (𝑓‘∅))
48		elunii 4862	. . . . . . . . . . 11 ⊢ ((𝑐 ∈ (𝑓‘∅) ∧ (𝑓‘∅) ∈ 𝐴) → 𝑐 ∈ ∪ 𝐴)
49	38, 48	sylan2 593	. . . . . . . . . 10 ⊢ ((𝑐 ∈ (𝑓‘∅) ∧ 𝑓:ω–1-1-onto→𝐴) → 𝑐 ∈ ∪ 𝐴)
50	35	ffvelcdmda 7012	. . . . . . . . . . . . . 14 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑛 ∈ ω) → (𝑓‘𝑛) ∈ 𝐴)
51		difabs 4251	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∖ {∅}) ∖ {∅}) = (𝑥 ∖ {∅})
52	2	difeq1i 4070	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∖ {∅}) = ((𝑥 ∖ {∅}) ∖ {∅})
53	51, 52, 2	3eqtr4i 2763	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∖ {∅}) = 𝐴
54		pwuni 4894	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐴 ⊆ 𝒫 ∪ 𝐴
55		ssdif 4092	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ⊆ 𝒫 ∪ 𝐴 → (𝐴 ∖ {∅}) ⊆ (𝒫 ∪ 𝐴 ∖ {∅}))
56	54, 55	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∖ {∅}) ⊆ (𝒫 ∪ 𝐴 ∖ {∅})
57	53, 56	eqsstrri 3980	. . . . . . . . . . . . . . . 16 ⊢ 𝐴 ⊆ (𝒫 ∪ 𝐴 ∖ {∅})
58	57	sseli 3928	. . . . . . . . . . . . . . 15 ⊢ ((𝑓‘𝑛) ∈ 𝐴 → (𝑓‘𝑛) ∈ (𝒫 ∪ 𝐴 ∖ {∅}))
59	58	ralrimivw 3126	. . . . . . . . . . . . . 14 ⊢ ((𝑓‘𝑛) ∈ 𝐴 → ∀𝑦 ∈ ∪ 𝐴(𝑓‘𝑛) ∈ (𝒫 ∪ 𝐴 ∖ {∅}))
60	50, 59	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑛 ∈ ω) → ∀𝑦 ∈ ∪ 𝐴(𝑓‘𝑛) ∈ (𝒫 ∪ 𝐴 ∖ {∅}))
61	60	ralrimiva 3122	. . . . . . . . . . . 12 ⊢ (𝑓:ω–1-1-onto→𝐴 → ∀𝑛 ∈ ω ∀𝑦 ∈ ∪ 𝐴(𝑓‘𝑛) ∈ (𝒫 ∪ 𝐴 ∖ {∅}))
62		axcclem.2	. . . . . . . . . . . . 13 ⊢ 𝐹 = (𝑛 ∈ ω, 𝑦 ∈ ∪ 𝐴 ↦ (𝑓‘𝑛))
63	62	fmpo 7995	. . . . . . . . . . . 12 ⊢ (∀𝑛 ∈ ω ∀𝑦 ∈ ∪ 𝐴(𝑓‘𝑛) ∈ (𝒫 ∪ 𝐴 ∖ {∅}) ↔ 𝐹:(ω × ∪ 𝐴)⟶(𝒫 ∪ 𝐴 ∖ {∅}))
64	61, 63	sylib 218	. . . . . . . . . . 11 ⊢ (𝑓:ω–1-1-onto→𝐴 → 𝐹:(ω × ∪ 𝐴)⟶(𝒫 ∪ 𝐴 ∖ {∅}))
65	64	adantl 481	. . . . . . . . . 10 ⊢ ((𝑐 ∈ (𝑓‘∅) ∧ 𝑓:ω–1-1-onto→𝐴) → 𝐹:(ω × ∪ 𝐴)⟶(𝒫 ∪ 𝐴 ∖ {∅}))
66	23	difexi 5266	. . . . . . . . . . . . 13 ⊢ (𝑥 ∖ {∅}) ∈ V
67	2, 66	eqeltri 2825	. . . . . . . . . . . 12 ⊢ 𝐴 ∈ V
68	67	uniex 7669	. . . . . . . . . . 11 ⊢ ∪ 𝐴 ∈ V
69	68	axdc4 10339	. . . . . . . . . 10 ⊢ ((𝑐 ∈ ∪ 𝐴 ∧ 𝐹:(ω × ∪ 𝐴)⟶(𝒫 ∪ 𝐴 ∖ {∅})) → ∃ℎ(ℎ:ω⟶∪ 𝐴 ∧ (ℎ‘∅) = 𝑐 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))))
70	49, 65, 69	syl2anc 584	. . . . . . . . 9 ⊢ ((𝑐 ∈ (𝑓‘∅) ∧ 𝑓:ω–1-1-onto→𝐴) → ∃ℎ(ℎ:ω⟶∪ 𝐴 ∧ (ℎ‘∅) = 𝑐 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))))
71		3simpb 1149	. . . . . . . . . 10 ⊢ ((ℎ:ω⟶∪ 𝐴 ∧ (ℎ‘∅) = 𝑐 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))) → (ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))))
72	71	eximi 1836	. . . . . . . . 9 ⊢ (∃ℎ(ℎ:ω⟶∪ 𝐴 ∧ (ℎ‘∅) = 𝑐 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))) → ∃ℎ(ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))))
73	70, 72	syl 17	. . . . . . . 8 ⊢ ((𝑐 ∈ (𝑓‘∅) ∧ 𝑓:ω–1-1-onto→𝐴) → ∃ℎ(ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))))
74	73	ex 412	. . . . . . 7 ⊢ (𝑐 ∈ (𝑓‘∅) → (𝑓:ω–1-1-onto→𝐴 → ∃ℎ(ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))))
75	74	exlimiv 1931	. . . . . 6 ⊢ (∃𝑐 𝑐 ∈ (𝑓‘∅) → (𝑓:ω–1-1-onto→𝐴 → ∃ℎ(ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))))
76	47, 75	mpcom 38	. . . . 5 ⊢ (𝑓:ω–1-1-onto→𝐴 → ∃ℎ(ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))))
77		velsn 4590	. . . . . . . . . . 11 ⊢ (𝑧 ∈ {∅} ↔ 𝑧 = ∅)
78	77	necon3bbii 2973	. . . . . . . . . 10 ⊢ (¬ 𝑧 ∈ {∅} ↔ 𝑧 ≠ ∅)
79	2	eleq2i 2821	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝐴 ↔ 𝑧 ∈ (𝑥 ∖ {∅}))
80		eldif 3910	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (𝑥 ∖ {∅}) ↔ (𝑧 ∈ 𝑥 ∧ ¬ 𝑧 ∈ {∅}))
81	79, 80	sylbbr 236	. . . . . . . . . 10 ⊢ ((𝑧 ∈ 𝑥 ∧ ¬ 𝑧 ∈ {∅}) → 𝑧 ∈ 𝐴)
82	78, 81	sylan2br 595	. . . . . . . . 9 ⊢ ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → 𝑧 ∈ 𝐴)
83		simpl 482	. . . . . . . . . . . 12 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑧 ∈ 𝐴) → 𝑓:ω–1-1-onto→𝐴)
84		f1ofo 6766	. . . . . . . . . . . . . 14 ⊢ (𝑓:ω–1-1-onto→𝐴 → 𝑓:ω–onto→𝐴)
85		foelrn 7035	. . . . . . . . . . . . . 14 ⊢ ((𝑓:ω–onto→𝐴 ∧ 𝑧 ∈ 𝐴) → ∃𝑖 ∈ ω 𝑧 = (𝑓‘𝑖))
86	84, 85	sylan 580	. . . . . . . . . . . . 13 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑧 ∈ 𝐴) → ∃𝑖 ∈ ω 𝑧 = (𝑓‘𝑖))
87		suceq 6370	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 = 𝑖 → suc 𝑘 = suc 𝑖)
88	87	fveq2d 6821	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 = 𝑖 → (ℎ‘suc 𝑘) = (ℎ‘suc 𝑖))
89		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 = 𝑖 → 𝑘 = 𝑖)
90		fveq2 6817	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 = 𝑖 → (ℎ‘𝑘) = (ℎ‘𝑖))
91	89, 90	oveq12d 7359	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 = 𝑖 → (𝑘𝐹(ℎ‘𝑘)) = (𝑖𝐹(ℎ‘𝑖)))
92	88, 91	eleq12d 2823	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 𝑖 → ((ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ↔ (ℎ‘suc 𝑖) ∈ (𝑖𝐹(ℎ‘𝑖))))
93	92	rspcv 3571	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 ∈ ω → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (ℎ‘suc 𝑖) ∈ (𝑖𝐹(ℎ‘𝑖))))
94	93	3ad2ant3 1135	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (ℎ‘suc 𝑖) ∈ (𝑖𝐹(ℎ‘𝑖))))
95	94	imp 406	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))) → (ℎ‘suc 𝑖) ∈ (𝑖𝐹(ℎ‘𝑖)))
96	95	3adant3 1132	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (ℎ‘suc 𝑖) ∈ (𝑖𝐹(ℎ‘𝑖)))
97		eqcom 2737	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 = (𝑓‘𝑖) ↔ (𝑓‘𝑖) = 𝑧)
98		f1ocnvfv 7207	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → ((𝑓‘𝑖) = 𝑧 → (◡𝑓‘𝑧) = 𝑖))
99	97, 98	biimtrid 242	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (𝑧 = (𝑓‘𝑖) → (◡𝑓‘𝑧) = 𝑖))
100	99	3adant1 1130	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (𝑧 = (𝑓‘𝑖) → (◡𝑓‘𝑧) = 𝑖))
101	100	imp 406	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ 𝑧 = (𝑓‘𝑖)) → (◡𝑓‘𝑧) = 𝑖)
102	101	eqcomd 2736	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ 𝑧 = (𝑓‘𝑖)) → 𝑖 = (◡𝑓‘𝑧))
103	102	3adant2 1131	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → 𝑖 = (◡𝑓‘𝑧))
104		suceq 6370	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = (◡𝑓‘𝑧) → suc 𝑖 = suc (◡𝑓‘𝑧))
105	103, 104	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → suc 𝑖 = suc (◡𝑓‘𝑧))
106	105	fveq2d 6821	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (ℎ‘suc 𝑖) = (ℎ‘suc (◡𝑓‘𝑧)))
107		simpr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ℎ:ω⟶∪ 𝐴 ∧ 𝑖 ∈ ω) → 𝑖 ∈ ω)
108		ffvelcdm 7009	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ℎ:ω⟶∪ 𝐴 ∧ 𝑖 ∈ ω) → (ℎ‘𝑖) ∈ ∪ 𝐴)
109		fveq2 6817	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑖 → (𝑓‘𝑛) = (𝑓‘𝑖))
110		eqidd 2731	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = (ℎ‘𝑖) → (𝑓‘𝑖) = (𝑓‘𝑖))
111		fvex 6830	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓‘𝑖) ∈ V
112	109, 110, 62, 111	ovmpo 7501	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑖 ∈ ω ∧ (ℎ‘𝑖) ∈ ∪ 𝐴) → (𝑖𝐹(ℎ‘𝑖)) = (𝑓‘𝑖))
113	107, 108, 112	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℎ:ω⟶∪ 𝐴 ∧ 𝑖 ∈ ω) → (𝑖𝐹(ℎ‘𝑖)) = (𝑓‘𝑖))
114	113	3adant2 1131	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (𝑖𝐹(ℎ‘𝑖)) = (𝑓‘𝑖))
115	114	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (𝑖𝐹(ℎ‘𝑖)) = (𝑓‘𝑖))
116	96, 106, 115	3eltr3d 2843	. . . . . . . . . . . . . . . . . . 19 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (ℎ‘suc (◡𝑓‘𝑧)) ∈ (𝑓‘𝑖))
117	35	ffvelcdmda 7012	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (𝑓‘𝑖) ∈ 𝐴)
118	117	3adant1 1130	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (𝑓‘𝑖) ∈ 𝐴)
119	118	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (𝑓‘𝑖) ∈ 𝐴)
120		eleq1 2817	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = (𝑓‘𝑖) → (𝑧 ∈ 𝐴 ↔ (𝑓‘𝑖) ∈ 𝐴))
121	120	3ad2ant3 1135	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (𝑧 ∈ 𝐴 ↔ (𝑓‘𝑖) ∈ 𝐴))
122	119, 121	mpbird 257	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → 𝑧 ∈ 𝐴)
123		fveq2 6817	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑧 → (◡𝑓‘𝑤) = (◡𝑓‘𝑧))
124		suceq 6370	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((◡𝑓‘𝑤) = (◡𝑓‘𝑧) → suc (◡𝑓‘𝑤) = suc (◡𝑓‘𝑧))
125	123, 124	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = 𝑧 → suc (◡𝑓‘𝑤) = suc (◡𝑓‘𝑧))
126	125	fveq2d 6821	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑧 → (ℎ‘suc (◡𝑓‘𝑤)) = (ℎ‘suc (◡𝑓‘𝑧)))
127		axcclem.3	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐺 = (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤)))
128		fvex 6830	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℎ‘suc (◡𝑓‘𝑧)) ∈ V
129	126, 127, 128	fvmpt 6924	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ 𝐴 → (𝐺‘𝑧) = (ℎ‘suc (◡𝑓‘𝑧)))
130	122, 129	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (𝐺‘𝑧) = (ℎ‘suc (◡𝑓‘𝑧)))
131		simp3 1138	. . . . . . . . . . . . . . . . . . 19 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → 𝑧 = (𝑓‘𝑖))
132	116, 130, 131	3eltr4d 2844	. . . . . . . . . . . . . . . . . 18 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (𝐺‘𝑧) ∈ 𝑧)
133	132	3exp 1119	. . . . . . . . . . . . . . . . 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 3124	. . . . . . . . . . . . 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 410	. . . . . . . . . 10 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑧 ∈ 𝐴) → ((ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))) → (𝐺‘𝑧) ∈ 𝑧))
141	140	impancom 451	. . . . . . . . 9 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ (ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))) → (𝑧 ∈ 𝐴 → (𝐺‘𝑧) ∈ 𝑧))
142	82, 141	syl5 34	. . . . . . . 8 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ (ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))) → ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → (𝐺‘𝑧) ∈ 𝑧))
143	142	expd 415	. . . . . . 7 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ (ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))) → (𝑧 ∈ 𝑥 → (𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧)))
144	143	ralrimiv 3121	. . . . . 6 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ (ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))) → ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧))
145		fvrn0 6845	. . . . . . . . . . 11 ⊢ (ℎ‘suc (◡𝑓‘𝑤)) ∈ (ran ℎ ∪ {∅})
146	145	rgenw 3049	. . . . . . . . . 10 ⊢ ∀𝑤 ∈ 𝐴 (ℎ‘suc (◡𝑓‘𝑤)) ∈ (ran ℎ ∪ {∅})
147		eqid 2730	. . . . . . . . . . 11 ⊢ (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤))) = (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤)))
148	147	fmpt 7038	. . . . . . . . . 10 ⊢ (∀𝑤 ∈ 𝐴 (ℎ‘suc (◡𝑓‘𝑤)) ∈ (ran ℎ ∪ {∅}) ↔ (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤))):𝐴⟶(ran ℎ ∪ {∅}))
149	146, 148	mpbi 230	. . . . . . . . 9 ⊢ (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤))):𝐴⟶(ran ℎ ∪ {∅})
150		vex 3438	. . . . . . . . . . 11 ⊢ ℎ ∈ V
151	150	rnex 7835	. . . . . . . . . 10 ⊢ ran ℎ ∈ V
152		p0ex 5320	. . . . . . . . . 10 ⊢ {∅} ∈ V
153	151, 152	unex 7672	. . . . . . . . 9 ⊢ (ran ℎ ∪ {∅}) ∈ V
154		fex2 7861	. . . . . . . . 9 ⊢ (((𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤))):𝐴⟶(ran ℎ ∪ {∅}) ∧ 𝐴 ∈ V ∧ (ran ℎ ∪ {∅}) ∈ V) → (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤))) ∈ V)
155	149, 67, 153, 154	mp3an 1463	. . . . . . . 8 ⊢ (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤))) ∈ V
156	127, 155	eqeltri 2825	. . . . . . 7 ⊢ 𝐺 ∈ V
157		fveq1 6816	. . . . . . . . . 10 ⊢ (𝑔 = 𝐺 → (𝑔‘𝑧) = (𝐺‘𝑧))
158	157	eleq1d 2814	. . . . . . . . 9 ⊢ (𝑔 = 𝐺 → ((𝑔‘𝑧) ∈ 𝑧 ↔ (𝐺‘𝑧) ∈ 𝑧))
159	158	imbi2d 340	. . . . . . . 8 ⊢ (𝑔 = 𝐺 → ((𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧) ↔ (𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧)))
160	159	ralbidv 3153	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧) ↔ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧)))
161	156, 160	spcev 3559	. . . . . 6 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧) → ∃𝑔∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧))
162	144, 161	syl 17	. . . . 5 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ (ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))) → ∃𝑔∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧))
163	76, 162	exlimddv 1936	. . . 4 ⊢ (𝑓:ω–1-1-onto→𝐴 → ∃𝑔∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧))
164	163	exlimiv 1931	. . 3 ⊢ (∃𝑓 𝑓:ω–1-1-onto→𝐴 → ∃𝑔∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧))
165	34, 164	sylbi 217	. 2 ⊢ (ω ≈ 𝐴 → ∃𝑔∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧))
166	32, 33, 165	3syl 18	1 ⊢ (𝑥 ≈ ω → ∃𝑔∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1541  ∃wex 1780   ∈ wcel 2110   ≠ wne 2926  ∀wral 3045  ∃wrex 3054  Vcvv 3434   ∖ cdif 3897   ∪ cun 3898   ⊆ wss 3900  ∅c0 4281  𝒫 cpw 4548  {csn 4574  ∪ cuni 4857   class class class wbr 5089   ↦ cmpt 5170   × cxp 5612  ^◡ccnv 5613  ran crn 5615  suc csuc 6304  ⟶wf 6473  –onto→wfo 6475  –1-1-onto→wf1o 6476  ‘cfv 6477  (class class class)co 7341   ∈ cmpo 7343  ωcom 7791   ≈ cen 8861   ≼ cdom 8862   ≺ csdm 8863  Fincfn 8864

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-10 2143  ax-11 2159  ax-12 2179  ax-ext 2702  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7663  ax-dc 10329

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-reu 3345  df-rab 3394  df-v 3436  df-sbc 3740  df-csb 3849  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-pss 3920  df-nul 4282  df-if 4474  df-pw 4550  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4858  df-int 4896  df-iun 4941  df-br 5090  df-opab 5152  df-mpt 5171  df-tr 5197  df-id 5509  df-eprel 5514  df-po 5522  df-so 5523  df-fr 5567  df-we 5569  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-pred 6244  df-ord 6305  df-on 6306  df-lim 6307  df-suc 6308  df-iota 6433  df-fun 6479  df-fn 6480  df-f 6481  df-f1 6482  df-fo 6483  df-f1o 6484  df-fv 6485  df-ov 7344  df-oprab 7345  df-mpo 7346  df-om 7792  df-1st 7916  df-2nd 7917  df-frecs 8206  df-wrecs 8237  df-recs 8286  df-rdg 8324  df-1o 8380  df-er 8617  df-en 8865  df-dom 8866  df-sdom 8867  df-fin 8868

This theorem is referenced by:  axcc  10341