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		dfima2	$⊢ H [A \cap R^{-1} [\{D\}]] = \{y \| \exists x \in (A \cap R^{-1} [\{D\}]) x H y\}$
2		elin	$⊢ y \in (B \cap S^{-1} [\{H (D)\}]) \leftrightarrow (y \in B \land y \in S^{-1} [\{H (D)\}])$
3		isof1o	$⊢ H {Isom}_{R, S} (A, B) \to H : A \underset{1-1 onto}{⟶} B$
4		f1ofo	$⊢ H : A \underset{1-1 onto}{⟶} B \to H : A \underset{onto}{⟶} B$
5		forn	$⊢ H : A \underset{onto}{⟶} B \to ran H = B$
6	5	eleq2d	$⊢ H : A \underset{onto}{⟶} B \to (y \in ran H \leftrightarrow y \in B)$
7	3 4 6	3syl	$⊢ H {Isom}_{R, S} (A, B) \to (y \in ran H \leftrightarrow y \in B)$
8		f1ofn	$⊢ H : A \underset{1-1 onto}{⟶} B \to H Fn A$
9		fvelrnb	$⊢ H Fn A \to (y \in ran H \leftrightarrow \exists x \in A H (x) = y)$
10	3 8 9	3syl	$⊢ H {Isom}_{R, S} (A, B) \to (y \in ran H \leftrightarrow \exists x \in A H (x) = y)$
11	7 10	bitr3d	$⊢ H {Isom}_{R, S} (A, B) \to (y \in B \leftrightarrow \exists x \in A H (x) = y)$
12		fvex	$⊢ H (D) \in V$
13		vex	$⊢ y \in V$
14	13	eliniseg	$⊢ H (D) \in V \to (y \in S^{-1} [\{H (D)\}] \leftrightarrow y S H (D))$
15	12 14	mp1i	$⊢ H {Isom}_{R, S} (A, B) \to (y \in S^{-1} [\{H (D)\}] \leftrightarrow y S H (D))$
16	11 15	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)))$
17	16	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)))$
18		elin	$⊢ x \in (A \cap R^{-1} [\{D\}]) \leftrightarrow (x \in A \land x \in R^{-1} [\{D\}])$
19		vex	$⊢ x \in V$
20	19	eliniseg	$⊢ D \in A \to (x \in R^{-1} [\{D\}] \leftrightarrow x R D)$
21	20	anbi2d	$⊢ D \in A \to ((x \in A \land x \in R^{-1} [\{D\}]) \leftrightarrow (x \in A \land x R D))$
22	18 21	bitrid	$⊢ D \in A \to (x \in (A \cap R^{-1} [\{D\}]) \leftrightarrow (x \in A \land x R D))$
23	22	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))$
24		anass	$⊢ ((x \in A \land x R D) \land x H y) \leftrightarrow (x \in A \land (x R D \land x H y))$
25	23 24	bitrdi	$⊢ 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	25	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)))$
27		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))$
28	3 8	syl	$⊢ H {Isom}_{R, S} (A, B) \to H Fn A$
29		fnbrfvb	$⊢ (H Fn A \land x \in A) \to (H (x) = y \leftrightarrow x H y)$
30	29	bicomd	$⊢ (H Fn A \land x \in A) \to (x H y \leftrightarrow H (x) = y)$
31	28 30	sylan	$⊢ (H {Isom}_{R, S} (A, B) \land x \in A) \to (x H y \leftrightarrow H (x) = y)$
32	31	adantrr	$⊢ (H {Isom}_{R, S} (A, B) \land (x \in A \land D \in A)) \to (x H y \leftrightarrow H (x) = y)$
33	27 32	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))$
34		ancom	$⊢ (H (x) S H (D) \land H (x) = y) \leftrightarrow (H (x) = y \land H (x) S H (D))$
35		breq1	$⊢ H (x) = y \to (H (x) S H (D) \leftrightarrow y S H (D))$
36	35	pm5.32i	$⊢ (H (x) = y \land H (x) S H (D)) \leftrightarrow (H (x) = y \land y S H (D))$
37	34 36	bitri	$⊢ (H (x) S H (D) \land H (x) = y) \leftrightarrow (H (x) = y \land y S H (D))$
38	33 37	bitrdi	$⊢ (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)))$
39	38	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)))))$
40	39	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)))))$
41	40	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))))$
42	41	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))))$
43	26 42	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))))$
44	43	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)))$
45		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))$
46	44 45	bitrdi	$⊢ (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)))$
47	17 46	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)$
48	2 47	bitrid	$⊢ (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)$
49	48	eqabdv	$⊢ (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\}$
50	1 49	eqtr4id	$⊢ (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