Step |
Hyp |
Ref |
Expression |
1 |
|
disjsn2 |
⊢ ( 𝐴 ≠ 𝐵 → ( { 𝐴 } ∩ { 𝐵 } ) = ∅ ) |
2 |
|
ensn1g |
⊢ ( 𝐴 ∈ 𝐶 → { 𝐴 } ≈ 1o ) |
3 |
|
ensn1g |
⊢ ( 𝐵 ∈ 𝐷 → { 𝐵 } ≈ 1o ) |
4 |
|
pm54.43 |
⊢ ( ( { 𝐴 } ≈ 1o ∧ { 𝐵 } ≈ 1o ) → ( ( { 𝐴 } ∩ { 𝐵 } ) = ∅ ↔ ( { 𝐴 } ∪ { 𝐵 } ) ≈ 2o ) ) |
5 |
|
df-pr |
⊢ { 𝐴 , 𝐵 } = ( { 𝐴 } ∪ { 𝐵 } ) |
6 |
5
|
breq1i |
⊢ ( { 𝐴 , 𝐵 } ≈ 2o ↔ ( { 𝐴 } ∪ { 𝐵 } ) ≈ 2o ) |
7 |
4 6
|
bitr4di |
⊢ ( ( { 𝐴 } ≈ 1o ∧ { 𝐵 } ≈ 1o ) → ( ( { 𝐴 } ∩ { 𝐵 } ) = ∅ ↔ { 𝐴 , 𝐵 } ≈ 2o ) ) |
8 |
7
|
biimpd |
⊢ ( ( { 𝐴 } ≈ 1o ∧ { 𝐵 } ≈ 1o ) → ( ( { 𝐴 } ∩ { 𝐵 } ) = ∅ → { 𝐴 , 𝐵 } ≈ 2o ) ) |
9 |
2 3 8
|
syl2an |
⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( ( { 𝐴 } ∩ { 𝐵 } ) = ∅ → { 𝐴 , 𝐵 } ≈ 2o ) ) |
10 |
9
|
ex |
⊢ ( 𝐴 ∈ 𝐶 → ( 𝐵 ∈ 𝐷 → ( ( { 𝐴 } ∩ { 𝐵 } ) = ∅ → { 𝐴 , 𝐵 } ≈ 2o ) ) ) |
11 |
1 10
|
syl7 |
⊢ ( 𝐴 ∈ 𝐶 → ( 𝐵 ∈ 𝐷 → ( 𝐴 ≠ 𝐵 → { 𝐴 , 𝐵 } ≈ 2o ) ) ) |
12 |
11
|
3imp |
⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } ≈ 2o ) |