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

Theorem axcclem 9231
Description: Lemma for axcc 9232. (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 8170 . . . . . . . 8 (𝐴 ≺ ω → 𝐴 ∈ Fin)
2 axcclem.1 . . . . . . . . . 10 𝐴 = (𝑥 ∖ {∅})
32eleq1i 2689 . . . . . . . . 9 (𝐴 ∈ Fin ↔ (𝑥 ∖ {∅}) ∈ Fin)
4 undif1 4020 . . . . . . . . . . 11 ((𝑥 ∖ {∅}) ∪ {∅}) = (𝑥 ∪ {∅})
5 snfi 7990 . . . . . . . . . . . 12 {∅} ∈ Fin
6 unfi 8179 . . . . . . . . . . . 12 (((𝑥 ∖ {∅}) ∈ Fin ∧ {∅} ∈ Fin) → ((𝑥 ∖ {∅}) ∪ {∅}) ∈ Fin)
75, 6mpan2 706 . . . . . . . . . . 11 ((𝑥 ∖ {∅}) ∈ Fin → ((𝑥 ∖ {∅}) ∪ {∅}) ∈ Fin)
84, 7syl5eqelr 2703 . . . . . . . . . 10 ((𝑥 ∖ {∅}) ∈ Fin → (𝑥 ∪ {∅}) ∈ Fin)
9 ssun1 3759 . . . . . . . . . 10 𝑥 ⊆ (𝑥 ∪ {∅})
10 ssfi 8132 . . . . . . . . . 10 (((𝑥 ∪ {∅}) ∈ Fin ∧ 𝑥 ⊆ (𝑥 ∪ {∅})) → 𝑥 ∈ Fin)
118, 9, 10sylancl 693 . . . . . . . . 9 ((𝑥 ∖ {∅}) ∈ Fin → 𝑥 ∈ Fin)
123, 11sylbi 207 . . . . . . . 8 (𝐴 ∈ Fin → 𝑥 ∈ Fin)
13 dcomex 9221 . . . . . . . . . 10 ω ∈ V
14 isfiniteg 8172 . . . . . . . . . 10 (ω ∈ V → (𝑥 ∈ Fin ↔ 𝑥 ≺ ω))
1513, 14ax-mp 5 . . . . . . . . 9 (𝑥 ∈ Fin ↔ 𝑥 ≺ ω)
16 sdomnen 7936 . . . . . . . . 9 (𝑥 ≺ ω → ¬ 𝑥 ≈ ω)
1715, 16sylbi 207 . . . . . . . 8 (𝑥 ∈ Fin → ¬ 𝑥 ≈ ω)
181, 12, 173syl 18 . . . . . . 7 (𝐴 ≺ ω → ¬ 𝑥 ≈ ω)
1918con2i 134 . . . . . 6 (𝑥 ≈ ω → ¬ 𝐴 ≺ ω)
20 sdomentr 8046 . . . . . . 7 ((𝐴𝑥𝑥 ≈ ω) → 𝐴 ≺ ω)
2120expcom 451 . . . . . 6 (𝑥 ≈ ω → (𝐴𝑥𝐴 ≺ ω))
2219, 21mtod 189 . . . . 5 (𝑥 ≈ ω → ¬ 𝐴𝑥)
23 vex 3192 . . . . . 6 𝑥 ∈ V
24 difss 3720 . . . . . . 7 (𝑥 ∖ {∅}) ⊆ 𝑥
252, 24eqsstri 3619 . . . . . 6 𝐴𝑥
26 ssdomg 7953 . . . . . 6 (𝑥 ∈ V → (𝐴𝑥𝐴𝑥))
2723, 25, 26mp2 9 . . . . 5 𝐴𝑥
2822, 27jctil 559 . . . 4 (𝑥 ≈ ω → (𝐴𝑥 ∧ ¬ 𝐴𝑥))
29 bren2 7938 . . . 4 (𝐴𝑥 ↔ (𝐴𝑥 ∧ ¬ 𝐴𝑥))
3028, 29sylibr 224 . . 3 (𝑥 ≈ ω → 𝐴𝑥)
31 entr 7960 . . 3 ((𝐴𝑥𝑥 ≈ ω) → 𝐴 ≈ ω)
3230, 31mpancom 702 . 2 (𝑥 ≈ ω → 𝐴 ≈ ω)
33 ensym 7957 . 2 (𝐴 ≈ ω → ω ≈ 𝐴)
34 bren 7916 . . 3 (ω ≈ 𝐴 ↔ ∃𝑓 𝑓:ω–1-1-onto𝐴)
35 f1of 6099 . . . . . . . 8 (𝑓:ω–1-1-onto𝐴𝑓:ω⟶𝐴)
36 peano1 7039 . . . . . . . 8 ∅ ∈ ω
37 ffvelrn 6318 . . . . . . . 8 ((𝑓:ω⟶𝐴 ∧ ∅ ∈ ω) → (𝑓‘∅) ∈ 𝐴)
3835, 36, 37sylancl 693 . . . . . . 7 (𝑓:ω–1-1-onto𝐴 → (𝑓‘∅) ∈ 𝐴)
39 eldifn 3716 . . . . . . . . 9 ((𝑓‘∅) ∈ (𝑥 ∖ {∅}) → ¬ (𝑓‘∅) ∈ {∅})
4039, 2eleq2s 2716 . . . . . . . 8 ((𝑓‘∅) ∈ 𝐴 → ¬ (𝑓‘∅) ∈ {∅})
41 fvex 6163 . . . . . . . . . . 11 (𝑓‘∅) ∈ V
4241elsn 4168 . . . . . . . . . 10 ((𝑓‘∅) ∈ {∅} ↔ (𝑓‘∅) = ∅)
4342notbii 310 . . . . . . . . 9 (¬ (𝑓‘∅) ∈ {∅} ↔ ¬ (𝑓‘∅) = ∅)
44 neq0 3911 . . . . . . . . 9 (¬ (𝑓‘∅) = ∅ ↔ ∃𝑐 𝑐 ∈ (𝑓‘∅))
4543, 44bitr2i 265 . . . . . . . 8 (∃𝑐 𝑐 ∈ (𝑓‘∅) ↔ ¬ (𝑓‘∅) ∈ {∅})
4640, 45sylibr 224 . . . . . . 7 ((𝑓‘∅) ∈ 𝐴 → ∃𝑐 𝑐 ∈ (𝑓‘∅))
4738, 46syl 17 . . . . . 6 (𝑓:ω–1-1-onto𝐴 → ∃𝑐 𝑐 ∈ (𝑓‘∅))
48 elunii 4412 . . . . . . . . . . 11 ((𝑐 ∈ (𝑓‘∅) ∧ (𝑓‘∅) ∈ 𝐴) → 𝑐 𝐴)
4938, 48sylan2 491 . . . . . . . . . 10 ((𝑐 ∈ (𝑓‘∅) ∧ 𝑓:ω–1-1-onto𝐴) → 𝑐 𝐴)
5035ffvelrnda 6320 . . . . . . . . . . . . . 14 ((𝑓:ω–1-1-onto𝐴𝑛 ∈ ω) → (𝑓𝑛) ∈ 𝐴)
51 difabs 3873 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∖ {∅}) ∖ {∅}) = (𝑥 ∖ {∅})
522difeq1i 3707 . . . . . . . . . . . . . . . . . 18 (𝐴 ∖ {∅}) = ((𝑥 ∖ {∅}) ∖ {∅})
5351, 52, 23eqtr4i 2653 . . . . . . . . . . . . . . . . 17 (𝐴 ∖ {∅}) = 𝐴
54 pwuni 4864 . . . . . . . . . . . . . . . . . 18 𝐴 ⊆ 𝒫 𝐴
55 ssdif 3728 . . . . . . . . . . . . . . . . . 18 (𝐴 ⊆ 𝒫 𝐴 → (𝐴 ∖ {∅}) ⊆ (𝒫 𝐴 ∖ {∅}))
5654, 55ax-mp 5 . . . . . . . . . . . . . . . . 17 (𝐴 ∖ {∅}) ⊆ (𝒫 𝐴 ∖ {∅})
5753, 56eqsstr3i 3620 . . . . . . . . . . . . . . . 16 𝐴 ⊆ (𝒫 𝐴 ∖ {∅})
5857sseli 3583 . . . . . . . . . . . . . . 15 ((𝑓𝑛) ∈ 𝐴 → (𝑓𝑛) ∈ (𝒫 𝐴 ∖ {∅}))
5958ralrimivw 2962 . . . . . . . . . . . . . 14 ((𝑓𝑛) ∈ 𝐴 → ∀𝑦 𝐴(𝑓𝑛) ∈ (𝒫 𝐴 ∖ {∅}))
6050, 59syl 17 . . . . . . . . . . . . 13 ((𝑓:ω–1-1-onto𝐴𝑛 ∈ ω) → ∀𝑦 𝐴(𝑓𝑛) ∈ (𝒫 𝐴 ∖ {∅}))
6160ralrimiva 2961 . . . . . . . . . . . 12 (𝑓:ω–1-1-onto𝐴 → ∀𝑛 ∈ ω ∀𝑦 𝐴(𝑓𝑛) ∈ (𝒫 𝐴 ∖ {∅}))
62 axcclem.2 . . . . . . . . . . . . 13 𝐹 = (𝑛 ∈ ω, 𝑦 𝐴 ↦ (𝑓𝑛))
6362fmpt2 7189 . . . . . . . . . . . 12 (∀𝑛 ∈ ω ∀𝑦 𝐴(𝑓𝑛) ∈ (𝒫 𝐴 ∖ {∅}) ↔ 𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}))
6461, 63sylib 208 . . . . . . . . . . 11 (𝑓:ω–1-1-onto𝐴𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}))
6564adantl 482 . . . . . . . . . 10 ((𝑐 ∈ (𝑓‘∅) ∧ 𝑓:ω–1-1-onto𝐴) → 𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅}))
66 difexg 4773 . . . . . . . . . . . . . 14 (𝑥 ∈ V → (𝑥 ∖ {∅}) ∈ V)
6723, 66ax-mp 5 . . . . . . . . . . . . 13 (𝑥 ∖ {∅}) ∈ V
682, 67eqeltri 2694 . . . . . . . . . . . 12 𝐴 ∈ V
6968uniex 6913 . . . . . . . . . . 11 𝐴 ∈ V
7069axdc4 9230 . . . . . . . . . 10 ((𝑐 𝐴𝐹:(ω × 𝐴)⟶(𝒫 𝐴 ∖ {∅})) → ∃(:ω⟶ 𝐴 ∧ (‘∅) = 𝑐 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘))))
7149, 65, 70syl2anc 692 . . . . . . . . 9 ((𝑐 ∈ (𝑓‘∅) ∧ 𝑓:ω–1-1-onto𝐴) → ∃(:ω⟶ 𝐴 ∧ (‘∅) = 𝑐 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘))))
72 3simpb 1057 . . . . . . . . . 10 ((:ω⟶ 𝐴 ∧ (‘∅) = 𝑐 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘))) → (:ω⟶ 𝐴 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘))))
7372eximi 1759 . . . . . . . . 9 (∃(:ω⟶ 𝐴 ∧ (‘∅) = 𝑐 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘))) → ∃(:ω⟶ 𝐴 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘))))
7471, 73syl 17 . . . . . . . 8 ((𝑐 ∈ (𝑓‘∅) ∧ 𝑓:ω–1-1-onto𝐴) → ∃(:ω⟶ 𝐴 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘))))
7574ex 450 . . . . . . 7 (𝑐 ∈ (𝑓‘∅) → (𝑓:ω–1-1-onto𝐴 → ∃(:ω⟶ 𝐴 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)))))
7675exlimiv 1855 . . . . . 6 (∃𝑐 𝑐 ∈ (𝑓‘∅) → (𝑓:ω–1-1-onto𝐴 → ∃(:ω⟶ 𝐴 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)))))
7747, 76mpcom 38 . . . . 5 (𝑓:ω–1-1-onto𝐴 → ∃(:ω⟶ 𝐴 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘))))
78 velsn 4169 . . . . . . . . . . 11 (𝑧 ∈ {∅} ↔ 𝑧 = ∅)
7978necon3bbii 2837 . . . . . . . . . 10 𝑧 ∈ {∅} ↔ 𝑧 ≠ ∅)
802eleq2i 2690 . . . . . . . . . . 11 (𝑧𝐴𝑧 ∈ (𝑥 ∖ {∅}))
81 eldif 3569 . . . . . . . . . . 11 (𝑧 ∈ (𝑥 ∖ {∅}) ↔ (𝑧𝑥 ∧ ¬ 𝑧 ∈ {∅}))
8280, 81sylbbr 226 . . . . . . . . . 10 ((𝑧𝑥 ∧ ¬ 𝑧 ∈ {∅}) → 𝑧𝐴)
8379, 82sylan2br 493 . . . . . . . . 9 ((𝑧𝑥𝑧 ≠ ∅) → 𝑧𝐴)
84 simpl 473 . . . . . . . . . . . 12 ((𝑓:ω–1-1-onto𝐴𝑧𝐴) → 𝑓:ω–1-1-onto𝐴)
85 f1ofo 6106 . . . . . . . . . . . . . 14 (𝑓:ω–1-1-onto𝐴𝑓:ω–onto𝐴)
86 foelrn 6339 . . . . . . . . . . . . . 14 ((𝑓:ω–onto𝐴𝑧𝐴) → ∃𝑖 ∈ ω 𝑧 = (𝑓𝑖))
8785, 86sylan 488 . . . . . . . . . . . . 13 ((𝑓:ω–1-1-onto𝐴𝑧𝐴) → ∃𝑖 ∈ ω 𝑧 = (𝑓𝑖))
88 suceq 5754 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑘 = 𝑖 → suc 𝑘 = suc 𝑖)
8988fveq2d 6157 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 = 𝑖 → (‘suc 𝑘) = (‘suc 𝑖))
90 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑘 = 𝑖𝑘 = 𝑖)
91 fveq2 6153 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑘 = 𝑖 → (𝑘) = (𝑖))
9290, 91oveq12d 6628 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 = 𝑖 → (𝑘𝐹(𝑘)) = (𝑖𝐹(𝑖)))
9389, 92eleq12d 2692 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝑖 → ((‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ↔ (‘suc 𝑖) ∈ (𝑖𝐹(𝑖))))
9493rspcv 3294 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ ω → (∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) → (‘suc 𝑖) ∈ (𝑖𝐹(𝑖))))
95943ad2ant3 1082 . . . . . . . . . . . . . . . . . . . . . 22 ((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) → (∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) → (‘suc 𝑖) ∈ (𝑖𝐹(𝑖))))
9695imp 445 . . . . . . . . . . . . . . . . . . . . 21 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘))) → (‘suc 𝑖) ∈ (𝑖𝐹(𝑖)))
97963adant3 1079 . . . . . . . . . . . . . . . . . . . 20 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ∧ 𝑧 = (𝑓𝑖)) → (‘suc 𝑖) ∈ (𝑖𝐹(𝑖)))
98 eqcom 2628 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 = (𝑓𝑖) ↔ (𝑓𝑖) = 𝑧)
99 f1ocnvfv 6494 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) → ((𝑓𝑖) = 𝑧 → (𝑓𝑧) = 𝑖))
10098, 99syl5bi 232 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) → (𝑧 = (𝑓𝑖) → (𝑓𝑧) = 𝑖))
1011003adant1 1077 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) → (𝑧 = (𝑓𝑖) → (𝑓𝑧) = 𝑖))
102101imp 445 . . . . . . . . . . . . . . . . . . . . . . . 24 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ 𝑧 = (𝑓𝑖)) → (𝑓𝑧) = 𝑖)
103102eqcomd 2627 . . . . . . . . . . . . . . . . . . . . . . 23 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ 𝑧 = (𝑓𝑖)) → 𝑖 = (𝑓𝑧))
1041033adant2 1078 . . . . . . . . . . . . . . . . . . . . . 22 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ∧ 𝑧 = (𝑓𝑖)) → 𝑖 = (𝑓𝑧))
105 suceq 5754 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = (𝑓𝑧) → suc 𝑖 = suc (𝑓𝑧))
106104, 105syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ∧ 𝑧 = (𝑓𝑖)) → suc 𝑖 = suc (𝑓𝑧))
107106fveq2d 6157 . . . . . . . . . . . . . . . . . . . 20 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ∧ 𝑧 = (𝑓𝑖)) → (‘suc 𝑖) = (‘suc (𝑓𝑧)))
108 simpr 477 . . . . . . . . . . . . . . . . . . . . . . 23 ((:ω⟶ 𝐴𝑖 ∈ ω) → 𝑖 ∈ ω)
109 ffvelrn 6318 . . . . . . . . . . . . . . . . . . . . . . 23 ((:ω⟶ 𝐴𝑖 ∈ ω) → (𝑖) ∈ 𝐴)
110 fveq2 6153 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑖 → (𝑓𝑛) = (𝑓𝑖))
111 eqidd 2622 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = (𝑖) → (𝑓𝑖) = (𝑓𝑖))
112 fvex 6163 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓𝑖) ∈ V
113110, 111, 62, 112ovmpt2 6756 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑖 ∈ ω ∧ (𝑖) ∈ 𝐴) → (𝑖𝐹(𝑖)) = (𝑓𝑖))
114108, 109, 113syl2anc 692 . . . . . . . . . . . . . . . . . . . . . 22 ((:ω⟶ 𝐴𝑖 ∈ ω) → (𝑖𝐹(𝑖)) = (𝑓𝑖))
1151143adant2 1078 . . . . . . . . . . . . . . . . . . . . 21 ((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) → (𝑖𝐹(𝑖)) = (𝑓𝑖))
1161153ad2ant1 1080 . . . . . . . . . . . . . . . . . . . 20 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ∧ 𝑧 = (𝑓𝑖)) → (𝑖𝐹(𝑖)) = (𝑓𝑖))
11797, 107, 1163eltr3d 2712 . . . . . . . . . . . . . . . . . . 19 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ∧ 𝑧 = (𝑓𝑖)) → (‘suc (𝑓𝑧)) ∈ (𝑓𝑖))
11835ffvelrnda 6320 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) → (𝑓𝑖) ∈ 𝐴)
1191183adant1 1077 . . . . . . . . . . . . . . . . . . . . . 22 ((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) → (𝑓𝑖) ∈ 𝐴)
1201193ad2ant1 1080 . . . . . . . . . . . . . . . . . . . . 21 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ∧ 𝑧 = (𝑓𝑖)) → (𝑓𝑖) ∈ 𝐴)
121 eleq1 2686 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = (𝑓𝑖) → (𝑧𝐴 ↔ (𝑓𝑖) ∈ 𝐴))
1221213ad2ant3 1082 . . . . . . . . . . . . . . . . . . . . 21 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ∧ 𝑧 = (𝑓𝑖)) → (𝑧𝐴 ↔ (𝑓𝑖) ∈ 𝐴))
123120, 122mpbird 247 . . . . . . . . . . . . . . . . . . . 20 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ∧ 𝑧 = (𝑓𝑖)) → 𝑧𝐴)
124 fveq2 6153 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 𝑧 → (𝑓𝑤) = (𝑓𝑧))
125 suceq 5754 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓𝑤) = (𝑓𝑧) → suc (𝑓𝑤) = suc (𝑓𝑧))
126124, 125syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = 𝑧 → suc (𝑓𝑤) = suc (𝑓𝑧))
127126fveq2d 6157 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = 𝑧 → (‘suc (𝑓𝑤)) = (‘suc (𝑓𝑧)))
128 axcclem.3 . . . . . . . . . . . . . . . . . . . . 21 𝐺 = (𝑤𝐴 ↦ (‘suc (𝑓𝑤)))
129 fvex 6163 . . . . . . . . . . . . . . . . . . . . 21 (‘suc (𝑓𝑧)) ∈ V
130127, 128, 129fvmpt 6244 . . . . . . . . . . . . . . . . . . . 20 (𝑧𝐴 → (𝐺𝑧) = (‘suc (𝑓𝑧)))
131123, 130syl 17 . . . . . . . . . . . . . . . . . . 19 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ∧ 𝑧 = (𝑓𝑖)) → (𝐺𝑧) = (‘suc (𝑓𝑧)))
132 simp3 1061 . . . . . . . . . . . . . . . . . . 19 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ∧ 𝑧 = (𝑓𝑖)) → 𝑧 = (𝑓𝑖))
133117, 131, 1323eltr4d 2713 . . . . . . . . . . . . . . . . . 18 (((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) ∧ 𝑧 = (𝑓𝑖)) → (𝐺𝑧) ∈ 𝑧)
1341333exp 1261 . . . . . . . . . . . . . . . . 17 ((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) → (∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) → (𝑧 = (𝑓𝑖) → (𝐺𝑧) ∈ 𝑧)))
135134com3r 87 . . . . . . . . . . . . . . . 16 (𝑧 = (𝑓𝑖) → ((:ω⟶ 𝐴𝑓:ω–1-1-onto𝐴𝑖 ∈ ω) → (∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) → (𝐺𝑧) ∈ 𝑧)))
1361353expd 1281 . . . . . . . . . . . . . . 15 (𝑧 = (𝑓𝑖) → (:ω⟶ 𝐴 → (𝑓:ω–1-1-onto𝐴 → (𝑖 ∈ ω → (∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) → (𝐺𝑧) ∈ 𝑧)))))
137136com4r 94 . . . . . . . . . . . . . 14 (𝑖 ∈ ω → (𝑧 = (𝑓𝑖) → (:ω⟶ 𝐴 → (𝑓:ω–1-1-onto𝐴 → (∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)) → (𝐺𝑧) ∈ 𝑧)))))
138137rexlimiv 3021 . . . . . . . . . . . . 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 447 . . . . . . . . . 10 ((𝑓:ω–1-1-onto𝐴𝑧𝐴) → ((:ω⟶ 𝐴 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘))) → (𝐺𝑧) ∈ 𝑧))
142141impancom 456 . . . . . . . . 9 ((𝑓:ω–1-1-onto𝐴 ∧ (:ω⟶ 𝐴 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)))) → (𝑧𝐴 → (𝐺𝑧) ∈ 𝑧))
14383, 142syl5 34 . . . . . . . 8 ((𝑓:ω–1-1-onto𝐴 ∧ (:ω⟶ 𝐴 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)))) → ((𝑧𝑥𝑧 ≠ ∅) → (𝐺𝑧) ∈ 𝑧))
144143expd 452 . . . . . . 7 ((𝑓:ω–1-1-onto𝐴 ∧ (:ω⟶ 𝐴 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)))) → (𝑧𝑥 → (𝑧 ≠ ∅ → (𝐺𝑧) ∈ 𝑧)))
145144ralrimiv 2960 . . . . . 6 ((𝑓:ω–1-1-onto𝐴 ∧ (:ω⟶ 𝐴 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)))) → ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝐺𝑧) ∈ 𝑧))
146 fvrn0 6178 . . . . . . . . . . 11 (‘suc (𝑓𝑤)) ∈ (ran ∪ {∅})
147146rgenw 2919 . . . . . . . . . 10 𝑤𝐴 (‘suc (𝑓𝑤)) ∈ (ran ∪ {∅})
148 eqid 2621 . . . . . . . . . . 11 (𝑤𝐴 ↦ (‘suc (𝑓𝑤))) = (𝑤𝐴 ↦ (‘suc (𝑓𝑤)))
149148fmpt 6342 . . . . . . . . . 10 (∀𝑤𝐴 (‘suc (𝑓𝑤)) ∈ (ran ∪ {∅}) ↔ (𝑤𝐴 ↦ (‘suc (𝑓𝑤))):𝐴⟶(ran ∪ {∅}))
150147, 149mpbi 220 . . . . . . . . 9 (𝑤𝐴 ↦ (‘suc (𝑓𝑤))):𝐴⟶(ran ∪ {∅})
151 vex 3192 . . . . . . . . . . 11 ∈ V
152151rnex 7054 . . . . . . . . . 10 ran ∈ V
153 p0ex 4818 . . . . . . . . . 10 {∅} ∈ V
154152, 153unex 6916 . . . . . . . . 9 (ran ∪ {∅}) ∈ V
155 fex2 7075 . . . . . . . . 9 (((𝑤𝐴 ↦ (‘suc (𝑓𝑤))):𝐴⟶(ran ∪ {∅}) ∧ 𝐴 ∈ V ∧ (ran ∪ {∅}) ∈ V) → (𝑤𝐴 ↦ (‘suc (𝑓𝑤))) ∈ V)
156150, 68, 154, 155mp3an 1421 . . . . . . . 8 (𝑤𝐴 ↦ (‘suc (𝑓𝑤))) ∈ V
157128, 156eqeltri 2694 . . . . . . 7 𝐺 ∈ V
158 fveq1 6152 . . . . . . . . . 10 (𝑔 = 𝐺 → (𝑔𝑧) = (𝐺𝑧))
159158eleq1d 2683 . . . . . . . . 9 (𝑔 = 𝐺 → ((𝑔𝑧) ∈ 𝑧 ↔ (𝐺𝑧) ∈ 𝑧))
160159imbi2d 330 . . . . . . . 8 (𝑔 = 𝐺 → ((𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧) ↔ (𝑧 ≠ ∅ → (𝐺𝑧) ∈ 𝑧)))
161160ralbidv 2981 . . . . . . 7 (𝑔 = 𝐺 → (∀𝑧𝑥 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧) ↔ ∀𝑧𝑥 (𝑧 ≠ ∅ → (𝐺𝑧) ∈ 𝑧)))
162157, 161spcev 3289 . . . . . 6 (∀𝑧𝑥 (𝑧 ≠ ∅ → (𝐺𝑧) ∈ 𝑧) → ∃𝑔𝑧𝑥 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧))
163145, 162syl 17 . . . . 5 ((𝑓:ω–1-1-onto𝐴 ∧ (:ω⟶ 𝐴 ∧ ∀𝑘 ∈ ω (‘suc 𝑘) ∈ (𝑘𝐹(𝑘)))) → ∃𝑔𝑧𝑥 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧))
16477, 163exlimddv 1860 . . . 4 (𝑓:ω–1-1-onto𝐴 → ∃𝑔𝑧𝑥 (𝑧 ≠ ∅ → (𝑔𝑧) ∈ 𝑧))
165164exlimiv 1855 . . 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 384  w3a 1036   = wceq 1480  wex 1701  wcel 1987  wne 2790  wral 2907  wrex 2908  Vcvv 3189  cdif 3556  cun 3557  wss 3559  c0 3896  𝒫 cpw 4135  {csn 4153   cuni 4407   class class class wbr 4618  cmpt 4678   × cxp 5077  ccnv 5078  ran crn 5080  suc csuc 5689  wf 5848  ontowfo 5850  1-1-ontowf1o 5851  cfv 5852  (class class class)co 6610  cmpt2 6612  ωcom 7019  cen 7904  cdom 7905  csdm 7906  Fincfn 7907
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-dc 9220
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-om 7020  df-1st 7120  df-2nd 7121  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-oadd 7516  df-er 7694  df-en 7908  df-dom 7909  df-sdom 7910  df-fin 7911
This theorem is referenced by:  axcc  9232
  Copyright terms: Public domain W3C validator