Proof of Theorem bj-2upln1upl
| Step | Hyp | Ref
| Expression |
| 1 | | xpundi 5754 |
. . . . . . 7
⊢
({∅} × (tag 𝐴 ∪ tag 𝐶)) = (({∅} × tag 𝐴) ∪ ({∅} × tag
𝐶)) |
| 2 | 1 | difeq2i 4123 |
. . . . . 6
⊢
(({1o} × tag 𝐵) ∖ ({∅} × (tag 𝐴 ∪ tag 𝐶))) = (({1o} × tag 𝐵) ∖ (({∅} ×
tag 𝐴) ∪ ({∅}
× tag 𝐶))) |
| 3 | | incom 4209 |
. . . . . . . . 9
⊢
(({∅} × (tag 𝐴 ∪ tag 𝐶)) ∩ ({1o} × tag 𝐵)) = (({1o} ×
tag 𝐵) ∩ ({∅}
× (tag 𝐴 ∪ tag
𝐶))) |
| 4 | | xp01disjl 8530 |
. . . . . . . . 9
⊢
(({∅} × (tag 𝐴 ∪ tag 𝐶)) ∩ ({1o} × tag 𝐵)) = ∅ |
| 5 | 3, 4 | eqtr3i 2767 |
. . . . . . . 8
⊢
(({1o} × tag 𝐵) ∩ ({∅} × (tag 𝐴 ∪ tag 𝐶))) = ∅ |
| 6 | | disjdif2 4480 |
. . . . . . . 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 8516 |
. . . . . . . . . 10
⊢
1o ∈ V |
| 9 | 8 | snnz 4776 |
. . . . . . . . 9
⊢
{1o} ≠ ∅ |
| 10 | | bj-tagn0 36980 |
. . . . . . . . 9
⊢ tag 𝐵 ≠ ∅ |
| 11 | 9, 10 | pm3.2i 470 |
. . . . . . . 8
⊢
({1o} ≠ ∅ ∧ tag 𝐵 ≠ ∅) |
| 12 | | xpnz 6179 |
. . . . . . . 8
⊢
(({1o} ≠ ∅ ∧ tag 𝐵 ≠ ∅) ↔ ({1o}
× tag 𝐵) ≠
∅) |
| 13 | 11, 12 | mpbi 230 |
. . . . . . 7
⊢
({1o} × tag 𝐵) ≠ ∅ |
| 14 | 7, 13 | eqnetri 3011 |
. . . . . 6
⊢
(({1o} × tag 𝐵) ∖ ({∅} × (tag 𝐴 ∪ tag 𝐶))) ≠ ∅ |
| 15 | 2, 14 | eqnetrri 3012 |
. . . . 5
⊢
(({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag
𝐶))) ≠
∅ |
| 16 | | 0pss 4447 |
. . . . 5
⊢ (∅
⊊ (({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag
𝐶))) ↔
(({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag
𝐶))) ≠
∅) |
| 17 | 15, 16 | mpbir 231 |
. . . 4
⊢ ∅
⊊ (({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag
𝐶))) |
| 18 | | ssun2 4179 |
. . . . . . . 8
⊢
({∅} × tag 𝐶) ⊆ (({∅} × tag 𝐴) ∪ ({∅} × tag
𝐶)) |
| 19 | | sscon 4143 |
. . . . . . . 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 4179 |
. . . . . . . 8
⊢
({1o} × tag 𝐵) ⊆ (({∅} × tag 𝐴) ∪ ({1o} ×
tag 𝐵)) |
| 22 | | ssdif 4144 |
. . . . . . . 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 3993 |
. . . . . 6
⊢
(({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag
𝐶))) ⊆ ((({∅}
× tag 𝐴) ∪
({1o} × tag 𝐵)) ∖ ({∅} × tag 𝐶)) |
| 25 | | df-bj-2upl 37012 |
. . . . . . . 8
⊢
⦅𝐴, 𝐵⦆ = (⦅𝐴⦆ ∪ ({1o}
× tag 𝐵)) |
| 26 | | df-bj-1upl 36999 |
. . . . . . . . 9
⊢
⦅𝐴⦆ =
({∅} × tag 𝐴) |
| 27 | 26 | uneq1i 4164 |
. . . . . . . 8
⊢
(⦅𝐴⦆
∪ ({1o} × tag 𝐵)) = (({∅} × tag 𝐴) ∪ ({1o} ×
tag 𝐵)) |
| 28 | 25, 27 | eqtri 2765 |
. . . . . . 7
⊢
⦅𝐴, 𝐵⦆ = (({∅} ×
tag 𝐴) ∪
({1o} × tag 𝐵)) |
| 29 | 28 | difeq1i 4122 |
. . . . . 6
⊢
(⦅𝐴, 𝐵⦆ ∖ ({∅}
× tag 𝐶)) =
((({∅} × tag 𝐴)
∪ ({1o} × tag 𝐵)) ∖ ({∅} × tag 𝐶)) |
| 30 | 24, 29 | sseqtrri 4033 |
. . . . 5
⊢
(({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag
𝐶))) ⊆ (⦅𝐴, 𝐵⦆ ∖ ({∅} × tag 𝐶)) |
| 31 | | df-bj-1upl 36999 |
. . . . . 6
⊢
⦅𝐶⦆ =
({∅} × tag 𝐶) |
| 32 | 31 | difeq2i 4123 |
. . . . 5
⊢
(⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆) = (⦅𝐴, 𝐵⦆ ∖ ({∅} × tag 𝐶)) |
| 33 | 30, 32 | sseqtrri 4033 |
. . . 4
⊢
(({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag
𝐶))) ⊆ (⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆) |
| 34 | | psssstr 4109 |
. . . 4
⊢ ((∅
⊊ (({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag
𝐶))) ∧
(({1o} × tag 𝐵) ∖ (({∅} × tag 𝐴) ∪ ({∅} × tag
𝐶))) ⊆ (⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆)) → ∅ ⊊
(⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆)) |
| 35 | 17, 33, 34 | mp2an 692 |
. . 3
⊢ ∅
⊊ (⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆) |
| 36 | | 0pss 4447 |
. . 3
⊢ (∅
⊊ (⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆) ↔ (⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆) ≠ ∅) |
| 37 | 35, 36 | mpbi 230 |
. 2
⊢
(⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆) ≠
∅ |
| 38 | | difn0 4367 |
. 2
⊢
((⦅𝐴, 𝐵⦆ ∖ ⦅𝐶⦆) ≠ ∅ →
⦅𝐴, 𝐵⦆ ≠ ⦅𝐶⦆) |
| 39 | 37, 38 | ax-mp 5 |
1
⊢
⦅𝐴, 𝐵⦆ ≠ ⦅𝐶⦆ |