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 )