Theorem axcclem 10462

Description: Lemma for axcc 10463. (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 9271	. . . . . . . 8 ⊢ (𝐴 ≺ ω → 𝐴 ∈ Fin)
2		axcclem.1	. . . . . . . . . 10 ⊢ 𝐴 = (𝑥 ∖ {∅})
3	2	eleq1i 2853	. . . . . . . . 9 ⊢ (𝐴 ∈ Fin ↔ (𝑥 ∖ {∅}) ∈ Fin)
4		undif1 4433	. . . . . . . . . . 11 ⊢ ((𝑥 ∖ {∅}) ∪ {∅}) = (𝑥 ∪ {∅})
5		snfi 9053	. . . . . . . . . . . 12 ⊢ {∅} ∈ Fin
6		unfi 9168	. . . . . . . . . . . 12 ⊢ (((𝑥 ∖ {∅}) ∈ Fin ∧ {∅} ∈ Fin) → ((𝑥 ∖ {∅}) ∪ {∅}) ∈ Fin)
7	5, 6	mpan2 704	. . . . . . . . . . 11 ⊢ ((𝑥 ∖ {∅}) ∈ Fin → ((𝑥 ∖ {∅}) ∪ {∅}) ∈ Fin)
8	4, 7	eqeltrrid 2867	. . . . . . . . . 10 ⊢ ((𝑥 ∖ {∅}) ∈ Fin → (𝑥 ∪ {∅}) ∈ Fin)
9		ssun1 4127	. . . . . . . . . 10 ⊢ 𝑥 ⊆ (𝑥 ∪ {∅})
10		ssfi 9170	. . . . . . . . . 10 ⊢ (((𝑥 ∪ {∅}) ∈ Fin ∧ 𝑥 ⊆ (𝑥 ∪ {∅})) → 𝑥 ∈ Fin)
11	8, 9, 10	sylancl 598	. . . . . . . . 9 ⊢ ((𝑥 ∖ {∅}) ∈ Fin → 𝑥 ∈ Fin)
12	3, 11	sylbi 220	. . . . . . . 8 ⊢ (𝐴 ∈ Fin → 𝑥 ∈ Fin)
13		dcomex 10452	. . . . . . . . . 10 ⊢ ω ∈ V
14		isfiniteg 9273	. . . . . . . . . 10 ⊢ (ω ∈ V → (𝑥 ∈ Fin ↔ 𝑥 ≺ ω))
15	13, 14	ax-mp 5	. . . . . . . . 9 ⊢ (𝑥 ∈ Fin ↔ 𝑥 ≺ ω)
16		sdomnen 8990	. . . . . . . . 9 ⊢ (𝑥 ≺ ω → ¬ 𝑥 ≈ ω)
17	15, 16	sylbi 220	. . . . . . . 8 ⊢ (𝑥 ∈ Fin → ¬ 𝑥 ≈ ω)
18	1, 12, 17	3syl 19	. . . . . . 7 ⊢ (𝐴 ≺ ω → ¬ 𝑥 ≈ ω)
19	18	con2i 140	. . . . . 6 ⊢ (𝑥 ≈ ω → ¬ 𝐴 ≺ ω)
20		sdomentr 9112	. . . . . . 7 ⊢ ((𝐴 ≺ 𝑥 ∧ 𝑥 ≈ ω) → 𝐴 ≺ ω)
21	20	expcom 419	. . . . . 6 ⊢ (𝑥 ≈ ω → (𝐴 ≺ 𝑥 → 𝐴 ≺ ω))
22	19, 21	mtod 201	. . . . 5 ⊢ (𝑥 ≈ ω → ¬ 𝐴 ≺ 𝑥)
23		vex 3457	. . . . . 6 ⊢ 𝑥 ∈ V
24		difss 4086	. . . . . . 7 ⊢ (𝑥 ∖ {∅}) ⊆ 𝑥
25	2, 24	eqsstri 3980	. . . . . 6 ⊢ 𝐴 ⊆ 𝑥
26		ssdomg 9009	. . . . . 6 ⊢ (𝑥 ∈ V → (𝐴 ⊆ 𝑥 → 𝐴 ≼ 𝑥))
27	23, 25, 26	mp2 9	. . . . 5 ⊢ 𝐴 ≼ 𝑥
28	22, 27	jctil 529	. . . 4 ⊢ (𝑥 ≈ ω → (𝐴 ≼ 𝑥 ∧ ¬ 𝐴 ≺ 𝑥))
29		bren2 8992	. . . 4 ⊢ (𝐴 ≈ 𝑥 ↔ (𝐴 ≼ 𝑥 ∧ ¬ 𝐴 ≺ 𝑥))
30	28, 29	sylibr 237	. . 3 ⊢ (𝑥 ≈ ω → 𝐴 ≈ 𝑥)
31		entr 9015	. . 3 ⊢ ((𝐴 ≈ 𝑥 ∧ 𝑥 ≈ ω) → 𝐴 ≈ ω)
32	30, 31	mpancom 701	. 2 ⊢ (𝑥 ≈ ω → 𝐴 ≈ ω)
33		ensym 9012	. 2 ⊢ (𝐴 ≈ ω → ω ≈ 𝐴)
34		bren 8965	. . 3 ⊢ (ω ≈ 𝐴 ↔ ∃𝑓 𝑓:ω–1-1-onto→𝐴)
35		f1of 6821	. . . . . . . 8 ⊢ (𝑓:ω–1-1-onto→𝐴 → 𝑓:ω⟶𝐴)
36		peano1 7888	. . . . . . . 8 ⊢ ∅ ∈ ω
37		ffvelcdm 7077	. . . . . . . 8 ⊢ ((𝑓:ω⟶𝐴 ∧ ∅ ∈ ω) → (𝑓‘∅) ∈ 𝐴)
38	35, 36, 37	sylancl 598	. . . . . . 7 ⊢ (𝑓:ω–1-1-onto→𝐴 → (𝑓‘∅) ∈ 𝐴)
39		eldifn 4082	. . . . . . . . 9 ⊢ ((𝑓‘∅) ∈ (𝑥 ∖ {∅}) → ¬ (𝑓‘∅) ∈ {∅})
40	39, 2	eleq2s 2880	. . . . . . . 8 ⊢ ((𝑓‘∅) ∈ 𝐴 → ¬ (𝑓‘∅) ∈ {∅})
41		fvex 6895	. . . . . . . . . . 11 ⊢ (𝑓‘∅) ∈ V
42	41	elsn 4602	. . . . . . . . . 10 ⊢ ((𝑓‘∅) ∈ {∅} ↔ (𝑓‘∅) = ∅)
43	42	notbii 323	. . . . . . . . 9 ⊢ (¬ (𝑓‘∅) ∈ {∅} ↔ ¬ (𝑓‘∅) = ∅)
44		neq0 4302	. . . . . . . . 9 ⊢ (¬ (𝑓‘∅) = ∅ ↔ ∃𝑐 𝑐 ∈ (𝑓‘∅))
45	43, 44	bitr2i 279	. . . . . . . 8 ⊢ (∃𝑐 𝑐 ∈ (𝑓‘∅) ↔ ¬ (𝑓‘∅) ∈ {∅})
46	40, 45	sylibr 237	. . . . . . 7 ⊢ ((𝑓‘∅) ∈ 𝐴 → ∃𝑐 𝑐 ∈ (𝑓‘∅))
47	38, 46	syl 18	. . . . . 6 ⊢ (𝑓:ω–1-1-onto→𝐴 → ∃𝑐 𝑐 ∈ (𝑓‘∅))
48		elunii 4875	. . . . . . . . . . 11 ⊢ ((𝑐 ∈ (𝑓‘∅) ∧ (𝑓‘∅) ∈ 𝐴) → 𝑐 ∈ ∪ 𝐴)
49	38, 48	sylan2 605	. . . . . . . . . 10 ⊢ ((𝑐 ∈ (𝑓‘∅) ∧ 𝑓:ω–1-1-onto→𝐴) → 𝑐 ∈ ∪ 𝐴)
50	35	ffvelcdmda 7080	. . . . . . . . . . . . . 14 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑛 ∈ ω) → (𝑓‘𝑛) ∈ 𝐴)
51		difabs 4252	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∖ {∅}) ∖ {∅}) = (𝑥 ∖ {∅})
52	2	difeq1i 4073	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∖ {∅}) = ((𝑥 ∖ {∅}) ∖ {∅})
53	51, 52, 2	3eqtr4i 2795	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∖ {∅}) = 𝐴
54		pwuni 4909	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐴 ⊆ 𝒫 ∪ 𝐴
55		ssdif 4094	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ⊆ 𝒫 ∪ 𝐴 → (𝐴 ∖ {∅}) ⊆ (𝒫 ∪ 𝐴 ∖ {∅}))
56	54, 55	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∖ {∅}) ⊆ (𝒫 ∪ 𝐴 ∖ {∅})
57	53, 56	eqsstrri 3981	. . . . . . . . . . . . . . . 16 ⊢ 𝐴 ⊆ (𝒫 ∪ 𝐴 ∖ {∅})
58	57	sseli 3930	. . . . . . . . . . . . . . 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 8068	. . . . . . . . . . . 12 ⊢ (∀𝑛 ∈ ω ∀𝑦 ∈ ∪ 𝐴(𝑓‘𝑛) ∈ (𝒫 ∪ 𝐴 ∖ {∅}) ↔ 𝐹:(ω × ∪ 𝐴)⟶(𝒫 ∪ 𝐴 ∖ {∅}))
64	61, 63	sylib 221	. . . . . . . . . . 11 ⊢ (𝑓:ω–1-1-onto→𝐴 → 𝐹:(ω × ∪ 𝐴)⟶(𝒫 ∪ 𝐴 ∖ {∅}))
65	64	adantl 487	. . . . . . . . . 10 ⊢ ((𝑐 ∈ (𝑓‘∅) ∧ 𝑓:ω–1-1-onto→𝐴) → 𝐹:(ω × ∪ 𝐴)⟶(𝒫 ∪ 𝐴 ∖ {∅}))
66	23	difexi 5299	. . . . . . . . . . . . 13 ⊢ (𝑥 ∖ {∅}) ∈ V
67	2, 66	eqeltri 2858	. . . . . . . . . . . 12 ⊢ 𝐴 ∈ V
68	67	uniex 7746	. . . . . . . . . . 11 ⊢ ∪ 𝐴 ∈ V
69	68	axdc4 10461	. . . . . . . . . 10 ⊢ ((𝑐 ∈ ∪ 𝐴 ∧ 𝐹:(ω × ∪ 𝐴)⟶(𝒫 ∪ 𝐴 ∖ {∅})) → ∃ℎ(ℎ:ω⟶∪ 𝐴 ∧ (ℎ‘∅) = 𝑐 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))))
70	49, 65, 69	syl2anc 596	. . . . . . . . 9 ⊢ ((𝑐 ∈ (𝑓‘∅) ∧ 𝑓:ω–1-1-onto→𝐴) → ∃ℎ(ℎ:ω⟶∪ 𝐴 ∧ (ℎ‘∅) = 𝑐 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))))
71		3simpb 1167	. . . . . . . . . 10 ⊢ ((ℎ:ω⟶∪ 𝐴 ∧ (ℎ‘∅) = 𝑐 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))) → (ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))))
72	71	eximi 1868	. . . . . . . . 9 ⊢ (∃ℎ(ℎ:ω⟶∪ 𝐴 ∧ (ℎ‘∅) = 𝑐 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))) → ∃ℎ(ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))))
73	70, 72	syl 18	. . . . . . . 8 ⊢ ((𝑐 ∈ (𝑓‘∅) ∧ 𝑓:ω–1-1-onto→𝐴) → ∃ℎ(ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))))
74	73	ex 418	. . . . . . 7 ⊢ (𝑐 ∈ (𝑓‘∅) → (𝑓:ω–1-1-onto→𝐴 → ∃ℎ(ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))))
75	74	exlimiv 1963	. . . . . 6 ⊢ (∃𝑐 𝑐 ∈ (𝑓‘∅) → (𝑓:ω–1-1-onto→𝐴 → ∃ℎ(ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))))
76	47, 75	mpcom 39	. . . . 5 ⊢ (𝑓:ω–1-1-onto→𝐴 → ∃ℎ(ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))))
77		velsn 4603	. . . . . . . . . . 11 ⊢ (𝑧 ∈ {∅} ↔ 𝑧 = ∅)
78	77	necon3bbii 3004	. . . . . . . . . 10 ⊢ (¬ 𝑧 ∈ {∅} ↔ 𝑧 ≠ ∅)
79	2	eleq2i 2854	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝐴 ↔ 𝑧 ∈ (𝑥 ∖ {∅}))
80		eldif 3912	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (𝑥 ∖ {∅}) ↔ (𝑧 ∈ 𝑥 ∧ ¬ 𝑧 ∈ {∅}))
81	79, 80	sylbbr 239	. . . . . . . . . 10 ⊢ ((𝑧 ∈ 𝑥 ∧ ¬ 𝑧 ∈ {∅}) → 𝑧 ∈ 𝐴)
82	78, 81	sylan2br 607	. . . . . . . . 9 ⊢ ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → 𝑧 ∈ 𝐴)
83		simpl 488	. . . . . . . . . . . 12 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑧 ∈ 𝐴) → 𝑓:ω–1-1-onto→𝐴)
84		f1ofo 6829	. . . . . . . . . . . . . 14 ⊢ (𝑓:ω–1-1-onto→𝐴 → 𝑓:ω–onto→𝐴)
85		foelrn 7103	. . . . . . . . . . . . . 14 ⊢ ((𝑓:ω–onto→𝐴 ∧ 𝑧 ∈ 𝐴) → ∃𝑖 ∈ ω 𝑧 = (𝑓‘𝑖))
86	84, 85	sylan 592	. . . . . . . . . . . . 13 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑧 ∈ 𝐴) → ∃𝑖 ∈ ω 𝑧 = (𝑓‘𝑖))
87		suceq 6430	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 = 𝑖 → suc 𝑘 = suc 𝑖)
88	87	fveq2d 6886	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 = 𝑖 → (ℎ‘suc 𝑘) = (ℎ‘suc 𝑖))
89		id 23	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 = 𝑖 → 𝑘 = 𝑖)
90		fveq2 6882	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 = 𝑖 → (ℎ‘𝑘) = (ℎ‘𝑖))
91	89, 90	oveq12d 7434	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 = 𝑖 → (𝑘𝐹(ℎ‘𝑘)) = (𝑖𝐹(ℎ‘𝑖)))
92	88, 91	eleq12d 2856	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 𝑖 → ((ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ↔ (ℎ‘suc 𝑖) ∈ (𝑖𝐹(ℎ‘𝑖))))
93	92	rspcv 3575	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 ∈ ω → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (ℎ‘suc 𝑖) ∈ (𝑖𝐹(ℎ‘𝑖))))
94	93	3ad2ant3 1153	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (ℎ‘suc 𝑖) ∈ (𝑖𝐹(ℎ‘𝑖))))
95	94	imp 412	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))) → (ℎ‘suc 𝑖) ∈ (𝑖𝐹(ℎ‘𝑖)))
96	95	3adant3 1150	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (ℎ‘suc 𝑖) ∈ (𝑖𝐹(ℎ‘𝑖)))
97		eqcom 2769	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 = (𝑓‘𝑖) ↔ (𝑓‘𝑖) = 𝑧)
98		f1ocnvfv 7282	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → ((𝑓‘𝑖) = 𝑧 → (◡𝑓‘𝑧) = 𝑖))
99	97, 98	biimtrid 245	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (𝑧 = (𝑓‘𝑖) → (◡𝑓‘𝑧) = 𝑖))
100	99	3adant1 1148	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (𝑧 = (𝑓‘𝑖) → (◡𝑓‘𝑧) = 𝑖))
101	100	imp 412	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ 𝑧 = (𝑓‘𝑖)) → (◡𝑓‘𝑧) = 𝑖)
102	101	eqcomd 2768	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ 𝑧 = (𝑓‘𝑖)) → 𝑖 = (◡𝑓‘𝑧))
103	102	3adant2 1149	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → 𝑖 = (◡𝑓‘𝑧))
104		suceq 6430	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = (◡𝑓‘𝑧) → suc 𝑖 = suc (◡𝑓‘𝑧))
105	103, 104	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → suc 𝑖 = suc (◡𝑓‘𝑧))
106	105	fveq2d 6886	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (ℎ‘suc 𝑖) = (ℎ‘suc (◡𝑓‘𝑧)))
107		simpr 490	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ℎ:ω⟶∪ 𝐴 ∧ 𝑖 ∈ ω) → 𝑖 ∈ ω)
108		ffvelcdm 7077	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ℎ:ω⟶∪ 𝐴 ∧ 𝑖 ∈ ω) → (ℎ‘𝑖) ∈ ∪ 𝐴)
109		fveq2 6882	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑖 → (𝑓‘𝑛) = (𝑓‘𝑖))
110		eqidd 2763	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = (ℎ‘𝑖) → (𝑓‘𝑖) = (𝑓‘𝑖))
111		fvex 6895	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓‘𝑖) ∈ V
112	109, 110, 62, 111	ovmpo 7576	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑖 ∈ ω ∧ (ℎ‘𝑖) ∈ ∪ 𝐴) → (𝑖𝐹(ℎ‘𝑖)) = (𝑓‘𝑖))
113	107, 108, 112	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℎ:ω⟶∪ 𝐴 ∧ 𝑖 ∈ ω) → (𝑖𝐹(ℎ‘𝑖)) = (𝑓‘𝑖))
114	113	3adant2 1149	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (𝑖𝐹(ℎ‘𝑖)) = (𝑓‘𝑖))
115	114	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (𝑖𝐹(ℎ‘𝑖)) = (𝑓‘𝑖))
116	96, 106, 115	3eltr3d 2876	. . . . . . . . . . . . . . . . . . 19 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (ℎ‘suc (◡𝑓‘𝑧)) ∈ (𝑓‘𝑖))
117	35	ffvelcdmda 7080	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (𝑓‘𝑖) ∈ 𝐴)
118	117	3adant1 1148	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (𝑓‘𝑖) ∈ 𝐴)
119	118	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (𝑓‘𝑖) ∈ 𝐴)
120		eleq1 2850	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = (𝑓‘𝑖) → (𝑧 ∈ 𝐴 ↔ (𝑓‘𝑖) ∈ 𝐴))
121	120	3ad2ant3 1153	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (𝑧 ∈ 𝐴 ↔ (𝑓‘𝑖) ∈ 𝐴))
122	119, 121	mpbird 260	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → 𝑧 ∈ 𝐴)
123		fveq2 6882	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑧 → (◡𝑓‘𝑤) = (◡𝑓‘𝑧))
124		suceq 6430	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((◡𝑓‘𝑤) = (◡𝑓‘𝑧) → suc (◡𝑓‘𝑤) = suc (◡𝑓‘𝑧))
125	123, 124	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = 𝑧 → suc (◡𝑓‘𝑤) = suc (◡𝑓‘𝑧))
126	125	fveq2d 6886	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑧 → (ℎ‘suc (◡𝑓‘𝑤)) = (ℎ‘suc (◡𝑓‘𝑧)))
127		axcclem.3	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐺 = (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤)))
128		fvex 6895	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℎ‘suc (◡𝑓‘𝑧)) ∈ V
129	126, 127, 128	fvmpt 6990	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ 𝐴 → (𝐺‘𝑧) = (ℎ‘suc (◡𝑓‘𝑧)))
130	122, 129	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (𝐺‘𝑧) = (ℎ‘suc (◡𝑓‘𝑧)))
131		simp3 1156	. . . . . . . . . . . . . . . . . . 19 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → 𝑧 = (𝑓‘𝑖))
132	116, 130, 131	3eltr4d 2877	. . . . . . . . . . . . . . . . . 18 ⊢ (((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) ∧ 𝑧 = (𝑓‘𝑖)) → (𝐺‘𝑧) ∈ 𝑧)
133	132	3exp 1137	. . . . . . . . . . . . . . . . 17 ⊢ ((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (𝑧 = (𝑓‘𝑖) → (𝐺‘𝑧) ∈ 𝑧)))
134	133	com3r 88	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝑓‘𝑖) → ((ℎ:ω⟶∪ 𝐴 ∧ 𝑓:ω–1-1-onto→𝐴 ∧ 𝑖 ∈ ω) → (∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)) → (𝐺‘𝑧) ∈ 𝑧)))
135	134	3expd 1372	. . . . . . . . . . . . . . 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 416	. . . . . . . . . 10 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ 𝑧 ∈ 𝐴) → ((ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘))) → (𝐺‘𝑧) ∈ 𝑧))
141	140	impancom 457	. . . . . . . . 9 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ (ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))) → (𝑧 ∈ 𝐴 → (𝐺‘𝑧) ∈ 𝑧))
142	82, 141	syl5 35	. . . . . . . 8 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ (ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))) → ((𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅) → (𝐺‘𝑧) ∈ 𝑧))
143	142	expd 421	. . . . . . 7 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ (ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))) → (𝑧 ∈ 𝑥 → (𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧)))
144	143	ralrimiv 3155	. . . . . 6 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ (ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))) → ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧))
145		fvrn0 6910	. . . . . . . . . . 11 ⊢ (ℎ‘suc (◡𝑓‘𝑤)) ∈ (ran ℎ ∪ {∅})
146	145	rgenw 3082	. . . . . . . . . 10 ⊢ ∀𝑤 ∈ 𝐴 (ℎ‘suc (◡𝑓‘𝑤)) ∈ (ran ℎ ∪ {∅})
147		eqid 2762	. . . . . . . . . . 11 ⊢ (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤))) = (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤)))
148	147	fmpt 7106	. . . . . . . . . 10 ⊢ (∀𝑤 ∈ 𝐴 (ℎ‘suc (◡𝑓‘𝑤)) ∈ (ran ℎ ∪ {∅}) ↔ (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤))):𝐴⟶(ran ℎ ∪ {∅}))
149	146, 148	mpbi 233	. . . . . . . . 9 ⊢ (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤))):𝐴⟶(ran ℎ ∪ {∅})
150		vex 3457	. . . . . . . . . . 11 ⊢ ℎ ∈ V
151	150	rnex 7910	. . . . . . . . . 10 ⊢ ran ℎ ∈ V
152		p0ex 5353	. . . . . . . . . 10 ⊢ {∅} ∈ V
153	151, 152	unex 7749	. . . . . . . . 9 ⊢ (ran ℎ ∪ {∅}) ∈ V
154		fex2 7936	. . . . . . . . 9 ⊢ (((𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤))):𝐴⟶(ran ℎ ∪ {∅}) ∧ 𝐴 ∈ V ∧ (ran ℎ ∪ {∅}) ∈ V) → (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤))) ∈ V)
155	149, 67, 153, 154	mp3an 1490	. . . . . . . 8 ⊢ (𝑤 ∈ 𝐴 ↦ (ℎ‘suc (◡𝑓‘𝑤))) ∈ V
156	127, 155	eqeltri 2858	. . . . . . 7 ⊢ 𝐺 ∈ V
157		fveq1 6881	. . . . . . . . . 10 ⊢ (𝑔 = 𝐺 → (𝑔‘𝑧) = (𝐺‘𝑧))
158	157	eleq1d 2847	. . . . . . . . 9 ⊢ (𝑔 = 𝐺 → ((𝑔‘𝑧) ∈ 𝑧 ↔ (𝐺‘𝑧) ∈ 𝑧))
159	158	imbi2d 343	. . . . . . . 8 ⊢ (𝑔 = 𝐺 → ((𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧) ↔ (𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧)))
160	159	ralbidv 3187	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧) ↔ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧)))
161	156, 160	spcev 3563	. . . . . 6 ⊢ (∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧) → ∃𝑔∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧))
162	144, 161	syl 18	. . . . 5 ⊢ ((𝑓:ω–1-1-onto→𝐴 ∧ (ℎ:ω⟶∪ 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘suc 𝑘) ∈ (𝑘𝐹(ℎ‘𝑘)))) → ∃𝑔∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧))
163	76, 162	exlimddv 1968	. . . 4 ⊢ (𝑓:ω–1-1-onto→𝐴 → ∃𝑔∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑔‘𝑧) ∈ 𝑧))
164	163	exlimiv 1963	. . 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 401   ∧ w3a 1103   = wceq 1570  ∃wex 1812   ∈ wcel 2145   ≠ wne 2957  ∀wral 3078  ∃wrex 3088  Vcvv 3453   ∖ cdif 3899   ∪ cun 3900   ⊆ wss 3902  ∅c0 4282  𝒫 cpw 4560  {csn 4587  ∪ cuni 4870   class class class wbr 5107   ↦ cmpt 5190   × cxp 5657  ^◡ccnv 5658  ran crn 5660  suc csuc 6363  ⟶wf 6533  –onto→wfo 6535  –1-1-onto→wf1o 6536  ‘cfv 6537  (class class class)co 7416   ∈ cmpo 7418  ωcom 7865   ≈ cen 8952   ≼ cdom 8953   ≺ csdm 8954  Fincfn 8955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7739  ax-dc 10451

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  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 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-int 4911  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7419  df-oprab 7420  df-mpo 7421  df-om 7866  df-1st 7989  df-2nd 7990  df-frecs 8283  df-wrecs 8314  df-recs 8363  df-rdg 8402  df-1o 8458  df-er 8699  df-en 8956  df-dom 8957  df-sdom 8958  df-fin 8959

This theorem is used by:  axcc  10463