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

Metamath Proof Explorer

Theorem isofr

Description: An isomorphism preserves well-foundedness. Proposition 6.32(1) of TakeutiZaring p. 33. (Contributed by NM, 30-Apr-2004) (Revised by Mario Carneiro, 18-Nov-2014)

Ref Expression
Assertion isofr ⊢ H Isom R , S A B → R Fr A ↔ S Fr B

Proof

Step Hyp Ref Expression
1 isocnv ⊢ H Isom R , S A B → H -1 Isom S , R B A
2 id ⊢ H -1 Isom S , R B A → H -1 Isom S , R B A
3 isof1o ⊢ H -1 Isom S , R B A → H -1 : B ⟶ 1-1 onto A
4 f1ofun ⊢ H -1 : B ⟶ 1-1 onto A → Fun ⁡ H -1
5 vex ⊢ x ∈ V
6 5 funimaex ⊢ Fun ⁡ H -1 → H -1 x ∈ V
7 3 4 6 3syl ⊢ H -1 Isom S , R B A → H -1 x ∈ V
8 2 7 isofrlem ⊢ H -1 Isom S , R B A → R Fr A → S Fr B
9 1 8 syl ⊢ H Isom R , S A B → R Fr A → S Fr B
10 id ⊢ H Isom R , S A B → H Isom R , S A B
11 isof1o ⊢ H Isom R , S A B → H : A ⟶ 1-1 onto B
12 f1ofun ⊢ H : A ⟶ 1-1 onto B → Fun ⁡ H
13 5 funimaex ⊢ Fun ⁡ H → H x ∈ V
14 11 12 13 3syl ⊢ H Isom R , S A B → H x ∈ V
15 10 14 isofrlem ⊢ H Isom R , S A B → S Fr B → R Fr A
16 9 15 impbid ⊢ H Isom R , S A B → R Fr A ↔ S Fr B