Metamath Proof Explorer

Theorem pmtrrn

Description: Transposing two points gives a transposition function. (Contributed by Stefan O'Rear, 22-Aug-2015)

Ref Expression
Hypotheses pmtrrn.t ⊢ 𝑇 = ( pmTrsp ‘ 𝐷 )
pmtrrn.r ⊢ 𝑅 = ran 𝑇
Assertion pmtrrn ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) → ( 𝑇 ‘ 𝑃 ) ∈ 𝑅 )

Proof

Step Hyp Ref Expression
1 pmtrrn.t ⊢ 𝑇 = ( pmTrsp ‘ 𝐷 )
2 pmtrrn.r ⊢ 𝑅 = ran 𝑇
3 mptexg ⊢ ( 𝐷 ∈ 𝑉 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑧 , ∪ ( 𝑧 ∖ { 𝑦 } ) , 𝑦 ) ) ∈ V )
4 3 ralrimivw ⊢ ( 𝐷 ∈ 𝑉 → ∀ 𝑧 ∈ { 𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2o } ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑧 , ∪ ( 𝑧 ∖ { 𝑦 } ) , 𝑦 ) ) ∈ V )
5 4 3ad2ant1 ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) → ∀ 𝑧 ∈ { 𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2o } ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑧 , ∪ ( 𝑧 ∖ { 𝑦 } ) , 𝑦 ) ) ∈ V )
6 eqid ⊢ ( 𝑧 ∈ { 𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2o } ↦ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑧 , ∪ ( 𝑧 ∖ { 𝑦 } ) , 𝑦 ) ) ) = ( 𝑧 ∈ { 𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2o } ↦ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑧 , ∪ ( 𝑧 ∖ { 𝑦 } ) , 𝑦 ) ) )
7 6 fnmpt ⊢ ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2o } ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑧 , ∪ ( 𝑧 ∖ { 𝑦 } ) , 𝑦 ) ) ∈ V → ( 𝑧 ∈ { 𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2o } ↦ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑧 , ∪ ( 𝑧 ∖ { 𝑦 } ) , 𝑦 ) ) ) Fn { 𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2o } )
8 5 7 syl ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) → ( 𝑧 ∈ { 𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2o } ↦ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑧 , ∪ ( 𝑧 ∖ { 𝑦 } ) , 𝑦 ) ) ) Fn { 𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2o } )
9 1 pmtrfval ⊢ ( 𝐷 ∈ 𝑉 → 𝑇 = ( 𝑧 ∈ { 𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2o } ↦ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑧 , ∪ ( 𝑧 ∖ { 𝑦 } ) , 𝑦 ) ) ) )
10 9 3ad2ant1 ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) → 𝑇 = ( 𝑧 ∈ { 𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2o } ↦ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑧 , ∪ ( 𝑧 ∖ { 𝑦 } ) , 𝑦 ) ) ) )
11 10 fneq1d ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) → ( 𝑇 Fn { 𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2o } ↔ ( 𝑧 ∈ { 𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2o } ↦ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑧 , ∪ ( 𝑧 ∖ { 𝑦 } ) , 𝑦 ) ) ) Fn { 𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2o } ) )
12 8 11 mpbird ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) → 𝑇 Fn { 𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2o } )
13 breq1 ⊢ ( 𝑥 = 𝑃 → ( 𝑥 ≈ 2o ↔ 𝑃 ≈ 2o ) )
14 elpw2g ⊢ ( 𝐷 ∈ 𝑉 → ( 𝑃 ∈ 𝒫 𝐷 ↔ 𝑃 ⊆ 𝐷 ) )
15 14 biimpar ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ) → 𝑃 ∈ 𝒫 𝐷 )
16 15 3adant3 ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) → 𝑃 ∈ 𝒫 𝐷 )
17 simp3 ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) → 𝑃 ≈ 2o )
18 13 16 17 elrabd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) → 𝑃 ∈ { 𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2o } )
19 fnfvelrn ⊢ ( ( 𝑇 Fn { 𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2o } ∧ 𝑃 ∈ { 𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2o } ) → ( 𝑇 ‘ 𝑃 ) ∈ ran 𝑇 )
20 12 18 19 syl2anc ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) → ( 𝑇 ‘ 𝑃 ) ∈ ran 𝑇 )
21 20 2 eleqtrrdi ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) → ( 𝑇 ‘ 𝑃 ) ∈ 𝑅 )