Metamath Proof Explorer


Theorem mnuprdlem1

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

Ref Expression
Hypotheses mnuprdlem1.1 F = A B
mnuprdlem1.3 φ A U
mnuprdlem1.4 φ B U
mnuprdlem1.8 φ i u F i u u w
Assertion mnuprdlem1 φ A w

Proof

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