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 ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ( 𝑅 Fr 𝐴 ↔ 𝑆 Fr 𝐵 ) )

Proof

Step Hyp Ref Expression
1 isocnv ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ◡ 𝐻 Isom 𝑆 , 𝑅 ( 𝐵 , 𝐴 ) )
2 id ⊢ ( ◡ 𝐻 Isom 𝑆 , 𝑅 ( 𝐵 , 𝐴 ) → ◡ 𝐻 Isom 𝑆 , 𝑅 ( 𝐵 , 𝐴 ) )
3 isof1o ⊢ ( ◡ 𝐻 Isom 𝑆 , 𝑅 ( 𝐵 , 𝐴 ) → ◡ 𝐻 : 𝐵 –1-1-onto→ 𝐴 )
4 f1ofun ⊢ ( ◡ 𝐻 : 𝐵 –1-1-onto→ 𝐴 → Fun ◡ 𝐻 )
5 vex ⊢ 𝑥 ∈ V
6 5 funimaex ⊢ ( Fun ◡ 𝐻 → ( ◡ 𝐻 “ 𝑥 ) ∈ V )
7 3 4 6 3syl ⊢ ( ◡ 𝐻 Isom 𝑆 , 𝑅 ( 𝐵 , 𝐴 ) → ( ◡ 𝐻 “ 𝑥 ) ∈ V )
8 2 7 isofrlem ⊢ ( ◡ 𝐻 Isom 𝑆 , 𝑅 ( 𝐵 , 𝐴 ) → ( 𝑅 Fr 𝐴 → 𝑆 Fr 𝐵 ) )
9 1 8 syl ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ( 𝑅 Fr 𝐴 → 𝑆 Fr 𝐵 ) )
10 id ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) )
11 isof1o ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → 𝐻 : 𝐴 –1-1-onto→ 𝐵 )
12 f1ofun ⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 → Fun 𝐻 )
13 5 funimaex ⊢ ( Fun 𝐻 → ( 𝐻 “ 𝑥 ) ∈ V )
14 11 12 13 3syl ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ( 𝐻 “ 𝑥 ) ∈ V )
15 10 14 isofrlem ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ( 𝑆 Fr 𝐵 → 𝑅 Fr 𝐴 ) )
16 9 15 impbid ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ( 𝑅 Fr 𝐴 ↔ 𝑆 Fr 𝐵 ) )