onprcf1acwevdlem1

		Ref	Expression
	Hypothesis	onprcf1acwevdlem1.1	$⊢ W = \{r \| \exists x \in On (r \subseteq R_{1} (x) \times R_{1} (x) \land r We R_{1} (x))\}$
	Assertion	onprcf1acwevdlem1	$⊢ (A \subseteq W \land B \in On \land \forall y \in A \neg y We R_{1} (B)) \to A \in V$

Proof

Step	Hyp	Ref	Expression
1		onprcf1acwevdlem1.1	$⊢ W = \{r \| \exists x \in On (r \subseteq R_{1} (x) \times R_{1} (x) \land r We R_{1} (x))\}$
2		19.28v	$⊢ \forall y ((A \subseteq W \land B \in On) \land (y \in A \to \neg y We R_{1} (B))) \leftrightarrow ((A \subseteq W \land B \in On) \land \forall y (y \in A \to \neg y We R_{1} (B)))$
3		df-ral	$⊢ \forall y \in A \neg y We R_{1} (B) \leftrightarrow \forall y (y \in A \to \neg y We R_{1} (B))$
4	3	anbi2i	$⊢ ((A \subseteq W \land B \in On) \land \forall y \in A \neg y We R_{1} (B)) \leftrightarrow ((A \subseteq W \land B \in On) \land \forall y (y \in A \to \neg y We R_{1} (B)))$
5	2 4	bitr4i	$⊢ \forall y ((A \subseteq W \land B \in On) \land (y \in A \to \neg y We R_{1} (B))) \leftrightarrow ((A \subseteq W \land B \in On) \land \forall y \in A \neg y We R_{1} (B))$
6		df-3an	$⊢ (A \subseteq W \land B \in On \land (y \in A \to \neg y We R_{1} (B))) \leftrightarrow ((A \subseteq W \land B \in On) \land (y \in A \to \neg y We R_{1} (B)))$
7	6	albii	$⊢ \forall y (A \subseteq W \land B \in On \land (y \in A \to \neg y We R_{1} (B))) \leftrightarrow \forall y ((A \subseteq W \land B \in On) \land (y \in A \to \neg y We R_{1} (B)))$
8		df-3an	$⊢ (A \subseteq W \land B \in On \land \forall y \in A \neg y We R_{1} (B)) \leftrightarrow ((A \subseteq W \land B \in On) \land \forall y \in A \neg y We R_{1} (B))$
9	5 7 8	3bitr4ri	$⊢ (A \subseteq W \land B \in On \land \forall y \in A \neg y We R_{1} (B)) \leftrightarrow \forall y (A \subseteq W \land B \in On \land (y \in A \to \neg y We R_{1} (B)))$
10		nfa1	$⊢ Ⅎ y \forall y (A \subseteq W \land B \in On \land (y \in A \to \neg y We R_{1} (B)))$
11		nfcv	$⊢ \underline{Ⅎ} y A$
12		nfcv	$⊢ \underline{Ⅎ} y \{v \| \exists w (w \subseteq R_{1} (B) \land v \subseteq w \times w \land v We w)\}$
13		idd	$⊢ y \in A \to (A \subseteq W \to A \subseteq W)$
14		idd	$⊢ y \in A \to (B \in On \to B \in On)$
15		pm2.27	$⊢ y \in A \to ((y \in A \to \neg y We R_{1} (B)) \to \neg y We R_{1} (B))$
16	13 14 15	3anim123d	$⊢ y \in A \to ((A \subseteq W \land B \in On \land (y \in A \to \neg y We R_{1} (B))) \to (A \subseteq W \land B \in On \land \neg y We R_{1} (B)))$
17		simp1	$⊢ (A \subseteq W \land B \in On \land \neg y We R_{1} (B)) \to A \subseteq W$
18		ssel2	$⊢ (A \subseteq W \land y \in A) \to y \in W$
19		vex	$⊢ y \in V$
20		sseq1	$⊢ r = y \to (r \subseteq R_{1} (x) \times R_{1} (x) \leftrightarrow y \subseteq R_{1} (x) \times R_{1} (x))$
21		weeq1	$⊢ r = y \to (r We R_{1} (x) \leftrightarrow y We R_{1} (x))$
22	20 21	anbi12d	$⊢ r = y \to ((r \subseteq R_{1} (x) \times R_{1} (x) \land r We R_{1} (x)) \leftrightarrow (y \subseteq R_{1} (x) \times R_{1} (x) \land y We R_{1} (x)))$
23	22	rexbidv	$⊢ r = y \to (\exists x \in On (r \subseteq R_{1} (x) \times R_{1} (x) \land r We R_{1} (x)) \leftrightarrow \exists x \in On (y \subseteq R_{1} (x) \times R_{1} (x) \land y We R_{1} (x)))$
24	19 23 1	elab2	$⊢ y \in W \leftrightarrow \exists x \in On (y \subseteq R_{1} (x) \times R_{1} (x) \land y We R_{1} (x))$
25	18 24	sylib	$⊢ (A \subseteq W \land y \in A) \to \exists x \in On (y \subseteq R_{1} (x) \times R_{1} (x) \land y We R_{1} (x))$
26	25	expcom	$⊢ y \in A \to (A \subseteq W \to \exists x \in On (y \subseteq R_{1} (x) \times R_{1} (x) \land y We R_{1} (x)))$
27	17 26	syl5	$⊢ y \in A \to ((A \subseteq W \land B \in On \land \neg y We R_{1} (B)) \to \exists x \in On (y \subseteq R_{1} (x) \times R_{1} (x) \land y We R_{1} (x)))$
28		ontri1	$⊢ (B \in On \land x \in On) \to (B \subseteq x \leftrightarrow \neg x \in B)$
29	28	biimprd	$⊢ (B \in On \land x \in On) \to (\neg x \in B \to B \subseteq x)$
30		r1ord3	$⊢ (B \in On \land x \in On) \to (B \subseteq x \to R_{1} (B) \subseteq R_{1} (x))$
31	30	3impia	$⊢ (B \in On \land x \in On \land B \subseteq x) \to R_{1} (B) \subseteq R_{1} (x)$
32		wess	$⊢ R_{1} (B) \subseteq R_{1} (x) \to (y We R_{1} (x) \to y We R_{1} (B))$
33	31 32	syl	$⊢ (B \in On \land x \in On \land B \subseteq x) \to (y We R_{1} (x) \to y We R_{1} (B))$
34	33	con3d	$⊢ (B \in On \land x \in On \land B \subseteq x) \to (\neg y We R_{1} (B) \to \neg y We R_{1} (x))$
35	34	3expia	$⊢ (B \in On \land x \in On) \to (B \subseteq x \to (\neg y We R_{1} (B) \to \neg y We R_{1} (x)))$
36	35	com23	$⊢ (B \in On \land x \in On) \to (\neg y We R_{1} (B) \to (B \subseteq x \to \neg y We R_{1} (x)))$
37	29 36	syl5d	$⊢ (B \in On \land x \in On) \to (\neg y We R_{1} (B) \to (\neg x \in B \to \neg y We R_{1} (x)))$
38	37	3impia	$⊢ (B \in On \land x \in On \land \neg y We R_{1} (B)) \to (\neg x \in B \to \neg y We R_{1} (x))$
39	38	con4d	$⊢ (B \in On \land x \in On \land \neg y We R_{1} (B)) \to (y We R_{1} (x) \to x \in B)$
40		simp1	$⊢ (B \in On \land x \in On \land \neg y We R_{1} (B)) \to B \in On$
41	39 40	jctild	$⊢ (B \in On \land x \in On \land \neg y We R_{1} (B)) \to (y We R_{1} (x) \to (B \in On \land x \in B))$
42	41	3expia	$⊢ (B \in On \land x \in On) \to (\neg y We R_{1} (B) \to (y We R_{1} (x) \to (B \in On \land x \in B)))$
43	42	impancom	$⊢ (B \in On \land \neg y We R_{1} (B)) \to (x \in On \to (y We R_{1} (x) \to (B \in On \land x \in B)))$
44	43	imp	$⊢ ((B \in On \land \neg y We R_{1} (B)) \land x \in On) \to (y We R_{1} (x) \to (B \in On \land x \in B))$
45	44	adantld	$⊢ ((B \in On \land \neg y We R_{1} (B)) \land x \in On) \to ((y \subseteq R_{1} (x) \times R_{1} (x) \land y We R_{1} (x)) \to (B \in On \land x \in B))$
46		r1ord2	$⊢ B \in On \to (x \in B \to R_{1} (x) \subseteq R_{1} (B))$
47	46	imp	$⊢ (B \in On \land x \in B) \to R_{1} (x) \subseteq R_{1} (B)$
48		fvex	$⊢ R_{1} (x) \in V$
49		sseq1	$⊢ w = R_{1} (x) \to (w \subseteq R_{1} (B) \leftrightarrow R_{1} (x) \subseteq R_{1} (B))$
50		id	$⊢ w = R_{1} (x) \to w = R_{1} (x)$
51	50	sqxpeqd	$⊢ w = R_{1} (x) \to w \times w = R_{1} (x) \times R_{1} (x)$
52	51	sseq2d	$⊢ w = R_{1} (x) \to (y \subseteq w \times w \leftrightarrow y \subseteq R_{1} (x) \times R_{1} (x))$
53		weeq2	$⊢ w = R_{1} (x) \to (y We w \leftrightarrow y We R_{1} (x))$
54	49 52 53	3anbi123d	$⊢ w = R_{1} (x) \to ((w \subseteq R_{1} (B) \land y \subseteq w \times w \land y We w) \leftrightarrow (R_{1} (x) \subseteq R_{1} (B) \land y \subseteq R_{1} (x) \times R_{1} (x) \land y We R_{1} (x)))$
55	48 54	spcev	$⊢ (R_{1} (x) \subseteq R_{1} (B) \land y \subseteq R_{1} (x) \times R_{1} (x) \land y We R_{1} (x)) \to \exists w (w \subseteq R_{1} (B) \land y \subseteq w \times w \land y We w)$
56	55	3expib	$⊢ R_{1} (x) \subseteq R_{1} (B) \to ((y \subseteq R_{1} (x) \times R_{1} (x) \land y We R_{1} (x)) \to \exists w (w \subseteq R_{1} (B) \land y \subseteq w \times w \land y We w))$
57	47 56	syl	$⊢ (B \in On \land x \in B) \to ((y \subseteq R_{1} (x) \times R_{1} (x) \land y We R_{1} (x)) \to \exists w (w \subseteq R_{1} (B) \land y \subseteq w \times w \land y We w))$
58	45 57	syli	$⊢ ((B \in On \land \neg y We R_{1} (B)) \land x \in On) \to ((y \subseteq R_{1} (x) \times R_{1} (x) \land y We R_{1} (x)) \to \exists w (w \subseteq R_{1} (B) \land y \subseteq w \times w \land y We w))$
59	58	rexlimdva	$⊢ (B \in On \land \neg y We R_{1} (B)) \to (\exists x \in On (y \subseteq R_{1} (x) \times R_{1} (x) \land y We R_{1} (x)) \to \exists w (w \subseteq R_{1} (B) \land y \subseteq w \times w \land y We w))$
60		sseq1	$⊢ v = y \to (v \subseteq w \times w \leftrightarrow y \subseteq w \times w)$
61		weeq1	$⊢ v = y \to (v We w \leftrightarrow y We w)$
62	60 61	3anbi23d	$⊢ v = y \to ((w \subseteq R_{1} (B) \land v \subseteq w \times w \land v We w) \leftrightarrow (w \subseteq R_{1} (B) \land y \subseteq w \times w \land y We w))$
63	62	exbidv	$⊢ v = y \to (\exists w (w \subseteq R_{1} (B) \land v \subseteq w \times w \land v We w) \leftrightarrow \exists w (w \subseteq R_{1} (B) \land y \subseteq w \times w \land y We w))$
64	19 63	elab	$⊢ y \in \{v \| \exists w (w \subseteq R_{1} (B) \land v \subseteq w \times w \land v We w)\} \leftrightarrow \exists w (w \subseteq R_{1} (B) \land y \subseteq w \times w \land y We w)$
65	59 64	imbitrrdi	$⊢ (B \in On \land \neg y We R_{1} (B)) \to (\exists x \in On (y \subseteq R_{1} (x) \times R_{1} (x) \land y We R_{1} (x)) \to y \in \{v \| \exists w (w \subseteq R_{1} (B) \land v \subseteq w \times w \land v We w)\})$
66	65	3adant1	$⊢ (A \subseteq W \land B \in On \land \neg y We R_{1} (B)) \to (\exists x \in On (y \subseteq R_{1} (x) \times R_{1} (x) \land y We R_{1} (x)) \to y \in \{v \| \exists w (w \subseteq R_{1} (B) \land v \subseteq w \times w \land v We w)\})$
67	27 66	sylcom	$⊢ y \in A \to ((A \subseteq W \land B \in On \land \neg y We R_{1} (B)) \to y \in \{v \| \exists w (w \subseteq R_{1} (B) \land v \subseteq w \times w \land v We w)\})$
68	16 67	syldc	$⊢ (A \subseteq W \land B \in On \land (y \in A \to \neg y We R_{1} (B))) \to (y \in A \to y \in \{v \| \exists w (w \subseteq R_{1} (B) \land v \subseteq w \times w \land v We w)\})$
69	68	sps	$⊢ \forall y (A \subseteq W \land B \in On \land (y \in A \to \neg y We R_{1} (B))) \to (y \in A \to y \in \{v \| \exists w (w \subseteq R_{1} (B) \land v \subseteq w \times w \land v We w)\})$
70	10 11 12 69	ssrd	$⊢ \forall y (A \subseteq W \land B \in On \land (y \in A \to \neg y We R_{1} (B))) \to A \subseteq \{v \| \exists w (w \subseteq R_{1} (B) \land v \subseteq w \times w \land v We w)\}$
71	9 70	sylbi	$⊢ (A \subseteq W \land B \in On \land \forall y \in A \neg y We R_{1} (B)) \to A \subseteq \{v \| \exists w (w \subseteq R_{1} (B) \land v \subseteq w \times w \land v We w)\}$
72		fvex	$⊢ R_{1} (B) \in V$
73		abweex	$⊢ R_{1} (B) \in V \to \{v \| \exists w (w \subseteq R_{1} (B) \land v \subseteq w \times w \land v We w)\} \in V$
74	72 73	ax-mp	$⊢ \{v \| \exists w (w \subseteq R_{1} (B) \land v \subseteq w \times w \land v We w)\} \in V$
75	74	ssex	$⊢ A \subseteq \{v \| \exists w (w \subseteq R_{1} (B) \land v \subseteq w \times w \land v We w)\} \to A \in V$
76	71 75	syl	$⊢ (A \subseteq W \land B \in On \land \forall y \in A \neg y We R_{1} (B)) \to A \in V$

Metamath Proof Explorer

Theorem onprcf1acwevdlem1

Proof