Metamath Proof Explorer

Theorem mnuop3d

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

		Ref	Expression
	Hypotheses	mnuop3d.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))))\}$
		mnuop3d.2	$⊢ φ \to U \in M$
		mnuop3d.3	$⊢ φ \to A \in U$
		mnuop3d.4	$⊢ φ \to F \subseteq U$
	Assertion	mnuop3d	$⊢ φ \to \exists w \in U \forall i \in A (\exists v \in F i \in v \to \exists u \in F (i \in u \land ⋃ u \subseteq w))$

Proof

Step	Hyp	Ref	Expression
1		mnuop3d.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		mnuop3d.2	$⊢ φ \to U \in M$
3		mnuop3d.3	$⊢ φ \to A \in U$
4		mnuop3d.4	$⊢ φ \to F \subseteq U$
5	2 4	sselpwd	$⊢ φ \to F \in 𝒫 U$
6	1 2 3 5	mnuop23d	$⊢ φ \to \exists w \in U (𝒫 A \subseteq w \land \forall i \in A (\exists v \in U (i \in v \land v \in F) \to \exists u \in F (i \in u \land ⋃ u \subseteq w)))$
7	4	sseld	$⊢ φ \to (v \in F \to v \in U)$
8	7	adantrd	$⊢ φ \to ((v \in F \land i \in v) \to v \in U)$
9		pm3.22	$⊢ (v \in F \land i \in v) \to (i \in v \land v \in F)$
10	8 9	jca2	$⊢ φ \to ((v \in F \land i \in v) \to (v \in U \land (i \in v \land v \in F)))$
11	10	reximdv2	$⊢ φ \to (\exists v \in F i \in v \to \exists v \in U (i \in v \land v \in F))$
12	11	imim1d	$⊢ φ \to ((\exists v \in U (i \in v \land v \in F) \to \exists u \in F (i \in u \land ⋃ u \subseteq w)) \to (\exists v \in F i \in v \to \exists u \in F (i \in u \land ⋃ u \subseteq w)))$
13	12	ralimdv	$⊢ φ \to (\forall i \in A (\exists v \in U (i \in v \land v \in F) \to \exists u \in F (i \in u \land ⋃ u \subseteq w)) \to \forall i \in A (\exists v \in F i \in v \to \exists u \in F (i \in u \land ⋃ u \subseteq w)))$
14	13	adantld	$⊢ φ \to ((𝒫 A \subseteq w \land \forall i \in A (\exists v \in U (i \in v \land v \in F) \to \exists u \in F (i \in u \land ⋃ u \subseteq w))) \to \forall i \in A (\exists v \in F i \in v \to \exists u \in F (i \in u \land ⋃ u \subseteq w)))$
15	14	reximdv	$⊢ φ \to (\exists w \in U (𝒫 A \subseteq w \land \forall i \in A (\exists v \in U (i \in v \land v \in F) \to \exists u \in F (i \in u \land ⋃ u \subseteq w))) \to \exists w \in U \forall i \in A (\exists v \in F i \in v \to \exists u \in F (i \in u \land ⋃ u \subseteq w)))$
16	6 15	mpd	$⊢ φ \to \exists w \in U \forall i \in A (\exists v \in F i \in v \to \exists u \in F (i \in u \land ⋃ u \subseteq w))$