Metamath Proof Explorer


Theorem pr2nelem

Description: Lemma for pr2ne . (Contributed by FL, 17-Aug-2008)

Ref Expression
Assertion pr2nelem ( ( 𝐴𝐶𝐵𝐷𝐴𝐵 ) → { 𝐴 , 𝐵 } ≈ 2o )

Proof

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 )