Proof of Theorem eldju2ndl
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | df-dju 9941 | . . . . 5
⊢ (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵)) | 
| 2 | 1 | eleq2i 2833 | . . . 4
⊢ (𝑋 ∈ (𝐴 ⊔ 𝐵) ↔ 𝑋 ∈ (({∅} × 𝐴) ∪ ({1o} ×
𝐵))) | 
| 3 |  | elun 4153 | . . . 4
⊢ (𝑋 ∈ (({∅} ×
𝐴) ∪ ({1o}
× 𝐵)) ↔ (𝑋 ∈ ({∅} × 𝐴) ∨ 𝑋 ∈ ({1o} × 𝐵))) | 
| 4 | 2, 3 | bitri 275 | . . 3
⊢ (𝑋 ∈ (𝐴 ⊔ 𝐵) ↔ (𝑋 ∈ ({∅} × 𝐴) ∨ 𝑋 ∈ ({1o} × 𝐵))) | 
| 5 |  | elxp6 8048 | . . . . 5
⊢ (𝑋 ∈ ({∅} × 𝐴) ↔ (𝑋 = 〈(1st ‘𝑋), (2nd ‘𝑋)〉 ∧ ((1st
‘𝑋) ∈ {∅}
∧ (2nd ‘𝑋) ∈ 𝐴))) | 
| 6 |  | simprr 773 | . . . . . 6
⊢ ((𝑋 = 〈(1st
‘𝑋), (2nd
‘𝑋)〉 ∧
((1st ‘𝑋)
∈ {∅} ∧ (2nd ‘𝑋) ∈ 𝐴)) → (2nd ‘𝑋) ∈ 𝐴) | 
| 7 | 6 | a1d 25 | . . . . 5
⊢ ((𝑋 = 〈(1st
‘𝑋), (2nd
‘𝑋)〉 ∧
((1st ‘𝑋)
∈ {∅} ∧ (2nd ‘𝑋) ∈ 𝐴)) → ((1st ‘𝑋) = ∅ →
(2nd ‘𝑋)
∈ 𝐴)) | 
| 8 | 5, 7 | sylbi 217 | . . . 4
⊢ (𝑋 ∈ ({∅} × 𝐴) → ((1st
‘𝑋) = ∅ →
(2nd ‘𝑋)
∈ 𝐴)) | 
| 9 |  | elxp6 8048 | . . . . 5
⊢ (𝑋 ∈ ({1o} ×
𝐵) ↔ (𝑋 = 〈(1st
‘𝑋), (2nd
‘𝑋)〉 ∧
((1st ‘𝑋)
∈ {1o} ∧ (2nd ‘𝑋) ∈ 𝐵))) | 
| 10 |  | elsni 4643 | . . . . . . 7
⊢
((1st ‘𝑋) ∈ {1o} →
(1st ‘𝑋) =
1o) | 
| 11 |  | 1n0 8526 | . . . . . . . 8
⊢
1o ≠ ∅ | 
| 12 |  | neeq1 3003 | . . . . . . . 8
⊢
((1st ‘𝑋) = 1o → ((1st
‘𝑋) ≠ ∅
↔ 1o ≠ ∅)) | 
| 13 | 11, 12 | mpbiri 258 | . . . . . . 7
⊢
((1st ‘𝑋) = 1o → (1st
‘𝑋) ≠
∅) | 
| 14 |  | eqneqall 2951 | . . . . . . . 8
⊢
((1st ‘𝑋) = ∅ → ((1st
‘𝑋) ≠ ∅
→ (2nd ‘𝑋) ∈ 𝐴)) | 
| 15 | 14 | com12 32 | . . . . . . 7
⊢
((1st ‘𝑋) ≠ ∅ → ((1st
‘𝑋) = ∅ →
(2nd ‘𝑋)
∈ 𝐴)) | 
| 16 | 10, 13, 15 | 3syl 18 | . . . . . 6
⊢
((1st ‘𝑋) ∈ {1o} →
((1st ‘𝑋)
= ∅ → (2nd ‘𝑋) ∈ 𝐴)) | 
| 17 | 16 | ad2antrl 728 | . . . . 5
⊢ ((𝑋 = 〈(1st
‘𝑋), (2nd
‘𝑋)〉 ∧
((1st ‘𝑋)
∈ {1o} ∧ (2nd ‘𝑋) ∈ 𝐵)) → ((1st ‘𝑋) = ∅ →
(2nd ‘𝑋)
∈ 𝐴)) | 
| 18 | 9, 17 | sylbi 217 | . . . 4
⊢ (𝑋 ∈ ({1o} ×
𝐵) → ((1st
‘𝑋) = ∅ →
(2nd ‘𝑋)
∈ 𝐴)) | 
| 19 | 8, 18 | jaoi 858 | . . 3
⊢ ((𝑋 ∈ ({∅} × 𝐴) ∨ 𝑋 ∈ ({1o} × 𝐵)) → ((1st
‘𝑋) = ∅ →
(2nd ‘𝑋)
∈ 𝐴)) | 
| 20 | 4, 19 | sylbi 217 | . 2
⊢ (𝑋 ∈ (𝐴 ⊔ 𝐵) → ((1st ‘𝑋) = ∅ →
(2nd ‘𝑋)
∈ 𝐴)) | 
| 21 | 20 | imp 406 | 1
⊢ ((𝑋 ∈ (𝐴 ⊔ 𝐵) ∧ (1st ‘𝑋) = ∅) →
(2nd ‘𝑋)
∈ 𝐴) |