Proof of Theorem dju1dif
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpl 482 | . . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (𝐴 ⊔ 1o)) → 𝐴 ∈ 𝑉) | 
| 2 |  | 1oex 8516 | . . . 4
⊢
1o ∈ V | 
| 3 |  | djuex 9948 | . . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 1o ∈ V) → (𝐴 ⊔ 1o) ∈
V) | 
| 4 | 1, 2, 3 | sylancl 586 | . . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (𝐴 ⊔ 1o)) → (𝐴 ⊔ 1o) ∈
V) | 
| 5 |  | simpr 484 | . . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (𝐴 ⊔ 1o)) → 𝐵 ∈ (𝐴 ⊔ 1o)) | 
| 6 |  | df1o2 8513 | . . . . . . . . 9
⊢
1o = {∅} | 
| 7 | 6 | xpeq2i 5712 | . . . . . . . 8
⊢
({1o} × 1o) = ({1o} ×
{∅}) | 
| 8 |  | 0ex 5307 | . . . . . . . . 9
⊢ ∅
∈ V | 
| 9 | 2, 8 | xpsn 7161 | . . . . . . . 8
⊢
({1o} × {∅}) = {〈1o,
∅〉} | 
| 10 | 7, 9 | eqtri 2765 | . . . . . . 7
⊢
({1o} × 1o) = {〈1o,
∅〉} | 
| 11 |  | ssun2 4179 | . . . . . . 7
⊢
({1o} × 1o) ⊆ (({∅} ×
𝐴) ∪ ({1o}
× 1o)) | 
| 12 | 10, 11 | eqsstrri 4031 | . . . . . 6
⊢
{〈1o, ∅〉} ⊆ (({∅} × 𝐴) ∪ ({1o} ×
1o)) | 
| 13 |  | opex 5469 | . . . . . . 7
⊢
〈1o, ∅〉 ∈ V | 
| 14 | 13 | snss 4785 | . . . . . 6
⊢
(〈1o, ∅〉 ∈ (({∅} × 𝐴) ∪ ({1o} ×
1o)) ↔ {〈1o, ∅〉} ⊆ (({∅}
× 𝐴) ∪
({1o} × 1o))) | 
| 15 | 12, 14 | mpbir 231 | . . . . 5
⊢
〈1o, ∅〉 ∈ (({∅} × 𝐴) ∪ ({1o} ×
1o)) | 
| 16 |  | df-dju 9941 | . . . . 5
⊢ (𝐴 ⊔ 1o) =
(({∅} × 𝐴)
∪ ({1o} × 1o)) | 
| 17 | 15, 16 | eleqtrri 2840 | . . . 4
⊢
〈1o, ∅〉 ∈ (𝐴 ⊔ 1o) | 
| 18 | 17 | a1i 11 | . . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (𝐴 ⊔ 1o)) →
〈1o, ∅〉 ∈ (𝐴 ⊔ 1o)) | 
| 19 |  | difsnen 9093 | . . 3
⊢ (((𝐴 ⊔ 1o) ∈
V ∧ 𝐵 ∈ (𝐴 ⊔ 1o) ∧
〈1o, ∅〉 ∈ (𝐴 ⊔ 1o)) → ((𝐴 ⊔ 1o) ∖
{𝐵}) ≈ ((𝐴 ⊔ 1o) ∖
{〈1o, ∅〉})) | 
| 20 | 4, 5, 18, 19 | syl3anc 1373 | . 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (𝐴 ⊔ 1o)) → ((𝐴 ⊔ 1o) ∖
{𝐵}) ≈ ((𝐴 ⊔ 1o) ∖
{〈1o, ∅〉})) | 
| 21 | 16 | difeq1i 4122 | . . . 4
⊢ ((𝐴 ⊔ 1o) ∖
{〈1o, ∅〉}) = ((({∅} × 𝐴) ∪ ({1o} ×
1o)) ∖ {〈1o, ∅〉}) | 
| 22 |  | xp01disjl 8530 | . . . . . 6
⊢
(({∅} × 𝐴) ∩ ({1o} ×
1o)) = ∅ | 
| 23 |  | disj3 4454 | . . . . . 6
⊢
((({∅} × 𝐴) ∩ ({1o} ×
1o)) = ∅ ↔ ({∅} × 𝐴) = (({∅} × 𝐴) ∖ ({1o} ×
1o))) | 
| 24 | 22, 23 | mpbi 230 | . . . . 5
⊢
({∅} × 𝐴) = (({∅} × 𝐴) ∖ ({1o} ×
1o)) | 
| 25 |  | difun2 4481 | . . . . 5
⊢
((({∅} × 𝐴) ∪ ({1o} ×
1o)) ∖ ({1o} × 1o)) = (({∅}
× 𝐴) ∖
({1o} × 1o)) | 
| 26 | 10 | difeq2i 4123 | . . . . 5
⊢
((({∅} × 𝐴) ∪ ({1o} ×
1o)) ∖ ({1o} × 1o)) = ((({∅}
× 𝐴) ∪
({1o} × 1o)) ∖ {〈1o,
∅〉}) | 
| 27 | 24, 25, 26 | 3eqtr2i 2771 | . . . 4
⊢
({∅} × 𝐴) = ((({∅} × 𝐴) ∪ ({1o} ×
1o)) ∖ {〈1o, ∅〉}) | 
| 28 | 21, 27 | eqtr4i 2768 | . . 3
⊢ ((𝐴 ⊔ 1o) ∖
{〈1o, ∅〉}) = ({∅} × 𝐴) | 
| 29 |  | xpsnen2g 9105 | . . . 4
⊢ ((∅
∈ V ∧ 𝐴 ∈
𝑉) → ({∅}
× 𝐴) ≈ 𝐴) | 
| 30 | 8, 1, 29 | sylancr 587 | . . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (𝐴 ⊔ 1o)) → ({∅}
× 𝐴) ≈ 𝐴) | 
| 31 | 28, 30 | eqbrtrid 5178 | . 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (𝐴 ⊔ 1o)) → ((𝐴 ⊔ 1o) ∖
{〈1o, ∅〉}) ≈ 𝐴) | 
| 32 |  | entr 9046 | . 2
⊢ ((((𝐴 ⊔ 1o) ∖
{𝐵}) ≈ ((𝐴 ⊔ 1o) ∖
{〈1o, ∅〉}) ∧ ((𝐴 ⊔ 1o) ∖
{〈1o, ∅〉}) ≈ 𝐴) → ((𝐴 ⊔ 1o) ∖ {𝐵}) ≈ 𝐴) | 
| 33 | 20, 31, 32 | syl2anc 584 | 1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (𝐴 ⊔ 1o)) → ((𝐴 ⊔ 1o) ∖
{𝐵}) ≈ 𝐴) |