This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isofr2

Description: A weak form of isofr that does not need Replacement. (Contributed by Mario Carneiro, 18-Nov-2014)

Ref Expression
Assertion isofr2 ⊢ H Isom R , S A B ∧ B ∈ V → S Fr B → R Fr A

Proof

Step Hyp Ref Expression
1 simpl ⊢ H Isom R , S A B ∧ B ∈ V → H Isom R , S A B
2 imassrn ⊢ H x ⊆ ran ⁡ H
3 isof1o ⊢ H Isom R , S A B → H : A ⟶ 1-1 onto B
4 f1of ⊢ H : A ⟶ 1-1 onto B → H : A ⟶ B
5 frn ⊢ H : A ⟶ B → ran ⁡ H ⊆ B
6 3 4 5 3syl ⊢ H Isom R , S A B → ran ⁡ H ⊆ B
7 2 6 sstrid ⊢ H Isom R , S A B → H x ⊆ B
8 ssexg ⊢ H x ⊆ B ∧ B ∈ V → H x ∈ V
9 7 8 sylan ⊢ H Isom R , S A B ∧ B ∈ V → H x ∈ V
10 1 9 isofrlem ⊢ H Isom R , S A B ∧ B ∈ V → S Fr B → R Fr A