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

Theorem axcclem 9958
Description: Lemma for axcc 9959. (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 8851 . . . . . . . 8 (𝐴 ≺ ω → 𝐴 ∈ Fin)
2 axcclem.1 . . . . . . . . . 10 𝐴 = (𝑥 ∖ {∅})
32eleq1i 2823 . . . . . . . . 9 (𝐴 ∈ Fin ↔ (𝑥 ∖ {∅}) ∈ Fin)
4 undif1 4366 . . . . . . . . . . 11 ((𝑥 ∖ {∅}) ∪ {∅}) = (𝑥 ∪ {∅})
5 snfi 8643 . . . . . . . . . . . 12 {∅} ∈ Fin
6 unfi 8772 . . . . . . . . . . . 12 (((𝑥 ∖ {∅}) ∈ Fin ∧ {∅} ∈ Fin) → ((𝑥 ∖ {∅}) ∪ {∅}) ∈ Fin)
75, 6mpan2 691 . . . . . . . . . . 11 ((𝑥 ∖ {∅}) ∈ Fin → ((𝑥 ∖ {∅}) ∪ {∅}) ∈ Fin)
84, 7eqeltrrid 2838 . . . . . . . . . 10 ((𝑥 ∖ {∅}) ∈ Fin → (𝑥 ∪ {∅}) ∈ Fin)
9 ssun1 4063 . . . . . . . . . 10 𝑥 ⊆ (𝑥 ∪ {∅})
10 ssfi 8773 . . . . . . . . . 10 (((𝑥 ∪ {∅}) ∈ Fin ∧ 𝑥 ⊆ (𝑥 ∪ {∅})) → 𝑥 ∈ Fin)
118, 9, 10sylancl 589 . . . . . . . . 9 ((𝑥 ∖ {∅}) ∈ Fin → 𝑥 ∈ Fin)
123, 11sylbi 220 . . . . . . . 8 (𝐴 ∈ Fin → 𝑥 ∈ Fin)
13 dcomex 9948 . . . . . . . . . 10 ω ∈ V
14 isfiniteg 8853 . . . . . . . . . 10 (ω ∈ V → (𝑥 ∈ Fin ↔ 𝑥 ≺ ω))
1513, 14ax-mp 5 . . . . . . . . 9 (𝑥 ∈ Fin ↔ 𝑥 ≺ ω)
16 sdomnen 8585 . . . . . . . . 9 (𝑥 ≺ ω → ¬ 𝑥 ≈ ω)
1715, 16sylbi 220 . . . . . . . 8 (𝑥 ∈ Fin → ¬ 𝑥 ≈ ω)
181, 12, 173syl 18 . . . . . . 7 (𝐴 ≺ ω → ¬ 𝑥 ≈ ω)
1918con2i 141 . . . . . 6 (𝑥 ≈ ω → ¬ 𝐴 ≺ ω)
20 sdomentr 8702 . . . . . . 7 ((𝐴𝑥𝑥 ≈ ω) → 𝐴 ≺ ω)
2120expcom 417 . . . . . 6 (𝑥 ≈ ω → (𝐴𝑥𝐴 ≺ ω))
2219, 21mtod 201 . . . . 5 (𝑥 ≈ ω → ¬ 𝐴𝑥)
23 vex 3402 . . . . . 6 𝑥 ∈ V
24 difss 4023 . . . . . . 7 (𝑥 ∖ {∅}) ⊆ 𝑥
252, 24eqsstri 3912 . . . . . 6 𝐴𝑥
26 ssdomg 8602 . . . . . 6 (𝑥 ∈ V → (𝐴𝑥𝐴𝑥))
2723, 25, 26mp2 9 . . . . 5 𝐴𝑥
2822, 27jctil 523 . . . 4 (𝑥 ≈ ω → (𝐴𝑥 ∧ ¬ 𝐴𝑥))
29 bren2 8587 . . . 4 (𝐴𝑥 ↔ (𝐴𝑥 ∧ ¬ 𝐴𝑥))
3028, 29sylibr 237 . . 3 (𝑥 ≈ ω → 𝐴𝑥)
31 entr 8608 . . 3 ((𝐴𝑥𝑥 ≈ ω) → 𝐴 ≈ ω)
3230, 31mpancom 688 . 2 (𝑥 ≈ ω → 𝐴 ≈ ω)
33 ensym 8605 . 2 (𝐴 ≈ ω → ω ≈ 𝐴)
34 bren 8565 . . 3 (ω ≈ 𝐴 ↔ ∃𝑓 𝑓:ω–1-1-onto𝐴)
35 f1of 6619 . . . . . . . 8 (𝑓:ω–1-1-onto𝐴𝑓:ω⟶𝐴)
36 peano1 7621 . . . . . . . 8 ∅ ∈ ω
37 ffvelrn 6860 . . . . . . . 8 ((𝑓:ω⟶𝐴 ∧ ∅ ∈ ω) → (𝑓‘∅) ∈ 𝐴)
3835, 36, 37sylancl 589 . . . . . . 7 (𝑓:ω–1-1-onto𝐴 → (𝑓‘∅) ∈ 𝐴)
39 eldifn 4019 . . . . . . . . 9 ((𝑓‘∅) ∈ (𝑥 ∖ {∅}) → ¬ (𝑓‘∅) ∈ {∅})
4039, 2eleq2s 2851 . . . . . . . 8 ((𝑓‘∅) ∈ 𝐴 → ¬ (𝑓‘∅) ∈ {∅})
41 fvex 6688 . . . . . . . . . . 11 (𝑓‘∅) ∈ V
4241elsn 4532 . . . . . . . . . 10 ((𝑓‘∅) ∈ {∅} ↔ (𝑓‘∅) = ∅)
4342notbii 323 . . . . . . . . 9 (¬ (𝑓‘∅) ∈ {∅} ↔ ¬ (𝑓‘∅) = ∅)
44 neq0 4235 . . . . . . . . 9 (¬ (𝑓‘∅) = ∅ ↔ ∃𝑐 𝑐 ∈ (𝑓‘∅))
4543, 44bitr2i 279 . . . . . . . 8 (∃𝑐 𝑐 ∈ (𝑓‘∅) ↔ ¬ (𝑓‘∅) ∈ {∅})
4640, 45sylibr 237 . . . . . . 7 ((𝑓‘∅) ∈ 𝐴 → ∃𝑐 𝑐 ∈ (𝑓‘∅))
4738, 46syl 17 . . . . . 6 (𝑓:ω–1-1-onto𝐴 → ∃𝑐 𝑐 ∈ (𝑓‘∅))
48 elunii 4802 . . . . . . . . . . 11 ((𝑐 ∈ (𝑓‘∅) ∧ (𝑓‘∅) ∈ 𝐴) → 𝑐 𝐴)
4938, 48sylan2 596 . . . . . . . . . 10 ((𝑐 ∈ (𝑓‘∅) ∧ 𝑓:ω–1-1-onto𝐴) → 𝑐 𝐴)
5035ffvelrnda 6862 . . . . . . . . . . . . . 14 ((𝑓:ω–1-1-onto𝐴𝑛 ∈ ω) → (𝑓𝑛) ∈ 𝐴)
51 difabs 4185 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∖ {∅}) ∖ {∅}) = (𝑥 ∖ {∅})
522difeq1i 4010 . . . . . . . . . . . . . . . . . 18 (𝐴 ∖ {∅}) = ((𝑥 ∖ {∅}) ∖ {∅})
5351, 52, 23eqtr4i 2771 . . . . . . . . . . . . . . . . 17 (𝐴 ∖ {∅}) = 𝐴
54 pwuni 4836 . . . . . . . . . . . . . . . . . 18 𝐴 ⊆ 𝒫 𝐴
55 ssdif 4031 . . . . . . . . . . . . . . . . . 18 (𝐴 ⊆ 𝒫 𝐴 → (𝐴 ∖ {∅}) ⊆ (𝒫 𝐴 ∖ {∅}))
5654, 55ax-mp 5 . . . . . . . . . . . . . . . . 17 (𝐴 ∖ {∅}) ⊆ (𝒫 𝐴 ∖ {∅})
5753, 56eqsstrri 3913 . . . . . . . . . . . . . . . 16 𝐴 ⊆ (𝒫 𝐴 ∖ {∅})
5857sseli 3874 . . . . . . . . . . . . . . 15 ((𝑓𝑛) ∈ 𝐴 → (𝑓𝑛) ∈ (𝒫 𝐴 ∖ {∅}))
5958ralrimivw 3097 . . . . . . . . . . . . . 14 ((𝑓𝑛) ∈ 𝐴 → ∀𝑦 𝐴(𝑓𝑛) ∈ (𝒫 𝐴 ∖ {∅}))
6050, 59syl 17 . . . . . . . . . . . . 13 ((𝑓:ω–1-1-onto𝐴𝑛 ∈ ω) → ∀𝑦 𝐴(𝑓𝑛) ∈ (𝒫 𝐴 ∖ {∅}))
6160ralrimiva 3096 . . . . . . . . . . . 12 (𝑓:ω–1-1-onto𝐴 → ∀𝑛 ∈ ω ∀𝑦 𝐴(𝑓𝑛) ∈ (𝒫 𝐴 ∖ {∅}))
62 axcclem.2 . . . . . . . . . . . . 13 𝐹 = (𝑛 ∈ ω, 𝑦 𝐴 ↦ (𝑓𝑛))
6362fmpo 7792 . . . . . . . . . . . 12 (∀𝑛 ∈ ω ∀𝑦 𝐴(𝑓𝑛) ∈ (𝒫 𝐴 ∖ {∅}) ↔ 𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}))
6461, 63sylib 221 . . . . . . . . . . 11 (𝑓:ω–1-1-onto𝐴𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}))
6564adantl 485 . . . . . . . . . 10 ((𝑐 ∈ (𝑓‘∅) ∧ 𝑓:ω–1-1-onto𝐴) → 𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}))
6623difexi 5197 . . . . . . . . . . . . 13 (𝑥 ∖ {∅}) ∈ V
672, 66eqeltri 2829 . . . . . . . . . . . 12 𝐴 ∈ V
6867uniex 7486 . . . . . . . . . . 11 𝐴 ∈ V
6968axdc4 9957 . . . . . . . . . 10 ((𝑐 𝐴𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅})) → ∃(:ω⟶ 𝐴 ∧ (‘∅) = 𝑐 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘))))
7049, 65, 69syl2anc 587 . . . . . . . . 9 ((𝑐 ∈ (𝑓‘∅) ∧ 𝑓:ω–1-1-onto𝐴) → ∃(:ω⟶ 𝐴 ∧ (‘∅) = 𝑐 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘))))
71 3simpb 1150 . . . . . . . . . 10 ((:ω⟶ 𝐴 ∧ (‘∅) = 𝑐 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘))) → (:ω⟶ 𝐴 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘))))
7271eximi 1841 . . . . . . . . 9 (∃(:ω⟶ 𝐴 ∧ (‘∅) = 𝑐 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘))) → ∃(:ω⟶ 𝐴 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘))))
7370, 72syl 17 . . . . . . . 8 ((𝑐 ∈ (𝑓‘∅) ∧ 𝑓:ω–1-1-onto𝐴) → ∃(:ω⟶ 𝐴 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘))))
7473ex 416 . . . . . . 7 (𝑐 ∈ (𝑓‘∅) → (𝑓:ω–1-1-onto𝐴 → ∃(:ω⟶ 𝐴 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)))))
7574exlimiv 1936 . . . . . 6 (∃𝑐 𝑐 ∈ (𝑓‘∅) → (𝑓:ω–1-1-onto𝐴 → ∃(:ω⟶ 𝐴 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)))))
7647, 75mpcom 38 . . . . 5 (𝑓:ω–1-1-onto𝐴 → ∃(:ω⟶ 𝐴 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘))))
77 velsn 4533 . . . . . . . . . . 11 (𝑧 ∈ {∅} ↔ 𝑧 = ∅)
7877necon3bbii 2981 . . . . . . . . . 10 𝑧 ∈ {∅} ↔ 𝑧 ≠ ∅)
792eleq2i 2824 . . . . . . . . . . 11 (𝑧𝐴𝑧 ∈ (𝑥 ∖ {∅}))
80 eldif 3854 . . . . . . . . . . 11 (𝑧 ∈ (𝑥 ∖ {∅}) ↔ (𝑧𝑥 ∧ ¬ 𝑧 ∈ {∅}))
8179, 80sylbbr 239 . . . . . . . . . 10 ((𝑧𝑥 ∧ ¬ 𝑧 ∈ {∅}) → 𝑧𝐴)
8278, 81sylan2br 598 . . . . . . . . 9 ((𝑧𝑥𝑧 ≠ ∅) → 𝑧𝐴)
83 simpl 486 . . . . . . . . . . . 12 ((𝑓:ω–1-1-onto𝐴𝑧𝐴) → 𝑓:ω–1-1-onto𝐴)
84 f1ofo 6626 . . . . . . . . . . . . . 14 (𝑓:ω–1-1-onto𝐴𝑓:ω–onto𝐴)
85 foelrn 6883 . . . . . . . . . . . . . 14 ((𝑓:ω–onto𝐴𝑧𝐴) → ∃𝑖 ∈ ω 𝑧 = (𝑓𝑖))
8684, 85sylan 583 . . . . . . . . . . . . 13 ((𝑓:ω–1-1-onto𝐴𝑧𝐴) → ∃𝑖 ∈ ω 𝑧 = (𝑓𝑖))
87 suceq 6238 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑘 = 𝑖 → suc 𝑘 = suc 𝑖)
8887fveq2d 6679 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 = 𝑖 → (‘suc 𝑘) = (‘suc 𝑖))
89 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑘 = 𝑖𝑘 = 𝑖)
90 fveq2 6675 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑘 = 𝑖 → (𝑘) = (𝑖))
9189, 90oveq12d 7189 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 = 𝑖 → (𝑘𝐹(𝑘)) = (𝑖𝐹(𝑖)))
9288, 91eleq12d 2827 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝑖 → ((‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ↔ (‘suc 𝑖) ∈ (𝑖𝐹(𝑖))))
9392rspcv 3522 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ ω → (∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) → (‘suc 𝑖) ∈ (𝑖𝐹(𝑖))))
94933ad2ant3 1136 . . . . . . . . . . . . . . . . . . . . . 22 ((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) → (∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) → (‘suc 𝑖) ∈ (𝑖𝐹(𝑖))))
9594imp 410 . . . . . . . . . . . . . . . . . . . . 21 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘))) → (‘suc 𝑖) ∈ (𝑖𝐹(𝑖)))
96953adant3 1133 . . . . . . . . . . . . . . . . . . . 20 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ∧ 𝑧 = (𝑓𝑖)) → (‘suc 𝑖) ∈ (𝑖𝐹(𝑖)))
97 eqcom 2745 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 = (𝑓𝑖) ↔ (𝑓𝑖) = 𝑧)
98 f1ocnvfv 7047 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) → ((𝑓𝑖) = 𝑧 → (𝑓𝑧) = 𝑖))
9997, 98syl5bi 245 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) → (𝑧 = (𝑓𝑖) → (𝑓𝑧) = 𝑖))
100993adant1 1131 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) → (𝑧 = (𝑓𝑖) → (𝑓𝑧) = 𝑖))
101100imp 410 . . . . . . . . . . . . . . . . . . . . . . . 24 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ 𝑧 = (𝑓𝑖)) → (𝑓𝑧) = 𝑖)
102101eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . . 23 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ 𝑧 = (𝑓𝑖)) → 𝑖 = (𝑓𝑧))
1031023adant2 1132 . . . . . . . . . . . . . . . . . . . . . 22 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ∧ 𝑧 = (𝑓𝑖)) → 𝑖 = (𝑓𝑧))
104 suceq 6238 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = (𝑓𝑧) → suc 𝑖 = suc (𝑓𝑧))
105103, 104syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ∧ 𝑧 = (𝑓𝑖)) → suc 𝑖 = suc (𝑓𝑧))
106105fveq2d 6679 . . . . . . . . . . . . . . . . . . . 20 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ∧ 𝑧 = (𝑓𝑖)) → (‘suc 𝑖) = (‘suc (𝑓𝑧)))
107 simpr 488 . . . . . . . . . . . . . . . . . . . . . . 23 ((:ω⟶ 𝐴𝑖 ∈ ω) → 𝑖 ∈ ω)
108 ffvelrn 6860 . . . . . . . . . . . . . . . . . . . . . . 23 ((:ω⟶ 𝐴𝑖 ∈ ω) → (𝑖) ∈ 𝐴)
109 fveq2 6675 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑖 → (𝑓𝑛) = (𝑓𝑖))
110 eqidd 2739 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = (𝑖) → (𝑓𝑖) = (𝑓𝑖))
111 fvex 6688 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓𝑖) ∈ V
112109, 110, 62, 111ovmpo 7326 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑖 ∈ ω ∧ (𝑖) ∈ 𝐴) → (𝑖𝐹(𝑖)) = (𝑓𝑖))
113107, 108, 112syl2anc 587 . . . . . . . . . . . . . . . . . . . . . 22 ((:ω⟶ 𝐴𝑖 ∈ ω) → (𝑖𝐹(𝑖)) = (𝑓𝑖))
1141133adant2 1132 . . . . . . . . . . . . . . . . . . . . 21 ((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) → (𝑖𝐹(𝑖)) = (𝑓𝑖))
1151143ad2ant1 1134 . . . . . . . . . . . . . . . . . . . 20 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ∧ 𝑧 = (𝑓𝑖)) → (𝑖𝐹(𝑖)) = (𝑓𝑖))
11696, 106, 1153eltr3d 2847 . . . . . . . . . . . . . . . . . . 19 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ∧ 𝑧 = (𝑓𝑖)) → (‘suc (𝑓𝑧)) ∈ (𝑓𝑖))
11735ffvelrnda 6862 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) → (𝑓𝑖) ∈ 𝐴)
1181173adant1 1131 . . . . . . . . . . . . . . . . . . . . . 22 ((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) → (𝑓𝑖) ∈ 𝐴)
1191183ad2ant1 1134 . . . . . . . . . . . . . . . . . . . . 21 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ∧ 𝑧 = (𝑓𝑖)) → (𝑓𝑖) ∈ 𝐴)
120 eleq1 2820 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = (𝑓𝑖) → (𝑧𝐴 ↔ (𝑓𝑖) ∈ 𝐴))
1211203ad2ant3 1136 . . . . . . . . . . . . . . . . . . . . 21 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ∧ 𝑧 = (𝑓𝑖)) → (𝑧𝐴 ↔ (𝑓𝑖) ∈ 𝐴))
122119, 121mpbird 260 . . . . . . . . . . . . . . . . . . . 20 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ∧ 𝑧 = (𝑓𝑖)) → 𝑧𝐴)
123 fveq2 6675 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 𝑧 → (𝑓𝑤) = (𝑓𝑧))
124 suceq 6238 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓𝑤) = (𝑓𝑧) → suc (𝑓𝑤) = suc (𝑓𝑧))
125123, 124syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = 𝑧 → suc (𝑓𝑤) = suc (𝑓𝑧))
126125fveq2d 6679 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = 𝑧 → (‘suc (𝑓𝑤)) = (‘suc (𝑓𝑧)))
127 axcclem.3 . . . . . . . . . . . . . . . . . . . . 21 𝐺 = (𝑤𝐴 ↦ (‘suc (𝑓𝑤)))
128 fvex 6688 . . . . . . . . . . . . . . . . . . . . 21 (‘suc (𝑓𝑧)) ∈ V
129126, 127, 128fvmpt 6776 . . . . . . . . . . . . . . . . . . . 20 (𝑧𝐴 → (𝐺𝑧) = (‘suc (𝑓𝑧)))
130122, 129syl 17 . . . . . . . . . . . . . . . . . . 19 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ∧ 𝑧 = (𝑓𝑖)) → (𝐺𝑧) = (‘suc (𝑓𝑧)))
131 simp3 1139 . . . . . . . . . . . . . . . . . . 19 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ∧ 𝑧 = (𝑓𝑖)) → 𝑧 = (𝑓𝑖))
132116, 130, 1313eltr4d 2848 . . . . . . . . . . . . . . . . . 18 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ∧ 𝑧 = (𝑓𝑖)) → (𝐺𝑧) ∈ 𝑧)
1331323exp 1120 . . . . . . . . . . . . . . . . 17 ((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) → (∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) → (𝑧 = (𝑓𝑖) → (𝐺𝑧) ∈ 𝑧)))
134133com3r 87 . . . . . . . . . . . . . . . 16 (𝑧 = (𝑓𝑖) → ((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) → (∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) → (𝐺𝑧) ∈ 𝑧)))
1351343expd 1354 . . . . . . . . . . . . . . 15 (𝑧 = (𝑓𝑖) → (:ω⟶ 𝐴 → (𝑓:ω–1-1-onto𝐴 → (𝑖 ∈ ω → (∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) → (𝐺𝑧) ∈ 𝑧)))))
136135com4r 94 . . . . . . . . . . . . . 14 (𝑖 ∈ ω → (𝑧 = (𝑓𝑖) → (:ω⟶ 𝐴 → (𝑓:ω–1-1-onto𝐴 → (∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) → (𝐺𝑧) ∈ 𝑧)))))
137136rexlimiv 3190 . . . . . . . . . . . . 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 414 . . . . . . . . . 10 ((𝑓:ω–1-1-onto𝐴𝑧𝐴) → ((:ω⟶ 𝐴 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘))) → (𝐺𝑧) ∈ 𝑧))
141140impancom 455 . . . . . . . . 9 ((𝑓:ω–1-1-onto𝐴 ∧ (:ω⟶ 𝐴 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)))) → (𝑧𝐴 → (𝐺𝑧) ∈ 𝑧))
14282, 141syl5 34 . . . . . . . 8 ((𝑓:ω–1-1-onto𝐴 ∧ (:ω⟶ 𝐴 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)))) → ((𝑧𝑥𝑧 ≠ ∅) → (𝐺𝑧) ∈ 𝑧))
143142expd 419 . . . . . . 7 ((𝑓:ω–1-1-onto𝐴 ∧ (:ω⟶ 𝐴 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)))) → (𝑧𝑥 → (𝑧 ≠ ∅ → (𝐺𝑧) ∈ 𝑧)))
144143ralrimiv 3095 . . . . . 6 ((𝑓:ω–1-1-onto𝐴 ∧ (:ω⟶ 𝐴 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)))) → ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝐺𝑧) ∈ 𝑧))
145 fvrn0 6703 . . . . . . . . . . 11 (‘suc (𝑓𝑤)) ∈ (ran ∪ {∅})
146145rgenw 3065 . . . . . . . . . 10 𝑤𝐴 (‘suc (𝑓𝑤)) ∈ (ran ∪ {∅})
147 eqid 2738 . . . . . . . . . . 11 (𝑤𝐴 ↦ (‘suc (𝑓𝑤))) = (𝑤𝐴 ↦ (‘suc (𝑓𝑤)))
148147fmpt 6885 . . . . . . . . . 10 (∀𝑤𝐴 (‘suc (𝑓𝑤)) ∈ (ran ∪ {∅}) ↔ (𝑤𝐴 ↦ (‘suc (𝑓𝑤))):𝐴⟶(ran ∪ {∅}))
149146, 148mpbi 233 . . . . . . . . 9 (𝑤𝐴 ↦ (‘suc (𝑓𝑤))):𝐴⟶(ran ∪ {∅})
150 vex 3402 . . . . . . . . . . 11 ∈ V
151150rnex 7644 . . . . . . . . . 10 ran ∈ V
152 p0ex 5252 . . . . . . . . . 10 {∅} ∈ V
153151, 152unex 7488 . . . . . . . . 9 (ran ∪ {∅}) ∈ V
154 fex2 7665 . . . . . . . . 9 (((𝑤𝐴 ↦ (‘suc (𝑓𝑤))):𝐴⟶(ran ∪ {∅}) ∧ 𝐴 ∈ V ∧ (ran ∪ {∅}) ∈ V) → (𝑤𝐴 ↦ (‘suc (𝑓𝑤))) ∈ V)
155149, 67, 153, 154mp3an 1462 . . . . . . . 8 (𝑤𝐴 ↦ (‘suc (𝑓𝑤))) ∈ V
156127, 155eqeltri 2829 . . . . . . 7 𝐺 ∈ V
157 fveq1 6674 . . . . . . . . . 10 (𝑔 = 𝐺 → (𝑔𝑧) = (𝐺𝑧))
158157eleq1d 2817 . . . . . . . . 9 (𝑔 = 𝐺 → ((𝑔𝑧) ∈ 𝑧 ↔ (𝐺𝑧) ∈ 𝑧))
159158imbi2d 344 . . . . . . . 8 (𝑔 = 𝐺 → ((𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧) ↔ (𝑧 ≠ ∅ → (𝐺𝑧) ∈ 𝑧)))
160159ralbidv 3109 . . . . . . 7 (𝑔 = 𝐺 → (∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧) ↔ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝐺𝑧) ∈ 𝑧)))
161156, 160spcev 3511 . . . . . 6 (∀𝑧𝑥 (𝑧 ≠ ∅ → (𝐺𝑧) ∈ 𝑧) → ∃𝑔𝑧𝑥 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧))
162144, 161syl 17 . . . . 5 ((𝑓:ω–1-1-onto𝐴 ∧ (:ω⟶ 𝐴 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)))) → ∃𝑔𝑧𝑥 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧))
16376, 162exlimddv 1941 . . . 4 (𝑓:ω–1-1-onto𝐴 → ∃𝑔𝑧𝑥 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧))
164163exlimiv 1936 . . 3 (∃𝑓 𝑓:ω–1-1-onto𝐴 → ∃𝑔𝑧𝑥 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧))
16534, 164sylbi 220 . 2 (ω ≈ 𝐴 → ∃𝑔𝑧𝑥 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧))
16632, 33, 1653syl 18 1 (𝑥 ≈ ω → ∃𝑔𝑧𝑥 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  w3a 1088   = wceq 1542  wex 1786  wcel 2113  wne 2934  wral 3053  wrex 3054  Vcvv 3398  cdif 3841  cun 3842  wss 3844  c0 4212  𝒫 cpw 4489  {csn 4517   cuni 4797   class class class wbr 5031  cmpt 5111   × cxp 5524  ccnv 5525  ran crn 5527  suc csuc 6175  wf 6336  ontowfo 6338  1-1-ontowf1o 6339  cfv 6340  (class class class)co 7171  cmpo 7173  ωcom 7600  cen 8553  cdom 8554  csdm 8555  Fincfn 8556
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-sep 5168  ax-nul 5175  ax-pow 5233  ax-pr 5297  ax-un 7480  ax-dc 9947
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-ral 3058  df-rex 3059  df-reu 3060  df-rab 3062  df-v 3400  df-sbc 3683  df-csb 3792  df-dif 3847  df-un 3849  df-in 3851  df-ss 3861  df-pss 3863  df-nul 4213  df-if 4416  df-pw 4491  df-sn 4518  df-pr 4520  df-tp 4522  df-op 4524  df-uni 4798  df-int 4838  df-iun 4884  df-br 5032  df-opab 5094  df-mpt 5112  df-tr 5138  df-id 5430  df-eprel 5435  df-po 5443  df-so 5444  df-fr 5484  df-we 5486  df-xp 5532  df-rel 5533  df-cnv 5534  df-co 5535  df-dm 5536  df-rn 5537  df-res 5538  df-ima 5539  df-pred 6130  df-ord 6176  df-on 6177  df-lim 6178  df-suc 6179  df-iota 6298  df-fun 6342  df-fn 6343  df-f 6344  df-f1 6345  df-fo 6346  df-f1o 6347  df-fv 6348  df-ov 7174  df-oprab 7175  df-mpo 7176  df-om 7601  df-1st 7715  df-2nd 7716  df-wrecs 7977  df-recs 8038  df-rdg 8076  df-1o 8132  df-er 8321  df-en 8557  df-dom 8558  df-sdom 8559  df-fin 8560
This theorem is referenced by:  axcc  9959
  Copyright terms: Public domain W3C validator