Proof of Theorem omctfn
Step | Hyp | Ref
| Expression |
1 | | omiunct.cc |
. 2
⊢ (𝜑 →
CCHOICE) |
2 | | fnmap 6589 |
. . . . 5
⊢
↑𝑚 Fn (V × V) |
3 | | omiunct.g |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ω) → ∃𝑔 𝑔:ω–onto→(𝐵 ⊔ 1o)) |
4 | | omex 4546 |
. . . . . . . 8
⊢ ω
∈ V |
5 | | fornex 6053 |
. . . . . . . 8
⊢ (ω
∈ V → (𝑔:ω–onto→(𝐵 ⊔ 1o) → (𝐵 ⊔ 1o) ∈
V)) |
6 | 4, 5 | ax-mp 5 |
. . . . . . 7
⊢ (𝑔:ω–onto→(𝐵 ⊔ 1o) → (𝐵 ⊔ 1o) ∈
V) |
7 | 6 | adantl 275 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ω) ∧ 𝑔:ω–onto→(𝐵 ⊔ 1o)) → (𝐵 ⊔ 1o) ∈
V) |
8 | 3, 7 | exlimddv 1875 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ω) → (𝐵 ⊔ 1o) ∈
V) |
9 | 4 | a1i 9 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ω) → ω ∈
V) |
10 | | fnovex 5844 |
. . . . 5
⊢ ((
↑𝑚 Fn (V × V) ∧ (𝐵 ⊔ 1o) ∈ V ∧
ω ∈ V) → ((𝐵 ⊔ 1o)
↑𝑚 ω) ∈ V) |
11 | 2, 8, 9, 10 | mp3an2i 1321 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ω) → ((𝐵 ⊔ 1o)
↑𝑚 ω) ∈ V) |
12 | | rabexg 4103 |
. . . 4
⊢ (((𝐵 ⊔ 1o)
↑𝑚 ω) ∈ V → {𝑔 ∈ ((𝐵 ⊔ 1o)
↑𝑚 ω) ∣ 𝑔:ω–onto→(𝐵 ⊔ 1o)} ∈
V) |
13 | 11, 12 | syl 14 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ω) → {𝑔 ∈ ((𝐵 ⊔ 1o)
↑𝑚 ω) ∣ 𝑔:ω–onto→(𝐵 ⊔ 1o)} ∈
V) |
14 | 13 | ralrimiva 2527 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ ω {𝑔 ∈ ((𝐵 ⊔ 1o)
↑𝑚 ω) ∣ 𝑔:ω–onto→(𝐵 ⊔ 1o)} ∈
V) |
15 | 4 | enref 6699 |
. . 3
⊢ ω
≈ ω |
16 | 15 | a1i 9 |
. 2
⊢ (𝜑 → ω ≈
ω) |
17 | | foeq1 5381 |
. 2
⊢ (𝑔 = (𝑓‘𝑥) → (𝑔:ω–onto→(𝐵 ⊔ 1o) ↔ (𝑓‘𝑥):ω–onto→(𝐵 ⊔ 1o))) |
18 | | fof 5385 |
. . . . . . . . . 10
⊢ (𝑔:ω–onto→(𝐵 ⊔ 1o) → 𝑔:ω⟶(𝐵 ⊔
1o)) |
19 | 18 | adantl 275 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ω) ∧ 𝑔:ω–onto→(𝐵 ⊔ 1o)) → 𝑔:ω⟶(𝐵 ⊔
1o)) |
20 | | elmapg 6595 |
. . . . . . . . . 10
⊢ (((𝐵 ⊔ 1o) ∈
V ∧ ω ∈ V) → (𝑔 ∈ ((𝐵 ⊔ 1o)
↑𝑚 ω) ↔ 𝑔:ω⟶(𝐵 ⊔ 1o))) |
21 | 7, 4, 20 | sylancl 410 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ω) ∧ 𝑔:ω–onto→(𝐵 ⊔ 1o)) → (𝑔 ∈ ((𝐵 ⊔ 1o)
↑𝑚 ω) ↔ 𝑔:ω⟶(𝐵 ⊔ 1o))) |
22 | 19, 21 | mpbird 166 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ω) ∧ 𝑔:ω–onto→(𝐵 ⊔ 1o)) → 𝑔 ∈ ((𝐵 ⊔ 1o)
↑𝑚 ω)) |
23 | | simpr 109 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ω) ∧ 𝑔:ω–onto→(𝐵 ⊔ 1o)) → 𝑔:ω–onto→(𝐵 ⊔ 1o)) |
24 | 22, 23 | jca 304 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ω) ∧ 𝑔:ω–onto→(𝐵 ⊔ 1o)) → (𝑔 ∈ ((𝐵 ⊔ 1o)
↑𝑚 ω) ∧ 𝑔:ω–onto→(𝐵 ⊔ 1o))) |
25 | 24 | ex 114 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ω) → (𝑔:ω–onto→(𝐵 ⊔ 1o) → (𝑔 ∈ ((𝐵 ⊔ 1o)
↑𝑚 ω) ∧ 𝑔:ω–onto→(𝐵 ⊔ 1o)))) |
26 | 25 | eximdv 1857 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ω) → (∃𝑔 𝑔:ω–onto→(𝐵 ⊔ 1o) → ∃𝑔(𝑔 ∈ ((𝐵 ⊔ 1o)
↑𝑚 ω) ∧ 𝑔:ω–onto→(𝐵 ⊔ 1o)))) |
27 | | df-rex 2438 |
. . . . 5
⊢
(∃𝑔 ∈
((𝐵 ⊔ 1o)
↑𝑚 ω)𝑔:ω–onto→(𝐵 ⊔ 1o) ↔ ∃𝑔(𝑔 ∈ ((𝐵 ⊔ 1o)
↑𝑚 ω) ∧ 𝑔:ω–onto→(𝐵 ⊔ 1o))) |
28 | 26, 27 | syl6ibr 161 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ω) → (∃𝑔 𝑔:ω–onto→(𝐵 ⊔ 1o) → ∃𝑔 ∈ ((𝐵 ⊔ 1o)
↑𝑚 ω)𝑔:ω–onto→(𝐵 ⊔ 1o))) |
29 | 3, 28 | mpd 13 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ω) → ∃𝑔 ∈ ((𝐵 ⊔ 1o)
↑𝑚 ω)𝑔:ω–onto→(𝐵 ⊔ 1o)) |
30 | 29 | ralrimiva 2527 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ ω ∃𝑔 ∈ ((𝐵 ⊔ 1o)
↑𝑚 ω)𝑔:ω–onto→(𝐵 ⊔ 1o)) |
31 | 1, 14, 16, 17, 30 | cc4n 7170 |
1
⊢ (𝜑 → ∃𝑓(𝑓 Fn ω ∧ ∀𝑥 ∈ ω (𝑓‘𝑥):ω–onto→(𝐵 ⊔ 1o))) |