Metamath Proof Explorer

Theorem orbsta

Description: The Orbit-Stabilizer theorem. The mapping F is a bijection from the cosets of the stabilizer subgroup of A to the orbit of A . (Contributed by Mario Carneiro, 15-Jan-2015)

Ref Expression
Hypotheses gasta.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
gasta.2 ⊢ 𝐻 = { 𝑢 ∈ 𝑋 ∣ ( 𝑢 ⊕ 𝐴 ) = 𝐴 }
orbsta.r ⊢ ∼ = ( 𝐺 ~QG 𝐻 )
orbsta.f ⊢ 𝐹 = ran ( 𝑘 ∈ 𝑋 ↦ ⟨ [ 𝑘 ] ∼ , ( 𝑘 ⊕ 𝐴 ) ⟩ )
orbsta.o ⊢ 𝑂 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑌 ∧ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ) }
Assertion orbsta ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) → 𝐹 : ( 𝑋 / ∼ ) –1-1-onto→ [ 𝐴 ] 𝑂 )

Proof

Step Hyp Ref Expression
1 gasta.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 gasta.2 ⊢ 𝐻 = { 𝑢 ∈ 𝑋 ∣ ( 𝑢 ⊕ 𝐴 ) = 𝐴 }
3 orbsta.r ⊢ ∼ = ( 𝐺 ~QG 𝐻 )
4 orbsta.f ⊢ 𝐹 = ran ( 𝑘 ∈ 𝑋 ↦ ⟨ [ 𝑘 ] ∼ , ( 𝑘 ⊕ 𝐴 ) ⟩ )
5 orbsta.o ⊢ 𝑂 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑌 ∧ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ) }
6 1 2 3 4 orbstafun ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) → Fun 𝐹 )
7 simpr ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) → 𝐴 ∈ 𝑌 )
8 7 adantr ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑘 ∈ 𝑋 ) → 𝐴 ∈ 𝑌 )
9 1 gaf ⊢ ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) → ⊕ : ( 𝑋 × 𝑌 ) ⟶ 𝑌 )
10 9 adantr ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) → ⊕ : ( 𝑋 × 𝑌 ) ⟶ 𝑌 )
11 10 adantr ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑘 ∈ 𝑋 ) → ⊕ : ( 𝑋 × 𝑌 ) ⟶ 𝑌 )
12 simpr ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑘 ∈ 𝑋 ) → 𝑘 ∈ 𝑋 )
13 11 12 8 fovcdmd ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑘 ⊕ 𝐴 ) ∈ 𝑌 )
14 eqid ⊢ ( 𝑘 ⊕ 𝐴 ) = ( 𝑘 ⊕ 𝐴 )
15 oveq1 ⊢ ( ℎ = 𝑘 → ( ℎ ⊕ 𝐴 ) = ( 𝑘 ⊕ 𝐴 ) )
16 15 eqeq1d ⊢ ( ℎ = 𝑘 → ( ( ℎ ⊕ 𝐴 ) = ( 𝑘 ⊕ 𝐴 ) ↔ ( 𝑘 ⊕ 𝐴 ) = ( 𝑘 ⊕ 𝐴 ) ) )
17 16 rspcev ⊢ ( ( 𝑘 ∈ 𝑋 ∧ ( 𝑘 ⊕ 𝐴 ) = ( 𝑘 ⊕ 𝐴 ) ) → ∃ ℎ ∈ 𝑋 ( ℎ ⊕ 𝐴 ) = ( 𝑘 ⊕ 𝐴 ) )
18 12 14 17 sylancl ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑘 ∈ 𝑋 ) → ∃ ℎ ∈ 𝑋 ( ℎ ⊕ 𝐴 ) = ( 𝑘 ⊕ 𝐴 ) )
19 5 gaorb ⊢ ( 𝐴 𝑂 ( 𝑘 ⊕ 𝐴 ) ↔ ( 𝐴 ∈ 𝑌 ∧ ( 𝑘 ⊕ 𝐴 ) ∈ 𝑌 ∧ ∃ ℎ ∈ 𝑋 ( ℎ ⊕ 𝐴 ) = ( 𝑘 ⊕ 𝐴 ) ) )
20 8 13 18 19 syl3anbrc ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑘 ∈ 𝑋 ) → 𝐴 𝑂 ( 𝑘 ⊕ 𝐴 ) )
21 ovex ⊢ ( 𝑘 ⊕ 𝐴 ) ∈ V
22 elecg ⊢ ( ( ( 𝑘 ⊕ 𝐴 ) ∈ V ∧ 𝐴 ∈ 𝑌 ) → ( ( 𝑘 ⊕ 𝐴 ) ∈ [ 𝐴 ] 𝑂 ↔ 𝐴 𝑂 ( 𝑘 ⊕ 𝐴 ) ) )
23 21 8 22 sylancr ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝑘 ⊕ 𝐴 ) ∈ [ 𝐴 ] 𝑂 ↔ 𝐴 𝑂 ( 𝑘 ⊕ 𝐴 ) ) )
24 20 23 mpbird ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑘 ⊕ 𝐴 ) ∈ [ 𝐴 ] 𝑂 )
25 1 2 gastacl ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) → 𝐻 ∈ ( SubGrp ‘ 𝐺 ) )
26 1 3 eqger ⊢ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) → ∼ Er 𝑋 )
27 25 26 syl ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) → ∼ Er 𝑋 )
28 1 fvexi ⊢ 𝑋 ∈ V
29 28 a1i ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) → 𝑋 ∈ V )
30 4 24 27 29 qliftf ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) → ( Fun 𝐹 ↔ 𝐹 : ( 𝑋 / ∼ ) ⟶ [ 𝐴 ] 𝑂 ) )
31 6 30 mpbid ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) → 𝐹 : ( 𝑋 / ∼ ) ⟶ [ 𝐴 ] 𝑂 )
32 eqid ⊢ ( 𝑋 / ∼ ) = ( 𝑋 / ∼ )
33 fveqeq2 ⊢ ( [ 𝑧 ] ∼ = 𝑎 → ( ( 𝐹 ‘ [ 𝑧 ] ∼ ) = ( 𝐹 ‘ 𝑏 ) ↔ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) )
34 eqeq1 ⊢ ( [ 𝑧 ] ∼ = 𝑎 → ( [ 𝑧 ] ∼ = 𝑏 ↔ 𝑎 = 𝑏 ) )
35 33 34 imbi12d ⊢ ( [ 𝑧 ] ∼ = 𝑎 → ( ( ( 𝐹 ‘ [ 𝑧 ] ∼ ) = ( 𝐹 ‘ 𝑏 ) → [ 𝑧 ] ∼ = 𝑏 ) ↔ ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) → 𝑎 = 𝑏 ) ) )
36 35 ralbidv ⊢ ( [ 𝑧 ] ∼ = 𝑎 → ( ∀ 𝑏 ∈ ( 𝑋 / ∼ ) ( ( 𝐹 ‘ [ 𝑧 ] ∼ ) = ( 𝐹 ‘ 𝑏 ) → [ 𝑧 ] ∼ = 𝑏 ) ↔ ∀ 𝑏 ∈ ( 𝑋 / ∼ ) ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) → 𝑎 = 𝑏 ) ) )
37 fveq2 ⊢ ( [ 𝑤 ] ∼ = 𝑏 → ( 𝐹 ‘ [ 𝑤 ] ∼ ) = ( 𝐹 ‘ 𝑏 ) )
38 37 eqeq2d ⊢ ( [ 𝑤 ] ∼ = 𝑏 → ( ( 𝐹 ‘ [ 𝑧 ] ∼ ) = ( 𝐹 ‘ [ 𝑤 ] ∼ ) ↔ ( 𝐹 ‘ [ 𝑧 ] ∼ ) = ( 𝐹 ‘ 𝑏 ) ) )
39 eqeq2 ⊢ ( [ 𝑤 ] ∼ = 𝑏 → ( [ 𝑧 ] ∼ = [ 𝑤 ] ∼ ↔ [ 𝑧 ] ∼ = 𝑏 ) )
40 38 39 imbi12d ⊢ ( [ 𝑤 ] ∼ = 𝑏 → ( ( ( 𝐹 ‘ [ 𝑧 ] ∼ ) = ( 𝐹 ‘ [ 𝑤 ] ∼ ) → [ 𝑧 ] ∼ = [ 𝑤 ] ∼ ) ↔ ( ( 𝐹 ‘ [ 𝑧 ] ∼ ) = ( 𝐹 ‘ 𝑏 ) → [ 𝑧 ] ∼ = 𝑏 ) ) )
41 1 2 3 4 orbstaval ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝐹 ‘ [ 𝑧 ] ∼ ) = ( 𝑧 ⊕ 𝐴 ) )
42 41 adantrr ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( 𝐹 ‘ [ 𝑧 ] ∼ ) = ( 𝑧 ⊕ 𝐴 ) )
43 1 2 3 4 orbstaval ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑤 ∈ 𝑋 ) → ( 𝐹 ‘ [ 𝑤 ] ∼ ) = ( 𝑤 ⊕ 𝐴 ) )
44 43 adantrl ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( 𝐹 ‘ [ 𝑤 ] ∼ ) = ( 𝑤 ⊕ 𝐴 ) )
45 42 44 eqeq12d ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ [ 𝑧 ] ∼ ) = ( 𝐹 ‘ [ 𝑤 ] ∼ ) ↔ ( 𝑧 ⊕ 𝐴 ) = ( 𝑤 ⊕ 𝐴 ) ) )
46 1 2 3 gastacos ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( 𝑧 ∼ 𝑤 ↔ ( 𝑧 ⊕ 𝐴 ) = ( 𝑤 ⊕ 𝐴 ) ) )
47 27 adantr ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ∼ Er 𝑋 )
48 simprl ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → 𝑧 ∈ 𝑋 )
49 47 48 erth ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( 𝑧 ∼ 𝑤 ↔ [ 𝑧 ] ∼ = [ 𝑤 ] ∼ ) )
50 45 46 49 3bitr2d ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ [ 𝑧 ] ∼ ) = ( 𝐹 ‘ [ 𝑤 ] ∼ ) ↔ [ 𝑧 ] ∼ = [ 𝑤 ] ∼ ) )
51 50 biimpd ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ [ 𝑧 ] ∼ ) = ( 𝐹 ‘ [ 𝑤 ] ∼ ) → [ 𝑧 ] ∼ = [ 𝑤 ] ∼ ) )
52 51 anassrs ⊢ ( ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑤 ∈ 𝑋 ) → ( ( 𝐹 ‘ [ 𝑧 ] ∼ ) = ( 𝐹 ‘ [ 𝑤 ] ∼ ) → [ 𝑧 ] ∼ = [ 𝑤 ] ∼ ) )
53 32 40 52 ectocld ⊢ ( ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑏 ∈ ( 𝑋 / ∼ ) ) → ( ( 𝐹 ‘ [ 𝑧 ] ∼ ) = ( 𝐹 ‘ 𝑏 ) → [ 𝑧 ] ∼ = 𝑏 ) )
54 53 ralrimiva ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑧 ∈ 𝑋 ) → ∀ 𝑏 ∈ ( 𝑋 / ∼ ) ( ( 𝐹 ‘ [ 𝑧 ] ∼ ) = ( 𝐹 ‘ 𝑏 ) → [ 𝑧 ] ∼ = 𝑏 ) )
55 32 36 54 ectocld ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑎 ∈ ( 𝑋 / ∼ ) ) → ∀ 𝑏 ∈ ( 𝑋 / ∼ ) ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) → 𝑎 = 𝑏 ) )
56 55 ralrimiva ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) → ∀ 𝑎 ∈ ( 𝑋 / ∼ ) ∀ 𝑏 ∈ ( 𝑋 / ∼ ) ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) → 𝑎 = 𝑏 ) )
57 dff13 ⊢ ( 𝐹 : ( 𝑋 / ∼ ) –1-1→ [ 𝐴 ] 𝑂 ↔ ( 𝐹 : ( 𝑋 / ∼ ) ⟶ [ 𝐴 ] 𝑂 ∧ ∀ 𝑎 ∈ ( 𝑋 / ∼ ) ∀ 𝑏 ∈ ( 𝑋 / ∼ ) ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) → 𝑎 = 𝑏 ) ) )
58 31 56 57 sylanbrc ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) → 𝐹 : ( 𝑋 / ∼ ) –1-1→ [ 𝐴 ] 𝑂 )
59 vex ⊢ ℎ ∈ V
60 elecg ⊢ ( ( ℎ ∈ V ∧ 𝐴 ∈ 𝑌 ) → ( ℎ ∈ [ 𝐴 ] 𝑂 ↔ 𝐴 𝑂 ℎ ) )
61 59 7 60 sylancr ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) → ( ℎ ∈ [ 𝐴 ] 𝑂 ↔ 𝐴 𝑂 ℎ ) )
62 5 gaorb ⊢ ( 𝐴 𝑂 ℎ ↔ ( 𝐴 ∈ 𝑌 ∧ ℎ ∈ 𝑌 ∧ ∃ 𝑤 ∈ 𝑋 ( 𝑤 ⊕ 𝐴 ) = ℎ ) )
63 61 62 bitrdi ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) → ( ℎ ∈ [ 𝐴 ] 𝑂 ↔ ( 𝐴 ∈ 𝑌 ∧ ℎ ∈ 𝑌 ∧ ∃ 𝑤 ∈ 𝑋 ( 𝑤 ⊕ 𝐴 ) = ℎ ) ) )
64 63 biimpa ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ ℎ ∈ [ 𝐴 ] 𝑂 ) → ( 𝐴 ∈ 𝑌 ∧ ℎ ∈ 𝑌 ∧ ∃ 𝑤 ∈ 𝑋 ( 𝑤 ⊕ 𝐴 ) = ℎ ) )
65 64 simp3d ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ ℎ ∈ [ 𝐴 ] 𝑂 ) → ∃ 𝑤 ∈ 𝑋 ( 𝑤 ⊕ 𝐴 ) = ℎ )
66 3 ovexi ⊢ ∼ ∈ V
67 66 ecelqsi ⊢ ( 𝑤 ∈ 𝑋 → [ 𝑤 ] ∼ ∈ ( 𝑋 / ∼ ) )
68 43 eqcomd ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑤 ∈ 𝑋 ) → ( 𝑤 ⊕ 𝐴 ) = ( 𝐹 ‘ [ 𝑤 ] ∼ ) )
69 fveq2 ⊢ ( 𝑧 = [ 𝑤 ] ∼ → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ [ 𝑤 ] ∼ ) )
70 69 rspceeqv ⊢ ( ( [ 𝑤 ] ∼ ∈ ( 𝑋 / ∼ ) ∧ ( 𝑤 ⊕ 𝐴 ) = ( 𝐹 ‘ [ 𝑤 ] ∼ ) ) → ∃ 𝑧 ∈ ( 𝑋 / ∼ ) ( 𝑤 ⊕ 𝐴 ) = ( 𝐹 ‘ 𝑧 ) )
71 67 68 70 syl2an2 ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑤 ∈ 𝑋 ) → ∃ 𝑧 ∈ ( 𝑋 / ∼ ) ( 𝑤 ⊕ 𝐴 ) = ( 𝐹 ‘ 𝑧 ) )
72 eqeq1 ⊢ ( ( 𝑤 ⊕ 𝐴 ) = ℎ → ( ( 𝑤 ⊕ 𝐴 ) = ( 𝐹 ‘ 𝑧 ) ↔ ℎ = ( 𝐹 ‘ 𝑧 ) ) )
73 72 rexbidv ⊢ ( ( 𝑤 ⊕ 𝐴 ) = ℎ → ( ∃ 𝑧 ∈ ( 𝑋 / ∼ ) ( 𝑤 ⊕ 𝐴 ) = ( 𝐹 ‘ 𝑧 ) ↔ ∃ 𝑧 ∈ ( 𝑋 / ∼ ) ℎ = ( 𝐹 ‘ 𝑧 ) ) )
74 71 73 syl5ibcom ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑤 ∈ 𝑋 ) → ( ( 𝑤 ⊕ 𝐴 ) = ℎ → ∃ 𝑧 ∈ ( 𝑋 / ∼ ) ℎ = ( 𝐹 ‘ 𝑧 ) ) )
75 74 rexlimdva ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) → ( ∃ 𝑤 ∈ 𝑋 ( 𝑤 ⊕ 𝐴 ) = ℎ → ∃ 𝑧 ∈ ( 𝑋 / ∼ ) ℎ = ( 𝐹 ‘ 𝑧 ) ) )
76 75 imp ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ ∃ 𝑤 ∈ 𝑋 ( 𝑤 ⊕ 𝐴 ) = ℎ ) → ∃ 𝑧 ∈ ( 𝑋 / ∼ ) ℎ = ( 𝐹 ‘ 𝑧 ) )
77 65 76 syldan ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ ℎ ∈ [ 𝐴 ] 𝑂 ) → ∃ 𝑧 ∈ ( 𝑋 / ∼ ) ℎ = ( 𝐹 ‘ 𝑧 ) )
78 77 ralrimiva ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) → ∀ ℎ ∈ [ 𝐴 ] 𝑂 ∃ 𝑧 ∈ ( 𝑋 / ∼ ) ℎ = ( 𝐹 ‘ 𝑧 ) )
79 dffo3 ⊢ ( 𝐹 : ( 𝑋 / ∼ ) –onto→ [ 𝐴 ] 𝑂 ↔ ( 𝐹 : ( 𝑋 / ∼ ) ⟶ [ 𝐴 ] 𝑂 ∧ ∀ ℎ ∈ [ 𝐴 ] 𝑂 ∃ 𝑧 ∈ ( 𝑋 / ∼ ) ℎ = ( 𝐹 ‘ 𝑧 ) ) )
80 31 78 79 sylanbrc ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) → 𝐹 : ( 𝑋 / ∼ ) –onto→ [ 𝐴 ] 𝑂 )
81 df-f1o ⊢ ( 𝐹 : ( 𝑋 / ∼ ) –1-1-onto→ [ 𝐴 ] 𝑂 ↔ ( 𝐹 : ( 𝑋 / ∼ ) –1-1→ [ 𝐴 ] 𝑂 ∧ 𝐹 : ( 𝑋 / ∼ ) –onto→ [ 𝐴 ] 𝑂 ) )
82 58 80 81 sylanbrc ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) → 𝐹 : ( 𝑋 / ∼ ) –1-1-onto→ [ 𝐴 ] 𝑂 )