Metamath Proof Explorer


Theorem ismnuprim

Description: Express the predicate on U in ismnu using only primitives. (Contributed by Rohan Ridenour, 13-Aug-2023)

Ref Expression
Assertion ismnuprim z U 𝒫 z U f w U 𝒫 z w i z v U i v v f u f i u u w z z U f ¬ w w U ¬ v ¬ t t v t z ¬ v U ¬ v w ¬ i i z v U i v v f ¬ u u f i u ¬ o o u s s o s w

Proof

Step Hyp Ref Expression
1 19.28v f 𝒫 z U w U 𝒫 z w i z v U i v v f u f i u u w 𝒫 z U f w U 𝒫 z w i z v U i v v f u f i u u w
2 r19.42v w U 𝒫 z U 𝒫 z w i z v U i v v f u f i u u w 𝒫 z U w U 𝒫 z w i z v U i v v f u f i u u w
3 19.26 v v z v U v w i z v U i v v f u f i u u w v v z v U v w v i z v U i v v f u f i u u w
4 19.26 v v z v U v z v w v v z v U v v z v w
5 jcab v z v U v w v z v U v z v w
6 5 albii v v z v U v w v v z v U v z v w
7 pwss 𝒫 z U v v z v U
8 pwss 𝒫 z w v v z v w
9 7 8 anbi12i 𝒫 z U 𝒫 z w v v z v U v v z v w
10 4 6 9 3bitr4i v v z v U v w 𝒫 z U 𝒫 z w
11 ralcom4 i z v v U i v v f u f i u u w v i z v U i v v f u f i u u w
12 19.23v v v U i v v f u f i u u w v v U i v v f u f i u u w
13 3anass v U i v v f v U i v v f
14 13 exbii v v U i v v f v v U i v v f
15 df-rex v U i v v f v v U i v v f
16 14 15 bitr4i v v U i v v f v U i v v f
17 16 imbi1i v v U i v v f u f i u u w v U i v v f u f i u u w
18 12 17 bitri v v U i v v f u f i u u w v U i v v f u f i u u w
19 18 ralbii i z v v U i v v f u f i u u w i z v U i v v f u f i u u w
20 11 19 bitr3i v i z v U i v v f u f i u u w i z v U i v v f u f i u u w
21 10 20 anbi12i v v z v U v w v i z v U i v v f u f i u u w 𝒫 z U 𝒫 z w i z v U i v v f u f i u u w
22 anass 𝒫 z U 𝒫 z w i z v U i v v f u f i u u w 𝒫 z U 𝒫 z w i z v U i v v f u f i u u w
23 21 22 bitri v v z v U v w v i z v U i v v f u f i u u w 𝒫 z U 𝒫 z w i z v U i v v f u f i u u w
24 3 23 bitri v v z v U v w i z v U i v v f u f i u u w 𝒫 z U 𝒫 z w i z v U i v v f u f i u u w
25 dfss2 v z t t v t z
26 df-an v U v w ¬ v U ¬ v w
27 25 26 imbi12i v z v U v w t t v t z ¬ v U ¬ v w
28 3impexp v U i v v f u f i u u w v U i v v f u f i u u w
29 biid i u i u
30 expanduniss u w o o u s s o s w
31 29 30 expandan i u u w ¬ i u ¬ o o u s s o s w
32 31 expandrexn u f i u u w ¬ u u f i u ¬ o o u s s o s w
33 32 imbi2i v f u f i u u w v f ¬ u u f i u ¬ o o u s s o s w
34 33 imbi2i i v v f u f i u u w i v v f ¬ u u f i u ¬ o o u s s o s w
35 34 imbi2i v U i v v f u f i u u w v U i v v f ¬ u u f i u ¬ o o u s s o s w
36 28 35 bitri v U i v v f u f i u u w v U i v v f ¬ u u f i u ¬ o o u s s o s w
37 36 expandral i z v U i v v f u f i u u w i i z v U i v v f ¬ u u f i u ¬ o o u s s o s w
38 27 37 expandan v z v U v w i z v U i v v f u f i u u w ¬ t t v t z ¬ v U ¬ v w ¬ i i z v U i v v f ¬ u u f i u ¬ o o u s s o s w
39 38 albii v v z v U v w i z v U i v v f u f i u u w v ¬ t t v t z ¬ v U ¬ v w ¬ i i z v U i v v f ¬ u u f i u ¬ o o u s s o s w
40 24 39 bitr3i 𝒫 z U 𝒫 z w i z v U i v v f u f i u u w v ¬ t t v t z ¬ v U ¬ v w ¬ i i z v U i v v f ¬ u u f i u ¬ o o u s s o s w
41 40 expandrex w U 𝒫 z U 𝒫 z w i z v U i v v f u f i u u w ¬ w w U ¬ v ¬ t t v t z ¬ v U ¬ v w ¬ i i z v U i v v f ¬ u u f i u ¬ o o u s s o s w
42 2 41 bitr3i 𝒫 z U w U 𝒫 z w i z v U i v v f u f i u u w ¬ w w U ¬ v ¬ t t v t z ¬ v U ¬ v w ¬ i i z v U i v v f ¬ u u f i u ¬ o o u s s o s w
43 42 albii f 𝒫 z U w U 𝒫 z w i z v U i v v f u f i u u w f ¬ w w U ¬ v ¬ t t v t z ¬ v U ¬ v w ¬ i i z v U i v v f ¬ u u f i u ¬ o o u s s o s w
44 1 43 bitr3i 𝒫 z U f w U 𝒫 z w i z v U i v v f u f i u u w f ¬ w w U ¬ v ¬ t t v t z ¬ v U ¬ v w ¬ i i z v U i v v f ¬ u u f i u ¬ o o u s s o s w
45 44 expandral z U 𝒫 z U f w U 𝒫 z w i z v U i v v f u f i u u w z z U f ¬ w w U ¬ v ¬ t t v t z ¬ v U ¬ v w ¬ i i z v U i v v f ¬ u u f i u ¬ o o u s s o s w