Theorem mnuprdlem2

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

	Ref	Expression
Hypotheses	mnuprdlem2.1	|- F = { { (/) , { A } } , { { (/) } , { B } } }
	mnuprdlem2.4	|- ( ph -> B e. U )
	mnuprdlem2.5	|- ( ph -> -. A = (/) )
	mnuprdlem2.8	|- ( ph -> A. i e. { (/) , { (/) } } E. u e. F ( i e. u /\ U. u C_ w ) )
Assertion	mnuprdlem2	|- ( ph -> B e. w )

Proof

Step	Hyp	Ref	Expression
1		mnuprdlem2.1	|- F = { { (/) , { A } } , { { (/) } , { B } } }
2		mnuprdlem2.4	|- ( ph -> B e. U )
3		mnuprdlem2.5	|- ( ph -> -. A = (/) )
4		mnuprdlem2.8	|- ( ph -> A. i e. { (/) , { (/) } } E. u e. F ( i e. u /\ U. u C_ w ) )
5		eleq1	|- ( i = { (/) } -> ( i e. u <-> { (/) } e. u ) )
6	5	anbi1d	|- ( i = { (/) } -> ( ( i e. u /\ U. u C_ w ) <-> ( { (/) } e. u /\ U. u C_ w ) ) )
7	6	rexbidv	|- ( i = { (/) } -> ( E. u e. F ( i e. u /\ U. u C_ w ) <-> E. u e. F ( { (/) } e. u /\ U. u C_ w ) ) )
8		p0ex	|- { (/) } e. _V
9	8	prid2	|- { (/) } e. { (/) , { (/) } }
10	9	a1i	|- ( ph -> { (/) } e. { (/) , { (/) } } )
11	7 4 10	rspcdva	|- ( ph -> E. u e. F ( { (/) } e. u /\ U. u C_ w ) )
12		simpl	|- ( ( ph /\ ( a e. F /\ ( { (/) } e. a /\ U. a C_ w ) ) ) -> ph )
13		simprl	|- ( ( ph /\ ( a e. F /\ ( { (/) } e. a /\ U. a C_ w ) ) ) -> a e. F )
14		simpr	|- ( ( ph /\ { (/) } e. a ) -> { (/) } e. a )
15		0nep0	|- (/) =/= { (/) }
16	15	necomi	|- { (/) } =/= (/)
17	16	a1i	|- ( ph -> { (/) } =/= (/) )
18		0ex	|- (/) e. _V
19	18	sneqr	|- ( { (/) } = { A } -> (/) = A )
20	19	eqcomd	|- ( { (/) } = { A } -> A = (/) )
21	3 20	nsyl	|- ( ph -> -. { (/) } = { A } )
22	21	neqned	|- ( ph -> { (/) } =/= { A } )
23	17 22	nelprd	|- ( ph -> -. { (/) } e. { (/) , { A } } )
24	23	adantr	|- ( ( ph /\ { (/) } e. a ) -> -. { (/) } e. { (/) , { A } } )
25	14 24	elnelneqd	|- ( ( ph /\ { (/) } e. a ) -> -. a = { (/) , { A } } )
26	25	adantrr	|- ( ( ph /\ ( { (/) } e. a /\ U. a C_ w ) ) -> -. a = { (/) , { A } } )
27	26	adantrl	|- ( ( ph /\ ( a e. F /\ ( { (/) } e. a /\ U. a C_ w ) ) ) -> -. a = { (/) , { A } } )
28		elpri	|- ( a e. { { (/) , { A } } , { { (/) } , { B } } } -> ( a = { (/) , { A } } \/ a = { { (/) } , { B } } ) )
29	28 1	eleq2s	|- ( a e. F -> ( a = { (/) , { A } } \/ a = { { (/) } , { B } } ) )
30	29	ord	|- ( a e. F -> ( -. a = { (/) , { A } } -> a = { { (/) } , { B } } ) )
31	13 27 30	sylc	|- ( ( ph /\ ( a e. F /\ ( { (/) } e. a /\ U. a C_ w ) ) ) -> a = { { (/) } , { B } } )
32	31	unieqd	|- ( ( ph /\ ( a e. F /\ ( { (/) } e. a /\ U. a C_ w ) ) ) -> U. a = U. { { (/) } , { B } } )
33		snex	|- { B } e. _V
34	8 33	unipr	|- U. { { (/) } , { B } } = ( { (/) } u. { B } )
35		df-pr	|- { (/) , B } = ( { (/) } u. { B } )
36	34 35	eqtr4i	|- U. { { (/) } , { B } } = { (/) , B }
37	32 36	eqtrdi	|- ( ( ph /\ ( a e. F /\ ( { (/) } e. a /\ U. a C_ w ) ) ) -> U. a = { (/) , B } )
38		simprrr	|- ( ( ph /\ ( a e. F /\ ( { (/) } e. a /\ U. a C_ w ) ) ) -> U. a C_ w )
39	37 38	eqsstrrd	|- ( ( ph /\ ( a e. F /\ ( { (/) } e. a /\ U. a C_ w ) ) ) -> { (/) , B } C_ w )
40		prssg	|- ( ( (/) e. _V /\ B e. U ) -> ( ( (/) e. w /\ B e. w ) <-> { (/) , B } C_ w ) )
41	18 2 40	sylancr	|- ( ph -> ( ( (/) e. w /\ B e. w ) <-> { (/) , B } C_ w ) )
42	41	biimprd	|- ( ph -> ( { (/) , B } C_ w -> ( (/) e. w /\ B e. w ) ) )
43	12 39 42	sylc	|- ( ( ph /\ ( a e. F /\ ( { (/) } e. a /\ U. a C_ w ) ) ) -> ( (/) e. w /\ B e. w ) )
44	43	simprd	|- ( ( ph /\ ( a e. F /\ ( { (/) } e. a /\ U. a C_ w ) ) ) -> B e. w )
45		eleq2w	|- ( u = a -> ( { (/) } e. u <-> { (/) } e. a ) )
46		unieq	|- ( u = a -> U. u = U. a )
47	46	sseq1d	|- ( u = a -> ( U. u C_ w <-> U. a C_ w ) )
48	45 47	anbi12d	|- ( u = a -> ( ( { (/) } e. u /\ U. u C_ w ) <-> ( { (/) } e. a /\ U. a C_ w ) ) )
49	11 44 48	rexlimddvcbvw	|- ( ph -> B e. w )