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∈Ui∈v∧v∈f→∃u∈fi∈u∧⋃u⊆w↔∀zz∈U→∀f¬∀ww∈U→¬∀v¬∀tt∈v→t∈z→¬v∈U→¬v∈w→¬∀ii∈z→v∈U→i∈v→v∈f→¬∀uu∈f→i∈u→¬∀oo∈u→∀ss∈o→s∈w

Proof

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