Metamath Proof Explorer

Theorem pmtrfrn

Description: A transposition (as a kind of function) is the function transposing the two points it moves. (Contributed by Stefan O'Rear, 22-Aug-2015)

Ref Expression
Hypotheses pmtrrn.t ⊢T=pmTrsp⁡D
pmtrrn.r ⊢R=ran⁡T
pmtrfrn.p ⊢P=dom⁡F∖I
Assertion pmtrfrn ⊢F∈R→D∈V∧P⊆D∧P≈2𝑜∧F=T⁡P

Proof

Step Hyp Ref Expression
1 pmtrrn.t ⊢T=pmTrsp⁡D
2 pmtrrn.r ⊢R=ran⁡T
3 pmtrfrn.p ⊢P=dom⁡F∖I
4 noel ⊢¬F∈∅
5 1 rnfvprc ⊢¬D∈V→ran⁡T=∅
6 2 5 eqtrid ⊢¬D∈V→R=∅
7 6 eleq2d ⊢¬D∈V→F∈R↔F∈∅
8 4 7 mtbiri ⊢¬D∈V→¬F∈R
9 8 con4i ⊢F∈R→D∈V
10 mptexg ⊢D∈V→z∈D⟼ifz∈w⋃w∖zz∈V
11 10 ralrimivw ⊢D∈V→∀w∈x∈𝒫D|x≈2𝑜z∈D⟼ifz∈w⋃w∖zz∈V
12 eqid ⊢w∈x∈𝒫D|x≈2𝑜⟼z∈D⟼ifz∈w⋃w∖zz=w∈x∈𝒫D|x≈2𝑜⟼z∈D⟼ifz∈w⋃w∖zz
13 12 fnmpt ⊢∀w∈x∈𝒫D|x≈2𝑜z∈D⟼ifz∈w⋃w∖zz∈V→w∈x∈𝒫D|x≈2𝑜⟼z∈D⟼ifz∈w⋃w∖zzFnx∈𝒫D|x≈2𝑜
14 11 13 syl ⊢D∈V→w∈x∈𝒫D|x≈2𝑜⟼z∈D⟼ifz∈w⋃w∖zzFnx∈𝒫D|x≈2𝑜
15 1 pmtrfval ⊢D∈V→T=w∈x∈𝒫D|x≈2𝑜⟼z∈D⟼ifz∈w⋃w∖zz
16 15 fneq1d ⊢D∈V→TFnx∈𝒫D|x≈2𝑜↔w∈x∈𝒫D|x≈2𝑜⟼z∈D⟼ifz∈w⋃w∖zzFnx∈𝒫D|x≈2𝑜
17 14 16 mpbird ⊢D∈V→TFnx∈𝒫D|x≈2𝑜
18 fvelrnb ⊢TFnx∈𝒫D|x≈2𝑜→F∈ran⁡T↔∃y∈x∈𝒫D|x≈2𝑜T⁡y=F
19 17 18 syl ⊢D∈V→F∈ran⁡T↔∃y∈x∈𝒫D|x≈2𝑜T⁡y=F
20 2 eleq2i ⊢F∈R↔F∈ran⁡T
21 breq1 ⊢x=y→x≈2𝑜↔y≈2𝑜
22 21 rexrab ⊢∃y∈x∈𝒫D|x≈2𝑜T⁡y=F↔∃y∈𝒫Dy≈2𝑜∧T⁡y=F
23 22 bicomi ⊢∃y∈𝒫Dy≈2𝑜∧T⁡y=F↔∃y∈x∈𝒫D|x≈2𝑜T⁡y=F
24 19 20 23 3bitr4g ⊢D∈V→F∈R↔∃y∈𝒫Dy≈2𝑜∧T⁡y=F
25 elpwi ⊢y∈𝒫D→y⊆D
26 simp1 ⊢D∈V∧y⊆D∧y≈2𝑜→D∈V
27 1 pmtrmvd ⊢D∈V∧y⊆D∧y≈2𝑜→dom⁡T⁡y∖I=y
28 simp2 ⊢D∈V∧y⊆D∧y≈2𝑜→y⊆D
29 27 28 eqsstrd ⊢D∈V∧y⊆D∧y≈2𝑜→dom⁡T⁡y∖I⊆D
30 simp3 ⊢D∈V∧y⊆D∧y≈2𝑜→y≈2𝑜
31 27 30 eqbrtrd ⊢D∈V∧y⊆D∧y≈2𝑜→dom⁡T⁡y∖I≈2𝑜
32 26 29 31 3jca ⊢D∈V∧y⊆D∧y≈2𝑜→D∈V∧dom⁡T⁡y∖I⊆D∧dom⁡T⁡y∖I≈2𝑜
33 27 eqcomd ⊢D∈V∧y⊆D∧y≈2𝑜→y=dom⁡T⁡y∖I
34 33 fveq2d ⊢D∈V∧y⊆D∧y≈2𝑜→T⁡y=T⁡dom⁡T⁡y∖I
35 32 34 jca ⊢D∈V∧y⊆D∧y≈2𝑜→D∈V∧dom⁡T⁡y∖I⊆D∧dom⁡T⁡y∖I≈2𝑜∧T⁡y=T⁡dom⁡T⁡y∖I
36 difeq1 ⊢T⁡y=F→T⁡y∖I=F∖I
37 36 dmeqd ⊢T⁡y=F→dom⁡T⁡y∖I=dom⁡F∖I
38 37 3 eqtr4di ⊢T⁡y=F→dom⁡T⁡y∖I=P
39 sseq1 ⊢dom⁡T⁡y∖I=P→dom⁡T⁡y∖I⊆D↔P⊆D
40 breq1 ⊢dom⁡T⁡y∖I=P→dom⁡T⁡y∖I≈2𝑜↔P≈2𝑜
41 39 40 3anbi23d ⊢dom⁡T⁡y∖I=P→D∈V∧dom⁡T⁡y∖I⊆D∧dom⁡T⁡y∖I≈2𝑜↔D∈V∧P⊆D∧P≈2𝑜
42 41 adantl ⊢T⁡y=F∧dom⁡T⁡y∖I=P→D∈V∧dom⁡T⁡y∖I⊆D∧dom⁡T⁡y∖I≈2𝑜↔D∈V∧P⊆D∧P≈2𝑜
43 simpl ⊢T⁡y=F∧dom⁡T⁡y∖I=P→T⁡y=F
44 fveq2 ⊢dom⁡T⁡y∖I=P→T⁡dom⁡T⁡y∖I=T⁡P
45 44 adantl ⊢T⁡y=F∧dom⁡T⁡y∖I=P→T⁡dom⁡T⁡y∖I=T⁡P
46 43 45 eqeq12d ⊢T⁡y=F∧dom⁡T⁡y∖I=P→T⁡y=T⁡dom⁡T⁡y∖I↔F=T⁡P
47 42 46 anbi12d ⊢T⁡y=F∧dom⁡T⁡y∖I=P→D∈V∧dom⁡T⁡y∖I⊆D∧dom⁡T⁡y∖I≈2𝑜∧T⁡y=T⁡dom⁡T⁡y∖I↔D∈V∧P⊆D∧P≈2𝑜∧F=T⁡P
48 38 47 mpdan ⊢T⁡y=F→D∈V∧dom⁡T⁡y∖I⊆D∧dom⁡T⁡y∖I≈2𝑜∧T⁡y=T⁡dom⁡T⁡y∖I↔D∈V∧P⊆D∧P≈2𝑜∧F=T⁡P
49 35 48 syl5ibcom ⊢D∈V∧y⊆D∧y≈2𝑜→T⁡y=F→D∈V∧P⊆D∧P≈2𝑜∧F=T⁡P
50 49 3exp ⊢D∈V→y⊆D→y≈2𝑜→T⁡y=F→D∈V∧P⊆D∧P≈2𝑜∧F=T⁡P
51 50 imp4a ⊢D∈V→y⊆D→y≈2𝑜∧T⁡y=F→D∈V∧P⊆D∧P≈2𝑜∧F=T⁡P
52 25 51 syl5 ⊢D∈V→y∈𝒫D→y≈2𝑜∧T⁡y=F→D∈V∧P⊆D∧P≈2𝑜∧F=T⁡P
53 52 rexlimdv ⊢D∈V→∃y∈𝒫Dy≈2𝑜∧T⁡y=F→D∈V∧P⊆D∧P≈2𝑜∧F=T⁡P
54 24 53 sylbid ⊢D∈V→F∈R→D∈V∧P⊆D∧P≈2𝑜∧F=T⁡P
55 9 54 mpcom ⊢F∈R→D∈V∧P⊆D∧P≈2𝑜∧F=T⁡P