Metamath Proof Explorer

Theorem odcl2

Description: The order of an element of a finite group is finite. (Contributed by Mario Carneiro, 14-Jan-2015)

Ref Expression
Hypotheses odcl2.1 ⊢ X = Base G
odcl2.2 ⊢ O = od ⁡ G
Assertion odcl2 ⊢ G ∈ Grp ∧ X ∈ Fin ∧ A ∈ X → O ⁡ A ∈ ℕ

Proof

Step Hyp Ref Expression
1 odcl2.1 ⊢ X = Base G
2 odcl2.2 ⊢ O = od ⁡ G
3 1 2 odcl ⊢ A ∈ X → O ⁡ A ∈ ℕ 0
4 3 adantl ⊢ G ∈ Grp ∧ A ∈ X → O ⁡ A ∈ ℕ 0
5 elnn0 ⊢ O ⁡ A ∈ ℕ 0 ↔ O ⁡ A ∈ ℕ ∨ O ⁡ A = 0
6 4 5 sylib ⊢ G ∈ Grp ∧ A ∈ X → O ⁡ A ∈ ℕ ∨ O ⁡ A = 0
7 6 ord ⊢ G ∈ Grp ∧ A ∈ X → ¬ O ⁡ A ∈ ℕ → O ⁡ A = 0
8 eqid ⊢ ⋅ G = ⋅ G
9 eqid ⊢ x ∈ ℤ ⟼ x ⋅ G A = x ∈ ℤ ⟼ x ⋅ G A
10 1 2 8 9 odinf ⊢ G ∈ Grp ∧ A ∈ X ∧ O ⁡ A = 0 → ¬ ran ⁡ x ∈ ℤ ⟼ x ⋅ G A ∈ Fin
11 1 2 8 9 odf1 ⊢ G ∈ Grp ∧ A ∈ X → O ⁡ A = 0 ↔ x ∈ ℤ ⟼ x ⋅ G A : ℤ ⟶ 1-1 X
12 11 biimp3a ⊢ G ∈ Grp ∧ A ∈ X ∧ O ⁡ A = 0 → x ∈ ℤ ⟼ x ⋅ G A : ℤ ⟶ 1-1 X
13 f1f ⊢ x ∈ ℤ ⟼ x ⋅ G A : ℤ ⟶ 1-1 X → x ∈ ℤ ⟼ x ⋅ G A : ℤ ⟶ X
14 frn ⊢ x ∈ ℤ ⟼ x ⋅ G A : ℤ ⟶ X → ran ⁡ x ∈ ℤ ⟼ x ⋅ G A ⊆ X
15 ssfi ⊢ X ∈ Fin ∧ ran ⁡ x ∈ ℤ ⟼ x ⋅ G A ⊆ X → ran ⁡ x ∈ ℤ ⟼ x ⋅ G A ∈ Fin
16 15 expcom ⊢ ran ⁡ x ∈ ℤ ⟼ x ⋅ G A ⊆ X → X ∈ Fin → ran ⁡ x ∈ ℤ ⟼ x ⋅ G A ∈ Fin
17 12 13 14 16 4syl ⊢ G ∈ Grp ∧ A ∈ X ∧ O ⁡ A = 0 → X ∈ Fin → ran ⁡ x ∈ ℤ ⟼ x ⋅ G A ∈ Fin
18 10 17 mtod ⊢ G ∈ Grp ∧ A ∈ X ∧ O ⁡ A = 0 → ¬ X ∈ Fin
19 18 3expia ⊢ G ∈ Grp ∧ A ∈ X → O ⁡ A = 0 → ¬ X ∈ Fin
20 7 19 syld ⊢ G ∈ Grp ∧ A ∈ X → ¬ O ⁡ A ∈ ℕ → ¬ X ∈ Fin
21 20 con4d ⊢ G ∈ Grp ∧ A ∈ X → X ∈ Fin → O ⁡ A ∈ ℕ
22 21 3impia ⊢ G ∈ Grp ∧ A ∈ X ∧ X ∈ Fin → O ⁡ A ∈ ℕ
23 22 3com23 ⊢ G ∈ Grp ∧ X ∈ Fin ∧ A ∈ X → O ⁡ A ∈ ℕ