Proof of Theorem bj-2upln1upl
Step | Hyp | Ref
| Expression |
1 | | xpundi 5656 |
. . . . . . 7
⊢
({∅} × (tag 𝐴 ∪ tag 𝐶)) = (({∅} × tag 𝐴) ∪ ({∅} × tag
𝐶)) |
2 | 1 | difeq2i 4059 |
. . . . . 6
⊢
(({1o} × tag 𝐵) ∖ ({∅} × (tag 𝐴 ∪ tag 𝐶))) = (({1o} × tag 𝐵) ∖ (({∅} ×
tag 𝐴) ∪ ({∅}
× tag 𝐶))) |
3 | | incom 4140 |
. . . . . . . . 9
⊢
(({∅} × (tag 𝐴 ∪ tag 𝐶)) ∩ ({1o} × tag 𝐵)) = (({1o} ×
tag 𝐵) ∩ ({∅}
× (tag 𝐴 ∪ tag
𝐶))) |
4 | | xp01disjl 8311 |
. . . . . . . . 9
⊢
(({∅} × (tag 𝐴 ∪ tag 𝐶)) ∩ ({1o} × tag 𝐵)) = ∅ |
5 | 3, 4 | eqtr3i 2770 |
. . . . . . . 8
⊢
(({1o} × tag 𝐵) ∩ ({∅} × (tag 𝐴 ∪ tag 𝐶))) = ∅ |
6 | | disjdif2 4419 |
. . . . . . . 8
⊢
((({1o} × tag 𝐵) ∩ ({∅} × (tag 𝐴 ∪ tag 𝐶))) = ∅ → (({1o}
× tag 𝐵) ∖
({∅} × (tag 𝐴
∪ tag 𝐶))) =
({1o} × tag 𝐵)) |
7 | 5, 6 | ax-mp 5 |
. . . . . . 7
⊢
(({1o} × tag 𝐵) ∖ ({∅} × (tag 𝐴 ∪ tag 𝐶))) = ({1o} × tag 𝐵) |
8 | | 1oex 8298 |
. . . . . . . . . 10
⊢
1o ∈ V |
9 | 8 | snnz 4718 |
. . . . . . . . 9
⊢
{1o} ≠ ∅ |
10 | | bj-tagn0 35165 |
. . . . . . . . 9
⊢ tag 𝐵 ≠ ∅ |
11 | 9, 10 | pm3.2i 471 |
. . . . . . . 8
⊢
({1o} ≠ ∅ ∧ tag 𝐵 ≠ ∅) |
12 | | xpnz 6061 |
. . . . . . . 8
⊢
(({1o} ≠ ∅ ∧ tag 𝐵 ≠ ∅) ↔ ({1o}
× tag 𝐵) ≠
∅) |
13 | 11, 12 | mpbi 229 |
. . . . . . 7
⊢
({1o} × tag 𝐵) ≠ ∅ |
14 | 7, 13 | eqnetri 3016 |
. . . . . 6
⊢
(({1o} × tag 𝐵) ∖ ({∅} × (tag 𝐴 ∪ tag 𝐶))) ≠ ∅ |
15 | 2, 14 | eqnetrri 3017 |
. . . . 5
⊢
(({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag
𝐶))) ≠
∅ |
16 | | 0pss 4384 |
. . . . 5
⊢ (∅
⊊ (({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag
𝐶))) ↔
(({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag
𝐶))) ≠
∅) |
17 | 15, 16 | mpbir 230 |
. . . 4
⊢ ∅
⊊ (({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag
𝐶))) |
18 | | ssun2 4112 |
. . . . . . . 8
⊢
({∅} × tag 𝐶) ⊆ (({∅} × tag 𝐴) ∪ ({∅} × tag
𝐶)) |
19 | | sscon 4078 |
. . . . . . . 8
⊢
(({∅} × tag 𝐶) ⊆ (({∅} × tag 𝐴) ∪ ({∅} × tag
𝐶)) →
(({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag
𝐶))) ⊆
(({1o} × tag 𝐵) ∖ ({∅} × tag 𝐶))) |
20 | 18, 19 | ax-mp 5 |
. . . . . . 7
⊢
(({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag
𝐶))) ⊆
(({1o} × tag 𝐵) ∖ ({∅} × tag 𝐶)) |
21 | | ssun2 4112 |
. . . . . . . 8
⊢
({1o} × tag 𝐵) ⊆ (({∅} × tag 𝐴) ∪ ({1o} ×
tag 𝐵)) |
22 | | ssdif 4079 |
. . . . . . . 8
⊢
(({1o} × tag 𝐵) ⊆ (({∅} × tag 𝐴) ∪ ({1o} ×
tag 𝐵)) →
(({1o} × tag 𝐵) ∖ ({∅} × tag 𝐶)) ⊆ ((({∅} ×
tag 𝐴) ∪
({1o} × tag 𝐵)) ∖ ({∅} × tag 𝐶))) |
23 | 21, 22 | ax-mp 5 |
. . . . . . 7
⊢
(({1o} × tag 𝐵) ∖ ({∅} × tag 𝐶)) ⊆ ((({∅} ×
tag 𝐴) ∪
({1o} × tag 𝐵)) ∖ ({∅} × tag 𝐶)) |
24 | 20, 23 | sstri 3935 |
. . . . . 6
⊢
(({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag
𝐶))) ⊆ ((({∅}
× tag 𝐴) ∪
({1o} × tag 𝐵)) ∖ ({∅} × tag 𝐶)) |
25 | | df-bj-2upl 35197 |
. . . . . . . 8
⊢
⦅𝐴, 𝐵⦆ = (⦅𝐴⦆ ∪ ({1o}
× tag 𝐵)) |
26 | | df-bj-1upl 35184 |
. . . . . . . . 9
⊢
⦅𝐴⦆ =
({∅} × tag 𝐴) |
27 | 26 | uneq1i 4098 |
. . . . . . . 8
⊢
(⦅𝐴⦆
∪ ({1o} × tag 𝐵)) = (({∅} × tag 𝐴) ∪ ({1o} ×
tag 𝐵)) |
28 | 25, 27 | eqtri 2768 |
. . . . . . 7
⊢
⦅𝐴, 𝐵⦆ = (({∅} ×
tag 𝐴) ∪
({1o} × tag 𝐵)) |
29 | 28 | difeq1i 4058 |
. . . . . 6
⊢
(⦅𝐴, 𝐵⦆ ∖ ({∅}
× tag 𝐶)) =
((({∅} × tag 𝐴)
∪ ({1o} × tag 𝐵)) ∖ ({∅} × tag 𝐶)) |
30 | 24, 29 | sseqtrri 3963 |
. . . . 5
⊢
(({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag
𝐶))) ⊆ (⦅𝐴, 𝐵⦆ ∖ ({∅} × tag 𝐶)) |
31 | | df-bj-1upl 35184 |
. . . . . 6
⊢
⦅𝐶⦆ =
({∅} × tag 𝐶) |
32 | 31 | difeq2i 4059 |
. . . . 5
⊢
(⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆) = (⦅𝐴, 𝐵⦆ ∖ ({∅} × tag 𝐶)) |
33 | 30, 32 | sseqtrri 3963 |
. . . 4
⊢
(({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag
𝐶))) ⊆ (⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆) |
34 | | psssstr 4046 |
. . . 4
⊢ ((∅
⊊ (({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag
𝐶))) ∧
(({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag
𝐶))) ⊆ (⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆)) → ∅ ⊊
(⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆)) |
35 | 17, 33, 34 | mp2an 689 |
. . 3
⊢ ∅
⊊ (⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆) |
36 | | 0pss 4384 |
. . 3
⊢ (∅
⊊ (⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆) ↔ (⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆) ≠ ∅) |
37 | 35, 36 | mpbi 229 |
. 2
⊢
(⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆) ≠
∅ |
38 | | difn0 4304 |
. 2
⊢
((⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆) ≠ ∅ →
⦅𝐴, 𝐵⦆ ≠ ⦅𝐶⦆) |
39 | 37, 38 | ax-mp 5 |
1
⊢
⦅𝐴, 𝐵⦆ ≠ ⦅𝐶⦆ |