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 ⟩ } }