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 ( 𝐴 𝐵 ↔ ( 𝐴𝑌𝐵𝑌 ∧ ∃ 𝑋 ( 𝐴 ) = 𝐵 ) )