onvf1odlem1

		Ref	Expression
	Assertion	onvf1odlem1	$⊢ A \in V \to \exists x \in On \exists y \in R_{1} (x) \neg y \in A$

Proof

Step	Hyp	Ref	Expression
1		nvel	$⊢ \neg V \in V$
2		eleq1	$⊢ V = A \to (V \in V \leftrightarrow A \in V)$
3	2	eqcoms	$⊢ A = V \to (V \in V \leftrightarrow A \in V)$
4	1 3	mtbii	$⊢ A = V \to \neg A \in V$
5	4	con2i	$⊢ A \in V \to \neg A = V$
6		eqv	$⊢ A = V \leftrightarrow \forall y y \in A$
7		alex	$⊢ \forall y y \in A \leftrightarrow \neg \exists y \neg y \in A$
8	6 7	bitri	$⊢ A = V \leftrightarrow \neg \exists y \neg y \in A$
9	8	con2bii	$⊢ \exists y \neg y \in A \leftrightarrow \neg A = V$
10	5 9	sylibr	$⊢ A \in V \to \exists y \neg y \in A$
11		ax-1	$⊢ \neg y \in A \to (x \in On \to \neg y \in A)$
12	11	ralrimiv	$⊢ \neg y \in A \to \forall x \in On \neg y \in A$
13	12	eximi	$⊢ \exists y \neg y \in A \to \exists y \forall x \in On \neg y \in A$
14		rexv	$⊢ \exists y \in V \forall x \in On \neg y \in A \leftrightarrow \exists y \forall x \in On \neg y \in A$
15	13 14	sylibr	$⊢ \exists y \neg y \in A \to \exists y \in V \forall x \in On \neg y \in A$
16		tz9.13g	$⊢ y \in V \to \exists x \in On y \in R_{1} (x)$
17	16	rgen	$⊢ \forall y \in V \exists x \in On y \in R_{1} (x)$
18		r19.29r	$⊢ (\exists y \in V \forall x \in On \neg y \in A \land \forall y \in V \exists x \in On y \in R_{1} (x)) \to \exists y \in V (\forall x \in On \neg y \in A \land \exists x \in On y \in R_{1} (x))$
19		r19.29	$⊢ (\forall x \in On \neg y \in A \land \exists x \in On y \in R_{1} (x)) \to \exists x \in On (\neg y \in A \land y \in R_{1} (x))$
20	19	reximi	$⊢ \exists y \in V (\forall x \in On \neg y \in A \land \exists x \in On y \in R_{1} (x)) \to \exists y \in V \exists x \in On (\neg y \in A \land y \in R_{1} (x))$
21	18 20	syl	$⊢ (\exists y \in V \forall x \in On \neg y \in A \land \forall y \in V \exists x \in On y \in R_{1} (x)) \to \exists y \in V \exists x \in On (\neg y \in A \land y \in R_{1} (x))$
22	17 21	mpan2	$⊢ \exists y \in V \forall x \in On \neg y \in A \to \exists y \in V \exists x \in On (\neg y \in A \land y \in R_{1} (x))$
23	10 15 22	3syl	$⊢ A \in V \to \exists y \in V \exists x \in On (\neg y \in A \land y \in R_{1} (x))$
24		rexcom	$⊢ \exists y \in V \exists x \in On (\neg y \in A \land y \in R_{1} (x)) \leftrightarrow \exists x \in On \exists y \in V (\neg y \in A \land y \in R_{1} (x))$
25		exancom	$⊢ \exists y (\neg y \in A \land y \in R_{1} (x)) \leftrightarrow \exists y (y \in R_{1} (x) \land \neg y \in A)$
26		rexv	$⊢ \exists y \in V (\neg y \in A \land y \in R_{1} (x)) \leftrightarrow \exists y (\neg y \in A \land y \in R_{1} (x))$
27		df-rex	$⊢ \exists y \in R_{1} (x) \neg y \in A \leftrightarrow \exists y (y \in R_{1} (x) \land \neg y \in A)$
28	25 26 27	3bitr4i	$⊢ \exists y \in V (\neg y \in A \land y \in R_{1} (x)) \leftrightarrow \exists y \in R_{1} (x) \neg y \in A$
29	28	rexbii	$⊢ \exists x \in On \exists y \in V (\neg y \in A \land y \in R_{1} (x)) \leftrightarrow \exists x \in On \exists y \in R_{1} (x) \neg y \in A$
30	24 29	bitri	$⊢ \exists y \in V \exists x \in On (\neg y \in A \land y \in R_{1} (x)) \leftrightarrow \exists x \in On \exists y \in R_{1} (x) \neg y \in A$
31	23 30	sylib	$⊢ A \in V \to \exists x \in On \exists y \in R_{1} (x) \neg y \in A$

Metamath Proof Explorer

Theorem onvf1odlem1

Proof