Metamath Proof Explorer

Theorem mnuop123d

Description: Operations of a minimal universe. (Contributed by Rohan Ridenour, 13-Aug-2023)

Ref Expression
Hypotheses mnuop123d.1 ⊢M=k|∀l∈k𝒫l⊆k∧∀m∃n∈k𝒫l⊆n∧∀p∈l∃q∈kp∈q∧q∈m→∃r∈mp∈r∧⋃r⊆n
mnuop123d.2 ⊢φ→U∈M
mnuop123d.3 ⊢φ→A∈U
Assertion mnuop123d ⊢φ→𝒫A⊆U∧∀f∃w∈U𝒫A⊆w∧∀i∈A∃v∈Ui∈v∧v∈f→∃u∈fi∈u∧⋃u⊆w

Proof

Step Hyp Ref Expression
1 mnuop123d.1 ⊢M=k|∀l∈k𝒫l⊆k∧∀m∃n∈k𝒫l⊆n∧∀p∈l∃q∈kp∈q∧q∈m→∃r∈mp∈r∧⋃r⊆n
2 mnuop123d.2 ⊢φ→U∈M
3 mnuop123d.3 ⊢φ→A∈U
4 pweq ⊢z=A→𝒫z=𝒫A
5 4 sseq1d ⊢z=A→𝒫z⊆U↔𝒫A⊆U
6 4 sseq1d ⊢z=A→𝒫z⊆w↔𝒫A⊆w
7 raleq ⊢z=A→∀i∈z∃v∈Ui∈v∧v∈f→∃u∈fi∈u∧⋃u⊆w↔∀i∈A∃v∈Ui∈v∧v∈f→∃u∈fi∈u∧⋃u⊆w
8 6 7 anbi12d ⊢z=A→𝒫z⊆w∧∀i∈z∃v∈Ui∈v∧v∈f→∃u∈fi∈u∧⋃u⊆w↔𝒫A⊆w∧∀i∈A∃v∈Ui∈v∧v∈f→∃u∈fi∈u∧⋃u⊆w
9 8 rexbidv ⊢z=A→∃w∈U𝒫z⊆w∧∀i∈z∃v∈Ui∈v∧v∈f→∃u∈fi∈u∧⋃u⊆w↔∃w∈U𝒫A⊆w∧∀i∈A∃v∈Ui∈v∧v∈f→∃u∈fi∈u∧⋃u⊆w
10 9 albidv ⊢z=A→∀f∃w∈U𝒫z⊆w∧∀i∈z∃v∈Ui∈v∧v∈f→∃u∈fi∈u∧⋃u⊆w↔∀f∃w∈U𝒫A⊆w∧∀i∈A∃v∈Ui∈v∧v∈f→∃u∈fi∈u∧⋃u⊆w
11 5 10 anbi12d ⊢z=A→𝒫z⊆U∧∀f∃w∈U𝒫z⊆w∧∀i∈z∃v∈Ui∈v∧v∈f→∃u∈fi∈u∧⋃u⊆w↔𝒫A⊆U∧∀f∃w∈U𝒫A⊆w∧∀i∈A∃v∈Ui∈v∧v∈f→∃u∈fi∈u∧⋃u⊆w
12 1 ismnu ⊢U∈M→U∈M↔∀z∈U𝒫z⊆U∧∀f∃w∈U𝒫z⊆w∧∀i∈z∃v∈Ui∈v∧v∈f→∃u∈fi∈u∧⋃u⊆w
13 12 ibi ⊢U∈M→∀z∈U𝒫z⊆U∧∀f∃w∈U𝒫z⊆w∧∀i∈z∃v∈Ui∈v∧v∈f→∃u∈fi∈u∧⋃u⊆w
14 2 13 syl ⊢φ→∀z∈U𝒫z⊆U∧∀f∃w∈U𝒫z⊆w∧∀i∈z∃v∈Ui∈v∧v∈f→∃u∈fi∈u∧⋃u⊆w
15 11 14 3 rspcdva ⊢φ→𝒫A⊆U∧∀f∃w∈U𝒫A⊆w∧∀i∈A∃v∈Ui∈v∧v∈f→∃u∈fi∈u∧⋃u⊆w