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 ⊢ ∼ ˙ = x y | x y ⊆ Y ∧ ∃ g ∈ X g ⊕ ˙ x = y
Assertion gaorb ⊢ A ∼ ˙ B ↔ A ∈ Y ∧ B ∈ Y ∧ ∃ h ∈ X h ⊕ ˙ A = B

Proof

Step Hyp Ref Expression
1 gaorb.1 ⊢ ∼ ˙ = x y | x y ⊆ Y ∧ ∃ g ∈ X g ⊕ ˙ 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 ∈ X g ⊕ ˙ x = y ↔ ∃ g ∈ X g ⊕ ˙ 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 ∈ X g ⊕ ˙ A = B ↔ ∃ h ∈ X h ⊕ ˙ A = B
9 5 8 bitrdi ⊢ x = A ∧ y = B → ∃ g ∈ X g ⊕ ˙ x = y ↔ ∃ h ∈ X h ⊕ ˙ A = B
10 vex ⊢ x ∈ V
11 vex ⊢ y ∈ V
12 10 11 prss ⊢ x ∈ Y ∧ y ∈ Y ↔ x y ⊆ Y
13 12 anbi1i ⊢ x ∈ Y ∧ y ∈ Y ∧ ∃ g ∈ X g ⊕ ˙ x = y ↔ x y ⊆ Y ∧ ∃ g ∈ X g ⊕ ˙ x = y
14 13 opabbii ⊢ x y | x ∈ Y ∧ y ∈ Y ∧ ∃ g ∈ X g ⊕ ˙ x = y = x y | x y ⊆ Y ∧ ∃ g ∈ X g ⊕ ˙ x = y
15 1 14 eqtr4i ⊢ ∼ ˙ = x y | x ∈ Y ∧ y ∈ Y ∧ ∃ g ∈ X g ⊕ ˙ x = y
16 9 15 brab2a ⊢ A ∼ ˙ B ↔ A ∈ Y ∧ B ∈ Y ∧ ∃ h ∈ X h ⊕ ˙ A = B
17 df-3an ⊢ A ∈ Y ∧ B ∈ Y ∧ ∃ h ∈ X h ⊕ ˙ A = B ↔ A ∈ Y ∧ B ∈ Y ∧ ∃ h ∈ X h ⊕ ˙ A = B
18 16 17 bitr4i ⊢ A ∼ ˙ B ↔ A ∈ Y ∧ B ∈ Y ∧ ∃ h ∈ X h ⊕ ˙ A = B