ismnushort

Description: Express the predicate on U and z in ismnu in a shorter form while avoiding complicated definitions. (Contributed by Rohan Ridenour, 10-Oct-2024)

		Ref	Expression
	Assertion	ismnushort	$⊢ \forall f \in 𝒫 U \exists w \in U (𝒫 z \subseteq U \cap w \land z \cap ⋃ f \subseteq ⋃ (f \cap 𝒫 𝒫 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))))$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (𝒫 z \subseteq U \cap w \land z \cap ⋃ f \subseteq ⋃ (f \cap 𝒫 𝒫 w)) \to 𝒫 z \subseteq U \cap w$
2	1	reximi	$⊢ \exists w \in U (𝒫 z \subseteq U \cap w \land z \cap ⋃ f \subseteq ⋃ (f \cap 𝒫 𝒫 w)) \to \exists w \in U 𝒫 z \subseteq U \cap w$
3	2	ralimi	$⊢ \forall f \in 𝒫 U \exists w \in U (𝒫 z \subseteq U \cap w \land z \cap ⋃ f \subseteq ⋃ (f \cap 𝒫 𝒫 w)) \to \forall f \in 𝒫 U \exists w \in U 𝒫 z \subseteq U \cap w$
4		0elpw	$⊢ \emptyset \in 𝒫 U$
5	4	a1i	$⊢ ⊤ \to \emptyset \in 𝒫 U$
6		biidd	$⊢ (⊤ \land f = \emptyset) \to (\exists w \in U 𝒫 z \subseteq U \cap w \leftrightarrow \exists w \in U 𝒫 z \subseteq U \cap w)$
7	5 6	rspcdv	$⊢ ⊤ \to (\forall f \in 𝒫 U \exists w \in U 𝒫 z \subseteq U \cap w \to \exists w \in U 𝒫 z \subseteq U \cap w)$
8	7	mptru	$⊢ \forall f \in 𝒫 U \exists w \in U 𝒫 z \subseteq U \cap w \to \exists w \in U 𝒫 z \subseteq U \cap w$
9		inss1	$⊢ U \cap w \subseteq U$
10		sstr2	$⊢ 𝒫 z \subseteq U \cap w \to (U \cap w \subseteq U \to 𝒫 z \subseteq U)$
11	9 10	mpi	$⊢ 𝒫 z \subseteq U \cap w \to 𝒫 z \subseteq U$
12	11	reximi	$⊢ \exists w \in U 𝒫 z \subseteq U \cap w \to \exists w \in U 𝒫 z \subseteq U$
13		rexex	$⊢ \exists w \in U 𝒫 z \subseteq U \to \exists w 𝒫 z \subseteq U$
14		ax5e	$⊢ \exists w 𝒫 z \subseteq U \to 𝒫 z \subseteq U$
15	13 14	syl	$⊢ \exists w \in U 𝒫 z \subseteq U \to 𝒫 z \subseteq U$
16	3 8 12 15	4syl	$⊢ \forall f \in 𝒫 U \exists w \in U (𝒫 z \subseteq U \cap w \land z \cap ⋃ f \subseteq ⋃ (f \cap 𝒫 𝒫 w)) \to 𝒫 z \subseteq U$
17		inss1	$⊢ U \cap g \subseteq U$
18		vex	$⊢ g \in V$
19	18	inex2	$⊢ U \cap g \in V$
20	19	elpw	$⊢ U \cap g \in 𝒫 U \leftrightarrow U \cap g \subseteq U$
21	17 20	mpbir	$⊢ U \cap g \in 𝒫 U$
22		unieq	$⊢ f = U \cap g \to ⋃ f = ⋃ (U \cap g)$
23	22	ineq2d	$⊢ f = U \cap g \to z \cap ⋃ f = z \cap ⋃ (U \cap g)$
24		ineq1	$⊢ f = U \cap g \to f \cap 𝒫 𝒫 w = (U \cap g) \cap 𝒫 𝒫 w$
25	24	unieqd	$⊢ f = U \cap g \to ⋃ (f \cap 𝒫 𝒫 w) = ⋃ ((U \cap g) \cap 𝒫 𝒫 w)$
26	23 25	sseq12d	$⊢ f = U \cap g \to (z \cap ⋃ f \subseteq ⋃ (f \cap 𝒫 𝒫 w) \leftrightarrow z \cap ⋃ (U \cap g) \subseteq ⋃ ((U \cap g) \cap 𝒫 𝒫 w))$
27	26	anbi2d	$⊢ f = U \cap g \to ((𝒫 z \subseteq U \cap w \land z \cap ⋃ f \subseteq ⋃ (f \cap 𝒫 𝒫 w)) \leftrightarrow (𝒫 z \subseteq U \cap w \land z \cap ⋃ (U \cap g) \subseteq ⋃ ((U \cap g) \cap 𝒫 𝒫 w)))$
28	27	rexbidv	$⊢ f = U \cap g \to (\exists w \in U (𝒫 z \subseteq U \cap w \land z \cap ⋃ f \subseteq ⋃ (f \cap 𝒫 𝒫 w)) \leftrightarrow \exists w \in U (𝒫 z \subseteq U \cap w \land z \cap ⋃ (U \cap g) \subseteq ⋃ ((U \cap g) \cap 𝒫 𝒫 w)))$
29	28	rspcv	$⊢ U \cap g \in 𝒫 U \to (\forall f \in 𝒫 U \exists w \in U (𝒫 z \subseteq U \cap w \land z \cap ⋃ f \subseteq ⋃ (f \cap 𝒫 𝒫 w)) \to \exists w \in U (𝒫 z \subseteq U \cap w \land z \cap ⋃ (U \cap g) \subseteq ⋃ ((U \cap g) \cap 𝒫 𝒫 w)))$
30	21 29	ax-mp	$⊢ \forall f \in 𝒫 U \exists w \in U (𝒫 z \subseteq U \cap w \land z \cap ⋃ f \subseteq ⋃ (f \cap 𝒫 𝒫 w)) \to \exists w \in U (𝒫 z \subseteq U \cap w \land z \cap ⋃ (U \cap g) \subseteq ⋃ ((U \cap g) \cap 𝒫 𝒫 w))$
31	30	alrimiv	$⊢ \forall f \in 𝒫 U \exists w \in U (𝒫 z \subseteq U \cap w \land z \cap ⋃ f \subseteq ⋃ (f \cap 𝒫 𝒫 w)) \to \forall g \exists w \in U (𝒫 z \subseteq U \cap w \land z \cap ⋃ (U \cap g) \subseteq ⋃ ((U \cap g) \cap 𝒫 𝒫 w))$
32		inss2	$⊢ U \cap w \subseteq w$
33		sstr2	$⊢ 𝒫 z \subseteq U \cap w \to (U \cap w \subseteq w \to 𝒫 z \subseteq w)$
34	32 33	mpi	$⊢ 𝒫 z \subseteq U \cap w \to 𝒫 z \subseteq w$
35		an12	$⊢ (v \in U \land (i \in v \land v \in g)) \leftrightarrow (i \in v \land (v \in U \land v \in g))$
36		elin	$⊢ v \in (U \cap g) \leftrightarrow (v \in U \land v \in g)$
37	36	bicomi	$⊢ (v \in U \land v \in g) \leftrightarrow v \in (U \cap g)$
38	37	anbi2i	$⊢ (i \in v \land (v \in U \land v \in g)) \leftrightarrow (i \in v \land v \in (U \cap g))$
39	35 38	bitri	$⊢ (v \in U \land (i \in v \land v \in g)) \leftrightarrow (i \in v \land v \in (U \cap g))$
40	39	exbii	$⊢ \exists v (v \in U \land (i \in v \land v \in g)) \leftrightarrow \exists v (i \in v \land v \in (U \cap g))$
41		df-rex	$⊢ \exists v \in U (i \in v \land v \in g) \leftrightarrow \exists v (v \in U \land (i \in v \land v \in g))$
42		eluni	$⊢ i \in ⋃ (U \cap g) \leftrightarrow \exists v (i \in v \land v \in (U \cap g))$
43	40 41 42	3bitr4i	$⊢ \exists v \in U (i \in v \land v \in g) \leftrightarrow i \in ⋃ (U \cap g)$
44		simp1	$⊢ (z \cap ⋃ (U \cap g) \subseteq ⋃ ((U \cap g) \cap 𝒫 𝒫 w) \land i \in z \land i \in ⋃ (U \cap g)) \to z \cap ⋃ (U \cap g) \subseteq ⋃ ((U \cap g) \cap 𝒫 𝒫 w)$
45		elin	$⊢ i \in (z \cap ⋃ (U \cap g)) \leftrightarrow (i \in z \land i \in ⋃ (U \cap g))$
46	45	biimpri	$⊢ (i \in z \land i \in ⋃ (U \cap g)) \to i \in (z \cap ⋃ (U \cap g))$
47	46	3adant1	$⊢ (z \cap ⋃ (U \cap g) \subseteq ⋃ ((U \cap g) \cap 𝒫 𝒫 w) \land i \in z \land i \in ⋃ (U \cap g)) \to i \in (z \cap ⋃ (U \cap g))$
48	44 47	sseldd	$⊢ (z \cap ⋃ (U \cap g) \subseteq ⋃ ((U \cap g) \cap 𝒫 𝒫 w) \land i \in z \land i \in ⋃ (U \cap g)) \to i \in ⋃ ((U \cap g) \cap 𝒫 𝒫 w)$
49		eluni	$⊢ i \in ⋃ ((U \cap g) \cap 𝒫 𝒫 w) \leftrightarrow \exists u (i \in u \land u \in ((U \cap g) \cap 𝒫 𝒫 w))$
50	48 49	sylib	$⊢ (z \cap ⋃ (U \cap g) \subseteq ⋃ ((U \cap g) \cap 𝒫 𝒫 w) \land i \in z \land i \in ⋃ (U \cap g)) \to \exists u (i \in u \land u \in ((U \cap g) \cap 𝒫 𝒫 w))$
51		elinel1	$⊢ u \in ((U \cap g) \cap 𝒫 𝒫 w) \to u \in (U \cap g)$
52	51	elin2d	$⊢ u \in ((U \cap g) \cap 𝒫 𝒫 w) \to u \in g$
53		elinel2	$⊢ u \in ((U \cap g) \cap 𝒫 𝒫 w) \to u \in 𝒫 𝒫 w$
54		elpwpw	$⊢ u \in 𝒫 𝒫 w \leftrightarrow (u \in V \land ⋃ u \subseteq w)$
55	54	simprbi	$⊢ u \in 𝒫 𝒫 w \to ⋃ u \subseteq w$
56	53 55	syl	$⊢ u \in ((U \cap g) \cap 𝒫 𝒫 w) \to ⋃ u \subseteq w$
57	52 56	jca	$⊢ u \in ((U \cap g) \cap 𝒫 𝒫 w) \to (u \in g \land ⋃ u \subseteq w)$
58	57	anim2i	$⊢ (i \in u \land u \in ((U \cap g) \cap 𝒫 𝒫 w)) \to (i \in u \land (u \in g \land ⋃ u \subseteq w))$
59		an12	$⊢ (i \in u \land (u \in g \land ⋃ u \subseteq w)) \leftrightarrow (u \in g \land (i \in u \land ⋃ u \subseteq w))$
60	58 59	sylib	$⊢ (i \in u \land u \in ((U \cap g) \cap 𝒫 𝒫 w)) \to (u \in g \land (i \in u \land ⋃ u \subseteq w))$
61	60	eximi	$⊢ \exists u (i \in u \land u \in ((U \cap g) \cap 𝒫 𝒫 w)) \to \exists u (u \in g \land (i \in u \land ⋃ u \subseteq w))$
62		df-rex	$⊢ \exists u \in g (i \in u \land ⋃ u \subseteq w) \leftrightarrow \exists u (u \in g \land (i \in u \land ⋃ u \subseteq w))$
63	61 62	sylibr	$⊢ \exists u (i \in u \land u \in ((U \cap g) \cap 𝒫 𝒫 w)) \to \exists u \in g (i \in u \land ⋃ u \subseteq w)$
64	50 63	syl	$⊢ (z \cap ⋃ (U \cap g) \subseteq ⋃ ((U \cap g) \cap 𝒫 𝒫 w) \land i \in z \land i \in ⋃ (U \cap g)) \to \exists u \in g (i \in u \land ⋃ u \subseteq w)$
65	64	3expia	$⊢ (z \cap ⋃ (U \cap g) \subseteq ⋃ ((U \cap g) \cap 𝒫 𝒫 w) \land i \in z) \to (i \in ⋃ (U \cap g) \to \exists u \in g (i \in u \land ⋃ u \subseteq w))$
66	43 65	biimtrid	$⊢ (z \cap ⋃ (U \cap g) \subseteq ⋃ ((U \cap g) \cap 𝒫 𝒫 w) \land i \in z) \to (\exists v \in U (i \in v \land v \in g) \to \exists u \in g (i \in u \land ⋃ u \subseteq w))$
67	66	ralrimiva	$⊢ z \cap ⋃ (U \cap g) \subseteq ⋃ ((U \cap g) \cap 𝒫 𝒫 w) \to \forall i \in z (\exists v \in U (i \in v \land v \in g) \to \exists u \in g (i \in u \land ⋃ u \subseteq w))$
68	34 67	anim12i	$⊢ (𝒫 z \subseteq U \cap w \land z \cap ⋃ (U \cap g) \subseteq ⋃ ((U \cap g) \cap 𝒫 𝒫 w)) \to (𝒫 z \subseteq w \land \forall i \in z (\exists v \in U (i \in v \land v \in g) \to \exists u \in g (i \in u \land ⋃ u \subseteq w)))$
69	68	reximi	$⊢ \exists w \in U (𝒫 z \subseteq U \cap w \land z \cap ⋃ (U \cap g) \subseteq ⋃ ((U \cap g) \cap 𝒫 𝒫 w)) \to \exists w \in U (𝒫 z \subseteq w \land \forall i \in z (\exists v \in U (i \in v \land v \in g) \to \exists u \in g (i \in u \land ⋃ u \subseteq w)))$
70	31 69	sylg	$⊢ \forall f \in 𝒫 U \exists w \in U (𝒫 z \subseteq U \cap w \land z \cap ⋃ f \subseteq ⋃ (f \cap 𝒫 𝒫 w)) \to \forall g \exists w \in U (𝒫 z \subseteq w \land \forall i \in z (\exists v \in U (i \in v \land v \in g) \to \exists u \in g (i \in u \land ⋃ u \subseteq w)))$
71		elequ2	$⊢ f = g \to (v \in f \leftrightarrow v \in g)$
72	71	anbi2d	$⊢ f = g \to ((i \in v \land v \in f) \leftrightarrow (i \in v \land v \in g))$
73	72	rexbidv	$⊢ f = g \to (\exists v \in U (i \in v \land v \in f) \leftrightarrow \exists v \in U (i \in v \land v \in g))$
74		rexeq	$⊢ f = g \to (\exists u \in f (i \in u \land ⋃ u \subseteq w) \leftrightarrow \exists u \in g (i \in u \land ⋃ u \subseteq w))$
75	73 74	imbi12d	$⊢ f = g \to ((\exists v \in U (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 g) \to \exists u \in g (i \in u \land ⋃ u \subseteq w)))$
76	75	ralbidv	$⊢ f = g \to (\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 i \in z (\exists v \in U (i \in v \land v \in g) \to \exists u \in g (i \in u \land ⋃ u \subseteq w)))$
77	76	anbi2d	$⊢ f = g \to ((𝒫 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 w \land \forall i \in z (\exists v \in U (i \in v \land v \in g) \to \exists u \in g (i \in u \land ⋃ u \subseteq w))))$
78	77	rexbidv	$⊢ f = g \to (\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 \exists w \in U (𝒫 z \subseteq w \land \forall i \in z (\exists v \in U (i \in v \land v \in g) \to \exists u \in g (i \in u \land ⋃ u \subseteq w))))$
79	78	cbvalvw	$⊢ \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 g \exists w \in U (𝒫 z \subseteq w \land \forall i \in z (\exists v \in U (i \in v \land v \in g) \to \exists u \in g (i \in u \land ⋃ u \subseteq w)))$
80	70 79	sylibr	$⊢ \forall f \in 𝒫 U \exists w \in U (𝒫 z \subseteq U \cap w \land z \cap ⋃ f \subseteq ⋃ (f \cap 𝒫 𝒫 w)) \to \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)))$
81	16 80	jca	$⊢ \forall f \in 𝒫 U \exists w \in U (𝒫 z \subseteq U \cap w \land z \cap ⋃ f \subseteq ⋃ (f \cap 𝒫 𝒫 w)) \to (𝒫 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))))$
82		nfv	$⊢ Ⅎ f 𝒫 z \subseteq U$
83		nfa1	$⊢ Ⅎ f \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)))$
84	82 83	nfan	$⊢ Ⅎ f (𝒫 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))))$
85		elpwi	$⊢ f \in 𝒫 U \to f \subseteq U$
86		sp	$⊢ \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))) \to \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)))$
87		ssin	$⊢ (𝒫 z \subseteq U \land 𝒫 z \subseteq w) \leftrightarrow 𝒫 z \subseteq U \cap w$
88	87	biimpi	$⊢ (𝒫 z \subseteq U \land 𝒫 z \subseteq w) \to 𝒫 z \subseteq U \cap w$
89	88	ex	$⊢ 𝒫 z \subseteq U \to (𝒫 z \subseteq w \to 𝒫 z \subseteq U \cap w)$
90	89	adantr	$⊢ (𝒫 z \subseteq U \land f \subseteq U) \to (𝒫 z \subseteq w \to 𝒫 z \subseteq U \cap w)$
91		simp3	$⊢ (𝒫 z \subseteq U \land f \subseteq U \land i \in ⋃ f) \to i \in ⋃ f$
92		eluni	$⊢ i \in ⋃ f \leftrightarrow \exists v (i \in v \land v \in f)$
93	91 92	sylib	$⊢ (𝒫 z \subseteq U \land f \subseteq U \land i \in ⋃ f) \to \exists v (i \in v \land v \in f)$
94		simpl2	$⊢ ((𝒫 z \subseteq U \land f \subseteq U \land i \in ⋃ f) \land (i \in v \land v \in f)) \to f \subseteq U$
95		simprr	$⊢ ((𝒫 z \subseteq U \land f \subseteq U \land i \in ⋃ f) \land (i \in v \land v \in f)) \to v \in f$
96	94 95	sseldd	$⊢ ((𝒫 z \subseteq U \land f \subseteq U \land i \in ⋃ f) \land (i \in v \land v \in f)) \to v \in U$
97		simprl	$⊢ ((𝒫 z \subseteq U \land f \subseteq U \land i \in ⋃ f) \land (i \in v \land v \in f)) \to i \in v$
98	96 97 95	3jca	$⊢ ((𝒫 z \subseteq U \land f \subseteq U \land i \in ⋃ f) \land (i \in v \land v \in f)) \to (v \in U \land i \in v \land v \in f)$
99	98	ex	$⊢ (𝒫 z \subseteq U \land f \subseteq U \land i \in ⋃ f) \to ((i \in v \land v \in f) \to (v \in U \land i \in v \land v \in f))$
100	99	eximdv	$⊢ (𝒫 z \subseteq U \land f \subseteq U \land i \in ⋃ f) \to (\exists v (i \in v \land v \in f) \to \exists v (v \in U \land i \in v \land v \in f))$
101	93 100	mpd	$⊢ (𝒫 z \subseteq U \land f \subseteq U \land i \in ⋃ f) \to \exists v (v \in U \land i \in v \land v \in f)$
102		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))$
103		3anass	$⊢ (v \in U \land i \in v \land v \in f) \leftrightarrow (v \in U \land (i \in v \land v \in f))$
104	103	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))$
105	102 104	bitr4i	$⊢ \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)$
106	101 105	sylibr	$⊢ (𝒫 z \subseteq U \land f \subseteq U \land i \in ⋃ f) \to \exists v \in U (i \in v \land v \in f)$
107	106	3expia	$⊢ (𝒫 z \subseteq U \land f \subseteq U) \to (i \in ⋃ f \to \exists v \in U (i \in v \land v \in f))$
108		elin	$⊢ u \in (f \cap 𝒫 𝒫 w) \leftrightarrow (u \in f \land u \in 𝒫 𝒫 w)$
109		vex	$⊢ u \in V$
110	109 54	mpbiran	$⊢ u \in 𝒫 𝒫 w \leftrightarrow ⋃ u \subseteq w$
111	110	anbi2i	$⊢ (u \in f \land u \in 𝒫 𝒫 w) \leftrightarrow (u \in f \land ⋃ u \subseteq w)$
112	108 111	bitri	$⊢ u \in (f \cap 𝒫 𝒫 w) \leftrightarrow (u \in f \land ⋃ u \subseteq w)$
113	112	anbi2i	$⊢ (i \in u \land u \in (f \cap 𝒫 𝒫 w)) \leftrightarrow (i \in u \land (u \in f \land ⋃ u \subseteq w))$
114		an12	$⊢ (u \in f \land (i \in u \land ⋃ u \subseteq w)) \leftrightarrow (i \in u \land (u \in f \land ⋃ u \subseteq w))$
115	113 114	bitr4i	$⊢ (i \in u \land u \in (f \cap 𝒫 𝒫 w)) \leftrightarrow (u \in f \land (i \in u \land ⋃ u \subseteq w))$
116	115	exbii	$⊢ \exists u (i \in u \land u \in (f \cap 𝒫 𝒫 w)) \leftrightarrow \exists u (u \in f \land (i \in u \land ⋃ u \subseteq w))$
117		eluni	$⊢ i \in ⋃ (f \cap 𝒫 𝒫 w) \leftrightarrow \exists u (i \in u \land u \in (f \cap 𝒫 𝒫 w))$
118		df-rex	$⊢ \exists u \in f (i \in u \land ⋃ u \subseteq w) \leftrightarrow \exists u (u \in f \land (i \in u \land ⋃ u \subseteq w))$
119	116 117 118	3bitr4i	$⊢ i \in ⋃ (f \cap 𝒫 𝒫 w) \leftrightarrow \exists u \in f (i \in u \land ⋃ u \subseteq w)$
120	119	biimpri	$⊢ \exists u \in f (i \in u \land ⋃ u \subseteq w) \to i \in ⋃ (f \cap 𝒫 𝒫 w)$
121	120	a1i	$⊢ (𝒫 z \subseteq U \land f \subseteq U) \to (\exists u \in f (i \in u \land ⋃ u \subseteq w) \to i \in ⋃ (f \cap 𝒫 𝒫 w))$
122	107 121	imim12d	$⊢ (𝒫 z \subseteq U \land f \subseteq U) \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 (i \in ⋃ f \to i \in ⋃ (f \cap 𝒫 𝒫 w)))$
123	122	ralimdv	$⊢ (𝒫 z \subseteq U \land f \subseteq U) \to (\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)) \to \forall i \in z (i \in ⋃ f \to i \in ⋃ (f \cap 𝒫 𝒫 w)))$
124		elin	$⊢ i \in (z \cap ⋃ f) \leftrightarrow (i \in z \land i \in ⋃ f)$
125	124	imbi1i	$⊢ (i \in (z \cap ⋃ f) \to i \in ⋃ (f \cap 𝒫 𝒫 w)) \leftrightarrow ((i \in z \land i \in ⋃ f) \to i \in ⋃ (f \cap 𝒫 𝒫 w))$
126		impexp	$⊢ ((i \in z \land i \in ⋃ f) \to i \in ⋃ (f \cap 𝒫 𝒫 w)) \leftrightarrow (i \in z \to (i \in ⋃ f \to i \in ⋃ (f \cap 𝒫 𝒫 w)))$
127	125 126	bitri	$⊢ (i \in (z \cap ⋃ f) \to i \in ⋃ (f \cap 𝒫 𝒫 w)) \leftrightarrow (i \in z \to (i \in ⋃ f \to i \in ⋃ (f \cap 𝒫 𝒫 w)))$
128	127	albii	$⊢ \forall i (i \in (z \cap ⋃ f) \to i \in ⋃ (f \cap 𝒫 𝒫 w)) \leftrightarrow \forall i (i \in z \to (i \in ⋃ f \to i \in ⋃ (f \cap 𝒫 𝒫 w)))$
129		df-ss	$⊢ z \cap ⋃ f \subseteq ⋃ (f \cap 𝒫 𝒫 w) \leftrightarrow \forall i (i \in (z \cap ⋃ f) \to i \in ⋃ (f \cap 𝒫 𝒫 w))$
130		df-ral	$⊢ \forall i \in z (i \in ⋃ f \to i \in ⋃ (f \cap 𝒫 𝒫 w)) \leftrightarrow \forall i (i \in z \to (i \in ⋃ f \to i \in ⋃ (f \cap 𝒫 𝒫 w)))$
131	128 129 130	3bitr4i	$⊢ z \cap ⋃ f \subseteq ⋃ (f \cap 𝒫 𝒫 w) \leftrightarrow \forall i \in z (i \in ⋃ f \to i \in ⋃ (f \cap 𝒫 𝒫 w))$
132	123 131	imbitrrdi	$⊢ (𝒫 z \subseteq U \land f \subseteq U) \to (\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)) \to z \cap ⋃ f \subseteq ⋃ (f \cap 𝒫 𝒫 w))$
133	90 132	anim12d	$⊢ (𝒫 z \subseteq U \land f \subseteq U) \to ((𝒫 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))) \to (𝒫 z \subseteq U \cap w \land z \cap ⋃ f \subseteq ⋃ (f \cap 𝒫 𝒫 w)))$
134	133	reximdv	$⊢ (𝒫 z \subseteq U \land f \subseteq U) \to (\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))) \to \exists w \in U (𝒫 z \subseteq U \cap w \land z \cap ⋃ f \subseteq ⋃ (f \cap 𝒫 𝒫 w)))$
135	134	3impia	$⊢ (𝒫 z \subseteq U \land f \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)))) \to \exists w \in U (𝒫 z \subseteq U \cap w \land z \cap ⋃ f \subseteq ⋃ (f \cap 𝒫 𝒫 w))$
136	135	3com23	$⊢ (𝒫 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))) \land f \subseteq U) \to \exists w \in U (𝒫 z \subseteq U \cap w \land z \cap ⋃ f \subseteq ⋃ (f \cap 𝒫 𝒫 w))$
137	86 136	syl3an2	$⊢ (𝒫 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))) \land f \subseteq U) \to \exists w \in U (𝒫 z \subseteq U \cap w \land z \cap ⋃ f \subseteq ⋃ (f \cap 𝒫 𝒫 w))$
138	137	3expa	$⊢ ((𝒫 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)))) \land f \subseteq U) \to \exists w \in U (𝒫 z \subseteq U \cap w \land z \cap ⋃ f \subseteq ⋃ (f \cap 𝒫 𝒫 w))$
139	85 138	sylan2	$⊢ ((𝒫 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)))) \land f \in 𝒫 U) \to \exists w \in U (𝒫 z \subseteq U \cap w \land z \cap ⋃ f \subseteq ⋃ (f \cap 𝒫 𝒫 w))$
140	84 139	ralrimia	$⊢ (𝒫 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)))) \to \forall f \in 𝒫 U \exists w \in U (𝒫 z \subseteq U \cap w \land z \cap ⋃ f \subseteq ⋃ (f \cap 𝒫 𝒫 w))$
141	81 140	impbii	$⊢ \forall f \in 𝒫 U \exists w \in U (𝒫 z \subseteq U \cap w \land z \cap ⋃ f \subseteq ⋃ (f \cap 𝒫 𝒫 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))))$

Metamath Proof Explorer

Theorem ismnushort

Proof