Metamath Proof Explorer

Theorem pmtrrn

Description: Transposing two points gives a transposition function. (Contributed by Stefan O'Rear, 22-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 pmtrrn.t ⊢T=pmTrsp⁡D
2 pmtrrn.r ⊢R=ran⁡T
3 mptexg ⊢D∈V→y∈D⟼ify∈z⋃z∖yy∈V
4 3 ralrimivw ⊢D∈V→∀z∈x∈𝒫D|x≈2𝑜y∈D⟼ify∈z⋃z∖yy∈V
5 4 3ad2ant1 ⊢D∈V∧P⊆D∧P≈2𝑜→∀z∈x∈𝒫D|x≈2𝑜y∈D⟼ify∈z⋃z∖yy∈V
6 eqid ⊢z∈x∈𝒫D|x≈2𝑜⟼y∈D⟼ify∈z⋃z∖yy=z∈x∈𝒫D|x≈2𝑜⟼y∈D⟼ify∈z⋃z∖yy
7 6 fnmpt ⊢∀z∈x∈𝒫D|x≈2𝑜y∈D⟼ify∈z⋃z∖yy∈V→z∈x∈𝒫D|x≈2𝑜⟼y∈D⟼ify∈z⋃z∖yyFnx∈𝒫D|x≈2𝑜
8 5 7 syl ⊢D∈V∧P⊆D∧P≈2𝑜→z∈x∈𝒫D|x≈2𝑜⟼y∈D⟼ify∈z⋃z∖yyFnx∈𝒫D|x≈2𝑜
9 1 pmtrfval ⊢D∈V→T=z∈x∈𝒫D|x≈2𝑜⟼y∈D⟼ify∈z⋃z∖yy
10 9 3ad2ant1 ⊢D∈V∧P⊆D∧P≈2𝑜→T=z∈x∈𝒫D|x≈2𝑜⟼y∈D⟼ify∈z⋃z∖yy
11 10 fneq1d ⊢D∈V∧P⊆D∧P≈2𝑜→TFnx∈𝒫D|x≈2𝑜↔z∈x∈𝒫D|x≈2𝑜⟼y∈D⟼ify∈z⋃z∖yyFnx∈𝒫D|x≈2𝑜
12 8 11 mpbird ⊢D∈V∧P⊆D∧P≈2𝑜→TFnx∈𝒫D|x≈2𝑜
13 breq1 ⊢x=P→x≈2𝑜↔P≈2𝑜
14 elpw2g ⊢D∈V→P∈𝒫D↔P⊆D
15 14 biimpar ⊢D∈V∧P⊆D→P∈𝒫D
16 15 3adant3 ⊢D∈V∧P⊆D∧P≈2𝑜→P∈𝒫D
17 simp3 ⊢D∈V∧P⊆D∧P≈2𝑜→P≈2𝑜
18 13 16 17 elrabd ⊢D∈V∧P⊆D∧P≈2𝑜→P∈x∈𝒫D|x≈2𝑜
19 fnfvelrn ⊢TFnx∈𝒫D|x≈2𝑜∧P∈x∈𝒫D|x≈2𝑜→T⁡P∈ran⁡T
20 12 18 19 syl2anc ⊢D∈V∧P⊆D∧P≈2𝑜→T⁡P∈ran⁡T
21 20 2 eleqtrrdi ⊢D∈V∧P⊆D∧P≈2𝑜→T⁡P∈R