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 ( ( 𝐷𝑉 ∧ ( 𝑋𝐷𝑌𝐷𝑋𝑌 ) ) → ( ( 𝑇 ‘ { 𝑋 , 𝑌 } ) ‘ 𝑋 ) = 𝑌 )