Theorem prdom2

Description: An unordered pair has at most two elements. (Contributed by FL, 22-Feb-2011)

	Ref	Expression
Assertion	prdom2	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → { 𝐴 , 𝐵 } ≼ 2o )

Proof

Step	Hyp	Ref	Expression
1		dfsn2	⊢ { 𝐴 } = { 𝐴 , 𝐴 }
2		ensn1g	⊢ ( 𝐴 ∈ 𝐶 → { 𝐴 } ≈ 1o )
3		endom	⊢ ( { 𝐴 } ≈ 1o → { 𝐴 } ≼ 1o )
4		1sdom2	⊢ 1o ≺ 2o
5		domsdomtr	⊢ ( ( { 𝐴 } ≼ 1o ∧ 1o ≺ 2o ) → { 𝐴 } ≺ 2o )
6		sdomdom	⊢ ( { 𝐴 } ≺ 2o → { 𝐴 } ≼ 2o )
7	5 6	syl	⊢ ( ( { 𝐴 } ≼ 1o ∧ 1o ≺ 2o ) → { 𝐴 } ≼ 2o )
8	3 4 7	sylancl	⊢ ( { 𝐴 } ≈ 1o → { 𝐴 } ≼ 2o )
9	2 8	syl	⊢ ( 𝐴 ∈ 𝐶 → { 𝐴 } ≼ 2o )
10	1 9	eqbrtrrid	⊢ ( 𝐴 ∈ 𝐶 → { 𝐴 , 𝐴 } ≼ 2o )
11		preq2	⊢ ( 𝐵 = 𝐴 → { 𝐴 , 𝐵 } = { 𝐴 , 𝐴 } )
12	11	breq1d	⊢ ( 𝐵 = 𝐴 → ( { 𝐴 , 𝐵 } ≼ 2o ↔ { 𝐴 , 𝐴 } ≼ 2o ) )
13	10 12	imbitrrid	⊢ ( 𝐵 = 𝐴 → ( 𝐴 ∈ 𝐶 → { 𝐴 , 𝐵 } ≼ 2o ) )
14	13	eqcoms	⊢ ( 𝐴 = 𝐵 → ( 𝐴 ∈ 𝐶 → { 𝐴 , 𝐵 } ≼ 2o ) )
15	14	adantrd	⊢ ( 𝐴 = 𝐵 → ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → { 𝐴 , 𝐵 } ≼ 2o ) )
16		pr2ne	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( { 𝐴 , 𝐵 } ≈ 2o ↔ 𝐴 ≠ 𝐵 ) )
17	16	biimprd	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 𝐴 ≠ 𝐵 → { 𝐴 , 𝐵 } ≈ 2o ) )
18		endom	⊢ ( { 𝐴 , 𝐵 } ≈ 2o → { 𝐴 , 𝐵 } ≼ 2o )
19	17 18	syl6com	⊢ ( 𝐴 ≠ 𝐵 → ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → { 𝐴 , 𝐵 } ≼ 2o ) )
20	15 19	pm2.61ine	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → { 𝐴 , 𝐵 } ≼ 2o )