Theorem iso0

Description: The empty set is an R , S isomorphism from the empty set to the empty set. (Contributed by Steve Rodriguez, 24-Oct-2015)

	Ref	Expression
Assertion	iso0	$$⊢\varnothing {Isom}_{R,S}\left(\varnothing ,\varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		f1o0	$$⊢\varnothing :\varnothing \underset{1-1\; onto}{⟶}\varnothing$$
2		ral0	$$⊢\forall x\in \varnothing \forall y\in \varnothing \left(xRy\leftrightarrow \varnothing \left(x\right)S\varnothing \left(y\right)\right)$$
3		df-isom	$$⊢\varnothing {Isom}_{R,S}\left(\varnothing ,\varnothing \right)\leftrightarrow \left(\varnothing :\varnothing \underset{1-1\; onto}{⟶}\varnothing \wedge \forall x\in \varnothing \forall y\in \varnothing \left(xRy\leftrightarrow \varnothing \left(x\right)S\varnothing \left(y\right)\right)\right)$$
4	1 2 3	mpbir2an	$$⊢\varnothing {Isom}_{R,S}\left(\varnothing ,\varnothing \right)$$