ismnuprim

Description: Express the predicate on U in ismnu using only primitives. (Contributed by Rohan Ridenour, 13-Aug-2023)

		Ref	Expression
	Assertion	ismnuprim	$⊢ \forall z \in U (𝒫 z \subseteq U \land \forall f \exists w \in U (𝒫 z \subseteq w \land \forall i \in z (\exists v \in U (i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w)))) \leftrightarrow \forall z (z \in U \to \forall f \neg \forall w (w \in U \to \neg \forall v \neg ((\forall t (t \in v \to t \in z) \to \neg (v \in U \to \neg v \in w)) \to \neg \forall i (i \in z \to (v \in U \to (i \in v \to (v \in f \to \neg \forall u (u \in f \to (i \in u \to \neg \forall o (o \in u \to \forall s (s \in o \to s \in w)))))))))))$

Proof

Step	Hyp	Ref	Expression
1		19.28v	$⊢ \forall f (𝒫 z \subseteq U \land \exists w \in U (𝒫 z \subseteq w \land \forall i \in z (\exists v \in U (i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w)))) \leftrightarrow (𝒫 z \subseteq U \land \forall f \exists w \in U (𝒫 z \subseteq w \land \forall i \in z (\exists v \in U (i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w))))$
2		r19.42v	$⊢ \exists w \in U (𝒫 z \subseteq U \land (𝒫 z \subseteq w \land \forall i \in z (\exists v \in U (i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w)))) \leftrightarrow (𝒫 z \subseteq U \land \exists w \in U (𝒫 z \subseteq w \land \forall i \in z (\exists v \in U (i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w))))$
3		19.26	$⊢ \forall v ((v \subseteq z \to (v \in U \land v \in w)) \land \forall i \in z ((v \in U \land i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w))) \leftrightarrow (\forall v (v \subseteq z \to (v \in U \land v \in w)) \land \forall v \forall i \in z ((v \in U \land i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w)))$
4		19.26	$⊢ \forall v ((v \subseteq z \to v \in U) \land (v \subseteq z \to v \in w)) \leftrightarrow (\forall v (v \subseteq z \to v \in U) \land \forall v (v \subseteq z \to v \in w))$
5		jcab	$⊢ (v \subseteq z \to (v \in U \land v \in w)) \leftrightarrow ((v \subseteq z \to v \in U) \land (v \subseteq z \to v \in w))$
6	5	albii	$⊢ \forall v (v \subseteq z \to (v \in U \land v \in w)) \leftrightarrow \forall v ((v \subseteq z \to v \in U) \land (v \subseteq z \to v \in w))$
7		pwss	$⊢ 𝒫 z \subseteq U \leftrightarrow \forall v (v \subseteq z \to v \in U)$
8		pwss	$⊢ 𝒫 z \subseteq w \leftrightarrow \forall v (v \subseteq z \to v \in w)$
9	7 8	anbi12i	$⊢ (𝒫 z \subseteq U \land 𝒫 z \subseteq w) \leftrightarrow (\forall v (v \subseteq z \to v \in U) \land \forall v (v \subseteq z \to v \in w))$
10	4 6 9	3bitr4i	$⊢ \forall v (v \subseteq z \to (v \in U \land v \in w)) \leftrightarrow (𝒫 z \subseteq U \land 𝒫 z \subseteq w)$
11		ralcom4	$⊢ \forall i \in z \forall v ((v \in U \land i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w)) \leftrightarrow \forall v \forall i \in z ((v \in U \land i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w))$
12		19.23v	$⊢ \forall v ((v \in U \land i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w)) \leftrightarrow (\exists v (v \in U \land i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w))$
13		3anass	$⊢ (v \in U \land i \in v \land v \in f) \leftrightarrow (v \in U \land (i \in v \land v \in f))$
14	13	exbii	$⊢ \exists v (v \in U \land i \in v \land v \in f) \leftrightarrow \exists v (v \in U \land (i \in v \land v \in f))$
15		df-rex	$⊢ \exists v \in U (i \in v \land v \in f) \leftrightarrow \exists v (v \in U \land (i \in v \land v \in f))$
16	14 15	bitr4i	$⊢ \exists v (v \in U \land i \in v \land v \in f) \leftrightarrow \exists v \in U (i \in v \land v \in f)$
17	16	imbi1i	$⊢ (\exists v (v \in U \land i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w)) \leftrightarrow (\exists v \in U (i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w))$
18	12 17	bitri	$⊢ \forall v ((v \in U \land i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w)) \leftrightarrow (\exists v \in U (i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w))$
19	18	ralbii	$⊢ \forall i \in z \forall v ((v \in U \land i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w)) \leftrightarrow \forall i \in z (\exists v \in U (i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w))$
20	11 19	bitr3i	$⊢ \forall v \forall i \in z ((v \in U \land i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w)) \leftrightarrow \forall i \in z (\exists v \in U (i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w))$
21	10 20	anbi12i	$⊢ (\forall v (v \subseteq z \to (v \in U \land v \in w)) \land \forall v \forall i \in z ((v \in U \land i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w))) \leftrightarrow ((𝒫 z \subseteq U \land 𝒫 z \subseteq w) \land \forall i \in z (\exists v \in U (i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w)))$
22		anass	$⊢ ((𝒫 z \subseteq U \land 𝒫 z \subseteq w) \land \forall i \in z (\exists v \in U (i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w))) \leftrightarrow (𝒫 z \subseteq U \land (𝒫 z \subseteq w \land \forall i \in z (\exists v \in U (i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w))))$
23	21 22	bitri	$⊢ (\forall v (v \subseteq z \to (v \in U \land v \in w)) \land \forall v \forall i \in z ((v \in U \land i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w))) \leftrightarrow (𝒫 z \subseteq U \land (𝒫 z \subseteq w \land \forall i \in z (\exists v \in U (i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w))))$
24	3 23	bitri	$⊢ \forall v ((v \subseteq z \to (v \in U \land v \in w)) \land \forall i \in z ((v \in U \land i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w))) \leftrightarrow (𝒫 z \subseteq U \land (𝒫 z \subseteq w \land \forall i \in z (\exists v \in U (i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w))))$
25		df-ss	$⊢ v \subseteq z \leftrightarrow \forall t (t \in v \to t \in z)$
26		df-an	$⊢ (v \in U \land v \in w) \leftrightarrow \neg (v \in U \to \neg v \in w)$
27	25 26	imbi12i	$⊢ (v \subseteq z \to (v \in U \land v \in w)) \leftrightarrow (\forall t (t \in v \to t \in z) \to \neg (v \in U \to \neg v \in w))$
28		3impexp	$⊢ ((v \in U \land i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w)) \leftrightarrow (v \in U \to (i \in v \to (v \in f \to \exists u \in f (i \in u \land ⋃ u \subseteq w))))$
29		biid	$⊢ i \in u \leftrightarrow i \in u$
30		expanduniss	$⊢ ⋃ u \subseteq w \leftrightarrow \forall o (o \in u \to \forall s (s \in o \to s \in w))$
31	29 30	expandan	$⊢ (i \in u \land ⋃ u \subseteq w) \leftrightarrow \neg (i \in u \to \neg \forall o (o \in u \to \forall s (s \in o \to s \in w)))$
32	31	expandrexn	$⊢ \exists u \in f (i \in u \land ⋃ u \subseteq w) \leftrightarrow \neg \forall u (u \in f \to (i \in u \to \neg \forall o (o \in u \to \forall s (s \in o \to s \in w))))$
33	32	imbi2i	$⊢ (v \in f \to \exists u \in f (i \in u \land ⋃ u \subseteq w)) \leftrightarrow (v \in f \to \neg \forall u (u \in f \to (i \in u \to \neg \forall o (o \in u \to \forall s (s \in o \to s \in w)))))$
34	33	imbi2i	$⊢ (i \in v \to (v \in f \to \exists u \in f (i \in u \land ⋃ u \subseteq w))) \leftrightarrow (i \in v \to (v \in f \to \neg \forall u (u \in f \to (i \in u \to \neg \forall o (o \in u \to \forall s (s \in o \to s \in w))))))$
35	34	imbi2i	$⊢ (v \in U \to (i \in v \to (v \in f \to \exists u \in f (i \in u \land ⋃ u \subseteq w)))) \leftrightarrow (v \in U \to (i \in v \to (v \in f \to \neg \forall u (u \in f \to (i \in u \to \neg \forall o (o \in u \to \forall s (s \in o \to s \in w)))))))$
36	28 35	bitri	$⊢ ((v \in U \land i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w)) \leftrightarrow (v \in U \to (i \in v \to (v \in f \to \neg \forall u (u \in f \to (i \in u \to \neg \forall o (o \in u \to \forall s (s \in o \to s \in w)))))))$
37	36	expandral	$⊢ \forall i \in z ((v \in U \land i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w)) \leftrightarrow \forall i (i \in z \to (v \in U \to (i \in v \to (v \in f \to \neg \forall u (u \in f \to (i \in u \to \neg \forall o (o \in u \to \forall s (s \in o \to s \in w))))))))$
38	27 37	expandan	$⊢ ((v \subseteq z \to (v \in U \land v \in w)) \land \forall i \in z ((v \in U \land i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w))) \leftrightarrow \neg ((\forall t (t \in v \to t \in z) \to \neg (v \in U \to \neg v \in w)) \to \neg \forall i (i \in z \to (v \in U \to (i \in v \to (v \in f \to \neg \forall u (u \in f \to (i \in u \to \neg \forall o (o \in u \to \forall s (s \in o \to s \in w)))))))))$
39	38	albii	$⊢ \forall v ((v \subseteq z \to (v \in U \land v \in w)) \land \forall i \in z ((v \in U \land i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w))) \leftrightarrow \forall v \neg ((\forall t (t \in v \to t \in z) \to \neg (v \in U \to \neg v \in w)) \to \neg \forall i (i \in z \to (v \in U \to (i \in v \to (v \in f \to \neg \forall u (u \in f \to (i \in u \to \neg \forall o (o \in u \to \forall s (s \in o \to s \in w)))))))))$
40	24 39	bitr3i	$⊢ (𝒫 z \subseteq U \land (𝒫 z \subseteq w \land \forall i \in z (\exists v \in U (i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w)))) \leftrightarrow \forall v \neg ((\forall t (t \in v \to t \in z) \to \neg (v \in U \to \neg v \in w)) \to \neg \forall i (i \in z \to (v \in U \to (i \in v \to (v \in f \to \neg \forall u (u \in f \to (i \in u \to \neg \forall o (o \in u \to \forall s (s \in o \to s \in w)))))))))$
41	40	expandrex	$⊢ \exists w \in U (𝒫 z \subseteq U \land (𝒫 z \subseteq w \land \forall i \in z (\exists v \in U (i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w)))) \leftrightarrow \neg \forall w (w \in U \to \neg \forall v \neg ((\forall t (t \in v \to t \in z) \to \neg (v \in U \to \neg v \in w)) \to \neg \forall i (i \in z \to (v \in U \to (i \in v \to (v \in f \to \neg \forall u (u \in f \to (i \in u \to \neg \forall o (o \in u \to \forall s (s \in o \to s \in w))))))))))$
42	2 41	bitr3i	$⊢ (𝒫 z \subseteq U \land \exists w \in U (𝒫 z \subseteq w \land \forall i \in z (\exists v \in U (i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w)))) \leftrightarrow \neg \forall w (w \in U \to \neg \forall v \neg ((\forall t (t \in v \to t \in z) \to \neg (v \in U \to \neg v \in w)) \to \neg \forall i (i \in z \to (v \in U \to (i \in v \to (v \in f \to \neg \forall u (u \in f \to (i \in u \to \neg \forall o (o \in u \to \forall s (s \in o \to s \in w))))))))))$
43	42	albii	$⊢ \forall f (𝒫 z \subseteq U \land \exists w \in U (𝒫 z \subseteq w \land \forall i \in z (\exists v \in U (i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w)))) \leftrightarrow \forall f \neg \forall w (w \in U \to \neg \forall v \neg ((\forall t (t \in v \to t \in z) \to \neg (v \in U \to \neg v \in w)) \to \neg \forall i (i \in z \to (v \in U \to (i \in v \to (v \in f \to \neg \forall u (u \in f \to (i \in u \to \neg \forall o (o \in u \to \forall s (s \in o \to s \in w))))))))))$
44	1 43	bitr3i	$⊢ (𝒫 z \subseteq U \land \forall f \exists w \in U (𝒫 z \subseteq w \land \forall i \in z (\exists v \in U (i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w)))) \leftrightarrow \forall f \neg \forall w (w \in U \to \neg \forall v \neg ((\forall t (t \in v \to t \in z) \to \neg (v \in U \to \neg v \in w)) \to \neg \forall i (i \in z \to (v \in U \to (i \in v \to (v \in f \to \neg \forall u (u \in f \to (i \in u \to \neg \forall o (o \in u \to \forall s (s \in o \to s \in w))))))))))$
45	44	expandral	$⊢ \forall z \in U (𝒫 z \subseteq U \land \forall f \exists w \in U (𝒫 z \subseteq w \land \forall i \in z (\exists v \in U (i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w)))) \leftrightarrow \forall z (z \in U \to \forall f \neg \forall w (w \in U \to \neg \forall v \neg ((\forall t (t \in v \to t \in z) \to \neg (v \in U \to \neg v \in w)) \to \neg \forall i (i \in z \to (v \in U \to (i \in v \to (v \in f \to \neg \forall u (u \in f \to (i \in u \to \neg \forall o (o \in u \to \forall s (s \in o \to s \in w)))))))))))$

Metamath Proof Explorer

Theorem ismnuprim

Proof