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 ) = 𝑃 )