Metamath Proof Explorer

Theorem isores1

Description: An isomorphism from one well-order to another can be restricted on either well-order. (Contributed by Mario Carneiro, 15-Jan-2013)

Ref Expression
Assertion isores1 ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ↔ 𝐻 Isom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) , 𝑆 ( 𝐴 , 𝐵 ) )

Proof

Step Hyp Ref Expression
1 isocnv ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ◡ 𝐻 Isom 𝑆 , 𝑅 ( 𝐵 , 𝐴 ) )
2 isores2 ⊢ ( ◡ 𝐻 Isom 𝑆 , 𝑅 ( 𝐵 , 𝐴 ) ↔ ◡ 𝐻 Isom 𝑆 , ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ( 𝐵 , 𝐴 ) )
3 1 2 sylib ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ◡ 𝐻 Isom 𝑆 , ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ( 𝐵 , 𝐴 ) )
4 isocnv ⊢ ( ◡ 𝐻 Isom 𝑆 , ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ( 𝐵 , 𝐴 ) → ◡ ◡ 𝐻 Isom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) , 𝑆 ( 𝐴 , 𝐵 ) )
5 3 4 syl ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ◡ ◡ 𝐻 Isom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) , 𝑆 ( 𝐴 , 𝐵 ) )
6 isof1o ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → 𝐻 : 𝐴 –1-1-onto→ 𝐵 )
7 f1orel ⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 → Rel 𝐻 )
8 dfrel2 ⊢ ( Rel 𝐻 ↔ ◡ ◡ 𝐻 = 𝐻 )
9 isoeq1 ⊢ ( ◡ ◡ 𝐻 = 𝐻 → ( ◡ ◡ 𝐻 Isom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) , 𝑆 ( 𝐴 , 𝐵 ) ↔ 𝐻 Isom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) , 𝑆 ( 𝐴 , 𝐵 ) ) )
10 8 9 sylbi ⊢ ( Rel 𝐻 → ( ◡ ◡ 𝐻 Isom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) , 𝑆 ( 𝐴 , 𝐵 ) ↔ 𝐻 Isom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) , 𝑆 ( 𝐴 , 𝐵 ) ) )
11 6 7 10 3syl ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ( ◡ ◡ 𝐻 Isom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) , 𝑆 ( 𝐴 , 𝐵 ) ↔ 𝐻 Isom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) , 𝑆 ( 𝐴 , 𝐵 ) ) )
12 5 11 mpbid ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → 𝐻 Isom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) , 𝑆 ( 𝐴 , 𝐵 ) )
13 isocnv ⊢ ( 𝐻 Isom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) , 𝑆 ( 𝐴 , 𝐵 ) → ◡ 𝐻 Isom 𝑆 , ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ( 𝐵 , 𝐴 ) )
14 13 2 sylibr ⊢ ( 𝐻 Isom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) , 𝑆 ( 𝐴 , 𝐵 ) → ◡ 𝐻 Isom 𝑆 , 𝑅 ( 𝐵 , 𝐴 ) )
15 isocnv ⊢ ( ◡ 𝐻 Isom 𝑆 , 𝑅 ( 𝐵 , 𝐴 ) → ◡ ◡ 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) )
16 14 15 syl ⊢ ( 𝐻 Isom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) , 𝑆 ( 𝐴 , 𝐵 ) → ◡ ◡ 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) )
17 isof1o ⊢ ( 𝐻 Isom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) , 𝑆 ( 𝐴 , 𝐵 ) → 𝐻 : 𝐴 –1-1-onto→ 𝐵 )
18 isoeq1 ⊢ ( ◡ ◡ 𝐻 = 𝐻 → ( ◡ ◡ 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ↔ 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ) )
19 8 18 sylbi ⊢ ( Rel 𝐻 → ( ◡ ◡ 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ↔ 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ) )
20 17 7 19 3syl ⊢ ( 𝐻 Isom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) , 𝑆 ( 𝐴 , 𝐵 ) → ( ◡ ◡ 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ↔ 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ) )
21 16 20 mpbid ⊢ ( 𝐻 Isom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) , 𝑆 ( 𝐴 , 𝐵 ) → 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) )
22 12 21 impbii ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ↔ 𝐻 Isom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) , 𝑆 ( 𝐴 , 𝐵 ) )