Theorem mnuprdlem1

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

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

Proof

Step	Hyp	Ref	Expression
1		mnuprdlem1.1	|- F = { { (/) , { A } } , { { (/) } , { B } } }
2		mnuprdlem1.3	|- ( ph -> A e. U )
3		mnuprdlem1.4	|- ( ph -> B e. U )
4		mnuprdlem1.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		0ex	|- (/) e. _V
9	8	prid1	|- (/) e. { (/) , { (/) } }
10	9	a1i	|- ( ph -> (/) e. { (/) , { (/) } } )
11	7 4 10	rspcdva	|- ( ph -> E. u e. F ( (/) e. u /\ U. u C_ w ) )
12	2	adantr	|- ( ( ph /\ ( a e. F /\ ( (/) e. a /\ U. a C_ w ) ) ) -> A e. U )
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	a1i	|- ( ph -> (/) =/= { (/) } )
17	3	snn0d	|- ( ph -> { B } =/= (/) )
18	17	necomd	|- ( ph -> (/) =/= { B } )
19	16 18	nelprd	|- ( ph -> -. (/) e. { { (/) } , { B } } )
20	19	adantr	|- ( ( ph /\ (/) e. a ) -> -. (/) e. { { (/) } , { B } } )
21	14 20	elnelneqd	|- ( ( ph /\ (/) e. a ) -> -. a = { { (/) } , { B } } )
22	21	adantrr	|- ( ( ph /\ ( (/) e. a /\ U. a C_ w ) ) -> -. a = { { (/) } , { B } } )
23	22	adantrl	|- ( ( ph /\ ( a e. F /\ ( (/) e. a /\ U. a C_ w ) ) ) -> -. a = { { (/) } , { B } } )
24		elpri	|- ( a e. { { (/) , { A } } , { { (/) } , { B } } } -> ( a = { (/) , { A } } \/ a = { { (/) } , { B } } ) )
25	24 1	eleq2s	|- ( a e. F -> ( a = { (/) , { A } } \/ a = { { (/) } , { B } } ) )
26	25	orcomd	|- ( a e. F -> ( a = { { (/) } , { B } } \/ a = { (/) , { A } } ) )
27	26	ord	|- ( a e. F -> ( -. a = { { (/) } , { B } } -> a = { (/) , { A } } ) )
28	13 23 27	sylc	|- ( ( ph /\ ( a e. F /\ ( (/) e. a /\ U. a C_ w ) ) ) -> a = { (/) , { A } } )
29	28	unieqd	|- ( ( ph /\ ( a e. F /\ ( (/) e. a /\ U. a C_ w ) ) ) -> U. a = U. { (/) , { A } } )
30		snex	|- { A } e. _V
31	8 30	unipr	|- U. { (/) , { A } } = ( (/) u. { A } )
32		uncom	|- ( (/) u. { A } ) = ( { A } u. (/) )
33		un0	|- ( { A } u. (/) ) = { A }
34	31 32 33	3eqtri	|- U. { (/) , { A } } = { A }
35	29 34	eqtrdi	|- ( ( ph /\ ( a e. F /\ ( (/) e. a /\ U. a C_ w ) ) ) -> U. a = { A } )
36		simprrr	|- ( ( ph /\ ( a e. F /\ ( (/) e. a /\ U. a C_ w ) ) ) -> U. a C_ w )
37	35 36	eqsstrrd	|- ( ( ph /\ ( a e. F /\ ( (/) e. a /\ U. a C_ w ) ) ) -> { A } C_ w )
38		snssg	|- ( A e. U -> ( A e. w <-> { A } C_ w ) )
39	38	biimprd	|- ( A e. U -> ( { A } C_ w -> A e. w ) )
40	12 37 39	sylc	|- ( ( ph /\ ( a e. F /\ ( (/) e. a /\ U. a C_ w ) ) ) -> A e. w )
41		eleq2w	|- ( u = a -> ( (/) e. u <-> (/) e. a ) )
42		unieq	|- ( u = a -> U. u = U. a )
43	42	sseq1d	|- ( u = a -> ( U. u C_ w <-> U. a C_ w ) )
44	41 43	anbi12d	|- ( u = a -> ( ( (/) e. u /\ U. u C_ w ) <-> ( (/) e. a /\ U. a C_ w ) ) )
45	11 40 44	rexlimddvcbvw	|- ( ph -> A e. w )