Metamath Proof Explorer

Theorem pmtrmvd

Description: A transposition moves precisely the transposed points. (Contributed by Stefan O'Rear, 16-Aug-2015)

Ref Expression
Hypothesis pmtrfval.t ⊢T=pmTrsp⁡D
Assertion pmtrmvd ⊢D∈V∧P⊆D∧P≈2𝑜→dom⁡T⁡P∖I=P

Proof

Step Hyp Ref Expression
1 pmtrfval.t ⊢T=pmTrsp⁡D
2 1 pmtrf ⊢D∈V∧P⊆D∧P≈2𝑜→T⁡P:D⟶D
3 ffn ⊢T⁡P:D⟶D→T⁡PFnD
4 fndifnfp ⊢T⁡PFnD→dom⁡T⁡P∖I=z∈D|T⁡P⁡z≠z
5 2 3 4 3syl ⊢D∈V∧P⊆D∧P≈2𝑜→dom⁡T⁡P∖I=z∈D|T⁡P⁡z≠z
6 1 pmtrfv ⊢D∈V∧P⊆D∧P≈2𝑜∧z∈D→T⁡P⁡z=ifz∈P⋃P∖zz
7 6 neeq1d ⊢D∈V∧P⊆D∧P≈2𝑜∧z∈D→T⁡P⁡z≠z↔ifz∈P⋃P∖zz≠z
8 iffalse ⊢¬z∈P→ifz∈P⋃P∖zz=z
9 8 necon1ai ⊢ifz∈P⋃P∖zz≠z→z∈P
10 iftrue ⊢z∈P→ifz∈P⋃P∖zz=⋃P∖z
11 10 adantl ⊢D∈V∧P⊆D∧P≈2𝑜∧z∈P→ifz∈P⋃P∖zz=⋃P∖z
12 1onn ⊢1𝑜∈ω
13 simpl3 ⊢D∈V∧P⊆D∧P≈2𝑜∧z∈P→P≈2𝑜
14 df-2o ⊢2𝑜=suc⁡1𝑜
15 13 14 breqtrdi ⊢D∈V∧P⊆D∧P≈2𝑜∧z∈P→P≈suc⁡1𝑜
16 simpr ⊢D∈V∧P⊆D∧P≈2𝑜∧z∈P→z∈P
17 dif1ennn ⊢1𝑜∈ω∧P≈suc⁡1𝑜∧z∈P→P∖z≈1𝑜
18 12 15 16 17 mp3an2i ⊢D∈V∧P⊆D∧P≈2𝑜∧z∈P→P∖z≈1𝑜
19 en1uniel ⊢P∖z≈1𝑜→⋃P∖z∈P∖z
20 eldifsni ⊢⋃P∖z∈P∖z→⋃P∖z≠z
21 18 19 20 3syl ⊢D∈V∧P⊆D∧P≈2𝑜∧z∈P→⋃P∖z≠z
22 11 21 eqnetrd ⊢D∈V∧P⊆D∧P≈2𝑜∧z∈P→ifz∈P⋃P∖zz≠z
23 22 ex ⊢D∈V∧P⊆D∧P≈2𝑜→z∈P→ifz∈P⋃P∖zz≠z
24 9 23 impbid2 ⊢D∈V∧P⊆D∧P≈2𝑜→ifz∈P⋃P∖zz≠z↔z∈P
25 24 adantr ⊢D∈V∧P⊆D∧P≈2𝑜∧z∈D→ifz∈P⋃P∖zz≠z↔z∈P
26 7 25 bitrd ⊢D∈V∧P⊆D∧P≈2𝑜∧z∈D→T⁡P⁡z≠z↔z∈P
27 26 rabbidva ⊢D∈V∧P⊆D∧P≈2𝑜→z∈D|T⁡P⁡z≠z=z∈D|z∈P
28 incom ⊢P∩D=D∩P
29 dfin5 ⊢D∩P=z∈D|z∈P
30 28 29 eqtri ⊢P∩D=z∈D|z∈P
31 27 30 eqtr4di ⊢D∈V∧P⊆D∧P≈2𝑜→z∈D|T⁡P⁡z≠z=P∩D
32 simp2 ⊢D∈V∧P⊆D∧P≈2𝑜→P⊆D
33 df-ss ⊢P⊆D↔P∩D=P
34 32 33 sylib ⊢D∈V∧P⊆D∧P≈2𝑜→P∩D=P
35 5 31 34 3eqtrd ⊢D∈V∧P⊆D∧P≈2𝑜→dom⁡T⁡P∖I=P