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

Theorem axcclem 9481
Description: Lemma for axcc 9482. (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 8374 . . . . . . . 8 (𝐴 ≺ ω → 𝐴 ∈ Fin)
2 axcclem.1 . . . . . . . . . 10 𝐴 = (𝑥 ∖ {∅})
32eleq1i 2841 . . . . . . . . 9 (𝐴 ∈ Fin ↔ (𝑥 ∖ {∅}) ∈ Fin)
4 undif1 4185 . . . . . . . . . . 11 ((𝑥 ∖ {∅}) ∪ {∅}) = (𝑥 ∪ {∅})
5 snfi 8194 . . . . . . . . . . . 12 {∅} ∈ Fin
6 unfi 8383 . . . . . . . . . . . 12 (((𝑥 ∖ {∅}) ∈ Fin ∧ {∅} ∈ Fin) → ((𝑥 ∖ {∅}) ∪ {∅}) ∈ Fin)
75, 6mpan2 663 . . . . . . . . . . 11 ((𝑥 ∖ {∅}) ∈ Fin → ((𝑥 ∖ {∅}) ∪ {∅}) ∈ Fin)
84, 7syl5eqelr 2855 . . . . . . . . . 10 ((𝑥 ∖ {∅}) ∈ Fin → (𝑥 ∪ {∅}) ∈ Fin)
9 ssun1 3927 . . . . . . . . . 10 𝑥 ⊆ (𝑥 ∪ {∅})
10 ssfi 8336 . . . . . . . . . 10 (((𝑥 ∪ {∅}) ∈ Fin ∧ 𝑥 ⊆ (𝑥 ∪ {∅})) → 𝑥 ∈ Fin)
118, 9, 10sylancl 566 . . . . . . . . 9 ((𝑥 ∖ {∅}) ∈ Fin → 𝑥 ∈ Fin)
123, 11sylbi 207 . . . . . . . 8 (𝐴 ∈ Fin → 𝑥 ∈ Fin)
13 dcomex 9471 . . . . . . . . . 10 ω ∈ V
14 isfiniteg 8376 . . . . . . . . . 10 (ω ∈ V → (𝑥 ∈ Fin ↔ 𝑥 ≺ ω))
1513, 14ax-mp 5 . . . . . . . . 9 (𝑥 ∈ Fin ↔ 𝑥 ≺ ω)
16 sdomnen 8138 . . . . . . . . 9 (𝑥 ≺ ω → ¬ 𝑥 ≈ ω)
1715, 16sylbi 207 . . . . . . . 8 (𝑥 ∈ Fin → ¬ 𝑥 ≈ ω)
181, 12, 173syl 18 . . . . . . 7 (𝐴 ≺ ω → ¬ 𝑥 ≈ ω)
1918con2i 136 . . . . . 6 (𝑥 ≈ ω → ¬ 𝐴 ≺ ω)
20 sdomentr 8250 . . . . . . 7 ((𝐴𝑥𝑥 ≈ ω) → 𝐴 ≺ ω)
2120expcom 398 . . . . . 6 (𝑥 ≈ ω → (𝐴𝑥𝐴 ≺ ω))
2219, 21mtod 189 . . . . 5 (𝑥 ≈ ω → ¬ 𝐴𝑥)
23 vex 3354 . . . . . 6 𝑥 ∈ V
24 difss 3888 . . . . . . 7 (𝑥 ∖ {∅}) ⊆ 𝑥
252, 24eqsstri 3784 . . . . . 6 𝐴𝑥
26 ssdomg 8155 . . . . . 6 (𝑥 ∈ V → (𝐴𝑥𝐴𝑥))
2723, 25, 26mp2 9 . . . . 5 𝐴𝑥
2822, 27jctil 503 . . . 4 (𝑥 ≈ ω → (𝐴𝑥 ∧ ¬ 𝐴𝑥))
29 bren2 8140 . . . 4 (𝐴𝑥 ↔ (𝐴𝑥 ∧ ¬ 𝐴𝑥))
3028, 29sylibr 224 . . 3 (𝑥 ≈ ω → 𝐴𝑥)
31 entr 8161 . . 3 ((𝐴𝑥𝑥 ≈ ω) → 𝐴 ≈ ω)
3230, 31mpancom 660 . 2 (𝑥 ≈ ω → 𝐴 ≈ ω)
33 ensym 8158 . 2 (𝐴 ≈ ω → ω ≈ 𝐴)
34 bren 8118 . . 3 (ω ≈ 𝐴 ↔ ∃𝑓 𝑓:ω–1-1-onto𝐴)
35 f1of 6278 . . . . . . . 8 (𝑓:ω–1-1-onto𝐴𝑓:ω⟶𝐴)
36 peano1 7232 . . . . . . . 8 ∅ ∈ ω
37 ffvelrn 6500 . . . . . . . 8 ((𝑓:ω⟶𝐴 ∧ ∅ ∈ ω) → (𝑓‘∅) ∈ 𝐴)
3835, 36, 37sylancl 566 . . . . . . 7 (𝑓:ω–1-1-onto𝐴 → (𝑓‘∅) ∈ 𝐴)
39 eldifn 3884 . . . . . . . . 9 ((𝑓‘∅) ∈ (𝑥 ∖ {∅}) → ¬ (𝑓‘∅) ∈ {∅})
4039, 2eleq2s 2868 . . . . . . . 8 ((𝑓‘∅) ∈ 𝐴 → ¬ (𝑓‘∅) ∈ {∅})
41 fvex 6342 . . . . . . . . . . 11 (𝑓‘∅) ∈ V
4241elsn 4331 . . . . . . . . . 10 ((𝑓‘∅) ∈ {∅} ↔ (𝑓‘∅) = ∅)
4342notbii 309 . . . . . . . . 9 (¬ (𝑓‘∅) ∈ {∅} ↔ ¬ (𝑓‘∅) = ∅)
44 neq0 4077 . . . . . . . . 9 (¬ (𝑓‘∅) = ∅ ↔ ∃𝑐 𝑐 ∈ (𝑓‘∅))
4543, 44bitr2i 265 . . . . . . . 8 (∃𝑐 𝑐 ∈ (𝑓‘∅) ↔ ¬ (𝑓‘∅) ∈ {∅})
4640, 45sylibr 224 . . . . . . 7 ((𝑓‘∅) ∈ 𝐴 → ∃𝑐 𝑐 ∈ (𝑓‘∅))
4738, 46syl 17 . . . . . 6 (𝑓:ω–1-1-onto𝐴 → ∃𝑐 𝑐 ∈ (𝑓‘∅))
48 elunii 4579 . . . . . . . . . . 11 ((𝑐 ∈ (𝑓‘∅) ∧ (𝑓‘∅) ∈ 𝐴) → 𝑐 𝐴)
4938, 48sylan2 572 . . . . . . . . . 10 ((𝑐 ∈ (𝑓‘∅) ∧ 𝑓:ω–1-1-onto𝐴) → 𝑐 𝐴)
5035ffvelrnda 6502 . . . . . . . . . . . . . 14 ((𝑓:ω–1-1-onto𝐴𝑛 ∈ ω) → (𝑓𝑛) ∈ 𝐴)
51 difabs 4040 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∖ {∅}) ∖ {∅}) = (𝑥 ∖ {∅})
522difeq1i 3875 . . . . . . . . . . . . . . . . . 18 (𝐴 ∖ {∅}) = ((𝑥 ∖ {∅}) ∖ {∅})
5351, 52, 23eqtr4i 2803 . . . . . . . . . . . . . . . . 17 (𝐴 ∖ {∅}) = 𝐴
54 pwuni 4610 . . . . . . . . . . . . . . . . . 18 𝐴 ⊆ 𝒫 𝐴
55 ssdif 3896 . . . . . . . . . . . . . . . . . 18 (𝐴 ⊆ 𝒫 𝐴 → (𝐴 ∖ {∅}) ⊆ (𝒫 𝐴 ∖ {∅}))
5654, 55ax-mp 5 . . . . . . . . . . . . . . . . 17 (𝐴 ∖ {∅}) ⊆ (𝒫 𝐴 ∖ {∅})
5753, 56eqsstr3i 3785 . . . . . . . . . . . . . . . 16 𝐴 ⊆ (𝒫 𝐴 ∖ {∅})
5857sseli 3748 . . . . . . . . . . . . . . 15 ((𝑓𝑛) ∈ 𝐴 → (𝑓𝑛) ∈ (𝒫 𝐴 ∖ {∅}))
5958ralrimivw 3116 . . . . . . . . . . . . . 14 ((𝑓𝑛) ∈ 𝐴 → ∀𝑦 𝐴(𝑓𝑛) ∈ (𝒫 𝐴 ∖ {∅}))
6050, 59syl 17 . . . . . . . . . . . . 13 ((𝑓:ω–1-1-onto𝐴𝑛 ∈ ω) → ∀𝑦 𝐴(𝑓𝑛) ∈ (𝒫 𝐴 ∖ {∅}))
6160ralrimiva 3115 . . . . . . . . . . . 12 (𝑓:ω–1-1-onto𝐴 → ∀𝑛 ∈ ω ∀𝑦 𝐴(𝑓𝑛) ∈ (𝒫 𝐴 ∖ {∅}))
62 axcclem.2 . . . . . . . . . . . . 13 𝐹 = (𝑛 ∈ ω, 𝑦 𝐴 ↦ (𝑓𝑛))
6362fmpt2 7387 . . . . . . . . . . . 12 (∀𝑛 ∈ ω ∀𝑦 𝐴(𝑓𝑛) ∈ (𝒫 𝐴 ∖ {∅}) ↔ 𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}))
6461, 63sylib 208 . . . . . . . . . . 11 (𝑓:ω–1-1-onto𝐴𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}))
6564adantl 467 . . . . . . . . . 10 ((𝑐 ∈ (𝑓‘∅) ∧ 𝑓:ω–1-1-onto𝐴) → 𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}))
66 difexg 4942 . . . . . . . . . . . . . 14 (𝑥 ∈ V → (𝑥 ∖ {∅}) ∈ V)
6723, 66ax-mp 5 . . . . . . . . . . . . 13 (𝑥 ∖ {∅}) ∈ V
682, 67eqeltri 2846 . . . . . . . . . . . 12 𝐴 ∈ V
6968uniex 7100 . . . . . . . . . . 11 𝐴 ∈ V
7069axdc4 9480 . . . . . . . . . 10 ((𝑐 𝐴𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅})) → ∃(:ω⟶ 𝐴 ∧ (‘∅) = 𝑐 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘))))
7149, 65, 70syl2anc 565 . . . . . . . . 9 ((𝑐 ∈ (𝑓‘∅) ∧ 𝑓:ω–1-1-onto𝐴) → ∃(:ω⟶ 𝐴 ∧ (‘∅) = 𝑐 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘))))
72 3simpb 1144 . . . . . . . . . 10 ((:ω⟶ 𝐴 ∧ (‘∅) = 𝑐 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘))) → (:ω⟶ 𝐴 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘))))
7372eximi 1910 . . . . . . . . 9 (∃(:ω⟶ 𝐴 ∧ (‘∅) = 𝑐 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘))) → ∃(:ω⟶ 𝐴 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘))))
7471, 73syl 17 . . . . . . . 8 ((𝑐 ∈ (𝑓‘∅) ∧ 𝑓:ω–1-1-onto𝐴) → ∃(:ω⟶ 𝐴 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘))))
7574ex 397 . . . . . . 7 (𝑐 ∈ (𝑓‘∅) → (𝑓:ω–1-1-onto𝐴 → ∃(:ω⟶ 𝐴 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)))))
7675exlimiv 2010 . . . . . 6 (∃𝑐 𝑐 ∈ (𝑓‘∅) → (𝑓:ω–1-1-onto𝐴 → ∃(:ω⟶ 𝐴 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)))))
7747, 76mpcom 38 . . . . 5 (𝑓:ω–1-1-onto𝐴 → ∃(:ω⟶ 𝐴 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘))))
78 velsn 4332 . . . . . . . . . . 11 (𝑧 ∈ {∅} ↔ 𝑧 = ∅)
7978necon3bbii 2990 . . . . . . . . . 10 𝑧 ∈ {∅} ↔ 𝑧 ≠ ∅)
802eleq2i 2842 . . . . . . . . . . 11 (𝑧𝐴𝑧 ∈ (𝑥 ∖ {∅}))
81 eldif 3733 . . . . . . . . . . 11 (𝑧 ∈ (𝑥 ∖ {∅}) ↔ (𝑧𝑥 ∧ ¬ 𝑧 ∈ {∅}))
8280, 81sylbbr 226 . . . . . . . . . 10 ((𝑧𝑥 ∧ ¬ 𝑧 ∈ {∅}) → 𝑧𝐴)
8379, 82sylan2br 574 . . . . . . . . 9 ((𝑧𝑥𝑧 ≠ ∅) → 𝑧𝐴)
84 simpl 468 . . . . . . . . . . . 12 ((𝑓:ω–1-1-onto𝐴𝑧𝐴) → 𝑓:ω–1-1-onto𝐴)
85 f1ofo 6285 . . . . . . . . . . . . . 14 (𝑓:ω–1-1-onto𝐴𝑓:ω–onto𝐴)
86 foelrn 6521 . . . . . . . . . . . . . 14 ((𝑓:ω–onto𝐴𝑧𝐴) → ∃𝑖 ∈ ω 𝑧 = (𝑓𝑖))
8785, 86sylan 561 . . . . . . . . . . . . 13 ((𝑓:ω–1-1-onto𝐴𝑧𝐴) → ∃𝑖 ∈ ω 𝑧 = (𝑓𝑖))
88 suceq 5933 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑘 = 𝑖 → suc 𝑘 = suc 𝑖)
8988fveq2d 6336 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 = 𝑖 → (‘suc 𝑘) = (‘suc 𝑖))
90 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑘 = 𝑖𝑘 = 𝑖)
91 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑘 = 𝑖 → (𝑘) = (𝑖))
9290, 91oveq12d 6811 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 = 𝑖 → (𝑘𝐹(𝑘)) = (𝑖𝐹(𝑖)))
9389, 92eleq12d 2844 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝑖 → ((‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ↔ (‘suc 𝑖) ∈ (𝑖𝐹(𝑖))))
9493rspcv 3456 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ ω → (∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) → (‘suc 𝑖) ∈ (𝑖𝐹(𝑖))))
95943ad2ant3 1129 . . . . . . . . . . . . . . . . . . . . . 22 ((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) → (∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) → (‘suc 𝑖) ∈ (𝑖𝐹(𝑖))))
9695imp 393 . . . . . . . . . . . . . . . . . . . . 21 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘))) → (‘suc 𝑖) ∈ (𝑖𝐹(𝑖)))
97963adant3 1126 . . . . . . . . . . . . . . . . . . . 20 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ∧ 𝑧 = (𝑓𝑖)) → (‘suc 𝑖) ∈ (𝑖𝐹(𝑖)))
98 eqcom 2778 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 = (𝑓𝑖) ↔ (𝑓𝑖) = 𝑧)
99 f1ocnvfv 6677 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) → ((𝑓𝑖) = 𝑧 → (𝑓𝑧) = 𝑖))
10098, 99syl5bi 232 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) → (𝑧 = (𝑓𝑖) → (𝑓𝑧) = 𝑖))
1011003adant1 1124 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) → (𝑧 = (𝑓𝑖) → (𝑓𝑧) = 𝑖))
102101imp 393 . . . . . . . . . . . . . . . . . . . . . . . 24 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ 𝑧 = (𝑓𝑖)) → (𝑓𝑧) = 𝑖)
103102eqcomd 2777 . . . . . . . . . . . . . . . . . . . . . . 23 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ 𝑧 = (𝑓𝑖)) → 𝑖 = (𝑓𝑧))
1041033adant2 1125 . . . . . . . . . . . . . . . . . . . . . 22 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ∧ 𝑧 = (𝑓𝑖)) → 𝑖 = (𝑓𝑧))
105 suceq 5933 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = (𝑓𝑧) → suc 𝑖 = suc (𝑓𝑧))
106104, 105syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ∧ 𝑧 = (𝑓𝑖)) → suc 𝑖 = suc (𝑓𝑧))
107106fveq2d 6336 . . . . . . . . . . . . . . . . . . . 20 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ∧ 𝑧 = (𝑓𝑖)) → (‘suc 𝑖) = (‘suc (𝑓𝑧)))
108 simpr 471 . . . . . . . . . . . . . . . . . . . . . . 23 ((:ω⟶ 𝐴𝑖 ∈ ω) → 𝑖 ∈ ω)
109 ffvelrn 6500 . . . . . . . . . . . . . . . . . . . . . . 23 ((:ω⟶ 𝐴𝑖 ∈ ω) → (𝑖) ∈ 𝐴)
110 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑖 → (𝑓𝑛) = (𝑓𝑖))
111 eqidd 2772 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = (𝑖) → (𝑓𝑖) = (𝑓𝑖))
112 fvex 6342 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓𝑖) ∈ V
113110, 111, 62, 112ovmpt2 6943 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑖 ∈ ω ∧ (𝑖) ∈ 𝐴) → (𝑖𝐹(𝑖)) = (𝑓𝑖))
114108, 109, 113syl2anc 565 . . . . . . . . . . . . . . . . . . . . . 22 ((:ω⟶ 𝐴𝑖 ∈ ω) → (𝑖𝐹(𝑖)) = (𝑓𝑖))
1151143adant2 1125 . . . . . . . . . . . . . . . . . . . . 21 ((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) → (𝑖𝐹(𝑖)) = (𝑓𝑖))
1161153ad2ant1 1127 . . . . . . . . . . . . . . . . . . . 20 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ∧ 𝑧 = (𝑓𝑖)) → (𝑖𝐹(𝑖)) = (𝑓𝑖))
11797, 107, 1163eltr3d 2864 . . . . . . . . . . . . . . . . . . 19 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ∧ 𝑧 = (𝑓𝑖)) → (‘suc (𝑓𝑧)) ∈ (𝑓𝑖))
11835ffvelrnda 6502 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) → (𝑓𝑖) ∈ 𝐴)
1191183adant1 1124 . . . . . . . . . . . . . . . . . . . . . 22 ((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) → (𝑓𝑖) ∈ 𝐴)
1201193ad2ant1 1127 . . . . . . . . . . . . . . . . . . . . 21 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ∧ 𝑧 = (𝑓𝑖)) → (𝑓𝑖) ∈ 𝐴)
121 eleq1 2838 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = (𝑓𝑖) → (𝑧𝐴 ↔ (𝑓𝑖) ∈ 𝐴))
1221213ad2ant3 1129 . . . . . . . . . . . . . . . . . . . . 21 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ∧ 𝑧 = (𝑓𝑖)) → (𝑧𝐴 ↔ (𝑓𝑖) ∈ 𝐴))
123120, 122mpbird 247 . . . . . . . . . . . . . . . . . . . 20 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ∧ 𝑧 = (𝑓𝑖)) → 𝑧𝐴)
124 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 𝑧 → (𝑓𝑤) = (𝑓𝑧))
125 suceq 5933 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓𝑤) = (𝑓𝑧) → suc (𝑓𝑤) = suc (𝑓𝑧))
126124, 125syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = 𝑧 → suc (𝑓𝑤) = suc (𝑓𝑧))
127126fveq2d 6336 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = 𝑧 → (‘suc (𝑓𝑤)) = (‘suc (𝑓𝑧)))
128 axcclem.3 . . . . . . . . . . . . . . . . . . . . 21 𝐺 = (𝑤𝐴 ↦ (‘suc (𝑓𝑤)))
129 fvex 6342 . . . . . . . . . . . . . . . . . . . . 21 (‘suc (𝑓𝑧)) ∈ V
130127, 128, 129fvmpt 6424 . . . . . . . . . . . . . . . . . . . 20 (𝑧𝐴 → (𝐺𝑧) = (‘suc (𝑓𝑧)))
131123, 130syl 17 . . . . . . . . . . . . . . . . . . 19 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ∧ 𝑧 = (𝑓𝑖)) → (𝐺𝑧) = (‘suc (𝑓𝑧)))
132 simp3 1132 . . . . . . . . . . . . . . . . . . 19 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ∧ 𝑧 = (𝑓𝑖)) → 𝑧 = (𝑓𝑖))
133117, 131, 1323eltr4d 2865 . . . . . . . . . . . . . . . . . 18 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ∧ 𝑧 = (𝑓𝑖)) → (𝐺𝑧) ∈ 𝑧)
1341333exp 1112 . . . . . . . . . . . . . . . . 17 ((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) → (∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) → (𝑧 = (𝑓𝑖) → (𝐺𝑧) ∈ 𝑧)))
135134com3r 87 . . . . . . . . . . . . . . . 16 (𝑧 = (𝑓𝑖) → ((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) → (∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) → (𝐺𝑧) ∈ 𝑧)))
1361353expd 1446 . . . . . . . . . . . . . . 15 (𝑧 = (𝑓𝑖) → (:ω⟶ 𝐴 → (𝑓:ω–1-1-onto𝐴 → (𝑖 ∈ ω → (∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) → (𝐺𝑧) ∈ 𝑧)))))
137136com4r 94 . . . . . . . . . . . . . 14 (𝑖 ∈ ω → (𝑧 = (𝑓𝑖) → (:ω⟶ 𝐴 → (𝑓:ω–1-1-onto𝐴 → (∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) → (𝐺𝑧) ∈ 𝑧)))))
138137rexlimiv 3175 . . . . . . . . . . . . 13 (∃𝑖 ∈ ω 𝑧 = (𝑓𝑖) → (:ω⟶ 𝐴 → (𝑓:ω–1-1-onto𝐴 → (∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) → (𝐺𝑧) ∈ 𝑧))))
13987, 138syl 17 . . . . . . . . . . . 12 ((𝑓:ω–1-1-onto𝐴𝑧𝐴) → (:ω⟶ 𝐴 → (𝑓:ω–1-1-onto𝐴 → (∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) → (𝐺𝑧) ∈ 𝑧))))
14084, 139mpid 44 . . . . . . . . . . 11 ((𝑓:ω–1-1-onto𝐴𝑧𝐴) → (:ω⟶ 𝐴 → (∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) → (𝐺𝑧) ∈ 𝑧)))
141140impd 396 . . . . . . . . . 10 ((𝑓:ω–1-1-onto𝐴𝑧𝐴) → ((:ω⟶ 𝐴 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘))) → (𝐺𝑧) ∈ 𝑧))
142141impancom 439 . . . . . . . . 9 ((𝑓:ω–1-1-onto𝐴 ∧ (:ω⟶ 𝐴 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)))) → (𝑧𝐴 → (𝐺𝑧) ∈ 𝑧))
14383, 142syl5 34 . . . . . . . 8 ((𝑓:ω–1-1-onto𝐴 ∧ (:ω⟶ 𝐴 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)))) → ((𝑧𝑥𝑧 ≠ ∅) → (𝐺𝑧) ∈ 𝑧))
144143expd 400 . . . . . . 7 ((𝑓:ω–1-1-onto𝐴 ∧ (:ω⟶ 𝐴 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)))) → (𝑧𝑥 → (𝑧 ≠ ∅ → (𝐺𝑧) ∈ 𝑧)))
145144ralrimiv 3114 . . . . . 6 ((𝑓:ω–1-1-onto𝐴 ∧ (:ω⟶ 𝐴 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)))) → ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝐺𝑧) ∈ 𝑧))
146 fvrn0 6357 . . . . . . . . . . 11 (‘suc (𝑓𝑤)) ∈ (ran ∪ {∅})
147146rgenw 3073 . . . . . . . . . 10 𝑤𝐴 (‘suc (𝑓𝑤)) ∈ (ran ∪ {∅})
148 eqid 2771 . . . . . . . . . . 11 (𝑤𝐴 ↦ (‘suc (𝑓𝑤))) = (𝑤𝐴 ↦ (‘suc (𝑓𝑤)))
149148fmpt 6523 . . . . . . . . . 10 (∀𝑤𝐴 (‘suc (𝑓𝑤)) ∈ (ran ∪ {∅}) ↔ (𝑤𝐴 ↦ (‘suc (𝑓𝑤))):𝐴⟶(ran ∪ {∅}))
150147, 149mpbi 220 . . . . . . . . 9 (𝑤𝐴 ↦ (‘suc (𝑓𝑤))):𝐴⟶(ran ∪ {∅})
151 vex 3354 . . . . . . . . . . 11 ∈ V
152151rnex 7247 . . . . . . . . . 10 ran ∈ V
153 p0ex 4984 . . . . . . . . . 10 {∅} ∈ V
154152, 153unex 7103 . . . . . . . . 9 (ran ∪ {∅}) ∈ V
155 fex2 7268 . . . . . . . . 9 (((𝑤𝐴 ↦ (‘suc (𝑓𝑤))):𝐴⟶(ran ∪ {∅}) ∧ 𝐴 ∈ V ∧ (ran ∪ {∅}) ∈ V) → (𝑤𝐴 ↦ (‘suc (𝑓𝑤))) ∈ V)
156150, 68, 154, 155mp3an 1572 . . . . . . . 8 (𝑤𝐴 ↦ (‘suc (𝑓𝑤))) ∈ V
157128, 156eqeltri 2846 . . . . . . 7 𝐺 ∈ V
158 fveq1 6331 . . . . . . . . . 10 (𝑔 = 𝐺 → (𝑔𝑧) = (𝐺𝑧))
159158eleq1d 2835 . . . . . . . . 9 (𝑔 = 𝐺 → ((𝑔𝑧) ∈ 𝑧 ↔ (𝐺𝑧) ∈ 𝑧))
160159imbi2d 329 . . . . . . . 8 (𝑔 = 𝐺 → ((𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧) ↔ (𝑧 ≠ ∅ → (𝐺𝑧) ∈ 𝑧)))
161160ralbidv 3135 . . . . . . 7 (𝑔 = 𝐺 → (∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧) ↔ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝐺𝑧) ∈ 𝑧)))
162157, 161spcev 3451 . . . . . 6 (∀𝑧𝑥 (𝑧 ≠ ∅ → (𝐺𝑧) ∈ 𝑧) → ∃𝑔𝑧𝑥 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧))
163145, 162syl 17 . . . . 5 ((𝑓:ω–1-1-onto𝐴 ∧ (:ω⟶ 𝐴 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)))) → ∃𝑔𝑧𝑥 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧))
16477, 163exlimddv 2015 . . . 4 (𝑓:ω–1-1-onto𝐴 → ∃𝑔𝑧𝑥 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧))
165164exlimiv 2010 . . 3 (∃𝑓 𝑓:ω–1-1-onto𝐴 → ∃𝑔𝑧𝑥 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧))
16634, 165sylbi 207 . 2 (ω ≈ 𝐴 → ∃𝑔𝑧𝑥 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧))
16732, 33, 1663syl 18 1 (𝑥 ≈ ω → ∃𝑔𝑧𝑥 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382  w3a 1071   = wceq 1631  wex 1852  wcel 2145  wne 2943  wral 3061  wrex 3062  Vcvv 3351  cdif 3720  cun 3721  wss 3723  c0 4063  𝒫 cpw 4297  {csn 4316   cuni 4574   class class class wbr 4786  cmpt 4863   × cxp 5247  ccnv 5248  ran crn 5250  suc csuc 5868  wf 6027  ontowfo 6029  1-1-ontowf1o 6030  cfv 6031  (class class class)co 6793  cmpt2 6795  ωcom 7212  cen 8106  cdom 8107  csdm 8108  Fincfn 8109
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-dc 9470
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-om 7213  df-1st 7315  df-2nd 7316  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-1o 7713  df-oadd 7717  df-er 7896  df-en 8110  df-dom 8111  df-sdom 8112  df-fin 8113
This theorem is referenced by:  axcc  9482
  Copyright terms: Public domain W3C validator