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

Metamath Proof Explorer

Theorem pmtrprfv3

Description: In a transposition of two given points, all other points are mapped to themselves. (Contributed by AV, 17-Mar-2019)

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

Proof

Step Hyp Ref Expression
1 pmtrfval.t ⊢ 𝑇 = ( pmTrsp ‘ 𝐷 )
2 simp1 ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → 𝐷 ∈ 𝑉 )
3 simp1 ⊢ ( ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) → 𝑋 ∈ 𝐷 )
4 3 3ad2ant2 ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → 𝑋 ∈ 𝐷 )
5 simp22 ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → 𝑌 ∈ 𝐷 )
6 4 5 prssd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → { 𝑋 , 𝑌 } ⊆ 𝐷 )
7 enpr2 ⊢ ( ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌 ) → { 𝑋 , 𝑌 } ≈ 2o )
8 7 3expia ⊢ ( ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) → ( 𝑋 ≠ 𝑌 → { 𝑋 , 𝑌 } ≈ 2o ) )
9 8 3adant3 ⊢ ( ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) → ( 𝑋 ≠ 𝑌 → { 𝑋 , 𝑌 } ≈ 2o ) )
10 9 com12 ⊢ ( 𝑋 ≠ 𝑌 → ( ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) → { 𝑋 , 𝑌 } ≈ 2o ) )
11 10 3ad2ant1 ⊢ ( ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) → ( ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) → { 𝑋 , 𝑌 } ≈ 2o ) )
12 11 impcom ⊢ ( ( ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → { 𝑋 , 𝑌 } ≈ 2o )
13 12 3adant1 ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → { 𝑋 , 𝑌 } ≈ 2o )
14 simp23 ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → 𝑍 ∈ 𝐷 )
15 1 pmtrfv ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ { 𝑋 , 𝑌 } ⊆ 𝐷 ∧ { 𝑋 , 𝑌 } ≈ 2o ) ∧ 𝑍 ∈ 𝐷 ) → ( ( 𝑇 ‘ { 𝑋 , 𝑌 } ) ‘ 𝑍 ) = if ( 𝑍 ∈ { 𝑋 , 𝑌 } , ∪ ( { 𝑋 , 𝑌 } ∖ { 𝑍 } ) , 𝑍 ) )
16 2 6 13 14 15 syl31anc ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( ( 𝑇 ‘ { 𝑋 , 𝑌 } ) ‘ 𝑍 ) = if ( 𝑍 ∈ { 𝑋 , 𝑌 } , ∪ ( { 𝑋 , 𝑌 } ∖ { 𝑍 } ) , 𝑍 ) )
17 necom ⊢ ( 𝑋 ≠ 𝑍 ↔ 𝑍 ≠ 𝑋 )
18 17 biimpi ⊢ ( 𝑋 ≠ 𝑍 → 𝑍 ≠ 𝑋 )
19 18 3ad2ant2 ⊢ ( ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) → 𝑍 ≠ 𝑋 )
20 19 3ad2ant3 ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → 𝑍 ≠ 𝑋 )
21 necom ⊢ ( 𝑌 ≠ 𝑍 ↔ 𝑍 ≠ 𝑌 )
22 21 biimpi ⊢ ( 𝑌 ≠ 𝑍 → 𝑍 ≠ 𝑌 )
23 22 3ad2ant3 ⊢ ( ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) → 𝑍 ≠ 𝑌 )
24 23 3ad2ant3 ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → 𝑍 ≠ 𝑌 )
25 20 24 nelprd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ¬ 𝑍 ∈ { 𝑋 , 𝑌 } )
26 25 iffalsed ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → if ( 𝑍 ∈ { 𝑋 , 𝑌 } , ∪ ( { 𝑋 , 𝑌 } ∖ { 𝑍 } ) , 𝑍 ) = 𝑍 )
27 16 26 eqtrd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷 ) ∧ ( 𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍 ) ) → ( ( 𝑇 ‘ { 𝑋 , 𝑌 } ) ‘ 𝑍 ) = 𝑍 )