Metamath Proof Explorer


Theorem mnuprdlem2

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

Ref Expression
Hypotheses mnuprdlem2.1 F = A B
mnuprdlem2.4 φ B U
mnuprdlem2.5 φ ¬ A =
mnuprdlem2.8 φ i u F i u u w
Assertion mnuprdlem2 φ B w

Proof

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