mnuprdlem4

Description: Lemma for mnuprd . General case. (Contributed by Rohan Ridenour, 13-Aug-2023)

	Ref	Expression
Hypotheses	mnuprdlem4.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))))\}$
	mnuprdlem4.2	$⊢ F = \{\{\emptyset, \{A\}\}, \{\{\emptyset\}, \{B\}\}\}$
	mnuprdlem4.3	$⊢ φ \to U \in M$
	mnuprdlem4.4	$⊢ φ \to A \in U$
	mnuprdlem4.5	$⊢ φ \to B \in U$
	mnuprdlem4.6	$⊢ φ \to \neg A = \emptyset$
Assertion	mnuprdlem4	$⊢ φ \to \{A, B\} \in U$

Proof

Step	Hyp	Ref	Expression
1		mnuprdlem4.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		mnuprdlem4.2	$⊢ F = \{\{\emptyset, \{A\}\}, \{\{\emptyset\}, \{B\}\}\}$
3		mnuprdlem4.3	$⊢ φ \to U \in M$
4		mnuprdlem4.4	$⊢ φ \to A \in U$
5		mnuprdlem4.5	$⊢ φ \to B \in U$
6		mnuprdlem4.6	$⊢ φ \to \neg A = \emptyset$
7	1 3 4	mnu0eld	$⊢ φ \to \emptyset \in U$
8	1 3 7	mnusnd	$⊢ φ \to \{\emptyset\} \in U$
9		0ss	$⊢ \emptyset \subseteq \{\emptyset\}$
10		ssid	$⊢ \{\emptyset\} \subseteq \{\emptyset\}$
11	1 3 8 9 10	mnuprss2d	$⊢ φ \to \{\emptyset, \{\emptyset\}\} \in U$
12	1 3 4	mnusnd	$⊢ φ \to \{A\} \in U$
13		0ss	$⊢ \emptyset \subseteq \{A\}$
14		ssid	$⊢ \{A\} \subseteq \{A\}$
15	1 3 12 13 14	mnuprss2d	$⊢ φ \to \{\emptyset, \{A\}\} \in U$
16		0ss	$⊢ \emptyset \subseteq B$
17		ssid	$⊢ B \subseteq B$
18	1 3 5 16 17	mnuprss2d	$⊢ φ \to \{\emptyset, B\} \in U$
19		snsspr1	$⊢ \{\emptyset\} \subseteq \{\emptyset, B\}$
20		snsspr2	$⊢ \{B\} \subseteq \{\emptyset, B\}$
21	1 3 18 19 20	mnuprss2d	$⊢ φ \to \{\{\emptyset\}, \{B\}\} \in U$
22	15 21	prssd	$⊢ φ \to \{\{\emptyset, \{A\}\}, \{\{\emptyset\}, \{B\}\}\} \subseteq U$
23	2 22	eqsstrid	$⊢ φ \to F \subseteq U$
24	1 3 11 23	mnuop3d	$⊢ φ \to \exists w \in U \forall i \in \{\emptyset, \{\emptyset\}\} (\exists v \in F i \in v \to \exists u \in F (i \in u \land ⋃ u \subseteq w))$
25		simprl	$⊢ (φ \land (w \in U \land \forall i \in \{\emptyset, \{\emptyset\}\} (\exists v \in F i \in v \to \exists u \in F (i \in u \land ⋃ u \subseteq w)))) \to w \in U$
26		eleq2w	$⊢ a = w \to (A \in a \leftrightarrow A \in w)$
27		eleq2w	$⊢ a = w \to (B \in a \leftrightarrow B \in w)$
28	26 27	anbi12d	$⊢ a = w \to ((A \in a \land B \in a) \leftrightarrow (A \in w \land B \in w))$
29	28	adantl	$⊢ ((φ \land (w \in U \land \forall i \in \{\emptyset, \{\emptyset\}\} (\exists v \in F i \in v \to \exists u \in F (i \in u \land ⋃ u \subseteq w)))) \land a = w) \to ((A \in a \land B \in a) \leftrightarrow (A \in w \land B \in w))$
30	4	adantr	$⊢ (φ \land (w \in U \land \forall i \in \{\emptyset, \{\emptyset\}\} (\exists v \in F i \in v \to \exists u \in F (i \in u \land ⋃ u \subseteq w)))) \to A \in U$
31	5	adantr	$⊢ (φ \land (w \in U \land \forall i \in \{\emptyset, \{\emptyset\}\} (\exists v \in F i \in v \to \exists u \in F (i \in u \land ⋃ u \subseteq w)))) \to B \in U$
32		nfv	$⊢ Ⅎ i φ$
33		nfv	$⊢ Ⅎ i w \in U$
34		nfra1	$⊢ Ⅎ i \forall i \in \{\emptyset, \{\emptyset\}\} (\exists v \in F i \in v \to \exists u \in F (i \in u \land ⋃ u \subseteq w))$
35	33 34	nfan	$⊢ Ⅎ i (w \in U \land \forall i \in \{\emptyset, \{\emptyset\}\} (\exists v \in F i \in v \to \exists u \in F (i \in u \land ⋃ u \subseteq w)))$
36	32 35	nfan	$⊢ Ⅎ i (φ \land (w \in U \land \forall i \in \{\emptyset, \{\emptyset\}\} (\exists v \in F i \in v \to \exists u \in F (i \in u \land ⋃ u \subseteq w))))$
37	2 36	mnuprdlem3	$⊢ (φ \land (w \in U \land \forall i \in \{\emptyset, \{\emptyset\}\} (\exists v \in F i \in v \to \exists u \in F (i \in u \land ⋃ u \subseteq w)))) \to \forall i \in \{\emptyset, \{\emptyset\}\} \exists v \in F i \in v$
38		ralim	$⊢ \forall i \in \{\emptyset, \{\emptyset\}\} (\exists v \in F i \in v \to \exists u \in F (i \in u \land ⋃ u \subseteq w)) \to (\forall i \in \{\emptyset, \{\emptyset\}\} \exists v \in F i \in v \to \forall i \in \{\emptyset, \{\emptyset\}\} \exists u \in F (i \in u \land ⋃ u \subseteq w))$
39	38	ad2antll	$⊢ (φ \land (w \in U \land \forall i \in \{\emptyset, \{\emptyset\}\} (\exists v \in F i \in v \to \exists u \in F (i \in u \land ⋃ u \subseteq w)))) \to (\forall i \in \{\emptyset, \{\emptyset\}\} \exists v \in F i \in v \to \forall i \in \{\emptyset, \{\emptyset\}\} \exists u \in F (i \in u \land ⋃ u \subseteq w))$
40	37 39	mpd	$⊢ (φ \land (w \in U \land \forall i \in \{\emptyset, \{\emptyset\}\} (\exists v \in F i \in v \to \exists u \in F (i \in u \land ⋃ u \subseteq w)))) \to \forall i \in \{\emptyset, \{\emptyset\}\} \exists u \in F (i \in u \land ⋃ u \subseteq w)$
41	2 30 31 40	mnuprdlem1	$⊢ (φ \land (w \in U \land \forall i \in \{\emptyset, \{\emptyset\}\} (\exists v \in F i \in v \to \exists u \in F (i \in u \land ⋃ u \subseteq w)))) \to A \in w$
42	6	adantr	$⊢ (φ \land (w \in U \land \forall i \in \{\emptyset, \{\emptyset\}\} (\exists v \in F i \in v \to \exists u \in F (i \in u \land ⋃ u \subseteq w)))) \to \neg A = \emptyset$
43	2 31 42 40	mnuprdlem2	$⊢ (φ \land (w \in U \land \forall i \in \{\emptyset, \{\emptyset\}\} (\exists v \in F i \in v \to \exists u \in F (i \in u \land ⋃ u \subseteq w)))) \to B \in w$
44	41 43	jca	$⊢ (φ \land (w \in U \land \forall i \in \{\emptyset, \{\emptyset\}\} (\exists v \in F i \in v \to \exists u \in F (i \in u \land ⋃ u \subseteq w)))) \to (A \in w \land B \in w)$
45	25 29 44	rspcedvd	$⊢ (φ \land (w \in U \land \forall i \in \{\emptyset, \{\emptyset\}\} (\exists v \in F i \in v \to \exists u \in F (i \in u \land ⋃ u \subseteq w)))) \to \exists a \in U (A \in a \land B \in a)$
46	24 45	rexlimddv	$⊢ φ \to \exists a \in U (A \in a \land B \in a)$
47	3	adantr	$⊢ (φ \land (a \in U \land (A \in a \land B \in a))) \to U \in M$
48		simprl	$⊢ (φ \land (a \in U \land (A \in a \land B \in a))) \to a \in U$
49		simprrl	$⊢ (φ \land (a \in U \land (A \in a \land B \in a))) \to A \in a$
50		simprrr	$⊢ (φ \land (a \in U \land (A \in a \land B \in a))) \to B \in a$
51	49 50	prssd	$⊢ (φ \land (a \in U \land (A \in a \land B \in a))) \to \{A, B\} \subseteq a$
52	1 47 48 51	mnussd	$⊢ (φ \land (a \in U \land (A \in a \land B \in a))) \to \{A, B\} \in U$
53	46 52	rexlimddv	$⊢ φ \to \{A, B\} \in U$

Metamath Proof Explorer

Theorem mnuprdlem4

Proof