Theorem elbasov

Description: Utility theorem: reverse closure for any structure defined as a two-argument function. (Contributed by Mario Carneiro, 3-Oct-2015)

	Ref	Expression
Hypotheses	elbasov.o	|- Rel dom O
	elbasov.s	|- S = ( X O Y )
	elbasov.b	|- B = ( Base ` S )
Assertion	elbasov	|- ( A e. B -> ( X e. _V /\ Y e. _V ) )

Proof

Step	Hyp	Ref	Expression
1		elbasov.o	|- Rel dom O
2		elbasov.s	|- S = ( X O Y )
3		elbasov.b	|- B = ( Base ` S )
4		n0i	|- ( A e. B -> -. B = (/) )
5	1	ovprc	|- ( -. ( X e. _V /\ Y e. _V ) -> ( X O Y ) = (/) )
6	2 5	syl5eq	|- ( -. ( X e. _V /\ Y e. _V ) -> S = (/) )
7	6	fveq2d	|- ( -. ( X e. _V /\ Y e. _V ) -> ( Base ` S ) = ( Base ` (/) ) )
8		base0	|- (/) = ( Base ` (/) )
9	7 3 8	3eqtr4g	|- ( -. ( X e. _V /\ Y e. _V ) -> B = (/) )
10	4 9	nsyl2	|- ( A e. B -> ( X e. _V /\ Y e. _V ) )