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 𝑂
	elbasov.s	⊢ 𝑆 = ( 𝑋 𝑂 𝑌 )
	elbasov.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
Assertion	elbasov	⊢ ( 𝐴 ∈ 𝐵 → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) )

Proof

Step	Hyp	Ref	Expression
1		elbasov.o	⊢ Rel dom 𝑂
2		elbasov.s	⊢ 𝑆 = ( 𝑋 𝑂 𝑌 )
3		elbasov.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
4		n0i	⊢ ( 𝐴 ∈ 𝐵 → ¬ 𝐵 = ∅ )
5	1	ovprc	⊢ ( ¬ ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ( 𝑋 𝑂 𝑌 ) = ∅ )
6	2 5	syl5eq	⊢ ( ¬ ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → 𝑆 = ∅ )
7	6	fveq2d	⊢ ( ¬ ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ( Base ‘ 𝑆 ) = ( Base ‘ ∅ ) )
8		base0	⊢ ∅ = ( Base ‘ ∅ )
9	7 3 8	3eqtr4g	⊢ ( ¬ ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → 𝐵 = ∅ )
10	4 9	nsyl2	⊢ ( 𝐴 ∈ 𝐵 → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) )