This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem gaorber

Description: The orbit equivalence relation is an equivalence relation on the target set of the group action. (Contributed by NM, 11-Aug-2009) (Revised by Mario Carneiro, 13-Jan-2015)

Ref Expression
Hypotheses gaorb.1 ⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑌 ∧ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ) }
gaorber.2 ⊢ 𝑋 = ( Base ‘ 𝐺 )
Assertion gaorber ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) → ∼ Er 𝑌 )

Proof

Step Hyp Ref Expression
1 gaorb.1 ⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑌 ∧ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ) }
2 gaorber.2 ⊢ 𝑋 = ( Base ‘ 𝐺 )
3 1 relopabiv ⊢ Rel ∼
4 3 a1i ⊢ ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) → Rel ∼ )
5 simpr ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑢 ∼ 𝑣 ) → 𝑢 ∼ 𝑣 )
6 1 gaorb ⊢ ( 𝑢 ∼ 𝑣 ↔ ( 𝑢 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌 ∧ ∃ ℎ ∈ 𝑋 ( ℎ ⊕ 𝑢 ) = 𝑣 ) )
7 5 6 sylib ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑢 ∼ 𝑣 ) → ( 𝑢 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌 ∧ ∃ ℎ ∈ 𝑋 ( ℎ ⊕ 𝑢 ) = 𝑣 ) )
8 7 simp2d ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑢 ∼ 𝑣 ) → 𝑣 ∈ 𝑌 )
9 7 simp1d ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑢 ∼ 𝑣 ) → 𝑢 ∈ 𝑌 )
10 7 simp3d ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑢 ∼ 𝑣 ) → ∃ ℎ ∈ 𝑋 ( ℎ ⊕ 𝑢 ) = 𝑣 )
11 simpll ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑢 ∼ 𝑣 ) ∧ ℎ ∈ 𝑋 ) → ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) )
12 simpr ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑢 ∼ 𝑣 ) ∧ ℎ ∈ 𝑋 ) → ℎ ∈ 𝑋 )
13 9 adantr ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑢 ∼ 𝑣 ) ∧ ℎ ∈ 𝑋 ) → 𝑢 ∈ 𝑌 )
14 8 adantr ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑢 ∼ 𝑣 ) ∧ ℎ ∈ 𝑋 ) → 𝑣 ∈ 𝑌 )
15 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
16 2 15 gacan ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( ℎ ∈ 𝑋 ∧ 𝑢 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌 ) ) → ( ( ℎ ⊕ 𝑢 ) = 𝑣 ↔ ( ( ( invg ‘ 𝐺 ) ‘ ℎ ) ⊕ 𝑣 ) = 𝑢 ) )
17 11 12 13 14 16 syl13anc ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑢 ∼ 𝑣 ) ∧ ℎ ∈ 𝑋 ) → ( ( ℎ ⊕ 𝑢 ) = 𝑣 ↔ ( ( ( invg ‘ 𝐺 ) ‘ ℎ ) ⊕ 𝑣 ) = 𝑢 ) )
18 gagrp ⊢ ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) → 𝐺 ∈ Grp )
19 18 adantr ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑢 ∼ 𝑣 ) → 𝐺 ∈ Grp )
20 2 15 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ ℎ ∈ 𝑋 ) → ( ( invg ‘ 𝐺 ) ‘ ℎ ) ∈ 𝑋 )
21 19 20 sylan ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑢 ∼ 𝑣 ) ∧ ℎ ∈ 𝑋 ) → ( ( invg ‘ 𝐺 ) ‘ ℎ ) ∈ 𝑋 )
22 oveq1 ⊢ ( 𝑘 = ( ( invg ‘ 𝐺 ) ‘ ℎ ) → ( 𝑘 ⊕ 𝑣 ) = ( ( ( invg ‘ 𝐺 ) ‘ ℎ ) ⊕ 𝑣 ) )
23 22 eqeq1d ⊢ ( 𝑘 = ( ( invg ‘ 𝐺 ) ‘ ℎ ) → ( ( 𝑘 ⊕ 𝑣 ) = 𝑢 ↔ ( ( ( invg ‘ 𝐺 ) ‘ ℎ ) ⊕ 𝑣 ) = 𝑢 ) )
24 23 rspcev ⊢ ( ( ( ( invg ‘ 𝐺 ) ‘ ℎ ) ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ ℎ ) ⊕ 𝑣 ) = 𝑢 ) → ∃ 𝑘 ∈ 𝑋 ( 𝑘 ⊕ 𝑣 ) = 𝑢 )
25 24 ex ⊢ ( ( ( invg ‘ 𝐺 ) ‘ ℎ ) ∈ 𝑋 → ( ( ( ( invg ‘ 𝐺 ) ‘ ℎ ) ⊕ 𝑣 ) = 𝑢 → ∃ 𝑘 ∈ 𝑋 ( 𝑘 ⊕ 𝑣 ) = 𝑢 ) )
26 21 25 syl ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑢 ∼ 𝑣 ) ∧ ℎ ∈ 𝑋 ) → ( ( ( ( invg ‘ 𝐺 ) ‘ ℎ ) ⊕ 𝑣 ) = 𝑢 → ∃ 𝑘 ∈ 𝑋 ( 𝑘 ⊕ 𝑣 ) = 𝑢 ) )
27 17 26 sylbid ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑢 ∼ 𝑣 ) ∧ ℎ ∈ 𝑋 ) → ( ( ℎ ⊕ 𝑢 ) = 𝑣 → ∃ 𝑘 ∈ 𝑋 ( 𝑘 ⊕ 𝑣 ) = 𝑢 ) )
28 27 rexlimdva ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑢 ∼ 𝑣 ) → ( ∃ ℎ ∈ 𝑋 ( ℎ ⊕ 𝑢 ) = 𝑣 → ∃ 𝑘 ∈ 𝑋 ( 𝑘 ⊕ 𝑣 ) = 𝑢 ) )
29 10 28 mpd ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑢 ∼ 𝑣 ) → ∃ 𝑘 ∈ 𝑋 ( 𝑘 ⊕ 𝑣 ) = 𝑢 )
30 1 gaorb ⊢ ( 𝑣 ∼ 𝑢 ↔ ( 𝑣 ∈ 𝑌 ∧ 𝑢 ∈ 𝑌 ∧ ∃ 𝑘 ∈ 𝑋 ( 𝑘 ⊕ 𝑣 ) = 𝑢 ) )
31 8 9 29 30 syl3anbrc ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑢 ∼ 𝑣 ) → 𝑣 ∼ 𝑢 )
32 9 adantrr ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) ) → 𝑢 ∈ 𝑌 )
33 simprr ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) ) → 𝑣 ∼ 𝑤 )
34 1 gaorb ⊢ ( 𝑣 ∼ 𝑤 ↔ ( 𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ∧ ∃ 𝑘 ∈ 𝑋 ( 𝑘 ⊕ 𝑣 ) = 𝑤 ) )
35 33 34 sylib ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) ) → ( 𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ∧ ∃ 𝑘 ∈ 𝑋 ( 𝑘 ⊕ 𝑣 ) = 𝑤 ) )
36 35 simp2d ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) ) → 𝑤 ∈ 𝑌 )
37 10 adantrr ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) ) → ∃ ℎ ∈ 𝑋 ( ℎ ⊕ 𝑢 ) = 𝑣 )
38 35 simp3d ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) ) → ∃ 𝑘 ∈ 𝑋 ( 𝑘 ⊕ 𝑣 ) = 𝑤 )
39 reeanv ⊢ ( ∃ ℎ ∈ 𝑋 ∃ 𝑘 ∈ 𝑋 ( ( ℎ ⊕ 𝑢 ) = 𝑣 ∧ ( 𝑘 ⊕ 𝑣 ) = 𝑤 ) ↔ ( ∃ ℎ ∈ 𝑋 ( ℎ ⊕ 𝑢 ) = 𝑣 ∧ ∃ 𝑘 ∈ 𝑋 ( 𝑘 ⊕ 𝑣 ) = 𝑤 ) )
40 18 ad2antrr ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) ) ∧ ( ( ℎ ∈ 𝑋 ∧ 𝑘 ∈ 𝑋 ) ∧ ( ( ℎ ⊕ 𝑢 ) = 𝑣 ∧ ( 𝑘 ⊕ 𝑣 ) = 𝑤 ) ) ) → 𝐺 ∈ Grp )
41 simprlr ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) ) ∧ ( ( ℎ ∈ 𝑋 ∧ 𝑘 ∈ 𝑋 ) ∧ ( ( ℎ ⊕ 𝑢 ) = 𝑣 ∧ ( 𝑘 ⊕ 𝑣 ) = 𝑤 ) ) ) → 𝑘 ∈ 𝑋 )
42 simprll ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) ) ∧ ( ( ℎ ∈ 𝑋 ∧ 𝑘 ∈ 𝑋 ) ∧ ( ( ℎ ⊕ 𝑢 ) = 𝑣 ∧ ( 𝑘 ⊕ 𝑣 ) = 𝑤 ) ) ) → ℎ ∈ 𝑋 )
43 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
44 2 43 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑘 ∈ 𝑋 ∧ ℎ ∈ 𝑋 ) → ( 𝑘 ( +g ‘ 𝐺 ) ℎ ) ∈ 𝑋 )
45 40 41 42 44 syl3anc ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) ) ∧ ( ( ℎ ∈ 𝑋 ∧ 𝑘 ∈ 𝑋 ) ∧ ( ( ℎ ⊕ 𝑢 ) = 𝑣 ∧ ( 𝑘 ⊕ 𝑣 ) = 𝑤 ) ) ) → ( 𝑘 ( +g ‘ 𝐺 ) ℎ ) ∈ 𝑋 )
46 simpll ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) ) ∧ ( ( ℎ ∈ 𝑋 ∧ 𝑘 ∈ 𝑋 ) ∧ ( ( ℎ ⊕ 𝑢 ) = 𝑣 ∧ ( 𝑘 ⊕ 𝑣 ) = 𝑤 ) ) ) → ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) )
47 32 adantr ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) ) ∧ ( ( ℎ ∈ 𝑋 ∧ 𝑘 ∈ 𝑋 ) ∧ ( ( ℎ ⊕ 𝑢 ) = 𝑣 ∧ ( 𝑘 ⊕ 𝑣 ) = 𝑤 ) ) ) → 𝑢 ∈ 𝑌 )
48 2 43 gaass ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑘 ∈ 𝑋 ∧ ℎ ∈ 𝑋 ∧ 𝑢 ∈ 𝑌 ) ) → ( ( 𝑘 ( +g ‘ 𝐺 ) ℎ ) ⊕ 𝑢 ) = ( 𝑘 ⊕ ( ℎ ⊕ 𝑢 ) ) )
49 46 41 42 47 48 syl13anc ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) ) ∧ ( ( ℎ ∈ 𝑋 ∧ 𝑘 ∈ 𝑋 ) ∧ ( ( ℎ ⊕ 𝑢 ) = 𝑣 ∧ ( 𝑘 ⊕ 𝑣 ) = 𝑤 ) ) ) → ( ( 𝑘 ( +g ‘ 𝐺 ) ℎ ) ⊕ 𝑢 ) = ( 𝑘 ⊕ ( ℎ ⊕ 𝑢 ) ) )
50 simprrl ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) ) ∧ ( ( ℎ ∈ 𝑋 ∧ 𝑘 ∈ 𝑋 ) ∧ ( ( ℎ ⊕ 𝑢 ) = 𝑣 ∧ ( 𝑘 ⊕ 𝑣 ) = 𝑤 ) ) ) → ( ℎ ⊕ 𝑢 ) = 𝑣 )
51 50 oveq2d ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) ) ∧ ( ( ℎ ∈ 𝑋 ∧ 𝑘 ∈ 𝑋 ) ∧ ( ( ℎ ⊕ 𝑢 ) = 𝑣 ∧ ( 𝑘 ⊕ 𝑣 ) = 𝑤 ) ) ) → ( 𝑘 ⊕ ( ℎ ⊕ 𝑢 ) ) = ( 𝑘 ⊕ 𝑣 ) )
52 simprrr ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) ) ∧ ( ( ℎ ∈ 𝑋 ∧ 𝑘 ∈ 𝑋 ) ∧ ( ( ℎ ⊕ 𝑢 ) = 𝑣 ∧ ( 𝑘 ⊕ 𝑣 ) = 𝑤 ) ) ) → ( 𝑘 ⊕ 𝑣 ) = 𝑤 )
53 49 51 52 3eqtrd ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) ) ∧ ( ( ℎ ∈ 𝑋 ∧ 𝑘 ∈ 𝑋 ) ∧ ( ( ℎ ⊕ 𝑢 ) = 𝑣 ∧ ( 𝑘 ⊕ 𝑣 ) = 𝑤 ) ) ) → ( ( 𝑘 ( +g ‘ 𝐺 ) ℎ ) ⊕ 𝑢 ) = 𝑤 )
54 oveq1 ⊢ ( 𝑓 = ( 𝑘 ( +g ‘ 𝐺 ) ℎ ) → ( 𝑓 ⊕ 𝑢 ) = ( ( 𝑘 ( +g ‘ 𝐺 ) ℎ ) ⊕ 𝑢 ) )
55 54 eqeq1d ⊢ ( 𝑓 = ( 𝑘 ( +g ‘ 𝐺 ) ℎ ) → ( ( 𝑓 ⊕ 𝑢 ) = 𝑤 ↔ ( ( 𝑘 ( +g ‘ 𝐺 ) ℎ ) ⊕ 𝑢 ) = 𝑤 ) )
56 55 rspcev ⊢ ( ( ( 𝑘 ( +g ‘ 𝐺 ) ℎ ) ∈ 𝑋 ∧ ( ( 𝑘 ( +g ‘ 𝐺 ) ℎ ) ⊕ 𝑢 ) = 𝑤 ) → ∃ 𝑓 ∈ 𝑋 ( 𝑓 ⊕ 𝑢 ) = 𝑤 )
57 45 53 56 syl2anc ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) ) ∧ ( ( ℎ ∈ 𝑋 ∧ 𝑘 ∈ 𝑋 ) ∧ ( ( ℎ ⊕ 𝑢 ) = 𝑣 ∧ ( 𝑘 ⊕ 𝑣 ) = 𝑤 ) ) ) → ∃ 𝑓 ∈ 𝑋 ( 𝑓 ⊕ 𝑢 ) = 𝑤 )
58 57 expr ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) ) ∧ ( ℎ ∈ 𝑋 ∧ 𝑘 ∈ 𝑋 ) ) → ( ( ( ℎ ⊕ 𝑢 ) = 𝑣 ∧ ( 𝑘 ⊕ 𝑣 ) = 𝑤 ) → ∃ 𝑓 ∈ 𝑋 ( 𝑓 ⊕ 𝑢 ) = 𝑤 ) )
59 58 rexlimdvva ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) ) → ( ∃ ℎ ∈ 𝑋 ∃ 𝑘 ∈ 𝑋 ( ( ℎ ⊕ 𝑢 ) = 𝑣 ∧ ( 𝑘 ⊕ 𝑣 ) = 𝑤 ) → ∃ 𝑓 ∈ 𝑋 ( 𝑓 ⊕ 𝑢 ) = 𝑤 ) )
60 39 59 biimtrrid ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) ) → ( ( ∃ ℎ ∈ 𝑋 ( ℎ ⊕ 𝑢 ) = 𝑣 ∧ ∃ 𝑘 ∈ 𝑋 ( 𝑘 ⊕ 𝑣 ) = 𝑤 ) → ∃ 𝑓 ∈ 𝑋 ( 𝑓 ⊕ 𝑢 ) = 𝑤 ) )
61 37 38 60 mp2and ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) ) → ∃ 𝑓 ∈ 𝑋 ( 𝑓 ⊕ 𝑢 ) = 𝑤 )
62 1 gaorb ⊢ ( 𝑢 ∼ 𝑤 ↔ ( 𝑢 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ∧ ∃ 𝑓 ∈ 𝑋 ( 𝑓 ⊕ 𝑢 ) = 𝑤 ) )
63 32 36 61 62 syl3anbrc ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑢 ∼ 𝑣 ∧ 𝑣 ∼ 𝑤 ) ) → 𝑢 ∼ 𝑤 )
64 18 adantr ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑢 ∈ 𝑌 ) → 𝐺 ∈ Grp )
65 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
66 2 65 grpidcl ⊢ ( 𝐺 ∈ Grp → ( 0g ‘ 𝐺 ) ∈ 𝑋 )
67 64 66 syl ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑢 ∈ 𝑌 ) → ( 0g ‘ 𝐺 ) ∈ 𝑋 )
68 65 gagrpid ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑢 ∈ 𝑌 ) → ( ( 0g ‘ 𝐺 ) ⊕ 𝑢 ) = 𝑢 )
69 oveq1 ⊢ ( ℎ = ( 0g ‘ 𝐺 ) → ( ℎ ⊕ 𝑢 ) = ( ( 0g ‘ 𝐺 ) ⊕ 𝑢 ) )
70 69 eqeq1d ⊢ ( ℎ = ( 0g ‘ 𝐺 ) → ( ( ℎ ⊕ 𝑢 ) = 𝑢 ↔ ( ( 0g ‘ 𝐺 ) ⊕ 𝑢 ) = 𝑢 ) )
71 70 rspcev ⊢ ( ( ( 0g ‘ 𝐺 ) ∈ 𝑋 ∧ ( ( 0g ‘ 𝐺 ) ⊕ 𝑢 ) = 𝑢 ) → ∃ ℎ ∈ 𝑋 ( ℎ ⊕ 𝑢 ) = 𝑢 )
72 67 68 71 syl2anc ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑢 ∈ 𝑌 ) → ∃ ℎ ∈ 𝑋 ( ℎ ⊕ 𝑢 ) = 𝑢 )
73 72 ex ⊢ ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) → ( 𝑢 ∈ 𝑌 → ∃ ℎ ∈ 𝑋 ( ℎ ⊕ 𝑢 ) = 𝑢 ) )
74 73 pm4.71rd ⊢ ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) → ( 𝑢 ∈ 𝑌 ↔ ( ∃ ℎ ∈ 𝑋 ( ℎ ⊕ 𝑢 ) = 𝑢 ∧ 𝑢 ∈ 𝑌 ) ) )
75 df-3an ⊢ ( ( 𝑢 ∈ 𝑌 ∧ 𝑢 ∈ 𝑌 ∧ ∃ ℎ ∈ 𝑋 ( ℎ ⊕ 𝑢 ) = 𝑢 ) ↔ ( ( 𝑢 ∈ 𝑌 ∧ 𝑢 ∈ 𝑌 ) ∧ ∃ ℎ ∈ 𝑋 ( ℎ ⊕ 𝑢 ) = 𝑢 ) )
76 anidm ⊢ ( ( 𝑢 ∈ 𝑌 ∧ 𝑢 ∈ 𝑌 ) ↔ 𝑢 ∈ 𝑌 )
77 76 anbi2ci ⊢ ( ( ( 𝑢 ∈ 𝑌 ∧ 𝑢 ∈ 𝑌 ) ∧ ∃ ℎ ∈ 𝑋 ( ℎ ⊕ 𝑢 ) = 𝑢 ) ↔ ( ∃ ℎ ∈ 𝑋 ( ℎ ⊕ 𝑢 ) = 𝑢 ∧ 𝑢 ∈ 𝑌 ) )
78 75 77 bitri ⊢ ( ( 𝑢 ∈ 𝑌 ∧ 𝑢 ∈ 𝑌 ∧ ∃ ℎ ∈ 𝑋 ( ℎ ⊕ 𝑢 ) = 𝑢 ) ↔ ( ∃ ℎ ∈ 𝑋 ( ℎ ⊕ 𝑢 ) = 𝑢 ∧ 𝑢 ∈ 𝑌 ) )
79 74 78 bitr4di ⊢ ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) → ( 𝑢 ∈ 𝑌 ↔ ( 𝑢 ∈ 𝑌 ∧ 𝑢 ∈ 𝑌 ∧ ∃ ℎ ∈ 𝑋 ( ℎ ⊕ 𝑢 ) = 𝑢 ) ) )
80 1 gaorb ⊢ ( 𝑢 ∼ 𝑢 ↔ ( 𝑢 ∈ 𝑌 ∧ 𝑢 ∈ 𝑌 ∧ ∃ ℎ ∈ 𝑋 ( ℎ ⊕ 𝑢 ) = 𝑢 ) )
81 79 80 bitr4di ⊢ ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) → ( 𝑢 ∈ 𝑌 ↔ 𝑢 ∼ 𝑢 ) )
82 4 31 63 81 iserd ⊢ ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) → ∼ Er 𝑌 )