Step | Hyp | Ref
| Expression |
1 | | 2onn 6489 |
. . . . . . . 8
⊢
2o ∈ ω |
2 | | nnfi 6838 |
. . . . . . . 8
⊢
(2o ∈ ω → 2o ∈
Fin) |
3 | | finct 7081 |
. . . . . . . 8
⊢
(2o ∈ Fin → ∃𝑗 𝑗:ω–onto→(2o ⊔
1o)) |
4 | 1, 2, 3 | mp2b 8 |
. . . . . . 7
⊢
∃𝑗 𝑗:ω–onto→(2o ⊔
1o) |
5 | 4 | a1i 9 |
. . . . . 6
⊢ ((𝑓:ω–onto→(𝐴 ⊔ 1o) ∧ 𝑔:ω–onto→(𝐵 ⊔ 1o)) →
∃𝑗 𝑗:ω–onto→(2o ⊔
1o)) |
6 | | simpr 109 |
. . . . . . . . 9
⊢ (((𝑓:ω–onto→(𝐴 ⊔ 1o) ∧ 𝑔:ω–onto→(𝐵 ⊔ 1o)) ∧ 𝑗:ω–onto→(2o ⊔ 1o)) →
𝑗:ω–onto→(2o ⊔
1o)) |
7 | | df2o3 6398 |
. . . . . . . . . 10
⊢
2o = {∅, 1o} |
8 | | djueq1 7005 |
. . . . . . . . . 10
⊢
(2o = {∅, 1o} → (2o ⊔
1o) = ({∅, 1o} ⊔
1o)) |
9 | | foeq3 5408 |
. . . . . . . . . 10
⊢
((2o ⊔ 1o) = ({∅, 1o}
⊔ 1o) → (𝑗:ω–onto→(2o ⊔ 1o) ↔
𝑗:ω–onto→({∅, 1o} ⊔
1o))) |
10 | 7, 8, 9 | mp2b 8 |
. . . . . . . . 9
⊢ (𝑗:ω–onto→(2o ⊔ 1o) ↔
𝑗:ω–onto→({∅, 1o} ⊔
1o)) |
11 | 6, 10 | sylib 121 |
. . . . . . . 8
⊢ (((𝑓:ω–onto→(𝐴 ⊔ 1o) ∧ 𝑔:ω–onto→(𝐵 ⊔ 1o)) ∧ 𝑗:ω–onto→(2o ⊔ 1o)) →
𝑗:ω–onto→({∅, 1o} ⊔
1o)) |
12 | | simplll 523 |
. . . . . . . . . . . 12
⊢ ((((𝑓:ω–onto→(𝐴 ⊔ 1o) ∧ 𝑔:ω–onto→(𝐵 ⊔ 1o)) ∧ 𝑗:ω–onto→(2o ⊔ 1o)) ∧
𝑥 = ∅) → 𝑓:ω–onto→(𝐴 ⊔ 1o)) |
13 | | iftrue 3525 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = ∅ → if(𝑥 = ∅, 𝑓, 𝑔) = 𝑓) |
14 | | eqidd 2166 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = ∅ → ω =
ω) |
15 | | iftrue 3525 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = ∅ → if(𝑥 = ∅, 𝐴, 𝐵) = 𝐴) |
16 | | djueq1 7005 |
. . . . . . . . . . . . . . 15
⊢ (if(𝑥 = ∅, 𝐴, 𝐵) = 𝐴 → (if(𝑥 = ∅, 𝐴, 𝐵) ⊔ 1o) = (𝐴 ⊔
1o)) |
17 | 15, 16 | syl 14 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = ∅ → (if(𝑥 = ∅, 𝐴, 𝐵) ⊔ 1o) = (𝐴 ⊔
1o)) |
18 | 13, 14, 17 | foeq123d 5426 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ∅ → (if(𝑥 = ∅, 𝑓, 𝑔):ω–onto→(if(𝑥 = ∅, 𝐴, 𝐵) ⊔ 1o) ↔ 𝑓:ω–onto→(𝐴 ⊔ 1o))) |
19 | 18 | adantl 275 |
. . . . . . . . . . . 12
⊢ ((((𝑓:ω–onto→(𝐴 ⊔ 1o) ∧ 𝑔:ω–onto→(𝐵 ⊔ 1o)) ∧ 𝑗:ω–onto→(2o ⊔ 1o)) ∧
𝑥 = ∅) →
(if(𝑥 = ∅, 𝑓, 𝑔):ω–onto→(if(𝑥 = ∅, 𝐴, 𝐵) ⊔ 1o) ↔ 𝑓:ω–onto→(𝐴 ⊔ 1o))) |
20 | 12, 19 | mpbird 166 |
. . . . . . . . . . 11
⊢ ((((𝑓:ω–onto→(𝐴 ⊔ 1o) ∧ 𝑔:ω–onto→(𝐵 ⊔ 1o)) ∧ 𝑗:ω–onto→(2o ⊔ 1o)) ∧
𝑥 = ∅) →
if(𝑥 = ∅, 𝑓, 𝑔):ω–onto→(if(𝑥 = ∅, 𝐴, 𝐵) ⊔ 1o)) |
21 | 20 | ex 114 |
. . . . . . . . . 10
⊢ (((𝑓:ω–onto→(𝐴 ⊔ 1o) ∧ 𝑔:ω–onto→(𝐵 ⊔ 1o)) ∧ 𝑗:ω–onto→(2o ⊔ 1o)) →
(𝑥 = ∅ →
if(𝑥 = ∅, 𝑓, 𝑔):ω–onto→(if(𝑥 = ∅, 𝐴, 𝐵) ⊔ 1o))) |
22 | | simpllr 524 |
. . . . . . . . . . . 12
⊢ ((((𝑓:ω–onto→(𝐴 ⊔ 1o) ∧ 𝑔:ω–onto→(𝐵 ⊔ 1o)) ∧ 𝑗:ω–onto→(2o ⊔ 1o)) ∧
𝑥 = 1o) →
𝑔:ω–onto→(𝐵 ⊔ 1o)) |
23 | | 1n0 6400 |
. . . . . . . . . . . . . . . 16
⊢
1o ≠ ∅ |
24 | 23 | neii 2338 |
. . . . . . . . . . . . . . 15
⊢ ¬
1o = ∅ |
25 | | eqeq1 2172 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 1o → (𝑥 = ∅ ↔ 1o
= ∅)) |
26 | 24, 25 | mtbiri 665 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 1o → ¬
𝑥 =
∅) |
27 | 26 | adantl 275 |
. . . . . . . . . . . . 13
⊢ ((((𝑓:ω–onto→(𝐴 ⊔ 1o) ∧ 𝑔:ω–onto→(𝐵 ⊔ 1o)) ∧ 𝑗:ω–onto→(2o ⊔ 1o)) ∧
𝑥 = 1o) →
¬ 𝑥 =
∅) |
28 | | iffalse 3528 |
. . . . . . . . . . . . . 14
⊢ (¬
𝑥 = ∅ → if(𝑥 = ∅, 𝑓, 𝑔) = 𝑔) |
29 | | eqidd 2166 |
. . . . . . . . . . . . . 14
⊢ (¬
𝑥 = ∅ → ω
= ω) |
30 | | iffalse 3528 |
. . . . . . . . . . . . . . 15
⊢ (¬
𝑥 = ∅ → if(𝑥 = ∅, 𝐴, 𝐵) = 𝐵) |
31 | | djueq1 7005 |
. . . . . . . . . . . . . . 15
⊢ (if(𝑥 = ∅, 𝐴, 𝐵) = 𝐵 → (if(𝑥 = ∅, 𝐴, 𝐵) ⊔ 1o) = (𝐵 ⊔
1o)) |
32 | 30, 31 | syl 14 |
. . . . . . . . . . . . . 14
⊢ (¬
𝑥 = ∅ →
(if(𝑥 = ∅, 𝐴, 𝐵) ⊔ 1o) = (𝐵 ⊔
1o)) |
33 | 28, 29, 32 | foeq123d 5426 |
. . . . . . . . . . . . 13
⊢ (¬
𝑥 = ∅ →
(if(𝑥 = ∅, 𝑓, 𝑔):ω–onto→(if(𝑥 = ∅, 𝐴, 𝐵) ⊔ 1o) ↔ 𝑔:ω–onto→(𝐵 ⊔ 1o))) |
34 | 27, 33 | syl 14 |
. . . . . . . . . . . 12
⊢ ((((𝑓:ω–onto→(𝐴 ⊔ 1o) ∧ 𝑔:ω–onto→(𝐵 ⊔ 1o)) ∧ 𝑗:ω–onto→(2o ⊔ 1o)) ∧
𝑥 = 1o) →
(if(𝑥 = ∅, 𝑓, 𝑔):ω–onto→(if(𝑥 = ∅, 𝐴, 𝐵) ⊔ 1o) ↔ 𝑔:ω–onto→(𝐵 ⊔ 1o))) |
35 | 22, 34 | mpbird 166 |
. . . . . . . . . . 11
⊢ ((((𝑓:ω–onto→(𝐴 ⊔ 1o) ∧ 𝑔:ω–onto→(𝐵 ⊔ 1o)) ∧ 𝑗:ω–onto→(2o ⊔ 1o)) ∧
𝑥 = 1o) →
if(𝑥 = ∅, 𝑓, 𝑔):ω–onto→(if(𝑥 = ∅, 𝐴, 𝐵) ⊔ 1o)) |
36 | 35 | ex 114 |
. . . . . . . . . 10
⊢ (((𝑓:ω–onto→(𝐴 ⊔ 1o) ∧ 𝑔:ω–onto→(𝐵 ⊔ 1o)) ∧ 𝑗:ω–onto→(2o ⊔ 1o)) →
(𝑥 = 1o →
if(𝑥 = ∅, 𝑓, 𝑔):ω–onto→(if(𝑥 = ∅, 𝐴, 𝐵) ⊔ 1o))) |
37 | 21, 36 | jaod 707 |
. . . . . . . . 9
⊢ (((𝑓:ω–onto→(𝐴 ⊔ 1o) ∧ 𝑔:ω–onto→(𝐵 ⊔ 1o)) ∧ 𝑗:ω–onto→(2o ⊔ 1o)) →
((𝑥 = ∅ ∨ 𝑥 = 1o) →
if(𝑥 = ∅, 𝑓, 𝑔):ω–onto→(if(𝑥 = ∅, 𝐴, 𝐵) ⊔ 1o))) |
38 | | elpri 3599 |
. . . . . . . . 9
⊢ (𝑥 ∈ {∅, 1o}
→ (𝑥 = ∅ ∨
𝑥 =
1o)) |
39 | 37, 38 | impel 278 |
. . . . . . . 8
⊢ ((((𝑓:ω–onto→(𝐴 ⊔ 1o) ∧ 𝑔:ω–onto→(𝐵 ⊔ 1o)) ∧ 𝑗:ω–onto→(2o ⊔ 1o)) ∧
𝑥 ∈ {∅,
1o}) → if(𝑥
= ∅, 𝑓, 𝑔):ω–onto→(if(𝑥 = ∅, 𝐴, 𝐵) ⊔ 1o)) |
40 | 11, 39 | ctiunct 12373 |
. . . . . . 7
⊢ (((𝑓:ω–onto→(𝐴 ⊔ 1o) ∧ 𝑔:ω–onto→(𝐵 ⊔ 1o)) ∧ 𝑗:ω–onto→(2o ⊔ 1o)) →
∃ℎ ℎ:ω–onto→(∪ 𝑥 ∈ {∅,
1o}if(𝑥 =
∅, 𝐴, 𝐵) ⊔
1o)) |
41 | | 0lt2o 6409 |
. . . . . . . . . 10
⊢ ∅
∈ 2o |
42 | | 1lt2o 6410 |
. . . . . . . . . 10
⊢
1o ∈ 2o |
43 | 26 | iffalsed 3530 |
. . . . . . . . . . 11
⊢ (𝑥 = 1o → if(𝑥 = ∅, 𝐴, 𝐵) = 𝐵) |
44 | 15, 43 | iunxprg 3946 |
. . . . . . . . . 10
⊢ ((∅
∈ 2o ∧ 1o ∈ 2o) → ∪ 𝑥 ∈ {∅, 1o}if(𝑥 = ∅, 𝐴, 𝐵) = (𝐴 ∪ 𝐵)) |
45 | 41, 42, 44 | mp2an 423 |
. . . . . . . . 9
⊢ ∪ 𝑥 ∈ {∅, 1o}if(𝑥 = ∅, 𝐴, 𝐵) = (𝐴 ∪ 𝐵) |
46 | | djueq1 7005 |
. . . . . . . . 9
⊢ (∪ 𝑥 ∈ {∅, 1o}if(𝑥 = ∅, 𝐴, 𝐵) = (𝐴 ∪ 𝐵) → (∪ 𝑥 ∈ {∅, 1o}if(𝑥 = ∅, 𝐴, 𝐵) ⊔ 1o) = ((𝐴 ∪ 𝐵) ⊔ 1o)) |
47 | | foeq3 5408 |
. . . . . . . . 9
⊢
((∪ 𝑥 ∈ {∅, 1o}if(𝑥 = ∅, 𝐴, 𝐵) ⊔ 1o) = ((𝐴 ∪ 𝐵) ⊔ 1o) → (ℎ:ω–onto→(∪ 𝑥 ∈ {∅,
1o}if(𝑥 =
∅, 𝐴, 𝐵) ⊔ 1o) ↔
ℎ:ω–onto→((𝐴 ∪ 𝐵) ⊔ 1o))) |
48 | 45, 46, 47 | mp2b 8 |
. . . . . . . 8
⊢ (ℎ:ω–onto→(∪ 𝑥 ∈ {∅,
1o}if(𝑥 =
∅, 𝐴, 𝐵) ⊔ 1o) ↔
ℎ:ω–onto→((𝐴 ∪ 𝐵) ⊔ 1o)) |
49 | 48 | exbii 1593 |
. . . . . . 7
⊢
(∃ℎ ℎ:ω–onto→(∪ 𝑥 ∈ {∅,
1o}if(𝑥 =
∅, 𝐴, 𝐵) ⊔ 1o) ↔
∃ℎ ℎ:ω–onto→((𝐴 ∪ 𝐵) ⊔ 1o)) |
50 | 40, 49 | sylib 121 |
. . . . . 6
⊢ (((𝑓:ω–onto→(𝐴 ⊔ 1o) ∧ 𝑔:ω–onto→(𝐵 ⊔ 1o)) ∧ 𝑗:ω–onto→(2o ⊔ 1o)) →
∃ℎ ℎ:ω–onto→((𝐴 ∪ 𝐵) ⊔ 1o)) |
51 | 5, 50 | exlimddv 1886 |
. . . . 5
⊢ ((𝑓:ω–onto→(𝐴 ⊔ 1o) ∧ 𝑔:ω–onto→(𝐵 ⊔ 1o)) →
∃ℎ ℎ:ω–onto→((𝐴 ∪ 𝐵) ⊔ 1o)) |
52 | 51 | ex 114 |
. . . 4
⊢ (𝑓:ω–onto→(𝐴 ⊔ 1o) → (𝑔:ω–onto→(𝐵 ⊔ 1o) → ∃ℎ ℎ:ω–onto→((𝐴 ∪ 𝐵) ⊔ 1o))) |
53 | 52 | exlimiv 1586 |
. . 3
⊢
(∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o) → (𝑔:ω–onto→(𝐵 ⊔ 1o) → ∃ℎ ℎ:ω–onto→((𝐴 ∪ 𝐵) ⊔ 1o))) |
54 | 53 | exlimdv 1807 |
. 2
⊢
(∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o) →
(∃𝑔 𝑔:ω–onto→(𝐵 ⊔ 1o) → ∃ℎ ℎ:ω–onto→((𝐴 ∪ 𝐵) ⊔ 1o))) |
55 | 54 | imp 123 |
1
⊢
((∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o) ∧ ∃𝑔 𝑔:ω–onto→(𝐵 ⊔ 1o)) →
∃ℎ ℎ:ω–onto→((𝐴 ∪ 𝐵) ⊔ 1o)) |