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 ↔ ( 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥𝑋𝑦𝑋𝑧𝑋 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ ∃ 𝑢𝑋𝑥𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ) ) )