MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  axcclem Structured version   Visualization version   GIF version

Theorem axcclem 9882
Description: Lemma for axcc 9883. (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.
StepHypRef Expression
1 isfinite2 8779 . . . . . . . 8 (𝐴 ≺ ω → 𝐴 ∈ Fin)
2 axcclem.1 . . . . . . . . . 10 𝐴 = (𝑥 ∖ {∅})
32eleq1i 2906 . . . . . . . . 9 (𝐴 ∈ Fin ↔ (𝑥 ∖ {∅}) ∈ Fin)
4 undif1 4427 . . . . . . . . . . 11 ((𝑥 ∖ {∅}) ∪ {∅}) = (𝑥 ∪ {∅})
5 snfi 8597 . . . . . . . . . . . 12 {∅} ∈ Fin
6 unfi 8788 . . . . . . . . . . . 12 (((𝑥 ∖ {∅}) ∈ Fin ∧ {∅} ∈ Fin) → ((𝑥 ∖ {∅}) ∪ {∅}) ∈ Fin)
75, 6mpan2 689 . . . . . . . . . . 11 ((𝑥 ∖ {∅}) ∈ Fin → ((𝑥 ∖ {∅}) ∪ {∅}) ∈ Fin)
84, 7eqeltrrid 2921 . . . . . . . . . 10 ((𝑥 ∖ {∅}) ∈ Fin → (𝑥 ∪ {∅}) ∈ Fin)
9 ssun1 4151 . . . . . . . . . 10 𝑥 ⊆ (𝑥 ∪ {∅})
10 ssfi 8741 . . . . . . . . . 10 (((𝑥 ∪ {∅}) ∈ Fin ∧ 𝑥 ⊆ (𝑥 ∪ {∅})) → 𝑥 ∈ Fin)
118, 9, 10sylancl 588 . . . . . . . . 9 ((𝑥 ∖ {∅}) ∈ Fin → 𝑥 ∈ Fin)
123, 11sylbi 219 . . . . . . . 8 (𝐴 ∈ Fin → 𝑥 ∈ Fin)
13 dcomex 9872 . . . . . . . . . 10 ω ∈ V
14 isfiniteg 8781 . . . . . . . . . 10 (ω ∈ V → (𝑥 ∈ Fin ↔ 𝑥 ≺ ω))
1513, 14ax-mp 5 . . . . . . . . 9 (𝑥 ∈ Fin ↔ 𝑥 ≺ ω)
16 sdomnen 8541 . . . . . . . . 9 (𝑥 ≺ ω → ¬ 𝑥 ≈ ω)
1715, 16sylbi 219 . . . . . . . 8 (𝑥 ∈ Fin → ¬ 𝑥 ≈ ω)
181, 12, 173syl 18 . . . . . . 7 (𝐴 ≺ ω → ¬ 𝑥 ≈ ω)
1918con2i 141 . . . . . 6 (𝑥 ≈ ω → ¬ 𝐴 ≺ ω)
20 sdomentr 8654 . . . . . . 7 ((𝐴𝑥𝑥 ≈ ω) → 𝐴 ≺ ω)
2120expcom 416 . . . . . 6 (𝑥 ≈ ω → (𝐴𝑥𝐴 ≺ ω))
2219, 21mtod 200 . . . . 5 (𝑥 ≈ ω → ¬ 𝐴𝑥)
23 vex 3500 . . . . . 6 𝑥 ∈ V
24 difss 4111 . . . . . . 7 (𝑥 ∖ {∅}) ⊆ 𝑥
252, 24eqsstri 4004 . . . . . 6 𝐴𝑥
26 ssdomg 8558 . . . . . 6 (𝑥 ∈ V → (𝐴𝑥𝐴𝑥))
2723, 25, 26mp2 9 . . . . 5 𝐴𝑥
2822, 27jctil 522 . . . 4 (𝑥 ≈ ω → (𝐴𝑥 ∧ ¬ 𝐴𝑥))
29 bren2 8543 . . . 4 (𝐴𝑥 ↔ (𝐴𝑥 ∧ ¬ 𝐴𝑥))
3028, 29sylibr 236 . . 3 (𝑥 ≈ ω → 𝐴𝑥)
31 entr 8564 . . 3 ((𝐴𝑥𝑥 ≈ ω) → 𝐴 ≈ ω)
3230, 31mpancom 686 . 2 (𝑥 ≈ ω → 𝐴 ≈ ω)
33 ensym 8561 . 2 (𝐴 ≈ ω → ω ≈ 𝐴)
34 bren 8521 . . 3 (ω ≈ 𝐴 ↔ ∃𝑓 𝑓:ω–1-1-onto𝐴)
35 f1of 6618 . . . . . . . 8 (𝑓:ω–1-1-onto𝐴𝑓:ω⟶𝐴)
36 peano1 7604 . . . . . . . 8 ∅ ∈ ω
37 ffvelrn 6852 . . . . . . . 8 ((𝑓:ω⟶𝐴 ∧ ∅ ∈ ω) → (𝑓‘∅) ∈ 𝐴)
3835, 36, 37sylancl 588 . . . . . . 7 (𝑓:ω–1-1-onto𝐴 → (𝑓‘∅) ∈ 𝐴)
39 eldifn 4107 . . . . . . . . 9 ((𝑓‘∅) ∈ (𝑥 ∖ {∅}) → ¬ (𝑓‘∅) ∈ {∅})
4039, 2eleq2s 2934 . . . . . . . 8 ((𝑓‘∅) ∈ 𝐴 → ¬ (𝑓‘∅) ∈ {∅})
41 fvex 6686 . . . . . . . . . . 11 (𝑓‘∅) ∈ V
4241elsn 4585 . . . . . . . . . 10 ((𝑓‘∅) ∈ {∅} ↔ (𝑓‘∅) = ∅)
4342notbii 322 . . . . . . . . 9 (¬ (𝑓‘∅) ∈ {∅} ↔ ¬ (𝑓‘∅) = ∅)
44 neq0 4312 . . . . . . . . 9 (¬ (𝑓‘∅) = ∅ ↔ ∃𝑐 𝑐 ∈ (𝑓‘∅))
4543, 44bitr2i 278 . . . . . . . 8 (∃𝑐 𝑐 ∈ (𝑓‘∅) ↔ ¬ (𝑓‘∅) ∈ {∅})
4640, 45sylibr 236 . . . . . . 7 ((𝑓‘∅) ∈ 𝐴 → ∃𝑐 𝑐 ∈ (𝑓‘∅))
4738, 46syl 17 . . . . . 6 (𝑓:ω–1-1-onto𝐴 → ∃𝑐 𝑐 ∈ (𝑓‘∅))
48 elunii 4846 . . . . . . . . . . 11 ((𝑐 ∈ (𝑓‘∅) ∧ (𝑓‘∅) ∈ 𝐴) → 𝑐 𝐴)
4938, 48sylan2 594 . . . . . . . . . 10 ((𝑐 ∈ (𝑓‘∅) ∧ 𝑓:ω–1-1-onto𝐴) → 𝑐 𝐴)
5035ffvelrnda 6854 . . . . . . . . . . . . . 14 ((𝑓:ω–1-1-onto𝐴𝑛 ∈ ω) → (𝑓𝑛) ∈ 𝐴)
51 difabs 4271 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∖ {∅}) ∖ {∅}) = (𝑥 ∖ {∅})
522difeq1i 4098 . . . . . . . . . . . . . . . . . 18 (𝐴 ∖ {∅}) = ((𝑥 ∖ {∅}) ∖ {∅})
5351, 52, 23eqtr4i 2857 . . . . . . . . . . . . . . . . 17 (𝐴 ∖ {∅}) = 𝐴
54 pwuni 4878 . . . . . . . . . . . . . . . . . 18 𝐴 ⊆ 𝒫 𝐴
55 ssdif 4119 . . . . . . . . . . . . . . . . . 18 (𝐴 ⊆ 𝒫 𝐴 → (𝐴 ∖ {∅}) ⊆ (𝒫 𝐴 ∖ {∅}))
5654, 55ax-mp 5 . . . . . . . . . . . . . . . . 17 (𝐴 ∖ {∅}) ⊆ (𝒫 𝐴 ∖ {∅})
5753, 56eqsstrri 4005 . . . . . . . . . . . . . . . 16 𝐴 ⊆ (𝒫 𝐴 ∖ {∅})
5857sseli 3966 . . . . . . . . . . . . . . 15 ((𝑓𝑛) ∈ 𝐴 → (𝑓𝑛) ∈ (𝒫 𝐴 ∖ {∅}))
5958ralrimivw 3186 . . . . . . . . . . . . . 14 ((𝑓𝑛) ∈ 𝐴 → ∀𝑦 𝐴(𝑓𝑛) ∈ (𝒫 𝐴 ∖ {∅}))
6050, 59syl 17 . . . . . . . . . . . . 13 ((𝑓:ω–1-1-onto𝐴𝑛 ∈ ω) → ∀𝑦 𝐴(𝑓𝑛) ∈ (𝒫 𝐴 ∖ {∅}))
6160ralrimiva 3185 . . . . . . . . . . . 12 (𝑓:ω–1-1-onto𝐴 → ∀𝑛 ∈ ω ∀𝑦 𝐴(𝑓𝑛) ∈ (𝒫 𝐴 ∖ {∅}))
62 axcclem.2 . . . . . . . . . . . . 13 𝐹 = (𝑛 ∈ ω, 𝑦 𝐴 ↦ (𝑓𝑛))
6362fmpo 7769 . . . . . . . . . . . 12 (∀𝑛 ∈ ω ∀𝑦 𝐴(𝑓𝑛) ∈ (𝒫 𝐴 ∖ {∅}) ↔ 𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}))
6461, 63sylib 220 . . . . . . . . . . 11 (𝑓:ω–1-1-onto𝐴𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}))
6564adantl 484 . . . . . . . . . 10 ((𝑐 ∈ (𝑓‘∅) ∧ 𝑓:ω–1-1-onto𝐴) → 𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}))
6623difexi 5235 . . . . . . . . . . . . 13 (𝑥 ∖ {∅}) ∈ V
672, 66eqeltri 2912 . . . . . . . . . . . 12 𝐴 ∈ V
6867uniex 7470 . . . . . . . . . . 11 𝐴 ∈ V
6968axdc4 9881 . . . . . . . . . 10 ((𝑐 𝐴𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅})) → ∃(:ω⟶ 𝐴 ∧ (‘∅) = 𝑐 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘))))
7049, 65, 69syl2anc 586 . . . . . . . . 9 ((𝑐 ∈ (𝑓‘∅) ∧ 𝑓:ω–1-1-onto𝐴) → ∃(:ω⟶ 𝐴 ∧ (‘∅) = 𝑐 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘))))
71 3simpb 1145 . . . . . . . . . 10 ((:ω⟶ 𝐴 ∧ (‘∅) = 𝑐 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘))) → (:ω⟶ 𝐴 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘))))
7271eximi 1834 . . . . . . . . 9 (∃(:ω⟶ 𝐴 ∧ (‘∅) = 𝑐 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘))) → ∃(:ω⟶ 𝐴 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘))))
7370, 72syl 17 . . . . . . . 8 ((𝑐 ∈ (𝑓‘∅) ∧ 𝑓:ω–1-1-onto𝐴) → ∃(:ω⟶ 𝐴 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘))))
7473ex 415 . . . . . . 7 (𝑐 ∈ (𝑓‘∅) → (𝑓:ω–1-1-onto𝐴 → ∃(:ω⟶ 𝐴 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)))))
7574exlimiv 1930 . . . . . 6 (∃𝑐 𝑐 ∈ (𝑓‘∅) → (𝑓:ω–1-1-onto𝐴 → ∃(:ω⟶ 𝐴 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)))))
7647, 75mpcom 38 . . . . 5 (𝑓:ω–1-1-onto𝐴 → ∃(:ω⟶ 𝐴 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘))))
77 velsn 4586 . . . . . . . . . . 11 (𝑧 ∈ {∅} ↔ 𝑧 = ∅)
7877necon3bbii 3066 . . . . . . . . . 10 𝑧 ∈ {∅} ↔ 𝑧 ≠ ∅)
792eleq2i 2907 . . . . . . . . . . 11 (𝑧𝐴𝑧 ∈ (𝑥 ∖ {∅}))
80 eldif 3949 . . . . . . . . . . 11 (𝑧 ∈ (𝑥 ∖ {∅}) ↔ (𝑧𝑥 ∧ ¬ 𝑧 ∈ {∅}))
8179, 80sylbbr 238 . . . . . . . . . 10 ((𝑧𝑥 ∧ ¬ 𝑧 ∈ {∅}) → 𝑧𝐴)
8278, 81sylan2br 596 . . . . . . . . 9 ((𝑧𝑥𝑧 ≠ ∅) → 𝑧𝐴)
83 simpl 485 . . . . . . . . . . . 12 ((𝑓:ω–1-1-onto𝐴𝑧𝐴) → 𝑓:ω–1-1-onto𝐴)
84 f1ofo 6625 . . . . . . . . . . . . . 14 (𝑓:ω–1-1-onto𝐴𝑓:ω–onto𝐴)
85 foelrn 6875 . . . . . . . . . . . . . 14 ((𝑓:ω–onto𝐴𝑧𝐴) → ∃𝑖 ∈ ω 𝑧 = (𝑓𝑖))
8684, 85sylan 582 . . . . . . . . . . . . 13 ((𝑓:ω–1-1-onto𝐴𝑧𝐴) → ∃𝑖 ∈ ω 𝑧 = (𝑓𝑖))
87 suceq 6259 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑘 = 𝑖 → suc 𝑘 = suc 𝑖)
8887fveq2d 6677 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 = 𝑖 → (‘suc 𝑘) = (‘suc 𝑖))
89 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑘 = 𝑖𝑘 = 𝑖)
90 fveq2 6673 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑘 = 𝑖 → (𝑘) = (𝑖))
9189, 90oveq12d 7177 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 = 𝑖 → (𝑘𝐹(𝑘)) = (𝑖𝐹(𝑖)))
9288, 91eleq12d 2910 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝑖 → ((‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ↔ (‘suc 𝑖) ∈ (𝑖𝐹(𝑖))))
9392rspcv 3621 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ ω → (∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) → (‘suc 𝑖) ∈ (𝑖𝐹(𝑖))))
94933ad2ant3 1131 . . . . . . . . . . . . . . . . . . . . . 22 ((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) → (∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) → (‘suc 𝑖) ∈ (𝑖𝐹(𝑖))))
9594imp 409 . . . . . . . . . . . . . . . . . . . . 21 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘))) → (‘suc 𝑖) ∈ (𝑖𝐹(𝑖)))
96953adant3 1128 . . . . . . . . . . . . . . . . . . . 20 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ∧ 𝑧 = (𝑓𝑖)) → (‘suc 𝑖) ∈ (𝑖𝐹(𝑖)))
97 eqcom 2831 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 = (𝑓𝑖) ↔ (𝑓𝑖) = 𝑧)
98 f1ocnvfv 7038 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) → ((𝑓𝑖) = 𝑧 → (𝑓𝑧) = 𝑖))
9997, 98syl5bi 244 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) → (𝑧 = (𝑓𝑖) → (𝑓𝑧) = 𝑖))
100993adant1 1126 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) → (𝑧 = (𝑓𝑖) → (𝑓𝑧) = 𝑖))
101100imp 409 . . . . . . . . . . . . . . . . . . . . . . . 24 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ 𝑧 = (𝑓𝑖)) → (𝑓𝑧) = 𝑖)
102101eqcomd 2830 . . . . . . . . . . . . . . . . . . . . . . 23 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ 𝑧 = (𝑓𝑖)) → 𝑖 = (𝑓𝑧))
1031023adant2 1127 . . . . . . . . . . . . . . . . . . . . . 22 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ∧ 𝑧 = (𝑓𝑖)) → 𝑖 = (𝑓𝑧))
104 suceq 6259 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = (𝑓𝑧) → suc 𝑖 = suc (𝑓𝑧))
105103, 104syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ∧ 𝑧 = (𝑓𝑖)) → suc 𝑖 = suc (𝑓𝑧))
106105fveq2d 6677 . . . . . . . . . . . . . . . . . . . 20 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ∧ 𝑧 = (𝑓𝑖)) → (‘suc 𝑖) = (‘suc (𝑓𝑧)))
107 simpr 487 . . . . . . . . . . . . . . . . . . . . . . 23 ((:ω⟶ 𝐴𝑖 ∈ ω) → 𝑖 ∈ ω)
108 ffvelrn 6852 . . . . . . . . . . . . . . . . . . . . . . 23 ((:ω⟶ 𝐴𝑖 ∈ ω) → (𝑖) ∈ 𝐴)
109 fveq2 6673 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑖 → (𝑓𝑛) = (𝑓𝑖))
110 eqidd 2825 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = (𝑖) → (𝑓𝑖) = (𝑓𝑖))
111 fvex 6686 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓𝑖) ∈ V
112109, 110, 62, 111ovmpo 7313 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑖 ∈ ω ∧ (𝑖) ∈ 𝐴) → (𝑖𝐹(𝑖)) = (𝑓𝑖))
113107, 108, 112syl2anc 586 . . . . . . . . . . . . . . . . . . . . . 22 ((:ω⟶ 𝐴𝑖 ∈ ω) → (𝑖𝐹(𝑖)) = (𝑓𝑖))
1141133adant2 1127 . . . . . . . . . . . . . . . . . . . . 21 ((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) → (𝑖𝐹(𝑖)) = (𝑓𝑖))
1151143ad2ant1 1129 . . . . . . . . . . . . . . . . . . . 20 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ∧ 𝑧 = (𝑓𝑖)) → (𝑖𝐹(𝑖)) = (𝑓𝑖))
11696, 106, 1153eltr3d 2930 . . . . . . . . . . . . . . . . . . 19 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ∧ 𝑧 = (𝑓𝑖)) → (‘suc (𝑓𝑧)) ∈ (𝑓𝑖))
11735ffvelrnda 6854 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) → (𝑓𝑖) ∈ 𝐴)
1181173adant1 1126 . . . . . . . . . . . . . . . . . . . . . 22 ((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) → (𝑓𝑖) ∈ 𝐴)
1191183ad2ant1 1129 . . . . . . . . . . . . . . . . . . . . 21 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ∧ 𝑧 = (𝑓𝑖)) → (𝑓𝑖) ∈ 𝐴)
120 eleq1 2903 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = (𝑓𝑖) → (𝑧𝐴 ↔ (𝑓𝑖) ∈ 𝐴))
1211203ad2ant3 1131 . . . . . . . . . . . . . . . . . . . . 21 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ∧ 𝑧 = (𝑓𝑖)) → (𝑧𝐴 ↔ (𝑓𝑖) ∈ 𝐴))
122119, 121mpbird 259 . . . . . . . . . . . . . . . . . . . 20 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ∧ 𝑧 = (𝑓𝑖)) → 𝑧𝐴)
123 fveq2 6673 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 𝑧 → (𝑓𝑤) = (𝑓𝑧))
124 suceq 6259 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓𝑤) = (𝑓𝑧) → suc (𝑓𝑤) = suc (𝑓𝑧))
125123, 124syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = 𝑧 → suc (𝑓𝑤) = suc (𝑓𝑧))
126125fveq2d 6677 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = 𝑧 → (‘suc (𝑓𝑤)) = (‘suc (𝑓𝑧)))
127 axcclem.3 . . . . . . . . . . . . . . . . . . . . 21 𝐺 = (𝑤𝐴 ↦ (‘suc (𝑓𝑤)))
128 fvex 6686 . . . . . . . . . . . . . . . . . . . . 21 (‘suc (𝑓𝑧)) ∈ V
129126, 127, 128fvmpt 6771 . . . . . . . . . . . . . . . . . . . 20 (𝑧𝐴 → (𝐺𝑧) = (‘suc (𝑓𝑧)))
130122, 129syl 17 . . . . . . . . . . . . . . . . . . 19 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ∧ 𝑧 = (𝑓𝑖)) → (𝐺𝑧) = (‘suc (𝑓𝑧)))
131 simp3 1134 . . . . . . . . . . . . . . . . . . 19 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ∧ 𝑧 = (𝑓𝑖)) → 𝑧 = (𝑓𝑖))
132116, 130, 1313eltr4d 2931 . . . . . . . . . . . . . . . . . 18 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ∧ 𝑧 = (𝑓𝑖)) → (𝐺𝑧) ∈ 𝑧)
1331323exp 1115 . . . . . . . . . . . . . . . . 17 ((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) → (∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) → (𝑧 = (𝑓𝑖) → (𝐺𝑧) ∈ 𝑧)))
134133com3r 87 . . . . . . . . . . . . . . . 16 (𝑧 = (𝑓𝑖) → ((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) → (∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) → (𝐺𝑧) ∈ 𝑧)))
1351343expd 1349 . . . . . . . . . . . . . . 15 (𝑧 = (𝑓𝑖) → (:ω⟶ 𝐴 → (𝑓:ω–1-1-onto𝐴 → (𝑖 ∈ ω → (∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) → (𝐺𝑧) ∈ 𝑧)))))
136135com4r 94 . . . . . . . . . . . . . 14 (𝑖 ∈ ω → (𝑧 = (𝑓𝑖) → (:ω⟶ 𝐴 → (𝑓:ω–1-1-onto𝐴 → (∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) → (𝐺𝑧) ∈ 𝑧)))))
137136rexlimiv 3283 . . . . . . . . . . . . 13 (∃𝑖 ∈ ω 𝑧 = (𝑓𝑖) → (:ω⟶ 𝐴 → (𝑓:ω–1-1-onto𝐴 → (∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) → (𝐺𝑧) ∈ 𝑧))))
13886, 137syl 17 . . . . . . . . . . . 12 ((𝑓:ω–1-1-onto𝐴𝑧𝐴) → (:ω⟶ 𝐴 → (𝑓:ω–1-1-onto𝐴 → (∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) → (𝐺𝑧) ∈ 𝑧))))
13983, 138mpid 44 . . . . . . . . . . 11 ((𝑓:ω–1-1-onto𝐴𝑧𝐴) → (:ω⟶ 𝐴 → (∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) → (𝐺𝑧) ∈ 𝑧)))
140139impd 413 . . . . . . . . . 10 ((𝑓:ω–1-1-onto𝐴𝑧𝐴) → ((:ω⟶ 𝐴 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘))) → (𝐺𝑧) ∈ 𝑧))
141140impancom 454 . . . . . . . . 9 ((𝑓:ω–1-1-onto𝐴 ∧ (:ω⟶ 𝐴 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)))) → (𝑧𝐴 → (𝐺𝑧) ∈ 𝑧))
14282, 141syl5 34 . . . . . . . 8 ((𝑓:ω–1-1-onto𝐴 ∧ (:ω⟶ 𝐴 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)))) → ((𝑧𝑥𝑧 ≠ ∅) → (𝐺𝑧) ∈ 𝑧))
143142expd 418 . . . . . . 7 ((𝑓:ω–1-1-onto𝐴 ∧ (:ω⟶ 𝐴 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)))) → (𝑧𝑥 → (𝑧 ≠ ∅ → (𝐺𝑧) ∈ 𝑧)))
144143ralrimiv 3184 . . . . . 6 ((𝑓:ω–1-1-onto𝐴 ∧ (:ω⟶ 𝐴 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)))) → ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝐺𝑧) ∈ 𝑧))
145 fvrn0 6701 . . . . . . . . . . 11 (‘suc (𝑓𝑤)) ∈ (ran ∪ {∅})
146145rgenw 3153 . . . . . . . . . 10 𝑤𝐴 (‘suc (𝑓𝑤)) ∈ (ran ∪ {∅})
147 eqid 2824 . . . . . . . . . . 11 (𝑤𝐴 ↦ (‘suc (𝑓𝑤))) = (𝑤𝐴 ↦ (‘suc (𝑓𝑤)))
148147fmpt 6877 . . . . . . . . . 10 (∀𝑤𝐴 (‘suc (𝑓𝑤)) ∈ (ran ∪ {∅}) ↔ (𝑤𝐴 ↦ (‘suc (𝑓𝑤))):𝐴⟶(ran ∪ {∅}))
149146, 148mpbi 232 . . . . . . . . 9 (𝑤𝐴 ↦ (‘suc (𝑓𝑤))):𝐴⟶(ran ∪ {∅})
150 vex 3500 . . . . . . . . . . 11 ∈ V
151150rnex 7620 . . . . . . . . . 10 ran ∈ V
152 p0ex 5288 . . . . . . . . . 10 {∅} ∈ V
153151, 152unex 7472 . . . . . . . . 9 (ran ∪ {∅}) ∈ V
154 fex2 7641 . . . . . . . . 9 (((𝑤𝐴 ↦ (‘suc (𝑓𝑤))):𝐴⟶(ran ∪ {∅}) ∧ 𝐴 ∈ V ∧ (ran ∪ {∅}) ∈ V) → (𝑤𝐴 ↦ (‘suc (𝑓𝑤))) ∈ V)
155149, 67, 153, 154mp3an 1457 . . . . . . . 8 (𝑤𝐴 ↦ (‘suc (𝑓𝑤))) ∈ V
156127, 155eqeltri 2912 . . . . . . 7 𝐺 ∈ V
157 fveq1 6672 . . . . . . . . . 10 (𝑔 = 𝐺 → (𝑔𝑧) = (𝐺𝑧))
158157eleq1d 2900 . . . . . . . . 9 (𝑔 = 𝐺 → ((𝑔𝑧) ∈ 𝑧 ↔ (𝐺𝑧) ∈ 𝑧))
159158imbi2d 343 . . . . . . . 8 (𝑔 = 𝐺 → ((𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧) ↔ (𝑧 ≠ ∅ → (𝐺𝑧) ∈ 𝑧)))
160159ralbidv 3200 . . . . . . 7 (𝑔 = 𝐺 → (∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧) ↔ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝐺𝑧) ∈ 𝑧)))
161156, 160spcev 3610 . . . . . 6 (∀𝑧𝑥 (𝑧 ≠ ∅ → (𝐺𝑧) ∈ 𝑧) → ∃𝑔𝑧𝑥 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧))
162144, 161syl 17 . . . . 5 ((𝑓:ω–1-1-onto𝐴 ∧ (:ω⟶ 𝐴 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)))) → ∃𝑔𝑧𝑥 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧))
16376, 162exlimddv 1935 . . . 4 (𝑓:ω–1-1-onto𝐴 → ∃𝑔𝑧𝑥 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧))
164163exlimiv 1930 . . 3 (∃𝑓 𝑓:ω–1-1-onto𝐴 → ∃𝑔𝑧𝑥 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧))
16534, 164sylbi 219 . 2 (ω ≈ 𝐴 → ∃𝑔𝑧𝑥 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧))
16632, 33, 1653syl 18 1 (𝑥 ≈ ω → ∃𝑔𝑧𝑥 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 208  wa 398  w3a 1083   = wceq 1536  wex 1779  wcel 2113  wne 3019  wral 3141  wrex 3142  Vcvv 3497  cdif 3936  cun 3937  wss 3939  c0 4294  𝒫 cpw 4542  {csn 4570   cuni 4841   class class class wbr 5069  cmpt 5149   × cxp 5556  ccnv 5557  ran crn 5559  suc csuc 6196  wf 6354  ontowfo 6356  1-1-ontowf1o 6357  cfv 6358  (class class class)co 7159  cmpo 7161  ωcom 7583  cen 8509  cdom 8510  csdm 8511  Fincfn 8512
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-sep 5206  ax-nul 5213  ax-pow 5269  ax-pr 5333  ax-un 7464  ax-dc 9871
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ne 3020  df-ral 3146  df-rex 3147  df-reu 3148  df-rab 3150  df-v 3499  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4471  df-pw 4544  df-sn 4571  df-pr 4573  df-tp 4575  df-op 4577  df-uni 4842  df-int 4880  df-iun 4924  df-br 5070  df-opab 5132  df-mpt 5150  df-tr 5176  df-id 5463  df-eprel 5468  df-po 5477  df-so 5478  df-fr 5517  df-we 5519  df-xp 5564  df-rel 5565  df-cnv 5566  df-co 5567  df-dm 5568  df-rn 5569  df-res 5570  df-ima 5571  df-pred 6151  df-ord 6197  df-on 6198  df-lim 6199  df-suc 6200  df-iota 6317  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-ov 7162  df-oprab 7163  df-mpo 7164  df-om 7584  df-1st 7692  df-2nd 7693  df-wrecs 7950  df-recs 8011  df-rdg 8049  df-1o 8105  df-oadd 8109  df-er 8292  df-en 8513  df-dom 8514  df-sdom 8515  df-fin 8516
This theorem is referenced by:  axcc  9883
  Copyright terms: Public domain W3C validator