This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑌 ∧ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ) }
Assertion gaorb ( 𝐴 ∼ 𝐵 ↔ ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌 ∧ ∃ ℎ ∈ 𝑋 ( ℎ ⊕ 𝐴 ) = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 gaorb.1 ⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑌 ∧ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ) }
2 oveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝑔 ⊕ 𝑥 ) = ( 𝑔 ⊕ 𝐴 ) )
3 eqeq12 ⊢ ( ( ( 𝑔 ⊕ 𝑥 ) = ( 𝑔 ⊕ 𝐴 ) ∧ 𝑦 = 𝐵 ) → ( ( 𝑔 ⊕ 𝑥 ) = 𝑦 ↔ ( 𝑔 ⊕ 𝐴 ) = 𝐵 ) )
4 2 3 sylan ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ( 𝑔 ⊕ 𝑥 ) = 𝑦 ↔ ( 𝑔 ⊕ 𝐴 ) = 𝐵 ) )
5 4 rexbidv ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ↔ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝐴 ) = 𝐵 ) )
6 oveq1 ⊢ ( 𝑔 = ℎ → ( 𝑔 ⊕ 𝐴 ) = ( ℎ ⊕ 𝐴 ) )
7 6 eqeq1d ⊢ ( 𝑔 = ℎ → ( ( 𝑔 ⊕ 𝐴 ) = 𝐵 ↔ ( ℎ ⊕ 𝐴 ) = 𝐵 ) )
8 7 cbvrexvw ⊢ ( ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝐴 ) = 𝐵 ↔ ∃ ℎ ∈ 𝑋 ( ℎ ⊕ 𝐴 ) = 𝐵 )
9 5 8 bitrdi ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ↔ ∃ ℎ ∈ 𝑋 ( ℎ ⊕ 𝐴 ) = 𝐵 ) )
10 vex ⊢ 𝑥 ∈ V
11 vex ⊢ 𝑦 ∈ V
12 10 11 prss ⊢ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ↔ { 𝑥 , 𝑦 } ⊆ 𝑌 )
13 12 anbi1i ⊢ ( ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ∧ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ) ↔ ( { 𝑥 , 𝑦 } ⊆ 𝑌 ∧ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ) )
14 13 opabbii ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ∧ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑌 ∧ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ) }
15 1 14 eqtr4i ⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ∧ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ) }
16 9 15 brab2a ⊢ ( 𝐴 ∼ 𝐵 ↔ ( ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌 ) ∧ ∃ ℎ ∈ 𝑋 ( ℎ ⊕ 𝐴 ) = 𝐵 ) )
17 df-3an ⊢ ( ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌 ∧ ∃ ℎ ∈ 𝑋 ( ℎ ⊕ 𝐴 ) = 𝐵 ) ↔ ( ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌 ) ∧ ∃ ℎ ∈ 𝑋 ( ℎ ⊕ 𝐴 ) = 𝐵 ) )
18 16 17 bitr4i ⊢ ( 𝐴 ∼ 𝐵 ↔ ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌 ∧ ∃ ℎ ∈ 𝑋 ( ℎ ⊕ 𝐴 ) = 𝐵 ) )