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 } C_ Y /\ E. g e. X ( g .(+) x ) = y ) }
Assertion	gaorb	|- ( A .~ B <-> ( A e. Y /\ B e. Y /\ E. h e. X ( h .(+) A ) = B ) )

Proof

Step	Hyp	Ref	Expression
1		gaorb.1	|- .~ = { <. x , y >. | ( { x , y } C_ Y /\ E. g e. 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 ) -> ( E. g e. X ( g .(+) x ) = y <-> E. g e. 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	|- ( E. g e. X ( g .(+) A ) = B <-> E. h e. X ( h .(+) A ) = B )
9	5 8	bitrdi	|- ( ( x = A /\ y = B ) -> ( E. g e. X ( g .(+) x ) = y <-> E. h e. X ( h .(+) A ) = B ) )
10		vex	|- x e. _V
11		vex	|- y e. _V
12	10 11	prss	|- ( ( x e. Y /\ y e. Y ) <-> { x , y } C_ Y )
13	12	anbi1i	|- ( ( ( x e. Y /\ y e. Y ) /\ E. g e. X ( g .(+) x ) = y ) <-> ( { x , y } C_ Y /\ E. g e. X ( g .(+) x ) = y ) )
14	13	opabbii	|- { <. x , y >. | ( ( x e. Y /\ y e. Y ) /\ E. g e. X ( g .(+) x ) = y ) } = { <. x , y >. | ( { x , y } C_ Y /\ E. g e. X ( g .(+) x ) = y ) }
15	1 14	eqtr4i	|- .~ = { <. x , y >. | ( ( x e. Y /\ y e. Y ) /\ E. g e. X ( g .(+) x ) = y ) }
16	9 15	brab2a	|- ( A .~ B <-> ( ( A e. Y /\ B e. Y ) /\ E. h e. X ( h .(+) A ) = B ) )
17		df-3an	|- ( ( A e. Y /\ B e. Y /\ E. h e. X ( h .(+) A ) = B ) <-> ( ( A e. Y /\ B e. Y ) /\ E. h e. X ( h .(+) A ) = B ) )
18	16 17	bitr4i	|- ( A .~ B <-> ( A e. Y /\ B e. Y /\ E. h e. X ( h .(+) A ) = B ) )