mnuss2d

Description: mnussd with arguments provided with an existential quantifier. (Contributed by Rohan Ridenour, 13-Aug-2023)

	Ref	Expression
Hypotheses	mnuss2d.1	$⊢ M = \{k \| \forall l \in k (𝒫 l \subseteq k \land \forall m \exists n \in k (𝒫 l \subseteq n \land \forall p \in l (\exists q \in k (p \in q \land q \in m) \to \exists r \in m (p \in r \land ⋃ r \subseteq n))))\}$
	mnuss2d.2	$⊢ φ \to U \in M$
	mnuss2d.3	$⊢ φ \to \exists x \in U A \subseteq x$
Assertion	mnuss2d	$⊢ φ \to A \in U$

Step	Hyp	Ref	Expression
1		mnuss2d.1	$⊢ M = \{k \| \forall l \in k (𝒫 l \subseteq k \land \forall m \exists n \in k (𝒫 l \subseteq n \land \forall p \in l (\exists q \in k (p \in q \land q \in m) \to \exists r \in m (p \in r \land ⋃ r \subseteq n))))\}$
2		mnuss2d.2	$⊢ φ \to U \in M$
3		mnuss2d.3	$⊢ φ \to \exists x \in U A \subseteq x$
4	2	adantr	$⊢ (φ \land (x \in U \land A \subseteq x)) \to U \in M$
5		simprl	$⊢ (φ \land (x \in U \land A \subseteq x)) \to x \in U$
6		simprr	$⊢ (φ \land (x \in U \land A \subseteq x)) \to A \subseteq x$
7	1 4 5 6	mnussd	$⊢ (φ \land (x \in U \land A \subseteq x)) \to A \in U$
8	3 7	rexlimddv	$⊢ φ \to A \in U$

Metamath Proof Explorer