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⟼ifz∈P⋃P∖zz

Proof

Step Hyp Ref Expression
1 pmtrfval.t ⊢T=pmTrsp⁡D
2 1 pmtrfval ⊢D∈V→T=p∈y∈𝒫D|y≈2𝑜⟼z∈D⟼ifz∈p⋃p∖zz
3 2 fveq1d ⊢D∈V→T⁡P=p∈y∈𝒫D|y≈2𝑜⟼z∈D⟼ifz∈p⋃p∖zz⁡P
4 3 3ad2ant1 ⊢D∈V∧P⊆D∧P≈2𝑜→T⁡P=p∈y∈𝒫D|y≈2𝑜⟼z∈D⟼ifz∈p⋃p∖zz⁡P
5 eqid ⊢p∈y∈𝒫D|y≈2𝑜⟼z∈D⟼ifz∈p⋃p∖zz=p∈y∈𝒫D|y≈2𝑜⟼z∈D⟼ifz∈p⋃p∖zz
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→ifz∈p⋃p∖zz=ifz∈P⋃P∖zz
10 9 mpteq2dv ⊢p=P→z∈D⟼ifz∈p⋃p∖zz=z∈D⟼ifz∈P⋃P∖zz
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⟼ifz∈P⋃P∖zz∈V
18 17 3ad2ant1 ⊢D∈V∧P⊆D∧P≈2𝑜→z∈D⟼ifz∈P⋃P∖zz∈V
19 5 10 16 18 fvmptd3 ⊢D∈V∧P⊆D∧P≈2𝑜→p∈y∈𝒫D|y≈2𝑜⟼z∈D⟼ifz∈p⋃p∖zz⁡P=z∈D⟼ifz∈P⋃P∖zz
20 4 19 eqtrd ⊢D∈V∧P⊆D∧P≈2𝑜→T⁡P=z∈D⟼ifz∈P⋃P∖zz