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

Metamath Proof Explorer

Theorem symg2hash

Description: The symmetric group on a (proper) pair has cardinality 2 . (Contributed by AV, 9-Dec-2018)

Ref Expression
Hypotheses symg1bas.1 ⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
symg1bas.2 ⊢ 𝐵 = ( Base ‘ 𝐺 )
symg2bas.0 ⊢ 𝐴 = { 𝐼 , 𝐽 }
Assertion symg2hash ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ∧ 𝐼 ≠ 𝐽 ) → ( ♯ ‘ 𝐵 ) = 2 )

Proof

Step Hyp Ref Expression
1 symg1bas.1 ⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
2 symg1bas.2 ⊢ 𝐵 = ( Base ‘ 𝐺 )
3 symg2bas.0 ⊢ 𝐴 = { 𝐼 , 𝐽 }
4 prfi ⊢ { 𝐼 , 𝐽 } ∈ Fin
5 3 4 eqeltri ⊢ 𝐴 ∈ Fin
6 1 2 symghash ⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐵 ) = ( ! ‘ ( ♯ ‘ 𝐴 ) ) )
7 5 6 ax-mp ⊢ ( ♯ ‘ 𝐵 ) = ( ! ‘ ( ♯ ‘ 𝐴 ) )
8 3 fveq2i ⊢ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ { 𝐼 , 𝐽 } )
9 elex ⊢ ( 𝐼 ∈ 𝑉 → 𝐼 ∈ V )
10 elex ⊢ ( 𝐽 ∈ 𝑊 → 𝐽 ∈ V )
11 id ⊢ ( 𝐼 ≠ 𝐽 → 𝐼 ≠ 𝐽 )
12 9 10 11 3anim123i ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ∧ 𝐼 ≠ 𝐽 ) → ( 𝐼 ∈ V ∧ 𝐽 ∈ V ∧ 𝐼 ≠ 𝐽 ) )
13 hashprb ⊢ ( ( 𝐼 ∈ V ∧ 𝐽 ∈ V ∧ 𝐼 ≠ 𝐽 ) ↔ ( ♯ ‘ { 𝐼 , 𝐽 } ) = 2 )
14 12 13 sylib ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ∧ 𝐼 ≠ 𝐽 ) → ( ♯ ‘ { 𝐼 , 𝐽 } ) = 2 )
15 8 14 eqtrid ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ∧ 𝐼 ≠ 𝐽 ) → ( ♯ ‘ 𝐴 ) = 2 )
16 15 fveq2d ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ∧ 𝐼 ≠ 𝐽 ) → ( ! ‘ ( ♯ ‘ 𝐴 ) ) = ( ! ‘ 2 ) )
17 fac2 ⊢ ( ! ‘ 2 ) = 2
18 16 17 eqtrdi ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ∧ 𝐼 ≠ 𝐽 ) → ( ! ‘ ( ♯ ‘ 𝐴 ) ) = 2 )
19 7 18 eqtrid ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ∧ 𝐼 ≠ 𝐽 ) → ( ♯ ‘ 𝐵 ) = 2 )