Metamath Proof Explorer

Theorem pmtrprfv

Description: In a transposition of two given points, each maps to the other. (Contributed by Stefan O'Rear, 25-Aug-2015)

Ref Expression
Hypothesis pmtrfval.t ⊢ 𝑇 = ( pmTrsp ‘ 𝐷 )
Assertion pmtrprfv ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌 ) ) → ( ( 𝑇 ‘ { 𝑋 , 𝑌 } ) ‘ 𝑋 ) = 𝑌 )

Proof

Step Hyp Ref Expression
1 pmtrfval.t ⊢ 𝑇 = ( pmTrsp ‘ 𝐷 )
2 simpl ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌 ) ) → 𝐷 ∈ 𝑉 )
3 simpr1 ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌 ) ) → 𝑋 ∈ 𝐷 )
4 simpr2 ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌 ) ) → 𝑌 ∈ 𝐷 )
5 3 4 prssd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌 ) ) → { 𝑋 , 𝑌 } ⊆ 𝐷 )
6 pr2nelem ⊢ ( ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌 ) → { 𝑋 , 𝑌 } ≈ 2o )
7 6 adantl ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌 ) ) → { 𝑋 , 𝑌 } ≈ 2o )
8 1 pmtrfv ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ { 𝑋 , 𝑌 } ⊆ 𝐷 ∧ { 𝑋 , 𝑌 } ≈ 2o ) ∧ 𝑋 ∈ 𝐷 ) → ( ( 𝑇 ‘ { 𝑋 , 𝑌 } ) ‘ 𝑋 ) = if ( 𝑋 ∈ { 𝑋 , 𝑌 } , ∪ ( { 𝑋 , 𝑌 } ∖ { 𝑋 } ) , 𝑋 ) )
9 2 5 7 3 8 syl31anc ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌 ) ) → ( ( 𝑇 ‘ { 𝑋 , 𝑌 } ) ‘ 𝑋 ) = if ( 𝑋 ∈ { 𝑋 , 𝑌 } , ∪ ( { 𝑋 , 𝑌 } ∖ { 𝑋 } ) , 𝑋 ) )
10 prid1g ⊢ ( 𝑋 ∈ 𝐷 → 𝑋 ∈ { 𝑋 , 𝑌 } )
11 3 10 syl ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌 ) ) → 𝑋 ∈ { 𝑋 , 𝑌 } )
12 11 iftrued ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌 ) ) → if ( 𝑋 ∈ { 𝑋 , 𝑌 } , ∪ ( { 𝑋 , 𝑌 } ∖ { 𝑋 } ) , 𝑋 ) = ∪ ( { 𝑋 , 𝑌 } ∖ { 𝑋 } ) )
13 difprsnss ⊢ ( { 𝑋 , 𝑌 } ∖ { 𝑋 } ) ⊆ { 𝑌 }
14 13 a1i ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌 ) ) → ( { 𝑋 , 𝑌 } ∖ { 𝑋 } ) ⊆ { 𝑌 } )
15 prid2g ⊢ ( 𝑌 ∈ 𝐷 → 𝑌 ∈ { 𝑋 , 𝑌 } )
16 4 15 syl ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌 ) ) → 𝑌 ∈ { 𝑋 , 𝑌 } )
17 simpr3 ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌 ) ) → 𝑋 ≠ 𝑌 )
18 17 necomd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌 ) ) → 𝑌 ≠ 𝑋 )
19 eldifsn ⊢ ( 𝑌 ∈ ( { 𝑋 , 𝑌 } ∖ { 𝑋 } ) ↔ ( 𝑌 ∈ { 𝑋 , 𝑌 } ∧ 𝑌 ≠ 𝑋 ) )
20 16 18 19 sylanbrc ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌 ) ) → 𝑌 ∈ ( { 𝑋 , 𝑌 } ∖ { 𝑋 } ) )
21 20 snssd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌 ) ) → { 𝑌 } ⊆ ( { 𝑋 , 𝑌 } ∖ { 𝑋 } ) )
22 14 21 eqssd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌 ) ) → ( { 𝑋 , 𝑌 } ∖ { 𝑋 } ) = { 𝑌 } )
23 22 unieqd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌 ) ) → ∪ ( { 𝑋 , 𝑌 } ∖ { 𝑋 } ) = ∪ { 𝑌 } )
24 unisng ⊢ ( 𝑌 ∈ 𝐷 → ∪ { 𝑌 } = 𝑌 )
25 4 24 syl ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌 ) ) → ∪ { 𝑌 } = 𝑌 )
26 23 25 eqtrd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌 ) ) → ∪ ( { 𝑋 , 𝑌 } ∖ { 𝑋 } ) = 𝑌 )
27 12 26 eqtrd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌 ) ) → if ( 𝑋 ∈ { 𝑋 , 𝑌 } , ∪ ( { 𝑋 , 𝑌 } ∖ { 𝑋 } ) , 𝑋 ) = 𝑌 )
28 9 27 eqtrd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌 ) ) → ( ( 𝑇 ‘ { 𝑋 , 𝑌 } ) ‘ 𝑋 ) = 𝑌 )