Proof of Theorem endjusym
Step | Hyp | Ref
| Expression |
1 | | djulf1o 7033 |
. . . . . . . . 9
⊢
inl:V–1-1-onto→({∅} × V) |
2 | | f1of1 5439 |
. . . . . . . . 9
⊢
(inl:V–1-1-onto→({∅} × V) → inl:V–1-1→({∅} × V)) |
3 | 1, 2 | ax-mp 5 |
. . . . . . . 8
⊢
inl:V–1-1→({∅}
× V) |
4 | | ssv 3169 |
. . . . . . . 8
⊢ 𝐴 ⊆ V |
5 | | f1ores 5455 |
. . . . . . . 8
⊢
((inl:V–1-1→({∅}
× V) ∧ 𝐴 ⊆
V) → (inl ↾ 𝐴):𝐴–1-1-onto→(inl
“ 𝐴)) |
6 | 3, 4, 5 | mp2an 424 |
. . . . . . 7
⊢ (inl
↾ 𝐴):𝐴–1-1-onto→(inl
“ 𝐴) |
7 | | f1oeng 6733 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ (inl ↾ 𝐴):𝐴–1-1-onto→(inl
“ 𝐴)) → 𝐴 ≈ (inl “ 𝐴)) |
8 | 6, 7 | mpan2 423 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → 𝐴 ≈ (inl “ 𝐴)) |
9 | 8 | ensymd 6759 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (inl “ 𝐴) ≈ 𝐴) |
10 | | djurf1o 7034 |
. . . . . . . 8
⊢
inr:V–1-1-onto→({1o} × V) |
11 | | f1of1 5439 |
. . . . . . . 8
⊢
(inr:V–1-1-onto→({1o} × V) →
inr:V–1-1→({1o}
× V)) |
12 | 10, 11 | ax-mp 5 |
. . . . . . 7
⊢
inr:V–1-1→({1o} × V) |
13 | | f1ores 5455 |
. . . . . . 7
⊢
((inr:V–1-1→({1o} × V) ∧ 𝐴 ⊆ V) → (inr ↾
𝐴):𝐴–1-1-onto→(inr
“ 𝐴)) |
14 | 12, 4, 13 | mp2an 424 |
. . . . . 6
⊢ (inr
↾ 𝐴):𝐴–1-1-onto→(inr
“ 𝐴) |
15 | | f1oeng 6733 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ (inr ↾ 𝐴):𝐴–1-1-onto→(inr
“ 𝐴)) → 𝐴 ≈ (inr “ 𝐴)) |
16 | 14, 15 | mpan2 423 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → 𝐴 ≈ (inr “ 𝐴)) |
17 | | entr 6760 |
. . . . 5
⊢ (((inl
“ 𝐴) ≈ 𝐴 ∧ 𝐴 ≈ (inr “ 𝐴)) → (inl “ 𝐴) ≈ (inr “ 𝐴)) |
18 | 9, 16, 17 | syl2anc 409 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → (inl “ 𝐴) ≈ (inr “ 𝐴)) |
19 | 18 | adantr 274 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (inl “ 𝐴) ≈ (inr “ 𝐴)) |
20 | | ssv 3169 |
. . . . . . . 8
⊢ 𝐵 ⊆ V |
21 | | f1ores 5455 |
. . . . . . . 8
⊢
((inr:V–1-1→({1o} × V) ∧ 𝐵 ⊆ V) → (inr ↾
𝐵):𝐵–1-1-onto→(inr
“ 𝐵)) |
22 | 12, 20, 21 | mp2an 424 |
. . . . . . 7
⊢ (inr
↾ 𝐵):𝐵–1-1-onto→(inr
“ 𝐵) |
23 | | f1oeng 6733 |
. . . . . . 7
⊢ ((𝐵 ∈ 𝑊 ∧ (inr ↾ 𝐵):𝐵–1-1-onto→(inr
“ 𝐵)) → 𝐵 ≈ (inr “ 𝐵)) |
24 | 22, 23 | mpan2 423 |
. . . . . 6
⊢ (𝐵 ∈ 𝑊 → 𝐵 ≈ (inr “ 𝐵)) |
25 | 24 | adantl 275 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐵 ≈ (inr “ 𝐵)) |
26 | 25 | ensymd 6759 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (inr “ 𝐵) ≈ 𝐵) |
27 | | f1ores 5455 |
. . . . . . 7
⊢
((inl:V–1-1→({∅}
× V) ∧ 𝐵 ⊆
V) → (inl ↾ 𝐵):𝐵–1-1-onto→(inl
“ 𝐵)) |
28 | 3, 20, 27 | mp2an 424 |
. . . . . 6
⊢ (inl
↾ 𝐵):𝐵–1-1-onto→(inl
“ 𝐵) |
29 | | f1oeng 6733 |
. . . . . 6
⊢ ((𝐵 ∈ 𝑊 ∧ (inl ↾ 𝐵):𝐵–1-1-onto→(inl
“ 𝐵)) → 𝐵 ≈ (inl “ 𝐵)) |
30 | 28, 29 | mpan2 423 |
. . . . 5
⊢ (𝐵 ∈ 𝑊 → 𝐵 ≈ (inl “ 𝐵)) |
31 | 30 | adantl 275 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐵 ≈ (inl “ 𝐵)) |
32 | | entr 6760 |
. . . 4
⊢ (((inr
“ 𝐵) ≈ 𝐵 ∧ 𝐵 ≈ (inl “ 𝐵)) → (inr “ 𝐵) ≈ (inl “ 𝐵)) |
33 | 26, 31, 32 | syl2anc 409 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (inr “ 𝐵) ≈ (inl “ 𝐵)) |
34 | | djuin 7039 |
. . . 4
⊢ ((inl
“ 𝐴) ∩ (inr
“ 𝐵)) =
∅ |
35 | 34 | a1i 9 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((inl “ 𝐴) ∩ (inr “ 𝐵)) = ∅) |
36 | | incom 3319 |
. . . . 5
⊢ ((inl
“ 𝐵) ∩ (inr
“ 𝐴)) = ((inr “
𝐴) ∩ (inl “ 𝐵)) |
37 | | djuin 7039 |
. . . . 5
⊢ ((inl
“ 𝐵) ∩ (inr
“ 𝐴)) =
∅ |
38 | 36, 37 | eqtr3i 2193 |
. . . 4
⊢ ((inr
“ 𝐴) ∩ (inl
“ 𝐵)) =
∅ |
39 | 38 | a1i 9 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((inr “ 𝐴) ∩ (inl “ 𝐵)) = ∅) |
40 | | unen 6792 |
. . 3
⊢ ((((inl
“ 𝐴) ≈ (inr
“ 𝐴) ∧ (inr
“ 𝐵) ≈ (inl
“ 𝐵)) ∧ (((inl
“ 𝐴) ∩ (inr
“ 𝐵)) = ∅ ∧
((inr “ 𝐴) ∩ (inl
“ 𝐵)) = ∅))
→ ((inl “ 𝐴)
∪ (inr “ 𝐵))
≈ ((inr “ 𝐴)
∪ (inl “ 𝐵))) |
41 | 19, 33, 35, 39, 40 | syl22anc 1234 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((inl “ 𝐴) ∪ (inr “ 𝐵)) ≈ ((inr “ 𝐴) ∪ (inl “ 𝐵))) |
42 | | djuun 7042 |
. 2
⊢ ((inl
“ 𝐴) ∪ (inr
“ 𝐵)) = (𝐴 ⊔ 𝐵) |
43 | | uncom 3271 |
. . 3
⊢ ((inr
“ 𝐴) ∪ (inl
“ 𝐵)) = ((inl “
𝐵) ∪ (inr “ 𝐴)) |
44 | | djuun 7042 |
. . 3
⊢ ((inl
“ 𝐵) ∪ (inr
“ 𝐴)) = (𝐵 ⊔ 𝐴) |
45 | 43, 44 | eqtri 2191 |
. 2
⊢ ((inr
“ 𝐴) ∪ (inl
“ 𝐵)) = (𝐵 ⊔ 𝐴) |
46 | 41, 42, 45 | 3brtr3g 4020 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ⊔ 𝐵) ≈ (𝐵 ⊔ 𝐴)) |