Proof of Theorem bj-2upln1upl
Step | Hyp | Ref
| Expression |
1 | | xpundi 5417 |
. . . . . . 7
⊢
({∅} × (tag 𝐴 ∪ tag 𝐶)) = (({∅} × tag 𝐴) ∪ ({∅} × tag
𝐶)) |
2 | 1 | difeq2i 3948 |
. . . . . 6
⊢
(({1o} × tag 𝐵) ∖ ({∅} × (tag 𝐴 ∪ tag 𝐶))) = (({1o} × tag 𝐵) ∖ (({∅} ×
tag 𝐴) ∪ ({∅}
× tag 𝐶))) |
3 | | incom 4028 |
. . . . . . . . 9
⊢
(({∅} × (tag 𝐴 ∪ tag 𝐶)) ∩ ({1o} × tag 𝐵)) = (({1o} ×
tag 𝐵) ∩ ({∅}
× (tag 𝐴 ∪ tag
𝐶))) |
4 | | bj-disjsn01 33510 |
. . . . . . . . . 10
⊢
({∅} ∩ {1o}) = ∅ |
5 | | xpdisj1 5809 |
. . . . . . . . . 10
⊢
(({∅} ∩ {1o}) = ∅ → (({∅} ×
(tag 𝐴 ∪ tag 𝐶)) ∩ ({1o}
× tag 𝐵)) =
∅) |
6 | 4, 5 | ax-mp 5 |
. . . . . . . . 9
⊢
(({∅} × (tag 𝐴 ∪ tag 𝐶)) ∩ ({1o} × tag 𝐵)) = ∅ |
7 | 3, 6 | eqtr3i 2804 |
. . . . . . . 8
⊢
(({1o} × tag 𝐵) ∩ ({∅} × (tag 𝐴 ∪ tag 𝐶))) = ∅ |
8 | | disjdif2 4271 |
. . . . . . . 8
⊢
((({1o} × tag 𝐵) ∩ ({∅} × (tag 𝐴 ∪ tag 𝐶))) = ∅ → (({1o}
× tag 𝐵) ∖
({∅} × (tag 𝐴
∪ tag 𝐶))) =
({1o} × tag 𝐵)) |
9 | 7, 8 | ax-mp 5 |
. . . . . . 7
⊢
(({1o} × tag 𝐵) ∖ ({∅} × (tag 𝐴 ∪ tag 𝐶))) = ({1o} × tag 𝐵) |
10 | | 1oex 7851 |
. . . . . . . . . 10
⊢
1o ∈ V |
11 | 10 | snnz 4542 |
. . . . . . . . 9
⊢
{1o} ≠ ∅ |
12 | | bj-tagn0 33539 |
. . . . . . . . 9
⊢ tag 𝐵 ≠ ∅ |
13 | 11, 12 | pm3.2i 464 |
. . . . . . . 8
⊢
({1o} ≠ ∅ ∧ tag 𝐵 ≠ ∅) |
14 | | xpnz 5807 |
. . . . . . . 8
⊢
(({1o} ≠ ∅ ∧ tag 𝐵 ≠ ∅) ↔ ({1o}
× tag 𝐵) ≠
∅) |
15 | 13, 14 | mpbi 222 |
. . . . . . 7
⊢
({1o} × tag 𝐵) ≠ ∅ |
16 | 9, 15 | eqnetri 3039 |
. . . . . 6
⊢
(({1o} × tag 𝐵) ∖ ({∅} × (tag 𝐴 ∪ tag 𝐶))) ≠ ∅ |
17 | 2, 16 | eqnetrri 3040 |
. . . . 5
⊢
(({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag
𝐶))) ≠
∅ |
18 | | 0pss 4239 |
. . . . 5
⊢ (∅
⊊ (({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag
𝐶))) ↔
(({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag
𝐶))) ≠
∅) |
19 | 17, 18 | mpbir 223 |
. . . 4
⊢ ∅
⊊ (({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag
𝐶))) |
20 | | ssun2 4000 |
. . . . . . . 8
⊢
({∅} × tag 𝐶) ⊆ (({∅} × tag 𝐴) ∪ ({∅} × tag
𝐶)) |
21 | | sscon 3967 |
. . . . . . . 8
⊢
(({∅} × tag 𝐶) ⊆ (({∅} × tag 𝐴) ∪ ({∅} × tag
𝐶)) →
(({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag
𝐶))) ⊆
(({1o} × tag 𝐵) ∖ ({∅} × tag 𝐶))) |
22 | 20, 21 | ax-mp 5 |
. . . . . . 7
⊢
(({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag
𝐶))) ⊆
(({1o} × tag 𝐵) ∖ ({∅} × tag 𝐶)) |
23 | | ssun2 4000 |
. . . . . . . 8
⊢
({1o} × tag 𝐵) ⊆ (({∅} × tag 𝐴) ∪ ({1o} ×
tag 𝐵)) |
24 | | ssdif 3968 |
. . . . . . . 8
⊢
(({1o} × tag 𝐵) ⊆ (({∅} × tag 𝐴) ∪ ({1o} ×
tag 𝐵)) →
(({1o} × tag 𝐵) ∖ ({∅} × tag 𝐶)) ⊆ ((({∅} ×
tag 𝐴) ∪
({1o} × tag 𝐵)) ∖ ({∅} × tag 𝐶))) |
25 | 23, 24 | ax-mp 5 |
. . . . . . 7
⊢
(({1o} × tag 𝐵) ∖ ({∅} × tag 𝐶)) ⊆ ((({∅} ×
tag 𝐴) ∪
({1o} × tag 𝐵)) ∖ ({∅} × tag 𝐶)) |
26 | 22, 25 | sstri 3830 |
. . . . . 6
⊢
(({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag
𝐶))) ⊆ ((({∅}
× tag 𝐴) ∪
({1o} × tag 𝐵)) ∖ ({∅} × tag 𝐶)) |
27 | | df-bj-2upl 33571 |
. . . . . . . 8
⊢
⦅𝐴, 𝐵⦆ = (⦅𝐴⦆ ∪ ({1o}
× tag 𝐵)) |
28 | | df-bj-1upl 33558 |
. . . . . . . . 9
⊢
⦅𝐴⦆ =
({∅} × tag 𝐴) |
29 | 28 | uneq1i 3986 |
. . . . . . . 8
⊢
(⦅𝐴⦆
∪ ({1o} × tag 𝐵)) = (({∅} × tag 𝐴) ∪ ({1o} ×
tag 𝐵)) |
30 | 27, 29 | eqtri 2802 |
. . . . . . 7
⊢
⦅𝐴, 𝐵⦆ = (({∅} ×
tag 𝐴) ∪
({1o} × tag 𝐵)) |
31 | 30 | difeq1i 3947 |
. . . . . 6
⊢
(⦅𝐴, 𝐵⦆ ∖ ({∅}
× tag 𝐶)) =
((({∅} × tag 𝐴)
∪ ({1o} × tag 𝐵)) ∖ ({∅} × tag 𝐶)) |
32 | 26, 31 | sseqtr4i 3857 |
. . . . 5
⊢
(({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag
𝐶))) ⊆ (⦅𝐴, 𝐵⦆ ∖ ({∅} × tag 𝐶)) |
33 | | df-bj-1upl 33558 |
. . . . . 6
⊢
⦅𝐶⦆ =
({∅} × tag 𝐶) |
34 | 33 | difeq2i 3948 |
. . . . 5
⊢
(⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆) = (⦅𝐴, 𝐵⦆ ∖ ({∅} × tag 𝐶)) |
35 | 32, 34 | sseqtr4i 3857 |
. . . 4
⊢
(({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag
𝐶))) ⊆ (⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆) |
36 | | psssstr 3935 |
. . . 4
⊢ ((∅
⊊ (({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag
𝐶))) ∧
(({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag
𝐶))) ⊆ (⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆)) → ∅ ⊊
(⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆)) |
37 | 19, 35, 36 | mp2an 682 |
. . 3
⊢ ∅
⊊ (⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆) |
38 | | 0pss 4239 |
. . 3
⊢ (∅
⊊ (⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆) ↔ (⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆) ≠ ∅) |
39 | 37, 38 | mpbi 222 |
. 2
⊢
(⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆) ≠
∅ |
40 | | difn0 4173 |
. 2
⊢
((⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆) ≠ ∅ →
⦅𝐴, 𝐵⦆ ≠ ⦅𝐶⦆) |
41 | 39, 40 | ax-mp 5 |
1
⊢
⦅𝐴, 𝐵⦆ ≠ ⦅𝐶⦆ |