isoini2

Description: Isomorphisms are isomorphisms on their initial segments. (Contributed by Mario Carneiro, 29-Mar-2014)

	Ref	Expression
Hypotheses	isoini2.1	$⊢ C = A \cap R^{-1} [\{X\}]$
	isoini2.2	$⊢ D = B \cap S^{-1} [\{H (X)\}]$
Assertion	isoini2	$⊢ (H {Isom}_{R, S} (A, B) \land X \in A) \to ({H ↾}_{C}) {Isom}_{R, S} (C, D)$

Proof

Step	Hyp	Ref	Expression
1		isoini2.1	$⊢ C = A \cap R^{-1} [\{X\}]$
2		isoini2.2	$⊢ D = B \cap S^{-1} [\{H (X)\}]$
3		isof1o	$⊢ H {Isom}_{R, S} (A, B) \to H : A \underset{1-1 onto}{⟶} B$
4		f1of1	$⊢ H : A \underset{1-1 onto}{⟶} B \to H : A \underset{1-1}{⟶} B$
5	3 4	syl	$⊢ H {Isom}_{R, S} (A, B) \to H : A \underset{1-1}{⟶} B$
6	5	adantr	$⊢ (H {Isom}_{R, S} (A, B) \land X \in A) \to H : A \underset{1-1}{⟶} B$
7		inss1	$⊢ A \cap R^{-1} [\{X\}] \subseteq A$
8	1 7	eqsstri	$⊢ C \subseteq A$
9		f1ores	$⊢ (H : A \underset{1-1}{⟶} B \land C \subseteq A) \to ({H ↾}_{C}) : C \underset{1-1 onto}{⟶} H [C]$
10	6 8 9	sylancl	$⊢ (H {Isom}_{R, S} (A, B) \land X \in A) \to ({H ↾}_{C}) : C \underset{1-1 onto}{⟶} H [C]$
11		isoini	$⊢ (H {Isom}_{R, S} (A, B) \land X \in A) \to H [A \cap R^{-1} [\{X\}]] = B \cap S^{-1} [\{H (X)\}]$
12	1	imaeq2i	$⊢ H [C] = H [A \cap R^{-1} [\{X\}]]$
13	11 12 2	3eqtr4g	$⊢ (H {Isom}_{R, S} (A, B) \land X \in A) \to H [C] = D$
14	13	f1oeq3d	$⊢ (H {Isom}_{R, S} (A, B) \land X \in A) \to (({H ↾}_{C}) : C \underset{1-1 onto}{⟶} H [C] \leftrightarrow ({H ↾}_{C}) : C \underset{1-1 onto}{⟶} D)$
15	10 14	mpbid	$⊢ (H {Isom}_{R, S} (A, B) \land X \in A) \to ({H ↾}_{C}) : C \underset{1-1 onto}{⟶} D$
16		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)))$
17	16	simprbi	$⊢ H {Isom}_{R, S} (A, B) \to \forall x \in A \forall y \in A (x R y \leftrightarrow H (x) S H (y))$
18	17	adantr	$⊢ (H {Isom}_{R, S} (A, B) \land X \in A) \to \forall x \in A \forall y \in A (x R y \leftrightarrow H (x) S H (y))$
19		ssralv	$⊢ C \subseteq A \to (\forall y \in A (x R y \leftrightarrow H (x) S H (y)) \to \forall y \in C (x R y \leftrightarrow H (x) S H (y)))$
20	19	ralimdv	$⊢ C \subseteq A \to (\forall x \in A \forall y \in A (x R y \leftrightarrow H (x) S H (y)) \to \forall x \in A \forall y \in C (x R y \leftrightarrow H (x) S H (y)))$
21	8 18 20	mpsyl	$⊢ (H {Isom}_{R, S} (A, B) \land X \in A) \to \forall x \in A \forall y \in C (x R y \leftrightarrow H (x) S H (y))$
22		ssralv	$⊢ C \subseteq A \to (\forall x \in A \forall y \in C (x R y \leftrightarrow H (x) S H (y)) \to \forall x \in C \forall y \in C (x R y \leftrightarrow H (x) S H (y)))$
23	8 21 22	mpsyl	$⊢ (H {Isom}_{R, S} (A, B) \land X \in A) \to \forall x \in C \forall y \in C (x R y \leftrightarrow H (x) S H (y))$
24		fvres	$⊢ x \in C \to ({H ↾}_{C}) (x) = H (x)$
25		fvres	$⊢ y \in C \to ({H ↾}_{C}) (y) = H (y)$
26	24 25	breqan12d	$⊢ (x \in C \land y \in C) \to (({H ↾}_{C}) (x) S ({H ↾}_{C}) (y) \leftrightarrow H (x) S H (y))$
27	26	bibi2d	$⊢ (x \in C \land y \in C) \to ((x R y \leftrightarrow ({H ↾}_{C}) (x) S ({H ↾}_{C}) (y)) \leftrightarrow (x R y \leftrightarrow H (x) S H (y)))$
28	27	ralbidva	$⊢ x \in C \to (\forall y \in C (x R y \leftrightarrow ({H ↾}_{C}) (x) S ({H ↾}_{C}) (y)) \leftrightarrow \forall y \in C (x R y \leftrightarrow H (x) S H (y)))$
29	28	ralbiia	$⊢ \forall x \in C \forall y \in C (x R y \leftrightarrow ({H ↾}_{C}) (x) S ({H ↾}_{C}) (y)) \leftrightarrow \forall x \in C \forall y \in C (x R y \leftrightarrow H (x) S H (y))$
30	23 29	sylibr	$⊢ (H {Isom}_{R, S} (A, B) \land X \in A) \to \forall x \in C \forall y \in C (x R y \leftrightarrow ({H ↾}_{C}) (x) S ({H ↾}_{C}) (y))$
31		df-isom	$⊢ ({H ↾}_{C}) {Isom}_{R, S} (C, D) \leftrightarrow (({H ↾}_{C}) : C \underset{1-1 onto}{⟶} D \land \forall x \in C \forall y \in C (x R y \leftrightarrow ({H ↾}_{C}) (x) S ({H ↾}_{C}) (y)))$
32	15 30 31	sylanbrc	$⊢ (H {Isom}_{R, S} (A, B) \land X \in A) \to ({H ↾}_{C}) {Isom}_{R, S} (C, D)$

Metamath Proof Explorer

Theorem isoini2

Proof