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	3	snn0d	$$⊢\phi \to \left\{B\right\}\ne \varnothing$$
18	17	necomd	$$⊢\phi \to \varnothing \ne \left\{B\right\}$$
19	16 18	nelprd	$$⊢\phi \to \neg \varnothing \in \left\{\left\{\varnothing \right\},\left\{B\right\}\right\}$$
20	19	adantr	$$⊢\left(\phi \wedge \varnothing \in a\right)\to \neg \varnothing \in \left\{\left\{\varnothing \right\},\left\{B\right\}\right\}$$
21	14 20	elnelneqd	$$⊢\left(\phi \wedge \varnothing \in a\right)\to \neg a=\left\{\left\{\varnothing \right\},\left\{B\right\}\right\}$$
22	21	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\}$$
23	22	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\}$$
24		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)$$
25	24 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)$$
26	25	orcomd	$$⊢a\in F\to \left(a=\left\{\left\{\varnothing \right\},\left\{B\right\}\right\}\vee a=\left\{\varnothing ,\left\{A\right\}\right\}\right)$$
27	26	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)$$
28	13 23 27	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\}$$
29	28	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\}$$
30		snex	$$⊢\left\{A\right\}\in \mathrm{V}$$
31	8 30	unipr	$$⊢\bigcup \left\{\varnothing ,\left\{A\right\}\right\}=\varnothing \cup \left\{A\right\}$$
32		uncom	$$⊢\varnothing \cup \left\{A\right\}=\left\{A\right\}\cup \varnothing$$
33		un0	$$⊢\left\{A\right\}\cup \varnothing =\left\{A\right\}$$
34	31 32 33	3eqtri	$$⊢\bigcup \left\{\varnothing ,\left\{A\right\}\right\}=\left\{A\right\}$$
35	29 34	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\}$$
36		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$$
37	35 36	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$$
38		snssg	$$⊢A\in U\to \left(A\in w\leftrightarrow \left\{A\right\}\subseteq w\right)$$
39	38	biimprd	$$⊢A\in U\to \left(\left\{A\right\}\subseteq w\to A\in w\right)$$
40	12 37 39	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$$
41		eleq2w	$$⊢u=a\to \left(\varnothing \in u\leftrightarrow \varnothing \in a\right)$$
42		unieq	$$⊢u=a\to \bigcup u=\bigcup a$$
43	42	sseq1d	$$⊢u=a\to \left(\bigcup u\subseteq w\leftrightarrow \bigcup a\subseteq w\right)$$
44	41 43	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)$$
45	11 40 44	rexlimddvcbvw	$$⊢\phi \to A\in w$$