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 𝐵 ) )