Step | Hyp | Ref
| Expression |
1 | | gasta.1 |
. . . . 5
⊢ 𝑋 = (Base‘𝐺) |
2 | | gasta.2 |
. . . . 5
⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐴) = 𝐴} |
3 | | orbsta.r |
. . . . 5
⊢ ∼ =
(𝐺 ~QG
𝐻) |
4 | | orbsta.f |
. . . . 5
⊢ 𝐹 = ran (𝑘 ∈ 𝑋 ↦ 〈[𝑘] ∼ , (𝑘 ⊕ 𝐴)〉) |
5 | 1, 2, 3, 4 | orbstafun 17567 |
. . . 4
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → Fun 𝐹) |
6 | | simpr 476 |
. . . . . . . 8
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → 𝐴 ∈ 𝑌) |
7 | 6 | adantr 480 |
. . . . . . 7
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑘 ∈ 𝑋) → 𝐴 ∈ 𝑌) |
8 | 1 | gaf 17551 |
. . . . . . . . . 10
⊢ ( ⊕ ∈
(𝐺 GrpAct 𝑌) → ⊕ :(𝑋 × 𝑌)⟶𝑌) |
9 | 8 | adantr 480 |
. . . . . . . . 9
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → ⊕ :(𝑋 × 𝑌)⟶𝑌) |
10 | 9 | adantr 480 |
. . . . . . . 8
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑘 ∈ 𝑋) → ⊕ :(𝑋 × 𝑌)⟶𝑌) |
11 | | simpr 476 |
. . . . . . . 8
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋) |
12 | 10, 11, 7 | fovrnd 6704 |
. . . . . . 7
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑘 ∈ 𝑋) → (𝑘 ⊕ 𝐴) ∈ 𝑌) |
13 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑘 ⊕ 𝐴) = (𝑘 ⊕ 𝐴) |
14 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (ℎ = 𝑘 → (ℎ ⊕ 𝐴) = (𝑘 ⊕ 𝐴)) |
15 | 14 | eqeq1d 2612 |
. . . . . . . . 9
⊢ (ℎ = 𝑘 → ((ℎ ⊕ 𝐴) = (𝑘 ⊕ 𝐴) ↔ (𝑘 ⊕ 𝐴) = (𝑘 ⊕ 𝐴))) |
16 | 15 | rspcev 3282 |
. . . . . . . 8
⊢ ((𝑘 ∈ 𝑋 ∧ (𝑘 ⊕ 𝐴) = (𝑘 ⊕ 𝐴)) → ∃ℎ ∈ 𝑋 (ℎ ⊕ 𝐴) = (𝑘 ⊕ 𝐴)) |
17 | 11, 13, 16 | sylancl 693 |
. . . . . . 7
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑘 ∈ 𝑋) → ∃ℎ ∈ 𝑋 (ℎ ⊕ 𝐴) = (𝑘 ⊕ 𝐴)) |
18 | | orbsta.o |
. . . . . . . 8
⊢ 𝑂 = {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝑌 ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} |
19 | 18 | gaorb 17563 |
. . . . . . 7
⊢ (𝐴𝑂(𝑘 ⊕ 𝐴) ↔ (𝐴 ∈ 𝑌 ∧ (𝑘 ⊕ 𝐴) ∈ 𝑌 ∧ ∃ℎ ∈ 𝑋 (ℎ ⊕ 𝐴) = (𝑘 ⊕ 𝐴))) |
20 | 7, 12, 17, 19 | syl3anbrc 1239 |
. . . . . 6
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑘 ∈ 𝑋) → 𝐴𝑂(𝑘 ⊕ 𝐴)) |
21 | | ovex 6577 |
. . . . . . 7
⊢ (𝑘 ⊕ 𝐴) ∈ V |
22 | | elecg 7672 |
. . . . . . 7
⊢ (((𝑘 ⊕ 𝐴) ∈ V ∧ 𝐴 ∈ 𝑌) → ((𝑘 ⊕ 𝐴) ∈ [𝐴]𝑂 ↔ 𝐴𝑂(𝑘 ⊕ 𝐴))) |
23 | 21, 7, 22 | sylancr 694 |
. . . . . 6
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑘 ∈ 𝑋) → ((𝑘 ⊕ 𝐴) ∈ [𝐴]𝑂 ↔ 𝐴𝑂(𝑘 ⊕ 𝐴))) |
24 | 20, 23 | mpbird 246 |
. . . . 5
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑘 ∈ 𝑋) → (𝑘 ⊕ 𝐴) ∈ [𝐴]𝑂) |
25 | 1, 2 | gastacl 17565 |
. . . . . 6
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → 𝐻 ∈ (SubGrp‘𝐺)) |
26 | 1, 3 | eqger 17467 |
. . . . . 6
⊢ (𝐻 ∈ (SubGrp‘𝐺) → ∼ Er 𝑋) |
27 | 25, 26 | syl 17 |
. . . . 5
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → ∼ Er 𝑋) |
28 | | fvex 6113 |
. . . . . . 7
⊢
(Base‘𝐺)
∈ V |
29 | 1, 28 | eqeltri 2684 |
. . . . . 6
⊢ 𝑋 ∈ V |
30 | 29 | a1i 11 |
. . . . 5
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → 𝑋 ∈ V) |
31 | 4, 24, 27, 30 | qliftf 7722 |
. . . 4
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → (Fun 𝐹 ↔ 𝐹:(𝑋 / ∼ )⟶[𝐴]𝑂)) |
32 | 5, 31 | mpbid 221 |
. . 3
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → 𝐹:(𝑋 / ∼ )⟶[𝐴]𝑂) |
33 | | eqid 2610 |
. . . . 5
⊢ (𝑋 / ∼ ) = (𝑋 / ∼ ) |
34 | | fveq2 6103 |
. . . . . . . 8
⊢ ([𝑧] ∼ = 𝑎 → (𝐹‘[𝑧] ∼ ) = (𝐹‘𝑎)) |
35 | 34 | eqeq1d 2612 |
. . . . . . 7
⊢ ([𝑧] ∼ = 𝑎 → ((𝐹‘[𝑧] ∼ ) = (𝐹‘𝑏) ↔ (𝐹‘𝑎) = (𝐹‘𝑏))) |
36 | | eqeq1 2614 |
. . . . . . 7
⊢ ([𝑧] ∼ = 𝑎 → ([𝑧] ∼ = 𝑏 ↔ 𝑎 = 𝑏)) |
37 | 35, 36 | imbi12d 333 |
. . . . . 6
⊢ ([𝑧] ∼ = 𝑎 → (((𝐹‘[𝑧] ∼ ) = (𝐹‘𝑏) → [𝑧] ∼ = 𝑏) ↔ ((𝐹‘𝑎) = (𝐹‘𝑏) → 𝑎 = 𝑏))) |
38 | 37 | ralbidv 2969 |
. . . . 5
⊢ ([𝑧] ∼ = 𝑎 → (∀𝑏 ∈ (𝑋 / ∼ )((𝐹‘[𝑧] ∼ ) = (𝐹‘𝑏) → [𝑧] ∼ = 𝑏) ↔ ∀𝑏 ∈ (𝑋 / ∼ )((𝐹‘𝑎) = (𝐹‘𝑏) → 𝑎 = 𝑏))) |
39 | | fveq2 6103 |
. . . . . . . . 9
⊢ ([𝑤] ∼ = 𝑏 → (𝐹‘[𝑤] ∼ ) = (𝐹‘𝑏)) |
40 | 39 | eqeq2d 2620 |
. . . . . . . 8
⊢ ([𝑤] ∼ = 𝑏 → ((𝐹‘[𝑧] ∼ ) = (𝐹‘[𝑤] ∼ ) ↔ (𝐹‘[𝑧] ∼ ) = (𝐹‘𝑏))) |
41 | | eqeq2 2621 |
. . . . . . . 8
⊢ ([𝑤] ∼ = 𝑏 → ([𝑧] ∼ = [𝑤] ∼ ↔ [𝑧] ∼ = 𝑏)) |
42 | 40, 41 | imbi12d 333 |
. . . . . . 7
⊢ ([𝑤] ∼ = 𝑏 → (((𝐹‘[𝑧] ∼ ) = (𝐹‘[𝑤] ∼ ) → [𝑧] ∼ = [𝑤] ∼ ) ↔ ((𝐹‘[𝑧] ∼ ) = (𝐹‘𝑏) → [𝑧] ∼ = 𝑏))) |
43 | 1, 2, 3, 4 | orbstaval 17568 |
. . . . . . . . . . . 12
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → (𝐹‘[𝑧] ∼ ) = (𝑧 ⊕ 𝐴)) |
44 | 43 | adantrr 749 |
. . . . . . . . . . 11
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → (𝐹‘[𝑧] ∼ ) = (𝑧 ⊕ 𝐴)) |
45 | 1, 2, 3, 4 | orbstaval 17568 |
. . . . . . . . . . . 12
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑤 ∈ 𝑋) → (𝐹‘[𝑤] ∼ ) = (𝑤 ⊕ 𝐴)) |
46 | 45 | adantrl 748 |
. . . . . . . . . . 11
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → (𝐹‘[𝑤] ∼ ) = (𝑤 ⊕ 𝐴)) |
47 | 44, 46 | eqeq12d 2625 |
. . . . . . . . . 10
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → ((𝐹‘[𝑧] ∼ ) = (𝐹‘[𝑤] ∼ ) ↔ (𝑧 ⊕ 𝐴) = (𝑤 ⊕ 𝐴))) |
48 | 1, 2, 3 | gastacos 17566 |
. . . . . . . . . 10
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → (𝑧 ∼ 𝑤 ↔ (𝑧 ⊕ 𝐴) = (𝑤 ⊕ 𝐴))) |
49 | 27 | adantr 480 |
. . . . . . . . . . 11
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → ∼ Er 𝑋) |
50 | | simprl 790 |
. . . . . . . . . . 11
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → 𝑧 ∈ 𝑋) |
51 | 49, 50 | erth 7678 |
. . . . . . . . . 10
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → (𝑧 ∼ 𝑤 ↔ [𝑧] ∼ = [𝑤] ∼ )) |
52 | 47, 48, 51 | 3bitr2d 295 |
. . . . . . . . 9
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → ((𝐹‘[𝑧] ∼ ) = (𝐹‘[𝑤] ∼ ) ↔ [𝑧] ∼ = [𝑤] ∼ )) |
53 | 52 | biimpd 218 |
. . . . . . . 8
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → ((𝐹‘[𝑧] ∼ ) = (𝐹‘[𝑤] ∼ ) → [𝑧] ∼ = [𝑤] ∼ )) |
54 | 53 | anassrs 678 |
. . . . . . 7
⊢ ((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) → ((𝐹‘[𝑧] ∼ ) = (𝐹‘[𝑤] ∼ ) → [𝑧] ∼ = [𝑤] ∼ )) |
55 | 33, 42, 54 | ectocld 7701 |
. . . . . 6
⊢ ((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) ∧ 𝑏 ∈ (𝑋 / ∼ )) → ((𝐹‘[𝑧] ∼ ) = (𝐹‘𝑏) → [𝑧] ∼ = 𝑏)) |
56 | 55 | ralrimiva 2949 |
. . . . 5
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → ∀𝑏 ∈ (𝑋 / ∼ )((𝐹‘[𝑧] ∼ ) = (𝐹‘𝑏) → [𝑧] ∼ = 𝑏)) |
57 | 33, 38, 56 | ectocld 7701 |
. . . 4
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑎 ∈ (𝑋 / ∼ )) →
∀𝑏 ∈ (𝑋 / ∼ )((𝐹‘𝑎) = (𝐹‘𝑏) → 𝑎 = 𝑏)) |
58 | 57 | ralrimiva 2949 |
. . 3
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → ∀𝑎 ∈ (𝑋 / ∼ )∀𝑏 ∈ (𝑋 / ∼ )((𝐹‘𝑎) = (𝐹‘𝑏) → 𝑎 = 𝑏)) |
59 | | dff13 6416 |
. . 3
⊢ (𝐹:(𝑋 / ∼ )–1-1→[𝐴]𝑂 ↔ (𝐹:(𝑋 / ∼ )⟶[𝐴]𝑂 ∧ ∀𝑎 ∈ (𝑋 / ∼ )∀𝑏 ∈ (𝑋 / ∼ )((𝐹‘𝑎) = (𝐹‘𝑏) → 𝑎 = 𝑏))) |
60 | 32, 58, 59 | sylanbrc 695 |
. 2
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → 𝐹:(𝑋 / ∼ )–1-1→[𝐴]𝑂) |
61 | | vex 3176 |
. . . . . . . . 9
⊢ ℎ ∈ V |
62 | | elecg 7672 |
. . . . . . . . 9
⊢ ((ℎ ∈ V ∧ 𝐴 ∈ 𝑌) → (ℎ ∈ [𝐴]𝑂 ↔ 𝐴𝑂ℎ)) |
63 | 61, 6, 62 | sylancr 694 |
. . . . . . . 8
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → (ℎ ∈ [𝐴]𝑂 ↔ 𝐴𝑂ℎ)) |
64 | 18 | gaorb 17563 |
. . . . . . . 8
⊢ (𝐴𝑂ℎ ↔ (𝐴 ∈ 𝑌 ∧ ℎ ∈ 𝑌 ∧ ∃𝑤 ∈ 𝑋 (𝑤 ⊕ 𝐴) = ℎ)) |
65 | 63, 64 | syl6bb 275 |
. . . . . . 7
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → (ℎ ∈ [𝐴]𝑂 ↔ (𝐴 ∈ 𝑌 ∧ ℎ ∈ 𝑌 ∧ ∃𝑤 ∈ 𝑋 (𝑤 ⊕ 𝐴) = ℎ))) |
66 | 65 | biimpa 500 |
. . . . . 6
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ ℎ ∈ [𝐴]𝑂) → (𝐴 ∈ 𝑌 ∧ ℎ ∈ 𝑌 ∧ ∃𝑤 ∈ 𝑋 (𝑤 ⊕ 𝐴) = ℎ)) |
67 | 66 | simp3d 1068 |
. . . . 5
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ ℎ ∈ [𝐴]𝑂) → ∃𝑤 ∈ 𝑋 (𝑤 ⊕ 𝐴) = ℎ) |
68 | | ovex 6577 |
. . . . . . . . . . . 12
⊢ (𝐺 ~QG 𝐻) ∈ V |
69 | 3, 68 | eqeltri 2684 |
. . . . . . . . . . 11
⊢ ∼ ∈
V |
70 | 69 | ecelqsi 7690 |
. . . . . . . . . 10
⊢ (𝑤 ∈ 𝑋 → [𝑤] ∼ ∈ (𝑋 / ∼ )) |
71 | 70 | adantl 481 |
. . . . . . . . 9
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑤 ∈ 𝑋) → [𝑤] ∼ ∈ (𝑋 / ∼ )) |
72 | 45 | eqcomd 2616 |
. . . . . . . . 9
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑤 ∈ 𝑋) → (𝑤 ⊕ 𝐴) = (𝐹‘[𝑤] ∼ )) |
73 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑧 = [𝑤] ∼ → (𝐹‘𝑧) = (𝐹‘[𝑤] ∼ )) |
74 | 73 | eqeq2d 2620 |
. . . . . . . . . 10
⊢ (𝑧 = [𝑤] ∼ → ((𝑤 ⊕ 𝐴) = (𝐹‘𝑧) ↔ (𝑤 ⊕ 𝐴) = (𝐹‘[𝑤] ∼
))) |
75 | 74 | rspcev 3282 |
. . . . . . . . 9
⊢ (([𝑤] ∼ ∈ (𝑋 / ∼ ) ∧ (𝑤 ⊕ 𝐴) = (𝐹‘[𝑤] ∼ )) →
∃𝑧 ∈ (𝑋 / ∼ )(𝑤 ⊕ 𝐴) = (𝐹‘𝑧)) |
76 | 71, 72, 75 | syl2anc 691 |
. . . . . . . 8
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑤 ∈ 𝑋) → ∃𝑧 ∈ (𝑋 / ∼ )(𝑤 ⊕ 𝐴) = (𝐹‘𝑧)) |
77 | | eqeq1 2614 |
. . . . . . . . 9
⊢ ((𝑤 ⊕ 𝐴) = ℎ → ((𝑤 ⊕ 𝐴) = (𝐹‘𝑧) ↔ ℎ = (𝐹‘𝑧))) |
78 | 77 | rexbidv 3034 |
. . . . . . . 8
⊢ ((𝑤 ⊕ 𝐴) = ℎ → (∃𝑧 ∈ (𝑋 / ∼ )(𝑤 ⊕ 𝐴) = (𝐹‘𝑧) ↔ ∃𝑧 ∈ (𝑋 / ∼ )ℎ = (𝐹‘𝑧))) |
79 | 76, 78 | syl5ibcom 234 |
. . . . . . 7
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑤 ∈ 𝑋) → ((𝑤 ⊕ 𝐴) = ℎ → ∃𝑧 ∈ (𝑋 / ∼ )ℎ = (𝐹‘𝑧))) |
80 | 79 | rexlimdva 3013 |
. . . . . 6
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → (∃𝑤 ∈ 𝑋 (𝑤 ⊕ 𝐴) = ℎ → ∃𝑧 ∈ (𝑋 / ∼ )ℎ = (𝐹‘𝑧))) |
81 | 80 | imp 444 |
. . . . 5
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ ∃𝑤 ∈ 𝑋 (𝑤 ⊕ 𝐴) = ℎ) → ∃𝑧 ∈ (𝑋 / ∼ )ℎ = (𝐹‘𝑧)) |
82 | 67, 81 | syldan 486 |
. . . 4
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ ℎ ∈ [𝐴]𝑂) → ∃𝑧 ∈ (𝑋 / ∼ )ℎ = (𝐹‘𝑧)) |
83 | 82 | ralrimiva 2949 |
. . 3
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → ∀ℎ ∈ [ 𝐴]𝑂∃𝑧 ∈ (𝑋 / ∼ )ℎ = (𝐹‘𝑧)) |
84 | | dffo3 6282 |
. . 3
⊢ (𝐹:(𝑋 / ∼ )–onto→[𝐴]𝑂 ↔ (𝐹:(𝑋 / ∼ )⟶[𝐴]𝑂 ∧ ∀ℎ ∈ [ 𝐴]𝑂∃𝑧 ∈ (𝑋 / ∼ )ℎ = (𝐹‘𝑧))) |
85 | 32, 83, 84 | sylanbrc 695 |
. 2
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → 𝐹:(𝑋 / ∼ )–onto→[𝐴]𝑂) |
86 | | df-f1o 5811 |
. 2
⊢ (𝐹:(𝑋 / ∼ )–1-1-onto→[𝐴]𝑂 ↔ (𝐹:(𝑋 / ∼ )–1-1→[𝐴]𝑂 ∧ 𝐹:(𝑋 / ∼ )–onto→[𝐴]𝑂)) |
87 | 60, 85, 86 | sylanbrc 695 |
1
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → 𝐹:(𝑋 / ∼ )–1-1-onto→[𝐴]𝑂) |