Theorem odval2

Description: A non-conditional definition of the group order. (Contributed by Stefan O'Rear, 6-Sep-2015)

	Ref	Expression
Hypotheses	odcl.1	⊢ 𝑋 = ( Base ‘ 𝐺 )
	odcl.2	⊢ 𝑂 = ( od ‘ 𝐺 )
	odid.3	⊢ · = ( .g ‘ 𝐺 )
	odid.4	⊢ 0 = ( 0g ‘ 𝐺 )
Assertion	odval2	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑂 ‘ 𝐴 ) = ( ℩ 𝑥 ∈ ℕ0 ∀ 𝑦 ∈ ℕ0 ( 𝑥 ∥ 𝑦 ↔ ( 𝑦 · 𝐴 ) = 0 ) ) )

Proof

Step	Hyp	Ref	Expression
1		odcl.1	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		odcl.2	⊢ 𝑂 = ( od ‘ 𝐺 )
3		odid.3	⊢ · = ( .g ‘ 𝐺 )
4		odid.4	⊢ 0 = ( 0g ‘ 𝐺 )
5	1 2	odcl	⊢ ( 𝐴 ∈ 𝑋 → ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 )
6	5	adantl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 )
7	1 2 3 4	odeq	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑥 ∈ ℕ0 ) → ( 𝑥 = ( 𝑂 ‘ 𝐴 ) ↔ ∀ 𝑦 ∈ ℕ0 ( 𝑥 ∥ 𝑦 ↔ ( 𝑦 · 𝐴 ) = 0 ) ) )
8	7	3expa	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑥 ∈ ℕ0 ) → ( 𝑥 = ( 𝑂 ‘ 𝐴 ) ↔ ∀ 𝑦 ∈ ℕ0 ( 𝑥 ∥ 𝑦 ↔ ( 𝑦 · 𝐴 ) = 0 ) ) )
9	8	bicomd	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑥 ∈ ℕ0 ) → ( ∀ 𝑦 ∈ ℕ0 ( 𝑥 ∥ 𝑦 ↔ ( 𝑦 · 𝐴 ) = 0 ) ↔ 𝑥 = ( 𝑂 ‘ 𝐴 ) ) )
10	6 9	riota5	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ℩ 𝑥 ∈ ℕ0 ∀ 𝑦 ∈ ℕ0 ( 𝑥 ∥ 𝑦 ↔ ( 𝑦 · 𝐴 ) = 0 ) ) = ( 𝑂 ‘ 𝐴 ) )
11	10	eqcomd	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑂 ‘ 𝐴 ) = ( ℩ 𝑥 ∈ ℕ0 ∀ 𝑦 ∈ ℕ0 ( 𝑥 ∥ 𝑦 ↔ ( 𝑦 · 𝐴 ) = 0 ) ) )