Metamath Proof Explorer

Theorem pmtrval

Description: A generated transposition, expressed in a symmetric form. (Contributed by Stefan O'Rear, 16-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 pmtrfval.t ⊢ T = pmTrsp ⁡ D
2 1 pmtrfval ⊢ D ∈ V → T = p ∈ y ∈ 𝒫 D | y ≈ 2 𝑜 ⟼ z ∈ D ⟼ if z ∈ p ⋃ p ∖ z z
3 2 fveq1d ⊢ D ∈ V → T ⁡ P = p ∈ y ∈ 𝒫 D | y ≈ 2 𝑜 ⟼ z ∈ D ⟼ if z ∈ p ⋃ p ∖ z z ⁡ P
4 3 3ad2ant1 ⊢ D ∈ V ∧ P ⊆ D ∧ P ≈ 2 𝑜 → T ⁡ P = p ∈ y ∈ 𝒫 D | y ≈ 2 𝑜 ⟼ z ∈ D ⟼ if z ∈ p ⋃ p ∖ z z ⁡ P
5 eqid ⊢ p ∈ y ∈ 𝒫 D | y ≈ 2 𝑜 ⟼ z ∈ D ⟼ if z ∈ p ⋃ p ∖ z z = p ∈ y ∈ 𝒫 D | y ≈ 2 𝑜 ⟼ z ∈ D ⟼ if z ∈ p ⋃ p ∖ z z
6 eleq2 ⊢ p = P → z ∈ p ↔ z ∈ P
7 difeq1 ⊢ p = P → p ∖ z = P ∖ z
8 7 unieqd ⊢ p = P → ⋃ p ∖ z = ⋃ P ∖ z
9 6 8 ifbieq1d ⊢ p = P → if z ∈ p ⋃ p ∖ z z = if z ∈ P ⋃ P ∖ z z
10 9 mpteq2dv ⊢ p = P → z ∈ D ⟼ if z ∈ p ⋃ p ∖ z z = z ∈ D ⟼ if z ∈ P ⋃ P ∖ z z
11 breq1 ⊢ y = P → y ≈ 2 𝑜 ↔ P ≈ 2 𝑜
12 elpw2g ⊢ D ∈ V → P ∈ 𝒫 D ↔ P ⊆ D
13 12 biimpar ⊢ D ∈ V ∧ P ⊆ D → P ∈ 𝒫 D
14 13 3adant3 ⊢ D ∈ V ∧ P ⊆ D ∧ P ≈ 2 𝑜 → P ∈ 𝒫 D
15 simp3 ⊢ D ∈ V ∧ P ⊆ D ∧ P ≈ 2 𝑜 → P ≈ 2 𝑜
16 11 14 15 elrabd ⊢ D ∈ V ∧ P ⊆ D ∧ P ≈ 2 𝑜 → P ∈ y ∈ 𝒫 D | y ≈ 2 𝑜
17 mptexg ⊢ D ∈ V → z ∈ D ⟼ if z ∈ P ⋃ P ∖ z z ∈ V
18 17 3ad2ant1 ⊢ D ∈ V ∧ P ⊆ D ∧ P ≈ 2 𝑜 → z ∈ D ⟼ if z ∈ P ⋃ P ∖ z z ∈ V
19 5 10 16 18 fvmptd3 ⊢ D ∈ V ∧ P ⊆ D ∧ P ≈ 2 𝑜 → p ∈ y ∈ 𝒫 D | y ≈ 2 𝑜 ⟼ z ∈ D ⟼ if z ∈ p ⋃ p ∖ z z ⁡ P = z ∈ D ⟼ if z ∈ P ⋃ P ∖ z z
20 4 19 eqtrd ⊢ D ∈ V ∧ P ⊆ D ∧ P ≈ 2 𝑜 → T ⁡ P = z ∈ D ⟼ if z ∈ P ⋃ P ∖ z z