Metamath Proof Explorer

Theorem pmtrprfval

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

Ref Expression
Assertion pmtrprfval ( pmTrsp ‘ { 1 , 2 } ) = ( 𝑝 ∈ { { 1 , 2 } } ↦ ( 𝑧 ∈ { 1 , 2 } ↦ if ( 𝑧 = 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 } ) = ( 𝑝 ∈ { 𝑡 ∈ 𝒫 { 1 , 2 } ∣ 𝑡 ≈ 2o } ↦ ( 𝑧 ∈ { 1 , 2 } ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) )
4 1 3 ax-mp ⊢ ( pmTrsp ‘ { 1 , 2 } ) = ( 𝑝 ∈ { 𝑡 ∈ 𝒫 { 1 , 2 } ∣ 𝑡 ≈ 2o } ↦ ( 𝑧 ∈ { 1 , 2 } ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) )
5 1ex ⊢ 1 ∈ V
6 2nn0 ⊢ 2 ∈ ℕ0
7 1ne2 ⊢ 1 ≠ 2
8 pr2pwpr ⊢ ( ( 1 ∈ V ∧ 2 ∈ ℕ0 ∧ 1 ≠ 2 ) → { 𝑡 ∈ 𝒫 { 1 , 2 } ∣ 𝑡 ≈ 2o } = { { 1 , 2 } } )
9 5 6 7 8 mp3an ⊢ { 𝑡 ∈ 𝒫 { 1 , 2 } ∣ 𝑡 ≈ 2o } = { { 1 , 2 } }
10 9 mpteq1i ⊢ ( 𝑝 ∈ { 𝑡 ∈ 𝒫 { 1 , 2 } ∣ 𝑡 ≈ 2o } ↦ ( 𝑧 ∈ { 1 , 2 } ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) = ( 𝑝 ∈ { { 1 , 2 } } ↦ ( 𝑧 ∈ { 1 , 2 } ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) )
11 elsni ⊢ ( 𝑝 ∈ { { 1 , 2 } } → 𝑝 = { 1 , 2 } )
12 eleq2 ⊢ ( 𝑝 = { 1 , 2 } → ( 𝑧 ∈ 𝑝 ↔ 𝑧 ∈ { 1 , 2 } ) )
13 12 biimpar ⊢ ( ( 𝑝 = { 1 , 2 } ∧ 𝑧 ∈ { 1 , 2 } ) → 𝑧 ∈ 𝑝 )
14 13 iftrued ⊢ ( ( 𝑝 = { 1 , 2 } ∧ 𝑧 ∈ { 1 , 2 } ) → if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) = ∪ ( 𝑝 ∖ { 𝑧 } ) )
15 elpri ⊢ ( 𝑧 ∈ { 1 , 2 } → ( 𝑧 = 1 ∨ 𝑧 = 2 ) )
16 2ex ⊢ 2 ∈ V
17 16 unisn ⊢ ∪ { 2 } = 2
18 simpr ⊢ ( ( 𝑧 = 1 ∧ 𝑝 = { 1 , 2 } ) → 𝑝 = { 1 , 2 } )
19 sneq ⊢ ( 𝑧 = 1 → { 𝑧 } = { 1 } )
20 19 adantr ⊢ ( ( 𝑧 = 1 ∧ 𝑝 = { 1 , 2 } ) → { 𝑧 } = { 1 } )
21 18 20 difeq12d ⊢ ( ( 𝑧 = 1 ∧ 𝑝 = { 1 , 2 } ) → ( 𝑝 ∖ { 𝑧 } ) = ( { 1 , 2 } ∖ { 1 } ) )
22 difprsn1 ⊢ ( 1 ≠ 2 → ( { 1 , 2 } ∖ { 1 } ) = { 2 } )
23 7 22 ax-mp ⊢ ( { 1 , 2 } ∖ { 1 } ) = { 2 }
24 21 23 eqtrdi ⊢ ( ( 𝑧 = 1 ∧ 𝑝 = { 1 , 2 } ) → ( 𝑝 ∖ { 𝑧 } ) = { 2 } )
25 24 unieqd ⊢ ( ( 𝑧 = 1 ∧ 𝑝 = { 1 , 2 } ) → ∪ ( 𝑝 ∖ { 𝑧 } ) = ∪ { 2 } )
26 iftrue ⊢ ( 𝑧 = 1 → if ( 𝑧 = 1 , 2 , 1 ) = 2 )
27 26 adantr ⊢ ( ( 𝑧 = 1 ∧ 𝑝 = { 1 , 2 } ) → if ( 𝑧 = 1 , 2 , 1 ) = 2 )
28 17 25 27 3eqtr4a ⊢ ( ( 𝑧 = 1 ∧ 𝑝 = { 1 , 2 } ) → ∪ ( 𝑝 ∖ { 𝑧 } ) = if ( 𝑧 = 1 , 2 , 1 ) )
29 28 ex ⊢ ( 𝑧 = 1 → ( 𝑝 = { 1 , 2 } → ∪ ( 𝑝 ∖ { 𝑧 } ) = if ( 𝑧 = 1 , 2 , 1 ) ) )
30 5 unisn ⊢ ∪ { 1 } = 1
31 simpr ⊢ ( ( 𝑧 = 2 ∧ 𝑝 = { 1 , 2 } ) → 𝑝 = { 1 , 2 } )
32 sneq ⊢ ( 𝑧 = 2 → { 𝑧 } = { 2 } )
33 32 adantr ⊢ ( ( 𝑧 = 2 ∧ 𝑝 = { 1 , 2 } ) → { 𝑧 } = { 2 } )
34 31 33 difeq12d ⊢ ( ( 𝑧 = 2 ∧ 𝑝 = { 1 , 2 } ) → ( 𝑝 ∖ { 𝑧 } ) = ( { 1 , 2 } ∖ { 2 } ) )
35 difprsn2 ⊢ ( 1 ≠ 2 → ( { 1 , 2 } ∖ { 2 } ) = { 1 } )
36 7 35 ax-mp ⊢ ( { 1 , 2 } ∖ { 2 } ) = { 1 }
37 34 36 eqtrdi ⊢ ( ( 𝑧 = 2 ∧ 𝑝 = { 1 , 2 } ) → ( 𝑝 ∖ { 𝑧 } ) = { 1 } )
38 37 unieqd ⊢ ( ( 𝑧 = 2 ∧ 𝑝 = { 1 , 2 } ) → ∪ ( 𝑝 ∖ { 𝑧 } ) = ∪ { 1 } )
39 7 nesymi ⊢ ¬ 2 = 1
40 eqeq1 ⊢ ( 𝑧 = 2 → ( 𝑧 = 1 ↔ 2 = 1 ) )
41 39 40 mtbiri ⊢ ( 𝑧 = 2 → ¬ 𝑧 = 1 )
42 41 iffalsed ⊢ ( 𝑧 = 2 → if ( 𝑧 = 1 , 2 , 1 ) = 1 )
43 42 adantr ⊢ ( ( 𝑧 = 2 ∧ 𝑝 = { 1 , 2 } ) → if ( 𝑧 = 1 , 2 , 1 ) = 1 )
44 30 38 43 3eqtr4a ⊢ ( ( 𝑧 = 2 ∧ 𝑝 = { 1 , 2 } ) → ∪ ( 𝑝 ∖ { 𝑧 } ) = if ( 𝑧 = 1 , 2 , 1 ) )
45 44 ex ⊢ ( 𝑧 = 2 → ( 𝑝 = { 1 , 2 } → ∪ ( 𝑝 ∖ { 𝑧 } ) = if ( 𝑧 = 1 , 2 , 1 ) ) )
46 29 45 jaoi ⊢ ( ( 𝑧 = 1 ∨ 𝑧 = 2 ) → ( 𝑝 = { 1 , 2 } → ∪ ( 𝑝 ∖ { 𝑧 } ) = if ( 𝑧 = 1 , 2 , 1 ) ) )
47 15 46 syl ⊢ ( 𝑧 ∈ { 1 , 2 } → ( 𝑝 = { 1 , 2 } → ∪ ( 𝑝 ∖ { 𝑧 } ) = if ( 𝑧 = 1 , 2 , 1 ) ) )
48 47 impcom ⊢ ( ( 𝑝 = { 1 , 2 } ∧ 𝑧 ∈ { 1 , 2 } ) → ∪ ( 𝑝 ∖ { 𝑧 } ) = if ( 𝑧 = 1 , 2 , 1 ) )
49 14 48 eqtrd ⊢ ( ( 𝑝 = { 1 , 2 } ∧ 𝑧 ∈ { 1 , 2 } ) → if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) = if ( 𝑧 = 1 , 2 , 1 ) )
50 11 49 sylan ⊢ ( ( 𝑝 ∈ { { 1 , 2 } } ∧ 𝑧 ∈ { 1 , 2 } ) → if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) = if ( 𝑧 = 1 , 2 , 1 ) )
51 50 mpteq2dva ⊢ ( 𝑝 ∈ { { 1 , 2 } } → ( 𝑧 ∈ { 1 , 2 } ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) = ( 𝑧 ∈ { 1 , 2 } ↦ if ( 𝑧 = 1 , 2 , 1 ) ) )
52 51 mpteq2ia ⊢ ( 𝑝 ∈ { { 1 , 2 } } ↦ ( 𝑧 ∈ { 1 , 2 } ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) = ( 𝑝 ∈ { { 1 , 2 } } ↦ ( 𝑧 ∈ { 1 , 2 } ↦ if ( 𝑧 = 1 , 2 , 1 ) ) )
53 10 52 eqtri ⊢ ( 𝑝 ∈ { 𝑡 ∈ 𝒫 { 1 , 2 } ∣ 𝑡 ≈ 2o } ↦ ( 𝑧 ∈ { 1 , 2 } ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) = ( 𝑝 ∈ { { 1 , 2 } } ↦ ( 𝑧 ∈ { 1 , 2 } ↦ if ( 𝑧 = 1 , 2 , 1 ) ) )
54 4 53 eqtri ⊢ ( pmTrsp ‘ { 1 , 2 } ) = ( 𝑝 ∈ { { 1 , 2 } } ↦ ( 𝑧 ∈ { 1 , 2 } ↦ if ( 𝑧 = 1 , 2 , 1 ) ) )