| 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 19329 |
. . . 4
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → Fun 𝐹) |
| 6 | | simpr 484 |
. . . . . . . 8
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → 𝐴 ∈ 𝑌) |
| 7 | 6 | adantr 480 |
. . . . . . 7
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑘 ∈ 𝑋) → 𝐴 ∈ 𝑌) |
| 8 | 1 | gaf 19313 |
. . . . . . . . . 10
⊢ ( ⊕ ∈
(𝐺 GrpAct 𝑌) → ⊕ :(𝑋 × 𝑌)⟶𝑌) |
| 9 | 8 | adantr 480 |
. . . . . . . . 9
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → ⊕ :(𝑋 × 𝑌)⟶𝑌) |
| 10 | 9 | adantr 480 |
. . . . . . . 8
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑘 ∈ 𝑋) → ⊕ :(𝑋 × 𝑌)⟶𝑌) |
| 11 | | simpr 484 |
. . . . . . . 8
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋) |
| 12 | 10, 11, 7 | fovcdmd 7605 |
. . . . . . 7
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑘 ∈ 𝑋) → (𝑘 ⊕ 𝐴) ∈ 𝑌) |
| 13 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑘 ⊕ 𝐴) = (𝑘 ⊕ 𝐴) |
| 14 | | oveq1 7438 |
. . . . . . . . . 10
⊢ (ℎ = 𝑘 → (ℎ ⊕ 𝐴) = (𝑘 ⊕ 𝐴)) |
| 15 | 14 | eqeq1d 2739 |
. . . . . . . . 9
⊢ (ℎ = 𝑘 → ((ℎ ⊕ 𝐴) = (𝑘 ⊕ 𝐴) ↔ (𝑘 ⊕ 𝐴) = (𝑘 ⊕ 𝐴))) |
| 16 | 15 | rspcev 3622 |
. . . . . . . 8
⊢ ((𝑘 ∈ 𝑋 ∧ (𝑘 ⊕ 𝐴) = (𝑘 ⊕ 𝐴)) → ∃ℎ ∈ 𝑋 (ℎ ⊕ 𝐴) = (𝑘 ⊕ 𝐴)) |
| 17 | 11, 13, 16 | sylancl 586 |
. . . . . . 7
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑘 ∈ 𝑋) → ∃ℎ ∈ 𝑋 (ℎ ⊕ 𝐴) = (𝑘 ⊕ 𝐴)) |
| 18 | | orbsta.o |
. . . . . . . 8
⊢ 𝑂 = {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝑌 ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} |
| 19 | 18 | gaorb 19325 |
. . . . . . 7
⊢ (𝐴𝑂(𝑘 ⊕ 𝐴) ↔ (𝐴 ∈ 𝑌 ∧ (𝑘 ⊕ 𝐴) ∈ 𝑌 ∧ ∃ℎ ∈ 𝑋 (ℎ ⊕ 𝐴) = (𝑘 ⊕ 𝐴))) |
| 20 | 7, 12, 17, 19 | syl3anbrc 1344 |
. . . . . 6
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑘 ∈ 𝑋) → 𝐴𝑂(𝑘 ⊕ 𝐴)) |
| 21 | | ovex 7464 |
. . . . . . 7
⊢ (𝑘 ⊕ 𝐴) ∈ V |
| 22 | | elecg 8789 |
. . . . . . 7
⊢ (((𝑘 ⊕ 𝐴) ∈ V ∧ 𝐴 ∈ 𝑌) → ((𝑘 ⊕ 𝐴) ∈ [𝐴]𝑂 ↔ 𝐴𝑂(𝑘 ⊕ 𝐴))) |
| 23 | 21, 7, 22 | sylancr 587 |
. . . . . 6
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑘 ∈ 𝑋) → ((𝑘 ⊕ 𝐴) ∈ [𝐴]𝑂 ↔ 𝐴𝑂(𝑘 ⊕ 𝐴))) |
| 24 | 20, 23 | mpbird 257 |
. . . . 5
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑘 ∈ 𝑋) → (𝑘 ⊕ 𝐴) ∈ [𝐴]𝑂) |
| 25 | 1, 2 | gastacl 19327 |
. . . . . 6
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → 𝐻 ∈ (SubGrp‘𝐺)) |
| 26 | 1, 3 | eqger 19196 |
. . . . . 6
⊢ (𝐻 ∈ (SubGrp‘𝐺) → ∼ Er 𝑋) |
| 27 | 25, 26 | syl 17 |
. . . . 5
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → ∼ Er 𝑋) |
| 28 | 1 | fvexi 6920 |
. . . . . 6
⊢ 𝑋 ∈ V |
| 29 | 28 | a1i 11 |
. . . . 5
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → 𝑋 ∈ V) |
| 30 | 4, 24, 27, 29 | qliftf 8845 |
. . . 4
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → (Fun 𝐹 ↔ 𝐹:(𝑋 / ∼ )⟶[𝐴]𝑂)) |
| 31 | 5, 30 | mpbid 232 |
. . 3
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → 𝐹:(𝑋 / ∼ )⟶[𝐴]𝑂) |
| 32 | | eqid 2737 |
. . . . 5
⊢ (𝑋 / ∼ ) = (𝑋 / ∼ ) |
| 33 | | fveqeq2 6915 |
. . . . . . 7
⊢ ([𝑧] ∼ = 𝑎 → ((𝐹‘[𝑧] ∼ ) = (𝐹‘𝑏) ↔ (𝐹‘𝑎) = (𝐹‘𝑏))) |
| 34 | | eqeq1 2741 |
. . . . . . 7
⊢ ([𝑧] ∼ = 𝑎 → ([𝑧] ∼ = 𝑏 ↔ 𝑎 = 𝑏)) |
| 35 | 33, 34 | imbi12d 344 |
. . . . . 6
⊢ ([𝑧] ∼ = 𝑎 → (((𝐹‘[𝑧] ∼ ) = (𝐹‘𝑏) → [𝑧] ∼ = 𝑏) ↔ ((𝐹‘𝑎) = (𝐹‘𝑏) → 𝑎 = 𝑏))) |
| 36 | 35 | ralbidv 3178 |
. . . . 5
⊢ ([𝑧] ∼ = 𝑎 → (∀𝑏 ∈ (𝑋 / ∼ )((𝐹‘[𝑧] ∼ ) = (𝐹‘𝑏) → [𝑧] ∼ = 𝑏) ↔ ∀𝑏 ∈ (𝑋 / ∼ )((𝐹‘𝑎) = (𝐹‘𝑏) → 𝑎 = 𝑏))) |
| 37 | | fveq2 6906 |
. . . . . . . . 9
⊢ ([𝑤] ∼ = 𝑏 → (𝐹‘[𝑤] ∼ ) = (𝐹‘𝑏)) |
| 38 | 37 | eqeq2d 2748 |
. . . . . . . 8
⊢ ([𝑤] ∼ = 𝑏 → ((𝐹‘[𝑧] ∼ ) = (𝐹‘[𝑤] ∼ ) ↔ (𝐹‘[𝑧] ∼ ) = (𝐹‘𝑏))) |
| 39 | | eqeq2 2749 |
. . . . . . . 8
⊢ ([𝑤] ∼ = 𝑏 → ([𝑧] ∼ = [𝑤] ∼ ↔ [𝑧] ∼ = 𝑏)) |
| 40 | 38, 39 | imbi12d 344 |
. . . . . . 7
⊢ ([𝑤] ∼ = 𝑏 → (((𝐹‘[𝑧] ∼ ) = (𝐹‘[𝑤] ∼ ) → [𝑧] ∼ = [𝑤] ∼ ) ↔ ((𝐹‘[𝑧] ∼ ) = (𝐹‘𝑏) → [𝑧] ∼ = 𝑏))) |
| 41 | 1, 2, 3, 4 | orbstaval 19330 |
. . . . . . . . . . . 12
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → (𝐹‘[𝑧] ∼ ) = (𝑧 ⊕ 𝐴)) |
| 42 | 41 | adantrr 717 |
. . . . . . . . . . 11
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → (𝐹‘[𝑧] ∼ ) = (𝑧 ⊕ 𝐴)) |
| 43 | 1, 2, 3, 4 | orbstaval 19330 |
. . . . . . . . . . . 12
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑤 ∈ 𝑋) → (𝐹‘[𝑤] ∼ ) = (𝑤 ⊕ 𝐴)) |
| 44 | 43 | adantrl 716 |
. . . . . . . . . . 11
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → (𝐹‘[𝑤] ∼ ) = (𝑤 ⊕ 𝐴)) |
| 45 | 42, 44 | eqeq12d 2753 |
. . . . . . . . . 10
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → ((𝐹‘[𝑧] ∼ ) = (𝐹‘[𝑤] ∼ ) ↔ (𝑧 ⊕ 𝐴) = (𝑤 ⊕ 𝐴))) |
| 46 | 1, 2, 3 | gastacos 19328 |
. . . . . . . . . 10
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → (𝑧 ∼ 𝑤 ↔ (𝑧 ⊕ 𝐴) = (𝑤 ⊕ 𝐴))) |
| 47 | 27 | adantr 480 |
. . . . . . . . . . 11
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → ∼ Er 𝑋) |
| 48 | | simprl 771 |
. . . . . . . . . . 11
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → 𝑧 ∈ 𝑋) |
| 49 | 47, 48 | erth 8796 |
. . . . . . . . . 10
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → (𝑧 ∼ 𝑤 ↔ [𝑧] ∼ = [𝑤] ∼ )) |
| 50 | 45, 46, 49 | 3bitr2d 307 |
. . . . . . . . 9
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → ((𝐹‘[𝑧] ∼ ) = (𝐹‘[𝑤] ∼ ) ↔ [𝑧] ∼ = [𝑤] ∼ )) |
| 51 | 50 | biimpd 229 |
. . . . . . . 8
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → ((𝐹‘[𝑧] ∼ ) = (𝐹‘[𝑤] ∼ ) → [𝑧] ∼ = [𝑤] ∼ )) |
| 52 | 51 | anassrs 467 |
. . . . . . 7
⊢ ((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) ∧ 𝑤 ∈ 𝑋) → ((𝐹‘[𝑧] ∼ ) = (𝐹‘[𝑤] ∼ ) → [𝑧] ∼ = [𝑤] ∼ )) |
| 53 | 32, 40, 52 | ectocld 8824 |
. . . . . 6
⊢ ((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) ∧ 𝑏 ∈ (𝑋 / ∼ )) → ((𝐹‘[𝑧] ∼ ) = (𝐹‘𝑏) → [𝑧] ∼ = 𝑏)) |
| 54 | 53 | ralrimiva 3146 |
. . . . 5
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑧 ∈ 𝑋) → ∀𝑏 ∈ (𝑋 / ∼ )((𝐹‘[𝑧] ∼ ) = (𝐹‘𝑏) → [𝑧] ∼ = 𝑏)) |
| 55 | 32, 36, 54 | ectocld 8824 |
. . . 4
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑎 ∈ (𝑋 / ∼ )) →
∀𝑏 ∈ (𝑋 / ∼ )((𝐹‘𝑎) = (𝐹‘𝑏) → 𝑎 = 𝑏)) |
| 56 | 55 | ralrimiva 3146 |
. . 3
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → ∀𝑎 ∈ (𝑋 / ∼ )∀𝑏 ∈ (𝑋 / ∼ )((𝐹‘𝑎) = (𝐹‘𝑏) → 𝑎 = 𝑏)) |
| 57 | | dff13 7275 |
. . 3
⊢ (𝐹:(𝑋 / ∼ )–1-1→[𝐴]𝑂 ↔ (𝐹:(𝑋 / ∼ )⟶[𝐴]𝑂 ∧ ∀𝑎 ∈ (𝑋 / ∼ )∀𝑏 ∈ (𝑋 / ∼ )((𝐹‘𝑎) = (𝐹‘𝑏) → 𝑎 = 𝑏))) |
| 58 | 31, 56, 57 | sylanbrc 583 |
. 2
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → 𝐹:(𝑋 / ∼ )–1-1→[𝐴]𝑂) |
| 59 | | vex 3484 |
. . . . . . . . 9
⊢ ℎ ∈ V |
| 60 | | elecg 8789 |
. . . . . . . . 9
⊢ ((ℎ ∈ V ∧ 𝐴 ∈ 𝑌) → (ℎ ∈ [𝐴]𝑂 ↔ 𝐴𝑂ℎ)) |
| 61 | 59, 6, 60 | sylancr 587 |
. . . . . . . 8
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → (ℎ ∈ [𝐴]𝑂 ↔ 𝐴𝑂ℎ)) |
| 62 | 18 | gaorb 19325 |
. . . . . . . 8
⊢ (𝐴𝑂ℎ ↔ (𝐴 ∈ 𝑌 ∧ ℎ ∈ 𝑌 ∧ ∃𝑤 ∈ 𝑋 (𝑤 ⊕ 𝐴) = ℎ)) |
| 63 | 61, 62 | bitrdi 287 |
. . . . . . 7
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → (ℎ ∈ [𝐴]𝑂 ↔ (𝐴 ∈ 𝑌 ∧ ℎ ∈ 𝑌 ∧ ∃𝑤 ∈ 𝑋 (𝑤 ⊕ 𝐴) = ℎ))) |
| 64 | 63 | biimpa 476 |
. . . . . 6
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ ℎ ∈ [𝐴]𝑂) → (𝐴 ∈ 𝑌 ∧ ℎ ∈ 𝑌 ∧ ∃𝑤 ∈ 𝑋 (𝑤 ⊕ 𝐴) = ℎ)) |
| 65 | 64 | simp3d 1145 |
. . . . 5
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ ℎ ∈ [𝐴]𝑂) → ∃𝑤 ∈ 𝑋 (𝑤 ⊕ 𝐴) = ℎ) |
| 66 | 3 | ovexi 7465 |
. . . . . . . . . 10
⊢ ∼ ∈
V |
| 67 | 66 | ecelqsi 8813 |
. . . . . . . . 9
⊢ (𝑤 ∈ 𝑋 → [𝑤] ∼ ∈ (𝑋 / ∼ )) |
| 68 | 43 | eqcomd 2743 |
. . . . . . . . 9
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑤 ∈ 𝑋) → (𝑤 ⊕ 𝐴) = (𝐹‘[𝑤] ∼ )) |
| 69 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑧 = [𝑤] ∼ → (𝐹‘𝑧) = (𝐹‘[𝑤] ∼ )) |
| 70 | 69 | rspceeqv 3645 |
. . . . . . . . 9
⊢ (([𝑤] ∼ ∈ (𝑋 / ∼ ) ∧ (𝑤 ⊕ 𝐴) = (𝐹‘[𝑤] ∼ )) →
∃𝑧 ∈ (𝑋 / ∼ )(𝑤 ⊕ 𝐴) = (𝐹‘𝑧)) |
| 71 | 67, 68, 70 | syl2an2 686 |
. . . . . . . 8
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑤 ∈ 𝑋) → ∃𝑧 ∈ (𝑋 / ∼ )(𝑤 ⊕ 𝐴) = (𝐹‘𝑧)) |
| 72 | | eqeq1 2741 |
. . . . . . . . 9
⊢ ((𝑤 ⊕ 𝐴) = ℎ → ((𝑤 ⊕ 𝐴) = (𝐹‘𝑧) ↔ ℎ = (𝐹‘𝑧))) |
| 73 | 72 | rexbidv 3179 |
. . . . . . . 8
⊢ ((𝑤 ⊕ 𝐴) = ℎ → (∃𝑧 ∈ (𝑋 / ∼ )(𝑤 ⊕ 𝐴) = (𝐹‘𝑧) ↔ ∃𝑧 ∈ (𝑋 / ∼ )ℎ = (𝐹‘𝑧))) |
| 74 | 71, 73 | syl5ibcom 245 |
. . . . . . 7
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑤 ∈ 𝑋) → ((𝑤 ⊕ 𝐴) = ℎ → ∃𝑧 ∈ (𝑋 / ∼ )ℎ = (𝐹‘𝑧))) |
| 75 | 74 | rexlimdva 3155 |
. . . . . 6
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → (∃𝑤 ∈ 𝑋 (𝑤 ⊕ 𝐴) = ℎ → ∃𝑧 ∈ (𝑋 / ∼ )ℎ = (𝐹‘𝑧))) |
| 76 | 75 | imp 406 |
. . . . 5
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ ∃𝑤 ∈ 𝑋 (𝑤 ⊕ 𝐴) = ℎ) → ∃𝑧 ∈ (𝑋 / ∼ )ℎ = (𝐹‘𝑧)) |
| 77 | 65, 76 | syldan 591 |
. . . 4
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ ℎ ∈ [𝐴]𝑂) → ∃𝑧 ∈ (𝑋 / ∼ )ℎ = (𝐹‘𝑧)) |
| 78 | 77 | ralrimiva 3146 |
. . 3
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → ∀ℎ ∈ [ 𝐴]𝑂∃𝑧 ∈ (𝑋 / ∼ )ℎ = (𝐹‘𝑧)) |
| 79 | | dffo3 7122 |
. . 3
⊢ (𝐹:(𝑋 / ∼ )–onto→[𝐴]𝑂 ↔ (𝐹:(𝑋 / ∼ )⟶[𝐴]𝑂 ∧ ∀ℎ ∈ [ 𝐴]𝑂∃𝑧 ∈ (𝑋 / ∼ )ℎ = (𝐹‘𝑧))) |
| 80 | 31, 78, 79 | sylanbrc 583 |
. 2
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → 𝐹:(𝑋 / ∼ )–onto→[𝐴]𝑂) |
| 81 | | df-f1o 6568 |
. 2
⊢ (𝐹:(𝑋 / ∼ )–1-1-onto→[𝐴]𝑂 ↔ (𝐹:(𝑋 / ∼ )–1-1→[𝐴]𝑂 ∧ 𝐹:(𝑋 / ∼ )–onto→[𝐴]𝑂)) |
| 82 | 58, 80, 81 | sylanbrc 583 |
1
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → 𝐹:(𝑋 / ∼ )–1-1-onto→[𝐴]𝑂) |