Step |
Hyp |
Ref |
Expression |
1 |
|
id |
⊢ ( ∅ ∈ 〈 𝐴 , 𝐵 〉 → ∅ ∈ 〈 𝐴 , 𝐵 〉 ) |
2 |
|
oprcl |
⊢ ( ∅ ∈ 〈 𝐴 , 𝐵 〉 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) |
3 |
|
dfopg |
⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → 〈 𝐴 , 𝐵 〉 = { { 𝐴 } , { 𝐴 , 𝐵 } } ) |
4 |
2 3
|
syl |
⊢ ( ∅ ∈ 〈 𝐴 , 𝐵 〉 → 〈 𝐴 , 𝐵 〉 = { { 𝐴 } , { 𝐴 , 𝐵 } } ) |
5 |
1 4
|
eleqtrd |
⊢ ( ∅ ∈ 〈 𝐴 , 𝐵 〉 → ∅ ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) |
6 |
|
elpri |
⊢ ( ∅ ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } → ( ∅ = { 𝐴 } ∨ ∅ = { 𝐴 , 𝐵 } ) ) |
7 |
5 6
|
syl |
⊢ ( ∅ ∈ 〈 𝐴 , 𝐵 〉 → ( ∅ = { 𝐴 } ∨ ∅ = { 𝐴 , 𝐵 } ) ) |
8 |
2
|
simpld |
⊢ ( ∅ ∈ 〈 𝐴 , 𝐵 〉 → 𝐴 ∈ V ) |
9 |
|
snnzg |
⊢ ( 𝐴 ∈ V → { 𝐴 } ≠ ∅ ) |
10 |
8 9
|
syl |
⊢ ( ∅ ∈ 〈 𝐴 , 𝐵 〉 → { 𝐴 } ≠ ∅ ) |
11 |
10
|
necomd |
⊢ ( ∅ ∈ 〈 𝐴 , 𝐵 〉 → ∅ ≠ { 𝐴 } ) |
12 |
|
prnzg |
⊢ ( 𝐴 ∈ V → { 𝐴 , 𝐵 } ≠ ∅ ) |
13 |
8 12
|
syl |
⊢ ( ∅ ∈ 〈 𝐴 , 𝐵 〉 → { 𝐴 , 𝐵 } ≠ ∅ ) |
14 |
13
|
necomd |
⊢ ( ∅ ∈ 〈 𝐴 , 𝐵 〉 → ∅ ≠ { 𝐴 , 𝐵 } ) |
15 |
11 14
|
jca |
⊢ ( ∅ ∈ 〈 𝐴 , 𝐵 〉 → ( ∅ ≠ { 𝐴 } ∧ ∅ ≠ { 𝐴 , 𝐵 } ) ) |
16 |
|
neanior |
⊢ ( ( ∅ ≠ { 𝐴 } ∧ ∅ ≠ { 𝐴 , 𝐵 } ) ↔ ¬ ( ∅ = { 𝐴 } ∨ ∅ = { 𝐴 , 𝐵 } ) ) |
17 |
15 16
|
sylib |
⊢ ( ∅ ∈ 〈 𝐴 , 𝐵 〉 → ¬ ( ∅ = { 𝐴 } ∨ ∅ = { 𝐴 , 𝐵 } ) ) |
18 |
7 17
|
pm2.65i |
⊢ ¬ ∅ ∈ 〈 𝐴 , 𝐵 〉 |