Metamath Proof Explorer

Theorem isgrpo

Description: The predicate "is a group operation." Note that X is the base set of the group. (Contributed by NM, 10-Oct-2006) (New usage is discouraged.)

Ref Expression
Hypothesis isgrp.1 ⊢ 𝑋 = ran 𝐺
Assertion isgrpo ( 𝐺 ∈ 𝐴 → ( 𝐺 ∈ GrpOp ↔ ( 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ) ) )

Proof

Step Hyp Ref Expression
1 isgrp.1 ⊢ 𝑋 = ran 𝐺
2 feq1 ⊢ ( 𝑔 = 𝐺 → ( 𝑔 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 ↔ 𝐺 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 ) )
3 oveq ⊢ ( 𝑔 = 𝐺 → ( ( 𝑥 𝑔 𝑦 ) 𝑔 𝑧 ) = ( ( 𝑥 𝑔 𝑦 ) 𝐺 𝑧 ) )
4 oveq ⊢ ( 𝑔 = 𝐺 → ( 𝑥 𝑔 𝑦 ) = ( 𝑥 𝐺 𝑦 ) )
5 4 oveq1d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑥 𝑔 𝑦 ) 𝐺 𝑧 ) = ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) )
6 3 5 eqtrd ⊢ ( 𝑔 = 𝐺 → ( ( 𝑥 𝑔 𝑦 ) 𝑔 𝑧 ) = ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) )
7 oveq ⊢ ( 𝑔 = 𝐺 → ( 𝑥 𝑔 ( 𝑦 𝑔 𝑧 ) ) = ( 𝑥 𝐺 ( 𝑦 𝑔 𝑧 ) ) )
8 oveq ⊢ ( 𝑔 = 𝐺 → ( 𝑦 𝑔 𝑧 ) = ( 𝑦 𝐺 𝑧 ) )
9 8 oveq2d ⊢ ( 𝑔 = 𝐺 → ( 𝑥 𝐺 ( 𝑦 𝑔 𝑧 ) ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) )
10 7 9 eqtrd ⊢ ( 𝑔 = 𝐺 → ( 𝑥 𝑔 ( 𝑦 𝑔 𝑧 ) ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) )
11 6 10 eqeq12d ⊢ ( 𝑔 = 𝐺 → ( ( ( 𝑥 𝑔 𝑦 ) 𝑔 𝑧 ) = ( 𝑥 𝑔 ( 𝑦 𝑔 𝑧 ) ) ↔ ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ) )
12 11 ralbidv ⊢ ( 𝑔 = 𝐺 → ( ∀ 𝑧 ∈ 𝑡 ( ( 𝑥 𝑔 𝑦 ) 𝑔 𝑧 ) = ( 𝑥 𝑔 ( 𝑦 𝑔 𝑧 ) ) ↔ ∀ 𝑧 ∈ 𝑡 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ) )
13 12 2ralbidv ⊢ ( 𝑔 = 𝐺 → ( ∀ 𝑥 ∈ 𝑡 ∀ 𝑦 ∈ 𝑡 ∀ 𝑧 ∈ 𝑡 ( ( 𝑥 𝑔 𝑦 ) 𝑔 𝑧 ) = ( 𝑥 𝑔 ( 𝑦 𝑔 𝑧 ) ) ↔ ∀ 𝑥 ∈ 𝑡 ∀ 𝑦 ∈ 𝑡 ∀ 𝑧 ∈ 𝑡 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ) )
14 oveq ⊢ ( 𝑔 = 𝐺 → ( 𝑢 𝑔 𝑥 ) = ( 𝑢 𝐺 𝑥 ) )
15 14 eqeq1d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑢 𝑔 𝑥 ) = 𝑥 ↔ ( 𝑢 𝐺 𝑥 ) = 𝑥 ) )
16 oveq ⊢ ( 𝑔 = 𝐺 → ( 𝑦 𝑔 𝑥 ) = ( 𝑦 𝐺 𝑥 ) )
17 16 eqeq1d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑦 𝑔 𝑥 ) = 𝑢 ↔ ( 𝑦 𝐺 𝑥 ) = 𝑢 ) )
18 17 rexbidv ⊢ ( 𝑔 = 𝐺 → ( ∃ 𝑦 ∈ 𝑡 ( 𝑦 𝑔 𝑥 ) = 𝑢 ↔ ∃ 𝑦 ∈ 𝑡 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) )
19 15 18 anbi12d ⊢ ( 𝑔 = 𝐺 → ( ( ( 𝑢 𝑔 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑡 ( 𝑦 𝑔 𝑥 ) = 𝑢 ) ↔ ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑡 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ) )
20 19 rexralbidv ⊢ ( 𝑔 = 𝐺 → ( ∃ 𝑢 ∈ 𝑡 ∀ 𝑥 ∈ 𝑡 ( ( 𝑢 𝑔 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑡 ( 𝑦 𝑔 𝑥 ) = 𝑢 ) ↔ ∃ 𝑢 ∈ 𝑡 ∀ 𝑥 ∈ 𝑡 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑡 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ) )
21 2 13 20 3anbi123d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑔 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ∀ 𝑦 ∈ 𝑡 ∀ 𝑧 ∈ 𝑡 ( ( 𝑥 𝑔 𝑦 ) 𝑔 𝑧 ) = ( 𝑥 𝑔 ( 𝑦 𝑔 𝑧 ) ) ∧ ∃ 𝑢 ∈ 𝑡 ∀ 𝑥 ∈ 𝑡 ( ( 𝑢 𝑔 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑡 ( 𝑦 𝑔 𝑥 ) = 𝑢 ) ) ↔ ( 𝐺 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ∀ 𝑦 ∈ 𝑡 ∀ 𝑧 ∈ 𝑡 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ ∃ 𝑢 ∈ 𝑡 ∀ 𝑥 ∈ 𝑡 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑡 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ) ) )
22 21 exbidv ⊢ ( 𝑔 = 𝐺 → ( ∃ 𝑡 ( 𝑔 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ∀ 𝑦 ∈ 𝑡 ∀ 𝑧 ∈ 𝑡 ( ( 𝑥 𝑔 𝑦 ) 𝑔 𝑧 ) = ( 𝑥 𝑔 ( 𝑦 𝑔 𝑧 ) ) ∧ ∃ 𝑢 ∈ 𝑡 ∀ 𝑥 ∈ 𝑡 ( ( 𝑢 𝑔 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑡 ( 𝑦 𝑔 𝑥 ) = 𝑢 ) ) ↔ ∃ 𝑡 ( 𝐺 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ∀ 𝑦 ∈ 𝑡 ∀ 𝑧 ∈ 𝑡 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ ∃ 𝑢 ∈ 𝑡 ∀ 𝑥 ∈ 𝑡 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑡 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ) ) )
23 df-grpo ⊢ GrpOp = { 𝑔 ∣ ∃ 𝑡 ( 𝑔 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ∀ 𝑦 ∈ 𝑡 ∀ 𝑧 ∈ 𝑡 ( ( 𝑥 𝑔 𝑦 ) 𝑔 𝑧 ) = ( 𝑥 𝑔 ( 𝑦 𝑔 𝑧 ) ) ∧ ∃ 𝑢 ∈ 𝑡 ∀ 𝑥 ∈ 𝑡 ( ( 𝑢 𝑔 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑡 ( 𝑦 𝑔 𝑥 ) = 𝑢 ) ) }
24 22 23 elab2g ⊢ ( 𝐺 ∈ 𝐴 → ( 𝐺 ∈ GrpOp ↔ ∃ 𝑡 ( 𝐺 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ∀ 𝑦 ∈ 𝑡 ∀ 𝑧 ∈ 𝑡 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ ∃ 𝑢 ∈ 𝑡 ∀ 𝑥 ∈ 𝑡 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑡 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ) ) )
25 simpl ⊢ ( ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑡 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) → ( 𝑢 𝐺 𝑥 ) = 𝑥 )
26 25 ralimi ⊢ ( ∀ 𝑥 ∈ 𝑡 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑡 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) → ∀ 𝑥 ∈ 𝑡 ( 𝑢 𝐺 𝑥 ) = 𝑥 )
27 oveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝑢 𝐺 𝑥 ) = ( 𝑢 𝐺 𝑧 ) )
28 id ⊢ ( 𝑥 = 𝑧 → 𝑥 = 𝑧 )
29 27 28 eqeq12d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ↔ ( 𝑢 𝐺 𝑧 ) = 𝑧 ) )
30 eqcom ⊢ ( ( 𝑢 𝐺 𝑧 ) = 𝑧 ↔ 𝑧 = ( 𝑢 𝐺 𝑧 ) )
31 29 30 bitrdi ⊢ ( 𝑥 = 𝑧 → ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ↔ 𝑧 = ( 𝑢 𝐺 𝑧 ) ) )
32 31 rspcv ⊢ ( 𝑧 ∈ 𝑡 → ( ∀ 𝑥 ∈ 𝑡 ( 𝑢 𝐺 𝑥 ) = 𝑥 → 𝑧 = ( 𝑢 𝐺 𝑧 ) ) )
33 oveq2 ⊢ ( 𝑦 = 𝑧 → ( 𝑢 𝐺 𝑦 ) = ( 𝑢 𝐺 𝑧 ) )
34 33 rspceeqv ⊢ ( ( 𝑧 ∈ 𝑡 ∧ 𝑧 = ( 𝑢 𝐺 𝑧 ) ) → ∃ 𝑦 ∈ 𝑡 𝑧 = ( 𝑢 𝐺 𝑦 ) )
35 34 ex ⊢ ( 𝑧 ∈ 𝑡 → ( 𝑧 = ( 𝑢 𝐺 𝑧 ) → ∃ 𝑦 ∈ 𝑡 𝑧 = ( 𝑢 𝐺 𝑦 ) ) )
36 32 35 syld ⊢ ( 𝑧 ∈ 𝑡 → ( ∀ 𝑥 ∈ 𝑡 ( 𝑢 𝐺 𝑥 ) = 𝑥 → ∃ 𝑦 ∈ 𝑡 𝑧 = ( 𝑢 𝐺 𝑦 ) ) )
37 26 36 syl5 ⊢ ( 𝑧 ∈ 𝑡 → ( ∀ 𝑥 ∈ 𝑡 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑡 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) → ∃ 𝑦 ∈ 𝑡 𝑧 = ( 𝑢 𝐺 𝑦 ) ) )
38 37 reximdv ⊢ ( 𝑧 ∈ 𝑡 → ( ∃ 𝑢 ∈ 𝑡 ∀ 𝑥 ∈ 𝑡 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑡 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) → ∃ 𝑢 ∈ 𝑡 ∃ 𝑦 ∈ 𝑡 𝑧 = ( 𝑢 𝐺 𝑦 ) ) )
39 38 impcom ⊢ ( ( ∃ 𝑢 ∈ 𝑡 ∀ 𝑥 ∈ 𝑡 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑡 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ∧ 𝑧 ∈ 𝑡 ) → ∃ 𝑢 ∈ 𝑡 ∃ 𝑦 ∈ 𝑡 𝑧 = ( 𝑢 𝐺 𝑦 ) )
40 39 ralrimiva ⊢ ( ∃ 𝑢 ∈ 𝑡 ∀ 𝑥 ∈ 𝑡 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑡 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) → ∀ 𝑧 ∈ 𝑡 ∃ 𝑢 ∈ 𝑡 ∃ 𝑦 ∈ 𝑡 𝑧 = ( 𝑢 𝐺 𝑦 ) )
41 40 anim2i ⊢ ( ( 𝐺 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 ∧ ∃ 𝑢 ∈ 𝑡 ∀ 𝑥 ∈ 𝑡 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑡 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ) → ( 𝐺 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 ∧ ∀ 𝑧 ∈ 𝑡 ∃ 𝑢 ∈ 𝑡 ∃ 𝑦 ∈ 𝑡 𝑧 = ( 𝑢 𝐺 𝑦 ) ) )
42 foov ⊢ ( 𝐺 : ( 𝑡 × 𝑡 ) –onto→ 𝑡 ↔ ( 𝐺 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 ∧ ∀ 𝑧 ∈ 𝑡 ∃ 𝑢 ∈ 𝑡 ∃ 𝑦 ∈ 𝑡 𝑧 = ( 𝑢 𝐺 𝑦 ) ) )
43 41 42 sylibr ⊢ ( ( 𝐺 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 ∧ ∃ 𝑢 ∈ 𝑡 ∀ 𝑥 ∈ 𝑡 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑡 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ) → 𝐺 : ( 𝑡 × 𝑡 ) –onto→ 𝑡 )
44 forn ⊢ ( 𝐺 : ( 𝑡 × 𝑡 ) –onto→ 𝑡 → ran 𝐺 = 𝑡 )
45 44 eqcomd ⊢ ( 𝐺 : ( 𝑡 × 𝑡 ) –onto→ 𝑡 → 𝑡 = ran 𝐺 )
46 43 45 syl ⊢ ( ( 𝐺 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 ∧ ∃ 𝑢 ∈ 𝑡 ∀ 𝑥 ∈ 𝑡 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑡 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ) → 𝑡 = ran 𝐺 )
47 46 3adant2 ⊢ ( ( 𝐺 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ∀ 𝑦 ∈ 𝑡 ∀ 𝑧 ∈ 𝑡 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ ∃ 𝑢 ∈ 𝑡 ∀ 𝑥 ∈ 𝑡 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑡 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ) → 𝑡 = ran 𝐺 )
48 47 pm4.71ri ⊢ ( ( 𝐺 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ∀ 𝑦 ∈ 𝑡 ∀ 𝑧 ∈ 𝑡 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ ∃ 𝑢 ∈ 𝑡 ∀ 𝑥 ∈ 𝑡 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑡 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ) ↔ ( 𝑡 = ran 𝐺 ∧ ( 𝐺 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ∀ 𝑦 ∈ 𝑡 ∀ 𝑧 ∈ 𝑡 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ ∃ 𝑢 ∈ 𝑡 ∀ 𝑥 ∈ 𝑡 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑡 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ) ) )
49 48 exbii ⊢ ( ∃ 𝑡 ( 𝐺 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ∀ 𝑦 ∈ 𝑡 ∀ 𝑧 ∈ 𝑡 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ ∃ 𝑢 ∈ 𝑡 ∀ 𝑥 ∈ 𝑡 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑡 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ) ↔ ∃ 𝑡 ( 𝑡 = ran 𝐺 ∧ ( 𝐺 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ∀ 𝑦 ∈ 𝑡 ∀ 𝑧 ∈ 𝑡 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ ∃ 𝑢 ∈ 𝑡 ∀ 𝑥 ∈ 𝑡 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑡 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ) ) )
50 24 49 bitrdi ⊢ ( 𝐺 ∈ 𝐴 → ( 𝐺 ∈ GrpOp ↔ ∃ 𝑡 ( 𝑡 = ran 𝐺 ∧ ( 𝐺 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ∀ 𝑦 ∈ 𝑡 ∀ 𝑧 ∈ 𝑡 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ ∃ 𝑢 ∈ 𝑡 ∀ 𝑥 ∈ 𝑡 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑡 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ) ) ) )
51 rnexg ⊢ ( 𝐺 ∈ 𝐴 → ran 𝐺 ∈ V )
52 1 eqeq2i ⊢ ( 𝑡 = 𝑋 ↔ 𝑡 = ran 𝐺 )
53 xpeq1 ⊢ ( 𝑡 = 𝑋 → ( 𝑡 × 𝑡 ) = ( 𝑋 × 𝑡 ) )
54 xpeq2 ⊢ ( 𝑡 = 𝑋 → ( 𝑋 × 𝑡 ) = ( 𝑋 × 𝑋 ) )
55 53 54 eqtrd ⊢ ( 𝑡 = 𝑋 → ( 𝑡 × 𝑡 ) = ( 𝑋 × 𝑋 ) )
56 55 feq2d ⊢ ( 𝑡 = 𝑋 → ( 𝐺 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 ↔ 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑡 ) )
57 feq3 ⊢ ( 𝑡 = 𝑋 → ( 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑡 ↔ 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) )
58 56 57 bitrd ⊢ ( 𝑡 = 𝑋 → ( 𝐺 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 ↔ 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) )
59 raleq ⊢ ( 𝑡 = 𝑋 → ( ∀ 𝑧 ∈ 𝑡 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ↔ ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ) )
60 59 raleqbi1dv ⊢ ( 𝑡 = 𝑋 → ( ∀ 𝑦 ∈ 𝑡 ∀ 𝑧 ∈ 𝑡 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ↔ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ) )
61 60 raleqbi1dv ⊢ ( 𝑡 = 𝑋 → ( ∀ 𝑥 ∈ 𝑡 ∀ 𝑦 ∈ 𝑡 ∀ 𝑧 ∈ 𝑡 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ) )
62 rexeq ⊢ ( 𝑡 = 𝑋 → ( ∃ 𝑦 ∈ 𝑡 ( 𝑦 𝐺 𝑥 ) = 𝑢 ↔ ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) )
63 62 anbi2d ⊢ ( 𝑡 = 𝑋 → ( ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑡 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ↔ ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ) )
64 63 raleqbi1dv ⊢ ( 𝑡 = 𝑋 → ( ∀ 𝑥 ∈ 𝑡 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑡 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ↔ ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ) )
65 64 rexeqbi1dv ⊢ ( 𝑡 = 𝑋 → ( ∃ 𝑢 ∈ 𝑡 ∀ 𝑥 ∈ 𝑡 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑡 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ↔ ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ) )
66 58 61 65 3anbi123d ⊢ ( 𝑡 = 𝑋 → ( ( 𝐺 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ∀ 𝑦 ∈ 𝑡 ∀ 𝑧 ∈ 𝑡 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ ∃ 𝑢 ∈ 𝑡 ∀ 𝑥 ∈ 𝑡 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑡 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ) ↔ ( 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ) ) )
67 52 66 sylbir ⊢ ( 𝑡 = ran 𝐺 → ( ( 𝐺 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ∀ 𝑦 ∈ 𝑡 ∀ 𝑧 ∈ 𝑡 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ ∃ 𝑢 ∈ 𝑡 ∀ 𝑥 ∈ 𝑡 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑡 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ) ↔ ( 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ) ) )
68 67 ceqsexgv ⊢ ( ran 𝐺 ∈ V → ( ∃ 𝑡 ( 𝑡 = ran 𝐺 ∧ ( 𝐺 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ∀ 𝑦 ∈ 𝑡 ∀ 𝑧 ∈ 𝑡 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ ∃ 𝑢 ∈ 𝑡 ∀ 𝑥 ∈ 𝑡 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑡 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ) ) ↔ ( 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ) ) )
69 51 68 syl ⊢ ( 𝐺 ∈ 𝐴 → ( ∃ 𝑡 ( 𝑡 = ran 𝐺 ∧ ( 𝐺 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ∀ 𝑦 ∈ 𝑡 ∀ 𝑧 ∈ 𝑡 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ ∃ 𝑢 ∈ 𝑡 ∀ 𝑥 ∈ 𝑡 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑡 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ) ) ↔ ( 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ) ) )
70 50 69 bitrd ⊢ ( 𝐺 ∈ 𝐴 → ( 𝐺 ∈ GrpOp ↔ ( 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ) ) )