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

Metamath Proof Explorer

Theorem pmtrf

Description: Functionality of a transposition. (Contributed by Stefan O'Rear, 16-Aug-2015)

Ref Expression
Hypothesis pmtrfval.t ⊢ 𝑇 = ( pmTrsp ‘ 𝐷 )
Assertion pmtrf ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) → ( 𝑇 ‘ 𝑃 ) : 𝐷 ⟶ 𝐷 )

Proof

Step Hyp Ref Expression
1 pmtrfval.t ⊢ 𝑇 = ( pmTrsp ‘ 𝐷 )
2 1 pmtrval ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) → ( 𝑇 ‘ 𝑃 ) = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑧 } ) , 𝑧 ) ) )
3 simpll2 ⊢ ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑧 ∈ 𝑃 ) → 𝑃 ⊆ 𝐷 )
4 1onn ⊢ 1o ∈ ω
5 simpll3 ⊢ ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑧 ∈ 𝑃 ) → 𝑃 ≈ 2o )
6 df-2o ⊢ 2o = suc 1o
7 5 6 breqtrdi ⊢ ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑧 ∈ 𝑃 ) → 𝑃 ≈ suc 1o )
8 simpr ⊢ ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑧 ∈ 𝑃 ) → 𝑧 ∈ 𝑃 )
9 dif1ennn ⊢ ( ( 1o ∈ ω ∧ 𝑃 ≈ suc 1o ∧ 𝑧 ∈ 𝑃 ) → ( 𝑃 ∖ { 𝑧 } ) ≈ 1o )
10 4 7 8 9 mp3an2i ⊢ ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑧 ∈ 𝑃 ) → ( 𝑃 ∖ { 𝑧 } ) ≈ 1o )
11 en1uniel ⊢ ( ( 𝑃 ∖ { 𝑧 } ) ≈ 1o → ∪ ( 𝑃 ∖ { 𝑧 } ) ∈ ( 𝑃 ∖ { 𝑧 } ) )
12 eldifi ⊢ ( ∪ ( 𝑃 ∖ { 𝑧 } ) ∈ ( 𝑃 ∖ { 𝑧 } ) → ∪ ( 𝑃 ∖ { 𝑧 } ) ∈ 𝑃 )
13 10 11 12 3syl ⊢ ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑧 ∈ 𝑃 ) → ∪ ( 𝑃 ∖ { 𝑧 } ) ∈ 𝑃 )
14 3 13 sseldd ⊢ ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑧 ∈ 𝑃 ) → ∪ ( 𝑃 ∖ { 𝑧 } ) ∈ 𝐷 )
15 simplr ⊢ ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) ∧ 𝑧 ∈ 𝐷 ) ∧ ¬ 𝑧 ∈ 𝑃 ) → 𝑧 ∈ 𝐷 )
16 14 15 ifclda ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) ∧ 𝑧 ∈ 𝐷 ) → if ( 𝑧 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑧 } ) , 𝑧 ) ∈ 𝐷 )
17 2 16 fmpt3d ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) → ( 𝑇 ‘ 𝑃 ) : 𝐷 ⟶ 𝐷 )