mnurndlem2

Description: Lemma for mnurnd . Deduction theorem input. (Contributed by Rohan Ridenour, 13-Aug-2023)

	Ref	Expression
Hypotheses	mnurndlem2.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))))\}$
	mnurndlem2.2	$⊢ φ \to U \in M$
	mnurndlem2.3	$⊢ φ \to A \in U$
	mnurndlem2.4	$⊢ φ \to F : A ⟶ U$
	mnurndlem2.5	$⊢ A \in V$
Assertion	mnurndlem2	$⊢ φ \to ran F \in U$

Proof

Step	Hyp	Ref	Expression
1		mnurndlem2.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		mnurndlem2.2	$⊢ φ \to U \in M$
3		mnurndlem2.3	$⊢ φ \to A \in U$
4		mnurndlem2.4	$⊢ φ \to F : A ⟶ U$
5		mnurndlem2.5	$⊢ A \in V$
6	2	adantr	$⊢ (φ \land a \in A) \to U \in M$
7	3	adantr	$⊢ (φ \land a \in A) \to A \in U$
8		simpr	$⊢ (φ \land a \in A) \to a \in A$
9	1 6 7 8	mnutrcld	$⊢ (φ \land a \in A) \to a \in U$
10	4	ffvelrnda	$⊢ (φ \land a \in A) \to F (a) \in U$
11	1 6 10 7	mnuprd	$⊢ (φ \land a \in A) \to \{F (a), A\} \in U$
12	1 6 9 11	mnuprd	$⊢ (φ \land a \in A) \to \{a, \{F (a), A\}\} \in U$
13	12	ralrimiva	$⊢ φ \to \forall a \in A \{a, \{F (a), A\}\} \in U$
14		eqid	$⊢ (a \in A ⟼ \{a, \{F (a), A\}\}) = (a \in A ⟼ \{a, \{F (a), A\}\})$
15	14	rnmptss	$⊢ \forall a \in A \{a, \{F (a), A\}\} \in U \to ran (a \in A ⟼ \{a, \{F (a), A\}\}) \subseteq U$
16	13 15	syl	$⊢ φ \to ran (a \in A ⟼ \{a, \{F (a), A\}\}) \subseteq U$
17	1 2 3 16	mnuop3d	$⊢ φ \to \exists w \in U \forall i \in A (\exists v \in ran (a \in A ⟼ \{a, \{F (a), A\}\}) i \in v \to \exists u \in ran (a \in A ⟼ \{a, \{F (a), A\}\}) (i \in u \land ⋃ u \subseteq w))$
18		simprl	$⊢ (φ \land (w \in U \land \forall i \in A (\exists v \in ran (a \in A ⟼ \{a, \{F (a), A\}\}) i \in v \to \exists u \in ran (a \in A ⟼ \{a, \{F (a), A\}\}) (i \in u \land ⋃ u \subseteq w)))) \to w \in U$
19		sseq2	$⊢ b = w \to (ran F \subseteq b \leftrightarrow ran F \subseteq w)$
20	19	adantl	$⊢ ((φ \land (w \in U \land \forall i \in A (\exists v \in ran (a \in A ⟼ \{a, \{F (a), A\}\}) i \in v \to \exists u \in ran (a \in A ⟼ \{a, \{F (a), A\}\}) (i \in u \land ⋃ u \subseteq w)))) \land b = w) \to (ran F \subseteq b \leftrightarrow ran F \subseteq w)$
21	4	adantr	$⊢ (φ \land (w \in U \land \forall i \in A (\exists v \in ran (a \in A ⟼ \{a, \{F (a), A\}\}) i \in v \to \exists u \in ran (a \in A ⟼ \{a, \{F (a), A\}\}) (i \in u \land ⋃ u \subseteq w)))) \to F : A ⟶ U$
22		simprr	$⊢ (φ \land (w \in U \land \forall i \in A (\exists v \in ran (a \in A ⟼ \{a, \{F (a), A\}\}) i \in v \to \exists u \in ran (a \in A ⟼ \{a, \{F (a), A\}\}) (i \in u \land ⋃ u \subseteq w)))) \to \forall i \in A (\exists v \in ran (a \in A ⟼ \{a, \{F (a), A\}\}) i \in v \to \exists u \in ran (a \in A ⟼ \{a, \{F (a), A\}\}) (i \in u \land ⋃ u \subseteq w))$
23	21 5 22	mnurndlem1	$⊢ (φ \land (w \in U \land \forall i \in A (\exists v \in ran (a \in A ⟼ \{a, \{F (a), A\}\}) i \in v \to \exists u \in ran (a \in A ⟼ \{a, \{F (a), A\}\}) (i \in u \land ⋃ u \subseteq w)))) \to ran F \subseteq w$
24	18 20 23	rspcedvd	$⊢ (φ \land (w \in U \land \forall i \in A (\exists v \in ran (a \in A ⟼ \{a, \{F (a), A\}\}) i \in v \to \exists u \in ran (a \in A ⟼ \{a, \{F (a), A\}\}) (i \in u \land ⋃ u \subseteq w)))) \to \exists b \in U ran F \subseteq b$
25	17 24	rexlimddv	$⊢ φ \to \exists b \in U ran F \subseteq b$
26	1 2 25	mnuss2d	$⊢ φ \to ran F \in U$

Metamath Proof Explorer

Theorem mnurndlem2

Proof