This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )