Metamath Proof Explorer


Theorem mnuprdlem4

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

Ref Expression
Hypotheses mnuprdlem4.1 M = k | l k 𝒫 l k m n k 𝒫 l n p l q k p q q m r m p r r n
mnuprdlem4.2 F = A B
mnuprdlem4.3 φ U M
mnuprdlem4.4 φ A U
mnuprdlem4.5 φ B U
mnuprdlem4.6 φ ¬ A =
Assertion mnuprdlem4 φ A B U

Proof

Step Hyp Ref Expression
1 mnuprdlem4.1 M = k | l k 𝒫 l k m n k 𝒫 l n p l q k p q q m r m p r r n
2 mnuprdlem4.2 F = A B
3 mnuprdlem4.3 φ U M
4 mnuprdlem4.4 φ A U
5 mnuprdlem4.5 φ B U
6 mnuprdlem4.6 φ ¬ A =
7 1 3 4 mnu0eld φ U
8 1 3 7 mnusnd φ U
9 0ss
10 ssid
11 1 3 8 9 10 mnuprss2d φ U
12 1 3 4 mnusnd φ A U
13 0ss A
14 ssid A A
15 1 3 12 13 14 mnuprss2d φ A U
16 0ss B
17 ssid B B
18 1 3 5 16 17 mnuprss2d φ B U
19 snsspr1 B
20 snsspr2 B B
21 1 3 18 19 20 mnuprss2d φ B U
22 15 21 prssd φ A B U
23 2 22 eqsstrid φ F U
24 1 3 11 23 mnuop3d φ w U i v F i v u F i u u w
25 simprl φ w U i v F i v u F i u u w w U
26 eleq2w a = w A a A w
27 eleq2w a = w B a B w
28 26 27 anbi12d a = w A a B a A w B w
29 28 adantl φ w U i v F i v u F i u u w a = w A a B a A w B w
30 4 adantr φ w U i v F i v u F i u u w A U
31 5 adantr φ w U i v F i v u F i u u w B U
32 nfv i φ
33 nfv i w U
34 nfra1 i i v F i v u F i u u w
35 33 34 nfan i w U i v F i v u F i u u w
36 32 35 nfan i φ w U i v F i v u F i u u w
37 2 36 mnuprdlem3 φ w U i v F i v u F i u u w i v F i v
38 ralim i v F i v u F i u u w i v F i v i u F i u u w
39 38 ad2antll φ w U i v F i v u F i u u w i v F i v i u F i u u w
40 37 39 mpd φ w U i v F i v u F i u u w i u F i u u w
41 2 30 31 40 mnuprdlem1 φ w U i v F i v u F i u u w A w
42 6 adantr φ w U i v F i v u F i u u w ¬ A =
43 2 31 42 40 mnuprdlem2 φ w U i v F i v u F i u u w B w
44 41 43 jca φ w U i v F i v u F i u u w A w B w
45 25 29 44 rspcedvd φ w U i v F i v u F i u u w a U A a B a
46 24 45 rexlimddv φ a U A a B a
47 3 adantr φ a U A a B a U M
48 simprl φ a U A a B a a U
49 simprrl φ a U A a B a A a
50 simprrr φ a U A a B a B a
51 49 50 prssd φ a U A a B a A B a
52 1 47 48 51 mnussd φ a U A a B a A B U
53 46 52 rexlimddv φ A B U