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	\|- .~ = { <. 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 ) )