isofrlem

Description: Lemma for isofr . (Contributed by NM, 29-Apr-2004) (Revised by Mario Carneiro, 18-Nov-2014)

	Ref	Expression
Hypotheses	isofrlem.1	$⊢ φ \to H {Isom}_{R, S} (A, B)$
	isofrlem.2	$⊢ φ \to H [x] \in V$
Assertion	isofrlem	$⊢ φ \to (S Fr B \to R Fr A)$

Proof

Step	Hyp	Ref	Expression
1		isofrlem.1	$⊢ φ \to H {Isom}_{R, S} (A, B)$
2		isofrlem.2	$⊢ φ \to H [x] \in V$
3		isof1o	$⊢ H {Isom}_{R, S} (A, B) \to H : A \underset{1-1 onto}{⟶} B$
4	1 3	syl	$⊢ φ \to H : A \underset{1-1 onto}{⟶} B$
5		f1ofn	$⊢ H : A \underset{1-1 onto}{⟶} B \to H Fn A$
6		n0	$⊢ x \neq \emptyset \leftrightarrow \exists y y \in x$
7		fnfvima	$⊢ (H Fn A \land x \subseteq A \land y \in x) \to H (y) \in H [x]$
8	7	ne0d	$⊢ (H Fn A \land x \subseteq A \land y \in x) \to H [x] \neq \emptyset$
9	8	3expia	$⊢ (H Fn A \land x \subseteq A) \to (y \in x \to H [x] \neq \emptyset)$
10	9	exlimdv	$⊢ (H Fn A \land x \subseteq A) \to (\exists y y \in x \to H [x] \neq \emptyset)$
11	6 10	syl5bi	$⊢ (H Fn A \land x \subseteq A) \to (x \neq \emptyset \to H [x] \neq \emptyset)$
12	11	expimpd	$⊢ H Fn A \to ((x \subseteq A \land x \neq \emptyset) \to H [x] \neq \emptyset)$
13	5 12	syl	$⊢ H : A \underset{1-1 onto}{⟶} B \to ((x \subseteq A \land x \neq \emptyset) \to H [x] \neq \emptyset)$
14		f1ofo	$⊢ H : A \underset{1-1 onto}{⟶} B \to H : A \underset{onto}{⟶} B$
15		imassrn	$⊢ H [x] \subseteq ran H$
16		forn	$⊢ H : A \underset{onto}{⟶} B \to ran H = B$
17	15 16	sseqtrid	$⊢ H : A \underset{onto}{⟶} B \to H [x] \subseteq B$
18	14 17	syl	$⊢ H : A \underset{1-1 onto}{⟶} B \to H [x] \subseteq B$
19	13 18	jctild	$⊢ H : A \underset{1-1 onto}{⟶} B \to ((x \subseteq A \land x \neq \emptyset) \to (H [x] \subseteq B \land H [x] \neq \emptyset))$
20	4 19	syl	$⊢ φ \to ((x \subseteq A \land x \neq \emptyset) \to (H [x] \subseteq B \land H [x] \neq \emptyset))$
21		dffr3	$⊢ S Fr B \leftrightarrow \forall z ((z \subseteq B \land z \neq \emptyset) \to \exists w \in z z \cap S^{-1} [\{w\}] = \emptyset)$
22		sseq1	$⊢ z = H [x] \to (z \subseteq B \leftrightarrow H [x] \subseteq B)$
23		neeq1	$⊢ z = H [x] \to (z \neq \emptyset \leftrightarrow H [x] \neq \emptyset)$
24	22 23	anbi12d	$⊢ z = H [x] \to ((z \subseteq B \land z \neq \emptyset) \leftrightarrow (H [x] \subseteq B \land H [x] \neq \emptyset))$
25		ineq1	$⊢ z = H [x] \to z \cap S^{-1} [\{w\}] = H [x] \cap S^{-1} [\{w\}]$
26	25	eqeq1d	$⊢ z = H [x] \to (z \cap S^{-1} [\{w\}] = \emptyset \leftrightarrow H [x] \cap S^{-1} [\{w\}] = \emptyset)$
27	26	rexeqbi1dv	$⊢ z = H [x] \to (\exists w \in z z \cap S^{-1} [\{w\}] = \emptyset \leftrightarrow \exists w \in H [x] H [x] \cap S^{-1} [\{w\}] = \emptyset)$
28	24 27	imbi12d	$⊢ z = H [x] \to (((z \subseteq B \land z \neq \emptyset) \to \exists w \in z z \cap S^{-1} [\{w\}] = \emptyset) \leftrightarrow ((H [x] \subseteq B \land H [x] \neq \emptyset) \to \exists w \in H [x] H [x] \cap S^{-1} [\{w\}] = \emptyset))$
29	28	spcgv	$⊢ H [x] \in V \to (\forall z ((z \subseteq B \land z \neq \emptyset) \to \exists w \in z z \cap S^{-1} [\{w\}] = \emptyset) \to ((H [x] \subseteq B \land H [x] \neq \emptyset) \to \exists w \in H [x] H [x] \cap S^{-1} [\{w\}] = \emptyset))$
30	2 29	syl	$⊢ φ \to (\forall z ((z \subseteq B \land z \neq \emptyset) \to \exists w \in z z \cap S^{-1} [\{w\}] = \emptyset) \to ((H [x] \subseteq B \land H [x] \neq \emptyset) \to \exists w \in H [x] H [x] \cap S^{-1} [\{w\}] = \emptyset))$
31	21 30	syl5bi	$⊢ φ \to (S Fr B \to ((H [x] \subseteq B \land H [x] \neq \emptyset) \to \exists w \in H [x] H [x] \cap S^{-1} [\{w\}] = \emptyset))$
32	20 31	syl5d	$⊢ φ \to (S Fr B \to ((x \subseteq A \land x \neq \emptyset) \to \exists w \in H [x] H [x] \cap S^{-1} [\{w\}] = \emptyset))$
33	4	adantr	$⊢ (φ \land x \subseteq A) \to H : A \underset{1-1 onto}{⟶} B$
34		f1ofun	$⊢ H : A \underset{1-1 onto}{⟶} B \to Fun H$
35	33 34	syl	$⊢ (φ \land x \subseteq A) \to Fun H$
36		simpl	$⊢ (w \in H [x] \land H [x] \cap S^{-1} [\{w\}] = \emptyset) \to w \in H [x]$
37		fvelima	$⊢ (Fun H \land w \in H [x]) \to \exists y \in x H (y) = w$
38	35 36 37	syl2an	$⊢ ((φ \land x \subseteq A) \land (w \in H [x] \land H [x] \cap S^{-1} [\{w\}] = \emptyset)) \to \exists y \in x H (y) = w$
39		simpr	$⊢ (w \in H [x] \land H [x] \cap S^{-1} [\{w\}] = \emptyset) \to H [x] \cap S^{-1} [\{w\}] = \emptyset$
40		ssel	$⊢ x \subseteq A \to (y \in x \to y \in A)$
41	40	imdistani	$⊢ (x \subseteq A \land y \in x) \to (x \subseteq A \land y \in A)$
42		isomin	$⊢ (H {Isom}_{R, S} (A, B) \land (x \subseteq A \land y \in A)) \to (x \cap R^{-1} [\{y\}] = \emptyset \leftrightarrow H [x] \cap S^{-1} [\{H (y)\}] = \emptyset)$
43	1 41 42	syl2an	$⊢ (φ \land (x \subseteq A \land y \in x)) \to (x \cap R^{-1} [\{y\}] = \emptyset \leftrightarrow H [x] \cap S^{-1} [\{H (y)\}] = \emptyset)$
44		sneq	$⊢ H (y) = w \to \{H (y)\} = \{w\}$
45	44	imaeq2d	$⊢ H (y) = w \to S^{-1} [\{H (y)\}] = S^{-1} [\{w\}]$
46	45	ineq2d	$⊢ H (y) = w \to H [x] \cap S^{-1} [\{H (y)\}] = H [x] \cap S^{-1} [\{w\}]$
47	46	eqeq1d	$⊢ H (y) = w \to (H [x] \cap S^{-1} [\{H (y)\}] = \emptyset \leftrightarrow H [x] \cap S^{-1} [\{w\}] = \emptyset)$
48	43 47	sylan9bb	$⊢ ((φ \land (x \subseteq A \land y \in x)) \land H (y) = w) \to (x \cap R^{-1} [\{y\}] = \emptyset \leftrightarrow H [x] \cap S^{-1} [\{w\}] = \emptyset)$
49	39 48	syl5ibr	$⊢ ((φ \land (x \subseteq A \land y \in x)) \land H (y) = w) \to ((w \in H [x] \land H [x] \cap S^{-1} [\{w\}] = \emptyset) \to x \cap R^{-1} [\{y\}] = \emptyset)$
50	49	exp42	$⊢ φ \to (x \subseteq A \to (y \in x \to (H (y) = w \to ((w \in H [x] \land H [x] \cap S^{-1} [\{w\}] = \emptyset) \to x \cap R^{-1} [\{y\}] = \emptyset))))$
51	50	imp	$⊢ (φ \land x \subseteq A) \to (y \in x \to (H (y) = w \to ((w \in H [x] \land H [x] \cap S^{-1} [\{w\}] = \emptyset) \to x \cap R^{-1} [\{y\}] = \emptyset)))$
52	51	com3l	$⊢ y \in x \to (H (y) = w \to ((φ \land x \subseteq A) \to ((w \in H [x] \land H [x] \cap S^{-1} [\{w\}] = \emptyset) \to x \cap R^{-1} [\{y\}] = \emptyset)))$
53	52	com4t	$⊢ (φ \land x \subseteq A) \to ((w \in H [x] \land H [x] \cap S^{-1} [\{w\}] = \emptyset) \to (y \in x \to (H (y) = w \to x \cap R^{-1} [\{y\}] = \emptyset)))$
54	53	imp	$⊢ ((φ \land x \subseteq A) \land (w \in H [x] \land H [x] \cap S^{-1} [\{w\}] = \emptyset)) \to (y \in x \to (H (y) = w \to x \cap R^{-1} [\{y\}] = \emptyset))$
55	54	reximdvai	$⊢ ((φ \land x \subseteq A) \land (w \in H [x] \land H [x] \cap S^{-1} [\{w\}] = \emptyset)) \to (\exists y \in x H (y) = w \to \exists y \in x x \cap R^{-1} [\{y\}] = \emptyset)$
56	38 55	mpd	$⊢ ((φ \land x \subseteq A) \land (w \in H [x] \land H [x] \cap S^{-1} [\{w\}] = \emptyset)) \to \exists y \in x x \cap R^{-1} [\{y\}] = \emptyset$
57	56	rexlimdvaa	$⊢ (φ \land x \subseteq A) \to (\exists w \in H [x] H [x] \cap S^{-1} [\{w\}] = \emptyset \to \exists y \in x x \cap R^{-1} [\{y\}] = \emptyset)$
58	57	ex	$⊢ φ \to (x \subseteq A \to (\exists w \in H [x] H [x] \cap S^{-1} [\{w\}] = \emptyset \to \exists y \in x x \cap R^{-1} [\{y\}] = \emptyset))$
59	58	adantrd	$⊢ φ \to ((x \subseteq A \land x \neq \emptyset) \to (\exists w \in H [x] H [x] \cap S^{-1} [\{w\}] = \emptyset \to \exists y \in x x \cap R^{-1} [\{y\}] = \emptyset))$
60	59	a2d	$⊢ φ \to (((x \subseteq A \land x \neq \emptyset) \to \exists w \in H [x] H [x] \cap S^{-1} [\{w\}] = \emptyset) \to ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x x \cap R^{-1} [\{y\}] = \emptyset))$
61	32 60	syld	$⊢ φ \to (S Fr B \to ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x x \cap R^{-1} [\{y\}] = \emptyset))$
62	61	alrimdv	$⊢ φ \to (S Fr B \to \forall x ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x x \cap R^{-1} [\{y\}] = \emptyset))$
63		dffr3	$⊢ R Fr A \leftrightarrow \forall x ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x x \cap R^{-1} [\{y\}] = \emptyset)$
64	62 63	syl6ibr	$⊢ φ \to (S Fr B \to R Fr A)$

Metamath Proof Explorer

Theorem isofrlem

Proof