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 ⊢ G = SymGrp ⁡ A
symg1bas.2 ⊢ B = Base G
symg2bas.0 ⊢ A = I J
Assertion symg2hash ⊢ I ∈ V ∧ J ∈ W ∧ I ≠ J → B = 2

Proof

Step Hyp Ref Expression
1 symg1bas.1 ⊢ G = SymGrp ⁡ A
2 symg1bas.2 ⊢ B = Base G
3 symg2bas.0 ⊢ A = I J
4 prfi ⊢ I J ∈ Fin
5 3 4 eqeltri ⊢ A ∈ Fin
6 1 2 symghash ⊢ A ∈ Fin → B = A !
7 5 6 ax-mp ⊢ B = A !
8 3 fveq2i ⊢ A = I J
9 elex ⊢ I ∈ V → I ∈ V
10 elex ⊢ J ∈ W → J ∈ V
11 id ⊢ I ≠ J → I ≠ J
12 9 10 11 3anim123i ⊢ I ∈ V ∧ J ∈ W ∧ I ≠ J → I ∈ V ∧ J ∈ V ∧ I ≠ J
13 hashprb ⊢ I ∈ V ∧ J ∈ V ∧ I ≠ J ↔ I J = 2
14 12 13 sylib ⊢ I ∈ V ∧ J ∈ W ∧ I ≠ J → I J = 2
15 8 14 eqtrid ⊢ I ∈ V ∧ J ∈ W ∧ I ≠ J → A = 2
16 15 fveq2d ⊢ I ∈ V ∧ J ∈ W ∧ I ≠ J → A ! = 2 !
17 fac2 ⊢ 2 ! = 2
18 16 17 eqtrdi ⊢ I ∈ V ∧ J ∈ W ∧ I ≠ J → A ! = 2
19 7 18 eqtrid ⊢ I ∈ V ∧ J ∈ W ∧ I ≠ J → B = 2