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 ) → ( 𝑇 ‘ 𝑃 ) : 𝐷 ⟶ 𝐷 )