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 ⟼ if y ∈ z ⋃ z ∖ y y ∈ V
4 3 ralrimivw ⊢ D ∈ V → ∀ z ∈ x ∈ 𝒫 D | x ≈ 2 𝑜 y ∈ D ⟼ if y ∈ z ⋃ z ∖ y y ∈ V
5 4 3ad2ant1 ⊢ D ∈ V ∧ P ⊆ D ∧ P ≈ 2 𝑜 → ∀ z ∈ x ∈ 𝒫 D | x ≈ 2 𝑜 y ∈ D ⟼ if y ∈ z ⋃ z ∖ y y ∈ V
6 eqid ⊢ z ∈ x ∈ 𝒫 D | x ≈ 2 𝑜 ⟼ y ∈ D ⟼ if y ∈ z ⋃ z ∖ y y = z ∈ x ∈ 𝒫 D | x ≈ 2 𝑜 ⟼ y ∈ D ⟼ if y ∈ z ⋃ z ∖ y y
7 6 fnmpt ⊢ ∀ z ∈ x ∈ 𝒫 D | x ≈ 2 𝑜 y ∈ D ⟼ if y ∈ z ⋃ z ∖ y y ∈ V → z ∈ x ∈ 𝒫 D | x ≈ 2 𝑜 ⟼ y ∈ D ⟼ if y ∈ z ⋃ z ∖ y y Fn x ∈ 𝒫 D | x ≈ 2 𝑜
8 5 7 syl ⊢ D ∈ V ∧ P ⊆ D ∧ P ≈ 2 𝑜 → z ∈ x ∈ 𝒫 D | x ≈ 2 𝑜 ⟼ y ∈ D ⟼ if y ∈ z ⋃ z ∖ y y Fn x ∈ 𝒫 D | x ≈ 2 𝑜
9 1 pmtrfval ⊢ D ∈ V → T = z ∈ x ∈ 𝒫 D | x ≈ 2 𝑜 ⟼ y ∈ D ⟼ if y ∈ z ⋃ z ∖ y y
10 9 3ad2ant1 ⊢ D ∈ V ∧ P ⊆ D ∧ P ≈ 2 𝑜 → T = z ∈ x ∈ 𝒫 D | x ≈ 2 𝑜 ⟼ y ∈ D ⟼ if y ∈ z ⋃ z ∖ y y
11 10 fneq1d ⊢ D ∈ V ∧ P ⊆ D ∧ P ≈ 2 𝑜 → T Fn x ∈ 𝒫 D | x ≈ 2 𝑜 ↔ z ∈ x ∈ 𝒫 D | x ≈ 2 𝑜 ⟼ y ∈ D ⟼ if y ∈ z ⋃ z ∖ y y Fn x ∈ 𝒫 D | x ≈ 2 𝑜
12 8 11 mpbird ⊢ D ∈ V ∧ P ⊆ D ∧ P ≈ 2 𝑜 → T Fn x ∈ 𝒫 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 ⊢ T Fn x ∈ 𝒫 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