isomin

Description: Isomorphisms preserve minimal elements. Note that (`' R " { D } ) ` is Takeuti and Zaring's idiom for the initial segment { x | x R D } . Proposition 6.31(1) of TakeutiZaring p. 33. (Contributed by NM, 19-Apr-2004)

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

Proof

Step	Hyp	Ref	Expression
1		neq0	$⊢ \neg H [C] \cap S^{-1} [\{H (D)\}] = \emptyset \leftrightarrow \exists y y \in (H [C] \cap S^{-1} [\{H (D)\}])$
2		vex	$⊢ y \in V$
3	2	elima	$⊢ y \in H [C] \leftrightarrow \exists x \in C x H y$
4		ssel	$⊢ C \subseteq A \to (x \in C \to x \in A)$
5		isof1o	$⊢ H {Isom}_{R, S} (A, B) \to H : A \underset{1-1 onto}{⟶} B$
6		f1ofn	$⊢ H : A \underset{1-1 onto}{⟶} B \to H Fn A$
7		fnbrfvb	$⊢ (H Fn A \land x \in A) \to (H (x) = y \leftrightarrow x H y)$
8	7	ex	$⊢ H Fn A \to (x \in A \to (H (x) = y \leftrightarrow x H y))$
9	5 6 8	3syl	$⊢ H {Isom}_{R, S} (A, B) \to (x \in A \to (H (x) = y \leftrightarrow x H y))$
10	4 9	syl9r	$⊢ H {Isom}_{R, S} (A, B) \to (C \subseteq A \to (x \in C \to (H (x) = y \leftrightarrow x H y)))$
11	10	imp31	$⊢ ((H {Isom}_{R, S} (A, B) \land C \subseteq A) \land x \in C) \to (H (x) = y \leftrightarrow x H y)$
12	11	rexbidva	$⊢ (H {Isom}_{R, S} (A, B) \land C \subseteq A) \to (\exists x \in C H (x) = y \leftrightarrow \exists x \in C x H y)$
13	3 12	bitr4id	$⊢ (H {Isom}_{R, S} (A, B) \land C \subseteq A) \to (y \in H [C] \leftrightarrow \exists x \in C H (x) = y)$
14		fvex	$⊢ H (D) \in V$
15	2	eliniseg	$⊢ H (D) \in V \to (y \in S^{-1} [\{H (D)\}] \leftrightarrow y S H (D))$
16	14 15	mp1i	$⊢ (H {Isom}_{R, S} (A, B) \land C \subseteq A) \to (y \in S^{-1} [\{H (D)\}] \leftrightarrow y S H (D))$
17	13 16	anbi12d	$⊢ (H {Isom}_{R, S} (A, B) \land C \subseteq A) \to ((y \in H [C] \land y \in S^{-1} [\{H (D)\}]) \leftrightarrow (\exists x \in C H (x) = y \land y S H (D)))$
18		elin	$⊢ y \in (H [C] \cap S^{-1} [\{H (D)\}]) \leftrightarrow (y \in H [C] \land y \in S^{-1} [\{H (D)\}])$
19		r19.41v	$⊢ \exists x \in C (H (x) = y \land y S H (D)) \leftrightarrow (\exists x \in C H (x) = y \land y S H (D))$
20	17 18 19	3bitr4g	$⊢ (H {Isom}_{R, S} (A, B) \land C \subseteq A) \to (y \in (H [C] \cap S^{-1} [\{H (D)\}]) \leftrightarrow \exists x \in C (H (x) = y \land y S H (D)))$
21	20	adantrr	$⊢ (H {Isom}_{R, S} (A, B) \land (C \subseteq A \land D \in A)) \to (y \in (H [C] \cap S^{-1} [\{H (D)\}]) \leftrightarrow \exists x \in C (H (x) = y \land y S H (D)))$
22		breq1	$⊢ H (x) = y \to (H (x) S H (D) \leftrightarrow y S H (D))$
23	22	biimpar	$⊢ (H (x) = y \land y S H (D)) \to H (x) S H (D)$
24		vex	$⊢ x \in V$
25	24	eliniseg	$⊢ D \in A \to (x \in R^{-1} [\{D\}] \leftrightarrow x R D)$
26	25	ad2antll	$⊢ (H {Isom}_{R, S} (A, B) \land (x \in A \land D \in A)) \to (x \in R^{-1} [\{D\}] \leftrightarrow x R D)$
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	26 27	bitrd	$⊢ (H {Isom}_{R, S} (A, B) \land (x \in A \land D \in A)) \to (x \in R^{-1} [\{D\}] \leftrightarrow H (x) S H (D))$
29	23 28	syl5ibr	$⊢ (H {Isom}_{R, S} (A, B) \land (x \in A \land D \in A)) \to ((H (x) = y \land y S H (D)) \to x \in R^{-1} [\{D\}])$
30	29	exp32	$⊢ H {Isom}_{R, S} (A, B) \to (x \in A \to (D \in A \to ((H (x) = y \land y S H (D)) \to x \in R^{-1} [\{D\}])))$
31	4 30	syl9r	$⊢ H {Isom}_{R, S} (A, B) \to (C \subseteq A \to (x \in C \to (D \in A \to ((H (x) = y \land y S H (D)) \to x \in R^{-1} [\{D\}]))))$
32	31	com34	$⊢ H {Isom}_{R, S} (A, B) \to (C \subseteq A \to (D \in A \to (x \in C \to ((H (x) = y \land y S H (D)) \to x \in R^{-1} [\{D\}]))))$
33	32	imp32	$⊢ (H {Isom}_{R, S} (A, B) \land (C \subseteq A \land D \in A)) \to (x \in C \to ((H (x) = y \land y S H (D)) \to x \in R^{-1} [\{D\}]))$
34	33	reximdvai	$⊢ (H {Isom}_{R, S} (A, B) \land (C \subseteq A \land D \in A)) \to (\exists x \in C (H (x) = y \land y S H (D)) \to \exists x \in C x \in R^{-1} [\{D\}])$
35	21 34	sylbid	$⊢ (H {Isom}_{R, S} (A, B) \land (C \subseteq A \land D \in A)) \to (y \in (H [C] \cap S^{-1} [\{H (D)\}]) \to \exists x \in C x \in R^{-1} [\{D\}])$
36		elin	$⊢ x \in (C \cap R^{-1} [\{D\}]) \leftrightarrow (x \in C \land x \in R^{-1} [\{D\}])$
37	36	exbii	$⊢ \exists x x \in (C \cap R^{-1} [\{D\}]) \leftrightarrow \exists x (x \in C \land x \in R^{-1} [\{D\}])$
38		neq0	$⊢ \neg C \cap R^{-1} [\{D\}] = \emptyset \leftrightarrow \exists x x \in (C \cap R^{-1} [\{D\}])$
39		df-rex	$⊢ \exists x \in C x \in R^{-1} [\{D\}] \leftrightarrow \exists x (x \in C \land x \in R^{-1} [\{D\}])$
40	37 38 39	3bitr4i	$⊢ \neg C \cap R^{-1} [\{D\}] = \emptyset \leftrightarrow \exists x \in C x \in R^{-1} [\{D\}]$
41	35 40	syl6ibr	$⊢ (H {Isom}_{R, S} (A, B) \land (C \subseteq A \land D \in A)) \to (y \in (H [C] \cap S^{-1} [\{H (D)\}]) \to \neg C \cap R^{-1} [\{D\}] = \emptyset)$
42	41	exlimdv	$⊢ (H {Isom}_{R, S} (A, B) \land (C \subseteq A \land D \in A)) \to (\exists y y \in (H [C] \cap S^{-1} [\{H (D)\}]) \to \neg C \cap R^{-1} [\{D\}] = \emptyset)$
43	1 42	syl5bi	$⊢ (H {Isom}_{R, S} (A, B) \land (C \subseteq A \land D \in A)) \to (\neg H [C] \cap S^{-1} [\{H (D)\}] = \emptyset \to \neg C \cap R^{-1} [\{D\}] = \emptyset)$
44	43	con4d	$⊢ (H {Isom}_{R, S} (A, B) \land (C \subseteq A \land D \in A)) \to (C \cap R^{-1} [\{D\}] = \emptyset \to H [C] \cap S^{-1} [\{H (D)\}] = \emptyset)$
45	5 6	syl	$⊢ H {Isom}_{R, S} (A, B) \to H Fn A$
46		fnfvima	$⊢ (H Fn A \land C \subseteq A \land x \in C) \to H (x) \in H [C]$
47	46	3expia	$⊢ (H Fn A \land C \subseteq A) \to (x \in C \to H (x) \in H [C])$
48	47	adantrr	$⊢ (H Fn A \land (C \subseteq A \land D \in A)) \to (x \in C \to H (x) \in H [C])$
49	45 48	sylan	$⊢ (H {Isom}_{R, S} (A, B) \land (C \subseteq A \land D \in A)) \to (x \in C \to H (x) \in H [C])$
50	49	adantrd	$⊢ (H {Isom}_{R, S} (A, B) \land (C \subseteq A \land D \in A)) \to ((x \in C \land x \in R^{-1} [\{D\}]) \to H (x) \in H [C])$
51	27	biimpd	$⊢ (H {Isom}_{R, S} (A, B) \land (x \in A \land D \in A)) \to (x R D \to H (x) S H (D))$
52		fvex	$⊢ H (x) \in V$
53	52	eliniseg	$⊢ H (D) \in V \to (H (x) \in S^{-1} [\{H (D)\}] \leftrightarrow H (x) S H (D))$
54	14 53	ax-mp	$⊢ H (x) \in S^{-1} [\{H (D)\}] \leftrightarrow H (x) S H (D)$
55	51 54	syl6ibr	$⊢ (H {Isom}_{R, S} (A, B) \land (x \in A \land D \in A)) \to (x R D \to H (x) \in S^{-1} [\{H (D)\}])$
56	26 55	sylbid	$⊢ (H {Isom}_{R, S} (A, B) \land (x \in A \land D \in A)) \to (x \in R^{-1} [\{D\}] \to H (x) \in S^{-1} [\{H (D)\}])$
57	56	exp32	$⊢ H {Isom}_{R, S} (A, B) \to (x \in A \to (D \in A \to (x \in R^{-1} [\{D\}] \to H (x) \in S^{-1} [\{H (D)\}])))$
58	4 57	syl9r	$⊢ H {Isom}_{R, S} (A, B) \to (C \subseteq A \to (x \in C \to (D \in A \to (x \in R^{-1} [\{D\}] \to H (x) \in S^{-1} [\{H (D)\}]))))$
59	58	com34	$⊢ H {Isom}_{R, S} (A, B) \to (C \subseteq A \to (D \in A \to (x \in C \to (x \in R^{-1} [\{D\}] \to H (x) \in S^{-1} [\{H (D)\}]))))$
60	59	imp32	$⊢ (H {Isom}_{R, S} (A, B) \land (C \subseteq A \land D \in A)) \to (x \in C \to (x \in R^{-1} [\{D\}] \to H (x) \in S^{-1} [\{H (D)\}]))$
61	60	impd	$⊢ (H {Isom}_{R, S} (A, B) \land (C \subseteq A \land D \in A)) \to ((x \in C \land x \in R^{-1} [\{D\}]) \to H (x) \in S^{-1} [\{H (D)\}])$
62	50 61	jcad	$⊢ (H {Isom}_{R, S} (A, B) \land (C \subseteq A \land D \in A)) \to ((x \in C \land x \in R^{-1} [\{D\}]) \to (H (x) \in H [C] \land H (x) \in S^{-1} [\{H (D)\}]))$
63		elin	$⊢ H (x) \in (H [C] \cap S^{-1} [\{H (D)\}]) \leftrightarrow (H (x) \in H [C] \land H (x) \in S^{-1} [\{H (D)\}])$
64	62 36 63	3imtr4g	$⊢ (H {Isom}_{R, S} (A, B) \land (C \subseteq A \land D \in A)) \to (x \in (C \cap R^{-1} [\{D\}]) \to H (x) \in (H [C] \cap S^{-1} [\{H (D)\}]))$
65		n0i	$⊢ H (x) \in (H [C] \cap S^{-1} [\{H (D)\}]) \to \neg H [C] \cap S^{-1} [\{H (D)\}] = \emptyset$
66	64 65	syl6	$⊢ (H {Isom}_{R, S} (A, B) \land (C \subseteq A \land D \in A)) \to (x \in (C \cap R^{-1} [\{D\}]) \to \neg H [C] \cap S^{-1} [\{H (D)\}] = \emptyset)$
67	66	exlimdv	$⊢ (H {Isom}_{R, S} (A, B) \land (C \subseteq A \land D \in A)) \to (\exists x x \in (C \cap R^{-1} [\{D\}]) \to \neg H [C] \cap S^{-1} [\{H (D)\}] = \emptyset)$
68	38 67	syl5bi	$⊢ (H {Isom}_{R, S} (A, B) \land (C \subseteq A \land D \in A)) \to (\neg C \cap R^{-1} [\{D\}] = \emptyset \to \neg H [C] \cap S^{-1} [\{H (D)\}] = \emptyset)$
69	44 68	impcon4bid	$⊢ (H {Isom}_{R, S} (A, B) \land (C \subseteq A \land D \in A)) \to (C \cap R^{-1} [\{D\}] = \emptyset \leftrightarrow H [C] \cap S^{-1} [\{H (D)\}] = \emptyset)$

Metamath Proof Explorer

Theorem isomin

Proof