onvf1odlem2

	Ref	Expression
Hypotheses	onvf1odlem2.1	$⊢ φ \to \forall z (z \neq \emptyset \to G (z) \in z)$
	onvf1odlem2.2	$⊢ M = ⋂ \{x \in On \| \exists y \in R_{1} (x) \neg y \in A\}$
	onvf1odlem2.3	$⊢ N = G (R_{1} (M) ∖ A)$
Assertion	onvf1odlem2	$⊢ φ \to (A \in V \to N \in (R_{1} (M) ∖ A))$

Proof

Step	Hyp	Ref	Expression
1		onvf1odlem2.1	$⊢ φ \to \forall z (z \neq \emptyset \to G (z) \in z)$
2		onvf1odlem2.2	$⊢ M = ⋂ \{x \in On \| \exists y \in R_{1} (x) \neg y \in A\}$
3		onvf1odlem2.3	$⊢ N = G (R_{1} (M) ∖ A)$
4		onvf1odlem1	$⊢ A \in V \to \exists x \in On \exists y \in R_{1} (x) \neg y \in A$
5		nfcv	$⊢ \underline{Ⅎ} x R_{1}$
6		nfrab1	$⊢ \underline{Ⅎ} x \{x \in On \| \exists y \in R_{1} (x) \neg y \in A\}$
7	6	nfint	$⊢ \underline{Ⅎ} x ⋂ \{x \in On \| \exists y \in R_{1} (x) \neg y \in A\}$
8	5 7	nffv	$⊢ \underline{Ⅎ} x R_{1} (⋂ \{x \in On \| \exists y \in R_{1} (x) \neg y \in A\})$
9		nfv	$⊢ Ⅎ x \neg v \in A$
10	8 9	nfrexw	$⊢ Ⅎ x \exists v \in R_{1} (⋂ \{x \in On \| \exists y \in R_{1} (x) \neg y \in A\}) \neg v \in A$
11		eleq1w	$⊢ y = v \to (y \in A \leftrightarrow v \in A)$
12	11	notbid	$⊢ y = v \to (\neg y \in A \leftrightarrow \neg v \in A)$
13	12	cbvrexvw	$⊢ \exists y \in R_{1} (x) \neg y \in A \leftrightarrow \exists v \in R_{1} (x) \neg v \in A$
14		fveq2	$⊢ x = ⋂ \{x \in On \| \exists y \in R_{1} (x) \neg y \in A\} \to R_{1} (x) = R_{1} (⋂ \{x \in On \| \exists y \in R_{1} (x) \neg y \in A\})$
15	14	rexeqdv	$⊢ x = ⋂ \{x \in On \| \exists y \in R_{1} (x) \neg y \in A\} \to (\exists v \in R_{1} (x) \neg v \in A \leftrightarrow \exists v \in R_{1} (⋂ \{x \in On \| \exists y \in R_{1} (x) \neg y \in A\}) \neg v \in A)$
16	13 15	bitrid	$⊢ x = ⋂ \{x \in On \| \exists y \in R_{1} (x) \neg y \in A\} \to (\exists y \in R_{1} (x) \neg y \in A \leftrightarrow \exists v \in R_{1} (⋂ \{x \in On \| \exists y \in R_{1} (x) \neg y \in A\}) \neg v \in A)$
17	10 16	onminsb	$⊢ \exists x \in On \exists y \in R_{1} (x) \neg y \in A \to \exists v \in R_{1} (⋂ \{x \in On \| \exists y \in R_{1} (x) \neg y \in A\}) \neg v \in A$
18	2	fveq2i	$⊢ R_{1} (M) = R_{1} (⋂ \{x \in On \| \exists y \in R_{1} (x) \neg y \in A\})$
19	18	rexeqi	$⊢ \exists v \in R_{1} (M) \neg v \in A \leftrightarrow \exists v \in R_{1} (⋂ \{x \in On \| \exists y \in R_{1} (x) \neg y \in A\}) \neg v \in A$
20	17 19	sylibr	$⊢ \exists x \in On \exists y \in R_{1} (x) \neg y \in A \to \exists v \in R_{1} (M) \neg v \in A$
21	4 20	syl	$⊢ A \in V \to \exists v \in R_{1} (M) \neg v \in A$
22		df-rex	$⊢ \exists v \in R_{1} (M) \neg v \in A \leftrightarrow \exists v (v \in R_{1} (M) \land \neg v \in A)$
23		nss	$⊢ \neg R_{1} (M) \subseteq A \leftrightarrow \exists v (v \in R_{1} (M) \land \neg v \in A)$
24		ssdif0	$⊢ R_{1} (M) \subseteq A \leftrightarrow R_{1} (M) ∖ A = \emptyset$
25	24	necon3bbii	$⊢ \neg R_{1} (M) \subseteq A \leftrightarrow R_{1} (M) ∖ A \neq \emptyset$
26	22 23 25	3bitr2i	$⊢ \exists v \in R_{1} (M) \neg v \in A \leftrightarrow R_{1} (M) ∖ A \neq \emptyset$
27	21 26	sylib	$⊢ A \in V \to R_{1} (M) ∖ A \neq \emptyset$
28		fvex	$⊢ R_{1} (M) \in V$
29	28	difexi	$⊢ R_{1} (M) ∖ A \in V$
30		neeq1	$⊢ z = R_{1} (M) ∖ A \to (z \neq \emptyset \leftrightarrow R_{1} (M) ∖ A \neq \emptyset)$
31		fveq2	$⊢ z = R_{1} (M) ∖ A \to G (z) = G (R_{1} (M) ∖ A)$
32		id	$⊢ z = R_{1} (M) ∖ A \to z = R_{1} (M) ∖ A$
33	31 32	eleq12d	$⊢ z = R_{1} (M) ∖ A \to (G (z) \in z \leftrightarrow G (R_{1} (M) ∖ A) \in (R_{1} (M) ∖ A))$
34	30 33	imbi12d	$⊢ z = R_{1} (M) ∖ A \to ((z \neq \emptyset \to G (z) \in z) \leftrightarrow (R_{1} (M) ∖ A \neq \emptyset \to G (R_{1} (M) ∖ A) \in (R_{1} (M) ∖ A)))$
35	29 34	spcv	$⊢ \forall z (z \neq \emptyset \to G (z) \in z) \to (R_{1} (M) ∖ A \neq \emptyset \to G (R_{1} (M) ∖ A) \in (R_{1} (M) ∖ A))$
36	1 27 35	syl2im	$⊢ φ \to (A \in V \to G (R_{1} (M) ∖ A) \in (R_{1} (M) ∖ A))$
37	3	eleq1i	$⊢ N \in (R_{1} (M) ∖ A) \leftrightarrow G (R_{1} (M) ∖ A) \in (R_{1} (M) ∖ A)$
38	36 37	imbitrrdi	$⊢ φ \to (A \in V \to N \in (R_{1} (M) ∖ A))$

Metamath Proof Explorer

Theorem onvf1odlem2

Proof