Metamath Proof Explorer

Theorem pmtrprfval

Description: The transpositions on a pair. (Contributed by AV, 9-Dec-2018)

Ref Expression
Assertion pmtrprfval ⊢ pmTrsp ⁡ 1 2 = p ∈ 1 2 ⟼ z ∈ 1 2 ⟼ if z = 1 2 1

Proof

Step Hyp Ref Expression
1 prex ⊢ 1 2 ∈ V
2 eqid ⊢ pmTrsp ⁡ 1 2 = pmTrsp ⁡ 1 2
3 2 pmtrfval ⊢ 1 2 ∈ V → pmTrsp ⁡ 1 2 = p ∈ t ∈ 𝒫 1 2 | t ≈ 2 𝑜 ⟼ z ∈ 1 2 ⟼ if z ∈ p ⋃ p ∖ z z
4 1 3 ax-mp ⊢ pmTrsp ⁡ 1 2 = p ∈ t ∈ 𝒫 1 2 | t ≈ 2 𝑜 ⟼ z ∈ 1 2 ⟼ if z ∈ p ⋃ p ∖ z z
5 1ex ⊢ 1 ∈ V
6 2nn0 ⊢ 2 ∈ ℕ 0
7 1ne2 ⊢ 1 ≠ 2
8 pr2pwpr ⊢ 1 ∈ V ∧ 2 ∈ ℕ 0 ∧ 1 ≠ 2 → t ∈ 𝒫 1 2 | t ≈ 2 𝑜 = 1 2
9 5 6 7 8 mp3an ⊢ t ∈ 𝒫 1 2 | t ≈ 2 𝑜 = 1 2
10 9 mpteq1i ⊢ p ∈ t ∈ 𝒫 1 2 | t ≈ 2 𝑜 ⟼ z ∈ 1 2 ⟼ if z ∈ p ⋃ p ∖ z z = p ∈ 1 2 ⟼ z ∈ 1 2 ⟼ if z ∈ p ⋃ p ∖ z z
11 elsni ⊢ p ∈ 1 2 → p = 1 2
12 eleq2 ⊢ p = 1 2 → z ∈ p ↔ z ∈ 1 2
13 12 biimpar ⊢ p = 1 2 ∧ z ∈ 1 2 → z ∈ p
14 13 iftrued ⊢ p = 1 2 ∧ z ∈ 1 2 → if z ∈ p ⋃ p ∖ z z = ⋃ p ∖ z
15 elpri ⊢ z ∈ 1 2 → z = 1 ∨ z = 2
16 2ex ⊢ 2 ∈ V
17 16 unisn ⊢ ⋃ 2 = 2
18 simpr ⊢ z = 1 ∧ p = 1 2 → p = 1 2
19 sneq ⊢ z = 1 → z = 1
20 19 adantr ⊢ z = 1 ∧ p = 1 2 → z = 1
21 18 20 difeq12d ⊢ z = 1 ∧ p = 1 2 → p ∖ z = 1 2 ∖ 1
22 difprsn1 ⊢ 1 ≠ 2 → 1 2 ∖ 1 = 2
23 7 22 ax-mp ⊢ 1 2 ∖ 1 = 2
24 21 23 eqtrdi ⊢ z = 1 ∧ p = 1 2 → p ∖ z = 2
25 24 unieqd ⊢ z = 1 ∧ p = 1 2 → ⋃ p ∖ z = ⋃ 2
26 iftrue ⊢ z = 1 → if z = 1 2 1 = 2
27 26 adantr ⊢ z = 1 ∧ p = 1 2 → if z = 1 2 1 = 2
28 17 25 27 3eqtr4a ⊢ z = 1 ∧ p = 1 2 → ⋃ p ∖ z = if z = 1 2 1
29 28 ex ⊢ z = 1 → p = 1 2 → ⋃ p ∖ z = if z = 1 2 1
30 5 unisn ⊢ ⋃ 1 = 1
31 simpr ⊢ z = 2 ∧ p = 1 2 → p = 1 2
32 sneq ⊢ z = 2 → z = 2
33 32 adantr ⊢ z = 2 ∧ p = 1 2 → z = 2
34 31 33 difeq12d ⊢ z = 2 ∧ p = 1 2 → p ∖ z = 1 2 ∖ 2
35 difprsn2 ⊢ 1 ≠ 2 → 1 2 ∖ 2 = 1
36 7 35 ax-mp ⊢ 1 2 ∖ 2 = 1
37 34 36 eqtrdi ⊢ z = 2 ∧ p = 1 2 → p ∖ z = 1
38 37 unieqd ⊢ z = 2 ∧ p = 1 2 → ⋃ p ∖ z = ⋃ 1
39 7 nesymi ⊢ ¬ 2 = 1
40 eqeq1 ⊢ z = 2 → z = 1 ↔ 2 = 1
41 39 40 mtbiri ⊢ z = 2 → ¬ z = 1
42 41 iffalsed ⊢ z = 2 → if z = 1 2 1 = 1
43 42 adantr ⊢ z = 2 ∧ p = 1 2 → if z = 1 2 1 = 1
44 30 38 43 3eqtr4a ⊢ z = 2 ∧ p = 1 2 → ⋃ p ∖ z = if z = 1 2 1
45 44 ex ⊢ z = 2 → p = 1 2 → ⋃ p ∖ z = if z = 1 2 1
46 29 45 jaoi ⊢ z = 1 ∨ z = 2 → p = 1 2 → ⋃ p ∖ z = if z = 1 2 1
47 15 46 syl ⊢ z ∈ 1 2 → p = 1 2 → ⋃ p ∖ z = if z = 1 2 1
48 47 impcom ⊢ p = 1 2 ∧ z ∈ 1 2 → ⋃ p ∖ z = if z = 1 2 1
49 14 48 eqtrd ⊢ p = 1 2 ∧ z ∈ 1 2 → if z ∈ p ⋃ p ∖ z z = if z = 1 2 1
50 11 49 sylan ⊢ p ∈ 1 2 ∧ z ∈ 1 2 → if z ∈ p ⋃ p ∖ z z = if z = 1 2 1
51 50 mpteq2dva ⊢ p ∈ 1 2 → z ∈ 1 2 ⟼ if z ∈ p ⋃ p ∖ z z = z ∈ 1 2 ⟼ if z = 1 2 1
52 51 mpteq2ia ⊢ p ∈ 1 2 ⟼ z ∈ 1 2 ⟼ if z ∈ p ⋃ p ∖ z z = p ∈ 1 2 ⟼ z ∈ 1 2 ⟼ if z = 1 2 1
53 10 52 eqtri ⊢ p ∈ t ∈ 𝒫 1 2 | t ≈ 2 𝑜 ⟼ z ∈ 1 2 ⟼ if z ∈ p ⋃ p ∖ z z = p ∈ 1 2 ⟼ z ∈ 1 2 ⟼ if z = 1 2 1
54 4 53 eqtri ⊢ pmTrsp ⁡ 1 2 = p ∈ 1 2 ⟼ z ∈ 1 2 ⟼ if z = 1 2 1