Theorem isores2

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	isores2	⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ↔ 𝐻 Isom 𝑅 , ( 𝑆 ∩ ( 𝐵 × 𝐵 ) ) ( 𝐴 , 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		f1of	⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 → 𝐻 : 𝐴 ⟶ 𝐵 )
2		ffvelrn	⊢ ( ( 𝐻 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑥 ) ∈ 𝐵 )
3	2	adantrr	⊢ ( ( 𝐻 : 𝐴 ⟶ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝐻 ‘ 𝑥 ) ∈ 𝐵 )
4		ffvelrn	⊢ ( ( 𝐻 : 𝐴 ⟶ 𝐵 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑦 ) ∈ 𝐵 )
5	4	adantrl	⊢ ( ( 𝐻 : 𝐴 ⟶ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝐻 ‘ 𝑦 ) ∈ 𝐵 )
6		brinxp	⊢ ( ( ( 𝐻 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝐻 ‘ 𝑦 ) ∈ 𝐵 ) → ( ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ↔ ( 𝐻 ‘ 𝑥 ) ( 𝑆 ∩ ( 𝐵 × 𝐵 ) ) ( 𝐻 ‘ 𝑦 ) ) )
7	3 5 6	syl2anc	⊢ ( ( 𝐻 : 𝐴 ⟶ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ↔ ( 𝐻 ‘ 𝑥 ) ( 𝑆 ∩ ( 𝐵 × 𝐵 ) ) ( 𝐻 ‘ 𝑦 ) ) )
8	1 7	sylan	⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ↔ ( 𝐻 ‘ 𝑥 ) ( 𝑆 ∩ ( 𝐵 × 𝐵 ) ) ( 𝐻 ‘ 𝑦 ) ) )
9	8	anassrs	⊢ ( ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ↔ ( 𝐻 ‘ 𝑥 ) ( 𝑆 ∩ ( 𝐵 × 𝐵 ) ) ( 𝐻 ‘ 𝑦 ) ) )
10	9	bibi2d	⊢ ( ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ↔ ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) ( 𝑆 ∩ ( 𝐵 × 𝐵 ) ) ( 𝐻 ‘ 𝑦 ) ) ) )
11	10	ralbidva	⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) ( 𝑆 ∩ ( 𝐵 × 𝐵 ) ) ( 𝐻 ‘ 𝑦 ) ) ) )
12	11	ralbidva	⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) ( 𝑆 ∩ ( 𝐵 × 𝐵 ) ) ( 𝐻 ‘ 𝑦 ) ) ) )
13	12	pm5.32i	⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) ↔ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) ( 𝑆 ∩ ( 𝐵 × 𝐵 ) ) ( 𝐻 ‘ 𝑦 ) ) ) )
14		df-isom	⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ↔ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) )
15		df-isom	⊢ ( 𝐻 Isom 𝑅 , ( 𝑆 ∩ ( 𝐵 × 𝐵 ) ) ( 𝐴 , 𝐵 ) ↔ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) ( 𝑆 ∩ ( 𝐵 × 𝐵 ) ) ( 𝐻 ‘ 𝑦 ) ) ) )
16	13 14 15	3bitr4i	⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ↔ 𝐻 Isom 𝑅 , ( 𝑆 ∩ ( 𝐵 × 𝐵 ) ) ( 𝐴 , 𝐵 ) )