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

Metamath Proof Explorer

Theorem pmtrmvd

Description: A transposition moves precisely the transposed points. (Contributed by Stefan O'Rear, 16-Aug-2015)

Ref Expression
Hypothesis pmtrfval.t ⊢ 𝑇 = ( pmTrsp ‘ 𝐷 )
Assertion pmtrmvd ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) → dom ( ( 𝑇 ‘ 𝑃 ) ∖ I ) = 𝑃 )

Proof

Step Hyp Ref Expression
1 pmtrfval.t ⊢ 𝑇 = ( pmTrsp ‘ 𝐷 )
2 1 pmtrf ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) → ( 𝑇 ‘ 𝑃 ) : 𝐷 ⟶ 𝐷 )
3 ffn ⊢ ( ( 𝑇 ‘ 𝑃 ) : 𝐷 ⟶ 𝐷 → ( 𝑇 ‘ 𝑃 ) Fn 𝐷 )
4 fndifnfp ⊢ ( ( 𝑇 ‘ 𝑃 ) Fn 𝐷 → dom ( ( 𝑇 ‘ 𝑃 ) ∖ I ) = { 𝑧 ∈ 𝐷 ∣ ( ( 𝑇 ‘ 𝑃 ) ‘ 𝑧 ) ≠ 𝑧 } )
5 2 3 4 3syl ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) → dom ( ( 𝑇 ‘ 𝑃 ) ∖ I ) = { 𝑧 ∈ 𝐷 ∣ ( ( 𝑇 ‘ 𝑃 ) ‘ 𝑧 ) ≠ 𝑧 } )
6 1 pmtrfv ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) ∧ 𝑧 ∈ 𝐷 ) → ( ( 𝑇 ‘ 𝑃 ) ‘ 𝑧 ) = if ( 𝑧 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑧 } ) , 𝑧 ) )
7 6 neeq1d ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) ∧ 𝑧 ∈ 𝐷 ) → ( ( ( 𝑇 ‘ 𝑃 ) ‘ 𝑧 ) ≠ 𝑧 ↔ if ( 𝑧 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑧 } ) , 𝑧 ) ≠ 𝑧 ) )
8 iffalse ⊢ ( ¬ 𝑧 ∈ 𝑃 → if ( 𝑧 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑧 } ) , 𝑧 ) = 𝑧 )
9 8 necon1ai ⊢ ( if ( 𝑧 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑧 } ) , 𝑧 ) ≠ 𝑧 → 𝑧 ∈ 𝑃 )
10 iftrue ⊢ ( 𝑧 ∈ 𝑃 → if ( 𝑧 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑧 } ) , 𝑧 ) = ∪ ( 𝑃 ∖ { 𝑧 } ) )
11 10 adantl ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) ∧ 𝑧 ∈ 𝑃 ) → if ( 𝑧 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑧 } ) , 𝑧 ) = ∪ ( 𝑃 ∖ { 𝑧 } ) )
12 1onn ⊢ 1o ∈ ω
13 simpl3 ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) ∧ 𝑧 ∈ 𝑃 ) → 𝑃 ≈ 2o )
14 df-2o ⊢ 2o = suc 1o
15 13 14 breqtrdi ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) ∧ 𝑧 ∈ 𝑃 ) → 𝑃 ≈ suc 1o )
16 simpr ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) ∧ 𝑧 ∈ 𝑃 ) → 𝑧 ∈ 𝑃 )
17 dif1ennn ⊢ ( ( 1o ∈ ω ∧ 𝑃 ≈ suc 1o ∧ 𝑧 ∈ 𝑃 ) → ( 𝑃 ∖ { 𝑧 } ) ≈ 1o )
18 12 15 16 17 mp3an2i ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) ∧ 𝑧 ∈ 𝑃 ) → ( 𝑃 ∖ { 𝑧 } ) ≈ 1o )
19 en1uniel ⊢ ( ( 𝑃 ∖ { 𝑧 } ) ≈ 1o → ∪ ( 𝑃 ∖ { 𝑧 } ) ∈ ( 𝑃 ∖ { 𝑧 } ) )
20 eldifsni ⊢ ( ∪ ( 𝑃 ∖ { 𝑧 } ) ∈ ( 𝑃 ∖ { 𝑧 } ) → ∪ ( 𝑃 ∖ { 𝑧 } ) ≠ 𝑧 )
21 18 19 20 3syl ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) ∧ 𝑧 ∈ 𝑃 ) → ∪ ( 𝑃 ∖ { 𝑧 } ) ≠ 𝑧 )
22 11 21 eqnetrd ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) ∧ 𝑧 ∈ 𝑃 ) → if ( 𝑧 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑧 } ) , 𝑧 ) ≠ 𝑧 )
23 22 ex ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) → ( 𝑧 ∈ 𝑃 → if ( 𝑧 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑧 } ) , 𝑧 ) ≠ 𝑧 ) )
24 9 23 impbid2 ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) → ( if ( 𝑧 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑧 } ) , 𝑧 ) ≠ 𝑧 ↔ 𝑧 ∈ 𝑃 ) )
25 24 adantr ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) ∧ 𝑧 ∈ 𝐷 ) → ( if ( 𝑧 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑧 } ) , 𝑧 ) ≠ 𝑧 ↔ 𝑧 ∈ 𝑃 ) )
26 7 25 bitrd ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) ∧ 𝑧 ∈ 𝐷 ) → ( ( ( 𝑇 ‘ 𝑃 ) ‘ 𝑧 ) ≠ 𝑧 ↔ 𝑧 ∈ 𝑃 ) )
27 26 rabbidva ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) → { 𝑧 ∈ 𝐷 ∣ ( ( 𝑇 ‘ 𝑃 ) ‘ 𝑧 ) ≠ 𝑧 } = { 𝑧 ∈ 𝐷 ∣ 𝑧 ∈ 𝑃 } )
28 incom ⊢ ( 𝑃 ∩ 𝐷 ) = ( 𝐷 ∩ 𝑃 )
29 dfin5 ⊢ ( 𝐷 ∩ 𝑃 ) = { 𝑧 ∈ 𝐷 ∣ 𝑧 ∈ 𝑃 }
30 28 29 eqtri ⊢ ( 𝑃 ∩ 𝐷 ) = { 𝑧 ∈ 𝐷 ∣ 𝑧 ∈ 𝑃 }
31 27 30 eqtr4di ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) → { 𝑧 ∈ 𝐷 ∣ ( ( 𝑇 ‘ 𝑃 ) ‘ 𝑧 ) ≠ 𝑧 } = ( 𝑃 ∩ 𝐷 ) )
32 simp2 ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) → 𝑃 ⊆ 𝐷 )
33 dfss2 ⊢ ( 𝑃 ⊆ 𝐷 ↔ ( 𝑃 ∩ 𝐷 ) = 𝑃 )
34 32 33 sylib ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) → ( 𝑃 ∩ 𝐷 ) = 𝑃 )
35 5 31 34 3eqtrd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) → dom ( ( 𝑇 ‘ 𝑃 ) ∖ I ) = 𝑃 )