Metamath Proof Explorer

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	$⊢ H {Isom}_{R, S} (A, B) \leftrightarrow H {Isom}_{R, S \cap (B \times B)} (A, B)$

Proof

Step	Hyp	Ref	Expression
1		f1of	$⊢ H : A \underset{1-1 onto}{⟶} B \to H : A ⟶ B$
2		ffvelcdm	$⊢ (H : A ⟶ B \land x \in A) \to H (x) \in B$
3	2	adantrr	$⊢ (H : A ⟶ B \land (x \in A \land y \in A)) \to H (x) \in B$
4		ffvelcdm	$⊢ (H : A ⟶ B \land y \in A) \to H (y) \in B$
5	4	adantrl	$⊢ (H : A ⟶ B \land (x \in A \land y \in A)) \to H (y) \in B$
6		brinxp	$⊢ (H (x) \in B \land H (y) \in B) \to (H (x) S H (y) \leftrightarrow H (x) (S \cap (B \times B)) H (y))$
7	3 5 6	syl2anc	$⊢ (H : A ⟶ B \land (x \in A \land y \in A)) \to (H (x) S H (y) \leftrightarrow H (x) (S \cap (B \times B)) H (y))$
8	1 7	sylan	$⊢ (H : A \underset{1-1 onto}{⟶} B \land (x \in A \land y \in A)) \to (H (x) S H (y) \leftrightarrow H (x) (S \cap (B \times B)) H (y))$
9	8	anassrs	$⊢ ((H : A \underset{1-1 onto}{⟶} B \land x \in A) \land y \in A) \to (H (x) S H (y) \leftrightarrow H (x) (S \cap (B \times B)) H (y))$
10	9	bibi2d	$⊢ ((H : A \underset{1-1 onto}{⟶} B \land x \in A) \land y \in A) \to ((x R y \leftrightarrow H (x) S H (y)) \leftrightarrow (x R y \leftrightarrow H (x) (S \cap (B \times B)) H (y)))$
11	10	ralbidva	$⊢ (H : A \underset{1-1 onto}{⟶} B \land x \in A) \to (\forall y \in A (x R y \leftrightarrow H (x) S H (y)) \leftrightarrow \forall y \in A (x R y \leftrightarrow H (x) (S \cap (B \times B)) H (y)))$
12	11	ralbidva	$⊢ H : A \underset{1-1 onto}{⟶} B \to (\forall x \in A \forall y \in A (x R y \leftrightarrow H (x) S H (y)) \leftrightarrow \forall x \in A \forall y \in A (x R y \leftrightarrow H (x) (S \cap (B \times B)) H (y)))$
13	12	pm5.32i	$⊢ (H : A \underset{1-1 onto}{⟶} B \land \forall x \in A \forall y \in A (x R y \leftrightarrow H (x) S H (y))) \leftrightarrow (H : A \underset{1-1 onto}{⟶} B \land \forall x \in A \forall y \in A (x R y \leftrightarrow H (x) (S \cap (B \times B)) H (y)))$
14		df-isom	$⊢ H {Isom}_{R, S} (A, B) \leftrightarrow (H : A \underset{1-1 onto}{⟶} B \land \forall x \in A \forall y \in A (x R y \leftrightarrow H (x) S H (y)))$
15		df-isom	$⊢ H {Isom}_{R, S \cap (B \times B)} (A, B) \leftrightarrow (H : A \underset{1-1 onto}{⟶} B \land \forall x \in A \forall y \in A (x R y \leftrightarrow H (x) (S \cap (B \times B)) H (y)))$
16	13 14 15	3bitr4i	$⊢ H {Isom}_{R, S} (A, B) \leftrightarrow H {Isom}_{R, S \cap (B \times B)} (A, B)$