Theorem mnuprdlem1

Description: Lemma for mnuprd . (Contributed by Rohan Ridenour, 11-Aug-2023)

	Ref	Expression
Hypotheses	mnuprdlem1.1	$$⊢F=\left\{\left\{\varnothing ,\left\{A\right\}\right\},\left\{\left\{\varnothing \right\},\left\{B\right\}\right\}\right\}$$
	mnuprdlem1.3	$$⊢\phi \to A\in U$$
	mnuprdlem1.4	$$⊢\phi \to B\in U$$
	mnuprdlem1.8	$$⊢\phi \to \forall i\in \left\{\varnothing ,\left\{\varnothing \right\}\right\}\exists u\in F\left(i\in u\wedge \bigcup u\subseteq w\right)$$
Assertion	mnuprdlem1	$$⊢\phi \to A\in w$$

Proof

Step	Hyp	Ref	Expression
1		mnuprdlem1.1	$$⊢F=\left\{\left\{\varnothing ,\left\{A\right\}\right\},\left\{\left\{\varnothing \right\},\left\{B\right\}\right\}\right\}$$
2		mnuprdlem1.3	$$⊢\phi \to A\in U$$
3		mnuprdlem1.4	$$⊢\phi \to B\in U$$
4		mnuprdlem1.8	$$⊢\phi \to \forall i\in \left\{\varnothing ,\left\{\varnothing \right\}\right\}\exists u\in F\left(i\in u\wedge \bigcup u\subseteq w\right)$$
5		eleq1	$$⊢i=\varnothing \to \left(i\in u\leftrightarrow \varnothing \in u\right)$$
6	5	anbi1d	$$⊢i=\varnothing \to \left(\left(i\in u\wedge \bigcup u\subseteq w\right)\leftrightarrow \left(\varnothing \in u\wedge \bigcup u\subseteq w\right)\right)$$
7	6	rexbidv	$$⊢i=\varnothing \to \left(\exists u\in F\left(i\in u\wedge \bigcup u\subseteq w\right)\leftrightarrow \exists u\in F\left(\varnothing \in u\wedge \bigcup u\subseteq w\right)\right)$$
8		0ex	$$⊢\varnothing \in \mathrm{V}$$
9	8	prid1	$$⊢\varnothing \in \left\{\varnothing ,\left\{\varnothing \right\}\right\}$$
10	9	a1i	$$⊢\phi \to \varnothing \in \left\{\varnothing ,\left\{\varnothing \right\}\right\}$$
11	7 4 10	rspcdva	$$⊢\phi \to \exists u\in F\left(\varnothing \in u\wedge \bigcup u\subseteq w\right)$$
12	2	adantr	$$⊢\left(\phi \wedge \left(a\in F\wedge \left(\varnothing \in a\wedge \bigcup a\subseteq w\right)\right)\right)\to A\in U$$
13		simprl	$$⊢\left(\phi \wedge \left(a\in F\wedge \left(\varnothing \in a\wedge \bigcup a\subseteq w\right)\right)\right)\to a\in F$$
14		simpr	$$⊢\left(\phi \wedge \varnothing \in a\right)\to \varnothing \in a$$
15		0nep0	$$⊢\varnothing \ne \left\{\varnothing \right\}$$
16	15	a1i	$$⊢\phi \to \varnothing \ne \left\{\varnothing \right\}$$
17		snnzg	$$⊢B\in U\to \left\{B\right\}\ne \varnothing$$
18	3 17	syl	$$⊢\phi \to \left\{B\right\}\ne \varnothing$$
19	18	necomd	$$⊢\phi \to \varnothing \ne \left\{B\right\}$$
20	16 19	nelprd	$$⊢\phi \to \neg \varnothing \in \left\{\left\{\varnothing \right\},\left\{B\right\}\right\}$$
21	20	adantr	$$⊢\left(\phi \wedge \varnothing \in a\right)\to \neg \varnothing \in \left\{\left\{\varnothing \right\},\left\{B\right\}\right\}$$
22	14 21	elnelneqd	$$⊢\left(\phi \wedge \varnothing \in a\right)\to \neg a=\left\{\left\{\varnothing \right\},\left\{B\right\}\right\}$$
23	22	adantrr	$$⊢\left(\phi \wedge \left(\varnothing \in a\wedge \bigcup a\subseteq w\right)\right)\to \neg a=\left\{\left\{\varnothing \right\},\left\{B\right\}\right\}$$
24	23	adantrl	$$⊢\left(\phi \wedge \left(a\in F\wedge \left(\varnothing \in a\wedge \bigcup a\subseteq w\right)\right)\right)\to \neg a=\left\{\left\{\varnothing \right\},\left\{B\right\}\right\}$$
25		elpri	$$⊢a\in \left\{\left\{\varnothing ,\left\{A\right\}\right\},\left\{\left\{\varnothing \right\},\left\{B\right\}\right\}\right\}\to \left(a=\left\{\varnothing ,\left\{A\right\}\right\}\vee a=\left\{\left\{\varnothing \right\},\left\{B\right\}\right\}\right)$$
26	25 1	eleq2s	$$⊢a\in F\to \left(a=\left\{\varnothing ,\left\{A\right\}\right\}\vee a=\left\{\left\{\varnothing \right\},\left\{B\right\}\right\}\right)$$
27	26	orcomd	$$⊢a\in F\to \left(a=\left\{\left\{\varnothing \right\},\left\{B\right\}\right\}\vee a=\left\{\varnothing ,\left\{A\right\}\right\}\right)$$
28	27	ord	$$⊢a\in F\to \left(\neg a=\left\{\left\{\varnothing \right\},\left\{B\right\}\right\}\to a=\left\{\varnothing ,\left\{A\right\}\right\}\right)$$
29	13 24 28	sylc	$$⊢\left(\phi \wedge \left(a\in F\wedge \left(\varnothing \in a\wedge \bigcup a\subseteq w\right)\right)\right)\to a=\left\{\varnothing ,\left\{A\right\}\right\}$$
30	29	unieqd	$$⊢\left(\phi \wedge \left(a\in F\wedge \left(\varnothing \in a\wedge \bigcup a\subseteq w\right)\right)\right)\to \bigcup a=\bigcup \left\{\varnothing ,\left\{A\right\}\right\}$$
31		snex	$$⊢\left\{A\right\}\in \mathrm{V}$$
32	8 31	unipr	$$⊢\bigcup \left\{\varnothing ,\left\{A\right\}\right\}=\varnothing \cup \left\{A\right\}$$
33		uncom	$$⊢\varnothing \cup \left\{A\right\}=\left\{A\right\}\cup \varnothing$$
34		un0	$$⊢\left\{A\right\}\cup \varnothing =\left\{A\right\}$$
35	32 33 34	3eqtri	$$⊢\bigcup \left\{\varnothing ,\left\{A\right\}\right\}=\left\{A\right\}$$
36	30 35	eqtrdi	$$⊢\left(\phi \wedge \left(a\in F\wedge \left(\varnothing \in a\wedge \bigcup a\subseteq w\right)\right)\right)\to \bigcup a=\left\{A\right\}$$
37		simprrr	$$⊢\left(\phi \wedge \left(a\in F\wedge \left(\varnothing \in a\wedge \bigcup a\subseteq w\right)\right)\right)\to \bigcup a\subseteq w$$
38	36 37	eqsstrrd	$$⊢\left(\phi \wedge \left(a\in F\wedge \left(\varnothing \in a\wedge \bigcup a\subseteq w\right)\right)\right)\to \left\{A\right\}\subseteq w$$
39		snssg	$$⊢A\in U\to \left(A\in w\leftrightarrow \left\{A\right\}\subseteq w\right)$$
40	39	biimprd	$$⊢A\in U\to \left(\left\{A\right\}\subseteq w\to A\in w\right)$$
41	12 38 40	sylc	$$⊢\left(\phi \wedge \left(a\in F\wedge \left(\varnothing \in a\wedge \bigcup a\subseteq w\right)\right)\right)\to A\in w$$
42		eleq2w	$$⊢u=a\to \left(\varnothing \in u\leftrightarrow \varnothing \in a\right)$$
43		unieq	$$⊢u=a\to \bigcup u=\bigcup a$$
44	43	sseq1d	$$⊢u=a\to \left(\bigcup u\subseteq w\leftrightarrow \bigcup a\subseteq w\right)$$
45	42 44	anbi12d	$$⊢u=a\to \left(\left(\varnothing \in u\wedge \bigcup u\subseteq w\right)\leftrightarrow \left(\varnothing \in a\wedge \bigcup a\subseteq w\right)\right)$$
46	11 41 45	rexlimddvcbvw	$$⊢\phi \to A\in w$$