isoini

Description: Isomorphisms preserve initial segments. Proposition 6.31(2) of TakeutiZaring p. 33. (Contributed by NM, 20-Apr-2004)

		Ref	Expression
	Assertion	isoini	$⊢ (H {Isom}_{R, S} (A, B) \land D \in A) \to H [A \cap R^{-1} [\{D\}]] = B \cap S^{-1} [\{H (D)\}]$

Proof

Step	Hyp	Ref	Expression
1		elin	$⊢ y \in (B \cap S^{-1} [\{H (D)\}]) \leftrightarrow (y \in B \land y \in S^{-1} [\{H (D)\}])$
2		isof1o	$⊢ H {Isom}_{R, S} (A, B) \to H : A \underset{1-1 onto}{⟶} B$
3		f1ofo	$⊢ H : A \underset{1-1 onto}{⟶} B \to H : A \underset{onto}{⟶} B$
4		forn	$⊢ H : A \underset{onto}{⟶} B \to ran H = B$
5	4	eleq2d	$⊢ H : A \underset{onto}{⟶} B \to (y \in ran H \leftrightarrow y \in B)$
6	2 3 5	3syl	$⊢ H {Isom}_{R, S} (A, B) \to (y \in ran H \leftrightarrow y \in B)$
7		f1ofn	$⊢ H : A \underset{1-1 onto}{⟶} B \to H Fn A$
8		fvelrnb	$⊢ H Fn A \to (y \in ran H \leftrightarrow \exists x \in A H (x) = y)$
9	2 7 8	3syl	$⊢ H {Isom}_{R, S} (A, B) \to (y \in ran H \leftrightarrow \exists x \in A H (x) = y)$
10	6 9	bitr3d	$⊢ H {Isom}_{R, S} (A, B) \to (y \in B \leftrightarrow \exists x \in A H (x) = y)$
11		fvex	$⊢ H (D) \in V$
12		vex	$⊢ y \in V$
13	12	eliniseg	$⊢ H (D) \in V \to (y \in S^{-1} [\{H (D)\}] \leftrightarrow y S H (D))$
14	11 13	mp1i	$⊢ H {Isom}_{R, S} (A, B) \to (y \in S^{-1} [\{H (D)\}] \leftrightarrow y S H (D))$
15	10 14	anbi12d	$⊢ H {Isom}_{R, S} (A, B) \to ((y \in B \land y \in S^{-1} [\{H (D)\}]) \leftrightarrow (\exists x \in A H (x) = y \land y S H (D)))$
16	15	adantr	$⊢ (H {Isom}_{R, S} (A, B) \land D \in A) \to ((y \in B \land y \in S^{-1} [\{H (D)\}]) \leftrightarrow (\exists x \in A H (x) = y \land y S H (D)))$
17		elin	$⊢ x \in (A \cap R^{-1} [\{D\}]) \leftrightarrow (x \in A \land x \in R^{-1} [\{D\}])$
18		vex	$⊢ x \in V$
19	18	eliniseg	$⊢ D \in A \to (x \in R^{-1} [\{D\}] \leftrightarrow x R D)$
20	19	anbi2d	$⊢ D \in A \to ((x \in A \land x \in R^{-1} [\{D\}]) \leftrightarrow (x \in A \land x R D))$
21	17 20	syl5bb	$⊢ D \in A \to (x \in (A \cap R^{-1} [\{D\}]) \leftrightarrow (x \in A \land x R D))$
22	21	anbi1d	$⊢ D \in A \to ((x \in (A \cap R^{-1} [\{D\}]) \land x H y) \leftrightarrow ((x \in A \land x R D) \land x H y))$
23		anass	$⊢ ((x \in A \land x R D) \land x H y) \leftrightarrow (x \in A \land (x R D \land x H y))$
24	22 23	syl6bb	$⊢ D \in A \to ((x \in (A \cap R^{-1} [\{D\}]) \land x H y) \leftrightarrow (x \in A \land (x R D \land x H y)))$
25	24	adantl	$⊢ (H {Isom}_{R, S} (A, B) \land D \in A) \to ((x \in (A \cap R^{-1} [\{D\}]) \land x H y) \leftrightarrow (x \in A \land (x R D \land x H y)))$
26		isorel	$⊢ (H {Isom}_{R, S} (A, B) \land (x \in A \land D \in A)) \to (x R D \leftrightarrow H (x) S H (D))$
27	2 7	syl	$⊢ H {Isom}_{R, S} (A, B) \to H Fn A$
28		fnbrfvb	$⊢ (H Fn A \land x \in A) \to (H (x) = y \leftrightarrow x H y)$
29	28	bicomd	$⊢ (H Fn A \land x \in A) \to (x H y \leftrightarrow H (x) = y)$
30	27 29	sylan	$⊢ (H {Isom}_{R, S} (A, B) \land x \in A) \to (x H y \leftrightarrow H (x) = y)$
31	30	adantrr	$⊢ (H {Isom}_{R, S} (A, B) \land (x \in A \land D \in A)) \to (x H y \leftrightarrow H (x) = y)$
32	26 31	anbi12d	$⊢ (H {Isom}_{R, S} (A, B) \land (x \in A \land D \in A)) \to ((x R D \land x H y) \leftrightarrow (H (x) S H (D) \land H (x) = y))$
33		ancom	$⊢ (H (x) S H (D) \land H (x) = y) \leftrightarrow (H (x) = y \land H (x) S H (D))$
34		breq1	$⊢ H (x) = y \to (H (x) S H (D) \leftrightarrow y S H (D))$
35	34	pm5.32i	$⊢ (H (x) = y \land H (x) S H (D)) \leftrightarrow (H (x) = y \land y S H (D))$
36	33 35	bitri	$⊢ (H (x) S H (D) \land H (x) = y) \leftrightarrow (H (x) = y \land y S H (D))$
37	32 36	syl6bb	$⊢ (H {Isom}_{R, S} (A, B) \land (x \in A \land D \in A)) \to ((x R D \land x H y) \leftrightarrow (H (x) = y \land y S H (D)))$
38	37	exp32	$⊢ H {Isom}_{R, S} (A, B) \to (x \in A \to (D \in A \to ((x R D \land x H y) \leftrightarrow (H (x) = y \land y S H (D)))))$
39	38	com23	$⊢ H {Isom}_{R, S} (A, B) \to (D \in A \to (x \in A \to ((x R D \land x H y) \leftrightarrow (H (x) = y \land y S H (D)))))$
40	39	imp	$⊢ (H {Isom}_{R, S} (A, B) \land D \in A) \to (x \in A \to ((x R D \land x H y) \leftrightarrow (H (x) = y \land y S H (D))))$
41	40	pm5.32d	$⊢ (H {Isom}_{R, S} (A, B) \land D \in A) \to ((x \in A \land (x R D \land x H y)) \leftrightarrow (x \in A \land (H (x) = y \land y S H (D))))$
42	25 41	bitrd	$⊢ (H {Isom}_{R, S} (A, B) \land D \in A) \to ((x \in (A \cap R^{-1} [\{D\}]) \land x H y) \leftrightarrow (x \in A \land (H (x) = y \land y S H (D))))$
43	42	rexbidv2	$⊢ (H {Isom}_{R, S} (A, B) \land D \in A) \to (\exists x \in (A \cap R^{-1} [\{D\}]) x H y \leftrightarrow \exists x \in A (H (x) = y \land y S H (D)))$
44		r19.41v	$⊢ \exists x \in A (H (x) = y \land y S H (D)) \leftrightarrow (\exists x \in A H (x) = y \land y S H (D))$
45	43 44	syl6bb	$⊢ (H {Isom}_{R, S} (A, B) \land D \in A) \to (\exists x \in (A \cap R^{-1} [\{D\}]) x H y \leftrightarrow (\exists x \in A H (x) = y \land y S H (D)))$
46	16 45	bitr4d	$⊢ (H {Isom}_{R, S} (A, B) \land D \in A) \to ((y \in B \land y \in S^{-1} [\{H (D)\}]) \leftrightarrow \exists x \in (A \cap R^{-1} [\{D\}]) x H y)$
47	1 46	syl5bb	$⊢ (H {Isom}_{R, S} (A, B) \land D \in A) \to (y \in (B \cap S^{-1} [\{H (D)\}]) \leftrightarrow \exists x \in (A \cap R^{-1} [\{D\}]) x H y)$
48	47	abbi2dv	$⊢ (H {Isom}_{R, S} (A, B) \land D \in A) \to B \cap S^{-1} [\{H (D)\}] = \{y \| \exists x \in (A \cap R^{-1} [\{D\}]) x H y\}$
49		dfima2	$⊢ H [A \cap R^{-1} [\{D\}]] = \{y \| \exists x \in (A \cap R^{-1} [\{D\}]) x H y\}$
50	48 49	syl6reqr	$⊢ (H {Isom}_{R, S} (A, B) \land D \in A) \to H [A \cap R^{-1} [\{D\}]] = B \cap S^{-1} [\{H (D)\}]$

Metamath Proof Explorer

Theorem isoini

Proof