This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pmtrprfvalrn

Description: The range of the transpositions on a pair is actually a singleton: the transposition of the two elements of the pair. (Contributed by AV, 9-Dec-2018)

Ref Expression
Assertion pmtrprfvalrn ran ( pmTrsp ‘ { 1 , 2 } ) = { { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } }

Proof

Step Hyp Ref Expression
1 pmtrprfval ⊢ ( pmTrsp ‘ { 1 , 2 } ) = ( 𝑝 ∈ { { 1 , 2 } } ↦ ( 𝑧 ∈ { 1 , 2 } ↦ if ( 𝑧 = 1 , 2 , 1 ) ) )
2 1 rneqi ⊢ ran ( pmTrsp ‘ { 1 , 2 } ) = ran ( 𝑝 ∈ { { 1 , 2 } } ↦ ( 𝑧 ∈ { 1 , 2 } ↦ if ( 𝑧 = 1 , 2 , 1 ) ) )
3 eqid ⊢ ( 𝑝 ∈ { { 1 , 2 } } ↦ ( 𝑧 ∈ { 1 , 2 } ↦ if ( 𝑧 = 1 , 2 , 1 ) ) ) = ( 𝑝 ∈ { { 1 , 2 } } ↦ ( 𝑧 ∈ { 1 , 2 } ↦ if ( 𝑧 = 1 , 2 , 1 ) ) )
4 3 rnmpt ⊢ ran ( 𝑝 ∈ { { 1 , 2 } } ↦ ( 𝑧 ∈ { 1 , 2 } ↦ if ( 𝑧 = 1 , 2 , 1 ) ) ) = { 𝑡 ∣ ∃ 𝑝 ∈ { { 1 , 2 } } 𝑡 = ( 𝑧 ∈ { 1 , 2 } ↦ if ( 𝑧 = 1 , 2 , 1 ) ) }
5 1ex ⊢ 1 ∈ V
6 id ⊢ ( 1 ∈ V → 1 ∈ V )
7 2nn ⊢ 2 ∈ ℕ
8 7 a1i ⊢ ( 1 ∈ V → 2 ∈ ℕ )
9 iftrue ⊢ ( 𝑧 = 1 → if ( 𝑧 = 1 , 2 , 1 ) = 2 )
10 9 adantl ⊢ ( ( 1 ∈ V ∧ 𝑧 = 1 ) → if ( 𝑧 = 1 , 2 , 1 ) = 2 )
11 1ne2 ⊢ 1 ≠ 2
12 11 nesymi ⊢ ¬ 2 = 1
13 eqeq1 ⊢ ( 𝑧 = 2 → ( 𝑧 = 1 ↔ 2 = 1 ) )
14 12 13 mtbiri ⊢ ( 𝑧 = 2 → ¬ 𝑧 = 1 )
15 14 iffalsed ⊢ ( 𝑧 = 2 → if ( 𝑧 = 1 , 2 , 1 ) = 1 )
16 15 adantl ⊢ ( ( 1 ∈ V ∧ 𝑧 = 2 ) → if ( 𝑧 = 1 , 2 , 1 ) = 1 )
17 6 8 8 6 10 16 fmptpr ⊢ ( 1 ∈ V → { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } = ( 𝑧 ∈ { 1 , 2 } ↦ if ( 𝑧 = 1 , 2 , 1 ) ) )
18 17 eqeq2d ⊢ ( 1 ∈ V → ( 𝑡 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ↔ 𝑡 = ( 𝑧 ∈ { 1 , 2 } ↦ if ( 𝑧 = 1 , 2 , 1 ) ) ) )
19 5 18 ax-mp ⊢ ( 𝑡 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ↔ 𝑡 = ( 𝑧 ∈ { 1 , 2 } ↦ if ( 𝑧 = 1 , 2 , 1 ) ) )
20 19 bicomi ⊢ ( 𝑡 = ( 𝑧 ∈ { 1 , 2 } ↦ if ( 𝑧 = 1 , 2 , 1 ) ) ↔ 𝑡 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } )
21 20 rexbii ⊢ ( ∃ 𝑝 ∈ { { 1 , 2 } } 𝑡 = ( 𝑧 ∈ { 1 , 2 } ↦ if ( 𝑧 = 1 , 2 , 1 ) ) ↔ ∃ 𝑝 ∈ { { 1 , 2 } } 𝑡 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } )
22 21 abbii ⊢ { 𝑡 ∣ ∃ 𝑝 ∈ { { 1 , 2 } } 𝑡 = ( 𝑧 ∈ { 1 , 2 } ↦ if ( 𝑧 = 1 , 2 , 1 ) ) } = { 𝑡 ∣ ∃ 𝑝 ∈ { { 1 , 2 } } 𝑡 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } }
23 prex ⊢ { 1 , 2 } ∈ V
24 23 snnz ⊢ { { 1 , 2 } } ≠ ∅
25 r19.9rzv ⊢ ( { { 1 , 2 } } ≠ ∅ → ( 𝑠 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ↔ ∃ 𝑝 ∈ { { 1 , 2 } } 𝑠 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) )
26 25 bicomd ⊢ ( { { 1 , 2 } } ≠ ∅ → ( ∃ 𝑝 ∈ { { 1 , 2 } } 𝑠 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ↔ 𝑠 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) )
27 24 26 ax-mp ⊢ ( ∃ 𝑝 ∈ { { 1 , 2 } } 𝑠 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ↔ 𝑠 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } )
28 vex ⊢ 𝑠 ∈ V
29 eqeq1 ⊢ ( 𝑡 = 𝑠 → ( 𝑡 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ↔ 𝑠 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) )
30 29 rexbidv ⊢ ( 𝑡 = 𝑠 → ( ∃ 𝑝 ∈ { { 1 , 2 } } 𝑡 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ↔ ∃ 𝑝 ∈ { { 1 , 2 } } 𝑠 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) )
31 28 30 elab ⊢ ( 𝑠 ∈ { 𝑡 ∣ ∃ 𝑝 ∈ { { 1 , 2 } } 𝑡 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } } ↔ ∃ 𝑝 ∈ { { 1 , 2 } } 𝑠 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } )
32 velsn ⊢ ( 𝑠 ∈ { { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } } ↔ 𝑠 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } )
33 27 31 32 3bitr4i ⊢ ( 𝑠 ∈ { 𝑡 ∣ ∃ 𝑝 ∈ { { 1 , 2 } } 𝑡 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } } ↔ 𝑠 ∈ { { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } } )
34 33 eqriv ⊢ { 𝑡 ∣ ∃ 𝑝 ∈ { { 1 , 2 } } 𝑡 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } } = { { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } }
35 22 34 eqtri ⊢ { 𝑡 ∣ ∃ 𝑝 ∈ { { 1 , 2 } } 𝑡 = ( 𝑧 ∈ { 1 , 2 } ↦ if ( 𝑧 = 1 , 2 , 1 ) ) } = { { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } }
36 4 35 eqtri ⊢ ran ( 𝑝 ∈ { { 1 , 2 } } ↦ ( 𝑧 ∈ { 1 , 2 } ↦ if ( 𝑧 = 1 , 2 , 1 ) ) ) = { { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } }
37 2 36 eqtri ⊢ ran ( pmTrsp ‘ { 1 , 2 } ) = { { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } }