Metamath Proof Explorer

Theorem gaorb

Description: The orbit equivalence relation puts two points in the group action in the same equivalence class iff there is a group element that takes one element to the other. (Contributed by Mario Carneiro, 14-Jan-2015)

Ref Expression
Hypothesis gaorb.1 ⊢∼˙=xy|xy⊆Y∧∃g∈Xg⊕˙x=y
Assertion gaorb ⊢A∼˙B↔A∈Y∧B∈Y∧∃h∈Xh⊕˙A=B

Proof

Step Hyp Ref Expression
1 gaorb.1 ⊢∼˙=xy|xy⊆Y∧∃g∈Xg⊕˙x=y
2 oveq2 ⊢x=A→g⊕˙x=g⊕˙A
3 eqeq12 ⊢g⊕˙x=g⊕˙A∧y=B→g⊕˙x=y↔g⊕˙A=B
4 2 3 sylan ⊢x=A∧y=B→g⊕˙x=y↔g⊕˙A=B
5 4 rexbidv ⊢x=A∧y=B→∃g∈Xg⊕˙x=y↔∃g∈Xg⊕˙A=B
6 oveq1 ⊢g=h→g⊕˙A=h⊕˙A
7 6 eqeq1d ⊢g=h→g⊕˙A=B↔h⊕˙A=B
8 7 cbvrexvw ⊢∃g∈Xg⊕˙A=B↔∃h∈Xh⊕˙A=B
9 5 8 bitrdi ⊢x=A∧y=B→∃g∈Xg⊕˙x=y↔∃h∈Xh⊕˙A=B
10 vex ⊢x∈V
11 vex ⊢y∈V
12 10 11 prss ⊢x∈Y∧y∈Y↔xy⊆Y
13 12 anbi1i ⊢x∈Y∧y∈Y∧∃g∈Xg⊕˙x=y↔xy⊆Y∧∃g∈Xg⊕˙x=y
14 13 opabbii ⊢xy|x∈Y∧y∈Y∧∃g∈Xg⊕˙x=y=xy|xy⊆Y∧∃g∈Xg⊕˙x=y
15 1 14 eqtr4i ⊢∼˙=xy|x∈Y∧y∈Y∧∃g∈Xg⊕˙x=y
16 9 15 brab2a ⊢A∼˙B↔A∈Y∧B∈Y∧∃h∈Xh⊕˙A=B
17 df-3an ⊢A∈Y∧B∈Y∧∃h∈Xh⊕˙A=B↔A∈Y∧B∈Y∧∃h∈Xh⊕˙A=B
18 16 17 bitr4i ⊢A∼˙B↔A∈Y∧B∈Y∧∃h∈Xh⊕˙A=B