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	|- (/) Isom R , S ( (/) , (/) )

Proof

Step	Hyp	Ref	Expression
1		f1o0	|- (/) : (/) -1-1-onto-> (/)
2		ral0	|- A. x e. (/) A. y e. (/) ( x R y <-> ( (/) ` x ) S ( (/) ` y ) )
3		df-isom	|- ( (/) Isom R , S ( (/) , (/) ) <-> ( (/) : (/) -1-1-onto-> (/) /\ A. x e. (/) A. y e. (/) ( x R y <-> ( (/) ` x ) S ( (/) ` y ) ) ) )
4	1 2 3	mpbir2an	|- (/) Isom R , S ( (/) , (/) )