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	⊢ ( 𝐴 ∼ 𝐵 ↔ ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌 ∧ ∃ ℎ ∈ 𝑋 ( ℎ ⊕ 𝐴 ) = 𝐵 ) )