Theorem pmtrfv

Description: General value of mapping a point under a transposition. (Contributed by Stefan O'Rear, 16-Aug-2015)

	Ref	Expression
Hypothesis	pmtrfval.t	⊢ 𝑇 = ( pmTrsp ‘ 𝐷 )
Assertion	pmtrfv	⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) ∧ 𝑍 ∈ 𝐷 ) → ( ( 𝑇 ‘ 𝑃 ) ‘ 𝑍 ) = if ( 𝑍 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑍 } ) , 𝑍 ) )

Proof

Step	Hyp	Ref	Expression
1		pmtrfval.t	⊢ 𝑇 = ( pmTrsp ‘ 𝐷 )
2	1	pmtrval	⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) → ( 𝑇 ‘ 𝑃 ) = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑧 } ) , 𝑧 ) ) )
3	2	fveq1d	⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) → ( ( 𝑇 ‘ 𝑃 ) ‘ 𝑍 ) = ( ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑧 } ) , 𝑧 ) ) ‘ 𝑍 ) )
4	3	adantr	⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) ∧ 𝑍 ∈ 𝐷 ) → ( ( 𝑇 ‘ 𝑃 ) ‘ 𝑍 ) = ( ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑧 } ) , 𝑧 ) ) ‘ 𝑍 ) )
5		eqid	⊢ ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑧 } ) , 𝑧 ) ) = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑧 } ) , 𝑧 ) )
6		eleq1	⊢ ( 𝑧 = 𝑍 → ( 𝑧 ∈ 𝑃 ↔ 𝑍 ∈ 𝑃 ) )
7		sneq	⊢ ( 𝑧 = 𝑍 → { 𝑧 } = { 𝑍 } )
8	7	difeq2d	⊢ ( 𝑧 = 𝑍 → ( 𝑃 ∖ { 𝑧 } ) = ( 𝑃 ∖ { 𝑍 } ) )
9	8	unieqd	⊢ ( 𝑧 = 𝑍 → ∪ ( 𝑃 ∖ { 𝑧 } ) = ∪ ( 𝑃 ∖ { 𝑍 } ) )
10		id	⊢ ( 𝑧 = 𝑍 → 𝑧 = 𝑍 )
11	6 9 10	ifbieq12d	⊢ ( 𝑧 = 𝑍 → if ( 𝑧 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑧 } ) , 𝑧 ) = if ( 𝑍 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑍 } ) , 𝑍 ) )
12		simpr	⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) ∧ 𝑍 ∈ 𝐷 ) → 𝑍 ∈ 𝐷 )
13		simpl3	⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) ∧ 𝑍 ∈ 𝐷 ) → 𝑃 ≈ 2o )
14		relen	⊢ Rel ≈
15	14	brrelex1i	⊢ ( 𝑃 ≈ 2o → 𝑃 ∈ V )
16		difexg	⊢ ( 𝑃 ∈ V → ( 𝑃 ∖ { 𝑍 } ) ∈ V )
17		uniexg	⊢ ( ( 𝑃 ∖ { 𝑍 } ) ∈ V → ∪ ( 𝑃 ∖ { 𝑍 } ) ∈ V )
18	13 15 16 17	4syl	⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) ∧ 𝑍 ∈ 𝐷 ) → ∪ ( 𝑃 ∖ { 𝑍 } ) ∈ V )
19		ifexg	⊢ ( ( ∪ ( 𝑃 ∖ { 𝑍 } ) ∈ V ∧ 𝑍 ∈ 𝐷 ) → if ( 𝑍 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑍 } ) , 𝑍 ) ∈ V )
20	18 19	sylancom	⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) ∧ 𝑍 ∈ 𝐷 ) → if ( 𝑍 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑍 } ) , 𝑍 ) ∈ V )
21	5 11 12 20	fvmptd3	⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) ∧ 𝑍 ∈ 𝐷 ) → ( ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑧 } ) , 𝑧 ) ) ‘ 𝑍 ) = if ( 𝑍 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑍 } ) , 𝑍 ) )
22	4 21	eqtrd	⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) ∧ 𝑍 ∈ 𝐷 ) → ( ( 𝑇 ‘ 𝑃 ) ‘ 𝑍 ) = if ( 𝑍 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑍 } ) , 𝑍 ) )