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 ∈ k p ∈ q ∧ q ∈ m → ∃ r ∈ m p ∈ r ∧ ⋃ r ⊆ n
mnuprss2d.2 ⊢ φ → U ∈ M
mnuprss2d.3 ⊢ φ → C ∈ U
mnuprss2d.4 ⊢ A ⊆ C
mnuprss2d.5 ⊢ B ⊆ C
Assertion mnuprss2d ⊢ φ → A B ∈ U

Proof

Step Hyp Ref Expression
1 mnuprss2d.1 ⊢ M = k | ∀ l ∈ k 𝒫 l ⊆ k ∧ ∀ m ∃ n ∈ k 𝒫 l ⊆ n ∧ ∀ p ∈ l ∃ q ∈ k p ∈ q ∧ q ∈ m → ∃ r ∈ m p ∈ 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 ⊢ φ → A B ∈ U