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 𝑅 , 𝑆 ( ∅ , ∅ )

Proof

Step	Hyp	Ref	Expression
1		f1o0	⊢ ∅ : ∅ –1-1-onto→ ∅
2		ral0	⊢ ∀ 𝑥 ∈ ∅ ∀ 𝑦 ∈ ∅ ( 𝑥 𝑅 𝑦 ↔ ( ∅ ‘ 𝑥 ) 𝑆 ( ∅ ‘ 𝑦 ) )
3		df-isom	⊢ ( ∅ Isom 𝑅 , 𝑆 ( ∅ , ∅ ) ↔ ( ∅ : ∅ –1-1-onto→ ∅ ∧ ∀ 𝑥 ∈ ∅ ∀ 𝑦 ∈ ∅ ( 𝑥 𝑅 𝑦 ↔ ( ∅ ‘ 𝑥 ) 𝑆 ( ∅ ‘ 𝑦 ) ) ) )
4	1 2 3	mpbir2an	⊢ ∅ Isom 𝑅 , 𝑆 ( ∅ , ∅ )