isoselem

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

Proof

Step	Hyp	Ref	Expression
1		isofrlem.1	$⊢ φ \to H {Isom}_{R, S} (A, B)$
2		isofrlem.2	$⊢ φ \to H [x] \in V$
3		dfse2	$⊢ R Se A \leftrightarrow \forall z \in A A \cap R^{-1} [\{z\}] \in V$
4	3	biimpi	$⊢ R Se A \to \forall z \in A A \cap R^{-1} [\{z\}] \in V$
5	4	r19.21bi	$⊢ (R Se A \land z \in A) \to A \cap R^{-1} [\{z\}] \in V$
6	5	expcom	$⊢ z \in A \to (R Se A \to A \cap R^{-1} [\{z\}] \in V)$
7	6	adantl	$⊢ (φ \land z \in A) \to (R Se A \to A \cap R^{-1} [\{z\}] \in V)$
8		imaeq2	$⊢ x = A \cap R^{-1} [\{z\}] \to H [x] = H [A \cap R^{-1} [\{z\}]]$
9	8	eleq1d	$⊢ x = A \cap R^{-1} [\{z\}] \to (H [x] \in V \leftrightarrow H [A \cap R^{-1} [\{z\}]] \in V)$
10	9	imbi2d	$⊢ x = A \cap R^{-1} [\{z\}] \to ((φ \to H [x] \in V) \leftrightarrow (φ \to H [A \cap R^{-1} [\{z\}]] \in V))$
11	10 2	vtoclg	$⊢ A \cap R^{-1} [\{z\}] \in V \to (φ \to H [A \cap R^{-1} [\{z\}]] \in V)$
12	11	com12	$⊢ φ \to (A \cap R^{-1} [\{z\}] \in V \to H [A \cap R^{-1} [\{z\}]] \in V)$
13	12	adantr	$⊢ (φ \land z \in A) \to (A \cap R^{-1} [\{z\}] \in V \to H [A \cap R^{-1} [\{z\}]] \in V)$
14		isoini	$⊢ (H {Isom}_{R, S} (A, B) \land z \in A) \to H [A \cap R^{-1} [\{z\}]] = B \cap S^{-1} [\{H (z)\}]$
15	1 14	sylan	$⊢ (φ \land z \in A) \to H [A \cap R^{-1} [\{z\}]] = B \cap S^{-1} [\{H (z)\}]$
16	15	eleq1d	$⊢ (φ \land z \in A) \to (H [A \cap R^{-1} [\{z\}]] \in V \leftrightarrow B \cap S^{-1} [\{H (z)\}] \in V)$
17	13 16	sylibd	$⊢ (φ \land z \in A) \to (A \cap R^{-1} [\{z\}] \in V \to B \cap S^{-1} [\{H (z)\}] \in V)$
18	7 17	syld	$⊢ (φ \land z \in A) \to (R Se A \to B \cap S^{-1} [\{H (z)\}] \in V)$
19	18	ralrimdva	$⊢ φ \to (R Se A \to \forall z \in A B \cap S^{-1} [\{H (z)\}] \in V)$
20		isof1o	$⊢ H {Isom}_{R, S} (A, B) \to H : A \underset{1-1 onto}{⟶} B$
21		f1ofn	$⊢ H : A \underset{1-1 onto}{⟶} B \to H Fn A$
22		sneq	$⊢ y = H (z) \to \{y\} = \{H (z)\}$
23	22	imaeq2d	$⊢ y = H (z) \to S^{-1} [\{y\}] = S^{-1} [\{H (z)\}]$
24	23	ineq2d	$⊢ y = H (z) \to B \cap S^{-1} [\{y\}] = B \cap S^{-1} [\{H (z)\}]$
25	24	eleq1d	$⊢ y = H (z) \to (B \cap S^{-1} [\{y\}] \in V \leftrightarrow B \cap S^{-1} [\{H (z)\}] \in V)$
26	25	ralrn	$⊢ H Fn A \to (\forall y \in ran H B \cap S^{-1} [\{y\}] \in V \leftrightarrow \forall z \in A B \cap S^{-1} [\{H (z)\}] \in V)$
27	1 20 21 26	4syl	$⊢ φ \to (\forall y \in ran H B \cap S^{-1} [\{y\}] \in V \leftrightarrow \forall z \in A B \cap S^{-1} [\{H (z)\}] \in V)$
28		f1ofo	$⊢ H : A \underset{1-1 onto}{⟶} B \to H : A \underset{onto}{⟶} B$
29		forn	$⊢ H : A \underset{onto}{⟶} B \to ran H = B$
30	1 20 28 29	4syl	$⊢ φ \to ran H = B$
31	30	raleqdv	$⊢ φ \to (\forall y \in ran H B \cap S^{-1} [\{y\}] \in V \leftrightarrow \forall y \in B B \cap S^{-1} [\{y\}] \in V)$
32	27 31	bitr3d	$⊢ φ \to (\forall z \in A B \cap S^{-1} [\{H (z)\}] \in V \leftrightarrow \forall y \in B B \cap S^{-1} [\{y\}] \in V)$
33	19 32	sylibd	$⊢ φ \to (R Se A \to \forall y \in B B \cap S^{-1} [\{y\}] \in V)$
34		dfse2	$⊢ S Se B \leftrightarrow \forall y \in B B \cap S^{-1} [\{y\}] \in V$
35	33 34	imbitrrdi	$⊢ φ \to (R Se A \to S Se B)$

Metamath Proof Explorer

Theorem isoselem

Proof