Metamath Proof Explorer

Theorem mnuop23d

Description: Second and third operations of a minimal universe. (Contributed by Rohan Ridenour, 13-Aug-2023)

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

Proof

Step Hyp Ref Expression
1 mnuop23d.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 mnuop23d.2 ⊢φ→U∈M
3 mnuop23d.3 ⊢φ→A∈U
4 mnuop23d.4 ⊢φ→F∈V
5 1 2 3 mnuop123d ⊢φ→𝒫A⊆U∧∀f∃w∈U𝒫A⊆w∧∀i∈A∃v∈Ui∈v∧v∈f→∃u∈fi∈u∧⋃u⊆w
6 5 simprd ⊢φ→∀f∃w∈U𝒫A⊆w∧∀i∈A∃v∈Ui∈v∧v∈f→∃u∈fi∈u∧⋃u⊆w
7 eleq2 ⊢f=F→v∈f↔v∈F
8 7 anbi2d ⊢f=F→i∈v∧v∈f↔i∈v∧v∈F
9 8 rexbidv ⊢f=F→∃v∈Ui∈v∧v∈f↔∃v∈Ui∈v∧v∈F
10 rexeq ⊢f=F→∃u∈fi∈u∧⋃u⊆w↔∃u∈Fi∈u∧⋃u⊆w
11 9 10 imbi12d ⊢f=F→∃v∈Ui∈v∧v∈f→∃u∈fi∈u∧⋃u⊆w↔∃v∈Ui∈v∧v∈F→∃u∈Fi∈u∧⋃u⊆w
12 11 ralbidv ⊢f=F→∀i∈A∃v∈Ui∈v∧v∈f→∃u∈fi∈u∧⋃u⊆w↔∀i∈A∃v∈Ui∈v∧v∈F→∃u∈Fi∈u∧⋃u⊆w
13 12 anbi2d ⊢f=F→𝒫A⊆w∧∀i∈A∃v∈Ui∈v∧v∈f→∃u∈fi∈u∧⋃u⊆w↔𝒫A⊆w∧∀i∈A∃v∈Ui∈v∧v∈F→∃u∈Fi∈u∧⋃u⊆w
14 13 rexbidv ⊢f=F→∃w∈U𝒫A⊆w∧∀i∈A∃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
15 14 spcgv ⊢F∈V→∀f∃w∈U𝒫A⊆w∧∀i∈A∃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
16 4 6 15 sylc ⊢φ→∃w∈U𝒫A⊆w∧∀i∈A∃v∈Ui∈v∧v∈F→∃u∈Fi∈u∧⋃u⊆w