Metamath Proof Explorer

Theorem mnuprss2d

Description: Special case of mnuprssd . (Contributed by Rohan Ridenour, 13-Aug-2023)

Ref Expression
Hypotheses mnuprss2d.1 ⊢M=k|∀l∈k𝒫l⊆k∧∀m∃n∈k𝒫l⊆n∧∀p∈l∃q∈kp∈q∧q∈m→∃r∈mp∈r∧⋃r⊆n
mnuprss2d.2 ⊢φ→U∈M
mnuprss2d.3 ⊢φ→C∈U
mnuprss2d.4 ⊢A⊆C
mnuprss2d.5 ⊢B⊆C
Assertion mnuprss2d ⊢φ→AB∈U

Proof

Step Hyp Ref Expression
1 mnuprss2d.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 mnuprss2d.2 ⊢φ→U∈M
3 mnuprss2d.3 ⊢φ→C∈U
4 mnuprss2d.4 ⊢A⊆C
5 mnuprss2d.5 ⊢B⊆C
6 4 a1i ⊢φ→A⊆C
7 5 a1i ⊢φ→B⊆C
8 1 2 3 6 7 mnuprssd ⊢φ→AB∈U