Metamath Proof Explorer

Theorem pmtrfv

Description: General value of mapping a point under a transposition. (Contributed by Stefan O'Rear, 16-Aug-2015)

Ref Expression
Hypothesis pmtrfval.t ⊢ T = pmTrsp ⁡ D
Assertion pmtrfv ⊢ D ∈ V ∧ P ⊆ D ∧ P ≈ 2 𝑜 ∧ Z ∈ D → T ⁡ P ⁡ Z = if Z ∈ P ⋃ P ∖ Z Z

Proof

Step Hyp Ref Expression
1 pmtrfval.t ⊢ T = pmTrsp ⁡ D
2 1 pmtrval ⊢ D ∈ V ∧ P ⊆ D ∧ P ≈ 2 𝑜 → T ⁡ P = z ∈ D ⟼ if z ∈ P ⋃ P ∖ z z
3 2 fveq1d ⊢ D ∈ V ∧ P ⊆ D ∧ P ≈ 2 𝑜 → T ⁡ P ⁡ Z = z ∈ D ⟼ if z ∈ P ⋃ P ∖ z z ⁡ Z
4 3 adantr ⊢ D ∈ V ∧ P ⊆ D ∧ P ≈ 2 𝑜 ∧ Z ∈ D → T ⁡ P ⁡ Z = z ∈ D ⟼ if z ∈ P ⋃ P ∖ z z ⁡ Z
5 eqid ⊢ z ∈ D ⟼ if z ∈ P ⋃ P ∖ z z = z ∈ D ⟼ if z ∈ P ⋃ P ∖ z z
6 eleq1 ⊢ z = Z → z ∈ P ↔ Z ∈ P
7 sneq ⊢ z = Z → z = Z
8 7 difeq2d ⊢ z = Z → P ∖ z = P ∖ Z
9 8 unieqd ⊢ z = Z → ⋃ P ∖ z = ⋃ P ∖ Z
10 id ⊢ z = Z → z = Z
11 6 9 10 ifbieq12d ⊢ z = Z → if z ∈ P ⋃ P ∖ z z = if Z ∈ P ⋃ P ∖ Z Z
12 simpr ⊢ D ∈ V ∧ P ⊆ D ∧ P ≈ 2 𝑜 ∧ Z ∈ D → Z ∈ D
13 simpl3 ⊢ D ∈ V ∧ P ⊆ D ∧ P ≈ 2 𝑜 ∧ Z ∈ D → P ≈ 2 𝑜
14 relen ⊢ Rel ⁡ ≈
15 14 brrelex1i ⊢ P ≈ 2 𝑜 → P ∈ V
16 difexg ⊢ P ∈ V → P ∖ Z ∈ V
17 uniexg ⊢ P ∖ Z ∈ V → ⋃ P ∖ Z ∈ V
18 13 15 16 17 4syl ⊢ D ∈ V ∧ P ⊆ D ∧ P ≈ 2 𝑜 ∧ Z ∈ D → ⋃ P ∖ Z ∈ V
19 ifexg ⊢ ⋃ P ∖ Z ∈ V ∧ Z ∈ D → if Z ∈ P ⋃ P ∖ Z Z ∈ V
20 18 19 sylancom ⊢ D ∈ V ∧ P ⊆ D ∧ P ≈ 2 𝑜 ∧ Z ∈ D → if Z ∈ P ⋃ P ∖ Z Z ∈ V
21 5 11 12 20 fvmptd3 ⊢ D ∈ V ∧ P ⊆ D ∧ P ≈ 2 𝑜 ∧ Z ∈ D → z ∈ D ⟼ if z ∈ P ⋃ P ∖ z z ⁡ Z = if Z ∈ P ⋃ P ∖ Z Z
22 4 21 eqtrd ⊢ D ∈ V ∧ P ⊆ D ∧ P ≈ 2 𝑜 ∧ Z ∈ D → T ⁡ P ⁡ Z = if Z ∈ P ⋃ P ∖ Z Z