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	8 12	syl	$⊢ \forall f \in 𝒫 U \exists w \in U 𝒫 z \subseteq U \cap w \to \exists w \in U 𝒫 z \subseteq U$
14		rexex	$⊢ \exists w \in U 𝒫 z \subseteq U \to \exists w 𝒫 z \subseteq U$
15		ax5e	$⊢ \exists w 𝒫 z \subseteq U \to 𝒫 z \subseteq U$
16	14 15	syl	$⊢ \exists w \in U 𝒫 z \subseteq U \to 𝒫 z \subseteq U$
17	3 13 16	3syl	$⊢ \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$
18		inss1	$⊢ U \cap g \subseteq U$
19		vex	$⊢ g \in V$
20	19	inex2	$⊢ U \cap g \in V$
21	20	elpw	$⊢ U \cap g \in 𝒫 U \leftrightarrow U \cap g \subseteq U$
22	18 21	mpbir	$⊢ U \cap g \in 𝒫 U$
23		unieq	$⊢ f = U \cap g \to ⋃ f = ⋃ (U \cap g)$
24	23	ineq2d	$⊢ f = U \cap g \to z \cap ⋃ f = z \cap ⋃ (U \cap g)$
25		ineq1	$⊢ f = U \cap g \to f \cap 𝒫 𝒫 w = (U \cap g) \cap 𝒫 𝒫 w$
26	25	unieqd	$⊢ f = U \cap g \to ⋃ (f \cap 𝒫 𝒫 w) = ⋃ ((U \cap g) \cap 𝒫 𝒫 w)$
27	24 26	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))$
28	27	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)))$
29	28	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)))$
30	29	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)))$
31	22 30	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))$
32	31	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))$
33		inss2	$⊢ U \cap w \subseteq w$
34		sstr2	$⊢ 𝒫 z \subseteq U \cap w \to (U \cap w \subseteq w \to 𝒫 z \subseteq w)$
35	33 34	mpi	$⊢ 𝒫 z \subseteq U \cap w \to 𝒫 z \subseteq w$
36		an12	$⊢ (v \in U \land (i \in v \land v \in g)) \leftrightarrow (i \in v \land (v \in U \land v \in g))$
37		elin	$⊢ v \in (U \cap g) \leftrightarrow (v \in U \land v \in g)$
38	37	bicomi	$⊢ (v \in U \land v \in g) \leftrightarrow v \in (U \cap g)$
39	38	anbi2i	$⊢ (i \in v \land (v \in U \land v \in g)) \leftrightarrow (i \in v \land v \in (U \cap g))$
40	36 39	bitri	$⊢ (v \in U \land (i \in v \land v \in g)) \leftrightarrow (i \in v \land v \in (U \cap g))$
41	40	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))$
42		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))$
43		eluni	$⊢ i \in ⋃ (U \cap g) \leftrightarrow \exists v (i \in v \land v \in (U \cap g))$
44	41 42 43	3bitr4i	$⊢ \exists v \in U (i \in v \land v \in g) \leftrightarrow i \in ⋃ (U \cap g)$
45		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)$
46		elin	$⊢ i \in (z \cap ⋃ (U \cap g)) \leftrightarrow (i \in z \land i \in ⋃ (U \cap g))$
47	46	biimpri	$⊢ (i \in z \land i \in ⋃ (U \cap g)) \to i \in (z \cap ⋃ (U \cap g))$
48	47	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))$
49	45 48	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)$
50		eluni	$⊢ i \in ⋃ ((U \cap g) \cap 𝒫 𝒫 w) \leftrightarrow \exists u (i \in u \land u \in ((U \cap g) \cap 𝒫 𝒫 w))$
51	49 50	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))$
52		elinel1	$⊢ u \in ((U \cap g) \cap 𝒫 𝒫 w) \to u \in (U \cap g)$
53	52	elin2d	$⊢ u \in ((U \cap g) \cap 𝒫 𝒫 w) \to u \in g$
54		elinel2	$⊢ u \in ((U \cap g) \cap 𝒫 𝒫 w) \to u \in 𝒫 𝒫 w$
55		elpwpw	$⊢ u \in 𝒫 𝒫 w \leftrightarrow (u \in V \land ⋃ u \subseteq w)$
56	55	simprbi	$⊢ u \in 𝒫 𝒫 w \to ⋃ u \subseteq w$
57	54 56	syl	$⊢ u \in ((U \cap g) \cap 𝒫 𝒫 w) \to ⋃ u \subseteq w$
58	53 57	jca	$⊢ u \in ((U \cap g) \cap 𝒫 𝒫 w) \to (u \in g \land ⋃ u \subseteq w)$
59	58	anim2i	$⊢ (i \in u \land u \in ((U \cap g) \cap 𝒫 𝒫 w)) \to (i \in u \land (u \in g \land ⋃ u \subseteq w))$
60		an12	$⊢ (i \in u \land (u \in g \land ⋃ u \subseteq w)) \leftrightarrow (u \in g \land (i \in u \land ⋃ u \subseteq w))$
61	59 60	sylib	$⊢ (i \in u \land u \in ((U \cap g) \cap 𝒫 𝒫 w)) \to (u \in g \land (i \in u \land ⋃ u \subseteq w))$
62	61	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))$
63		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))$
64	62 63	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)$
65	51 64	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)$
66	65	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))$
67	44 66	syl5bi	$⊢ (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))$
68	67	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))$
69	35 68	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)))$
70	69	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)))$
71	32 70	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)))$
72		elequ2	$⊢ f = g \to (v \in f \leftrightarrow v \in g)$
73	72	anbi2d	$⊢ f = g \to ((i \in v \land v \in f) \leftrightarrow (i \in v \land v \in g))$
74	73	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))$
75		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))$
76	74 75	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)))$
77	76	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)))$
78	77	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))))$
79	78	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))))$
80	79	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)))$
81	71 80	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)))$
82	17 81	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))))$
83		nfv	$⊢ Ⅎ f 𝒫 z \subseteq U$
84		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)))$
85	83 84	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))))$
86		elpwi	$⊢ f \in 𝒫 U \to f \subseteq U$
87		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)))$
88		ssin	$⊢ (𝒫 z \subseteq U \land 𝒫 z \subseteq w) \leftrightarrow 𝒫 z \subseteq U \cap w$
89	88	biimpi	$⊢ (𝒫 z \subseteq U \land 𝒫 z \subseteq w) \to 𝒫 z \subseteq U \cap w$
90	89	ex	$⊢ 𝒫 z \subseteq U \to (𝒫 z \subseteq w \to 𝒫 z \subseteq U \cap w)$
91	90	adantr	$⊢ (𝒫 z \subseteq U \land f \subseteq U) \to (𝒫 z \subseteq w \to 𝒫 z \subseteq U \cap w)$
92		simp3	$⊢ (𝒫 z \subseteq U \land f \subseteq U \land i \in ⋃ f) \to i \in ⋃ f$
93		eluni	$⊢ i \in ⋃ f \leftrightarrow \exists v (i \in v \land v \in f)$
94	92 93	sylib	$⊢ (𝒫 z \subseteq U \land f \subseteq U \land i \in ⋃ f) \to \exists v (i \in v \land v \in f)$
95		simpl2	$⊢ ((𝒫 z \subseteq U \land f \subseteq U \land i \in ⋃ f) \land (i \in v \land v \in f)) \to f \subseteq U$
96		simprr	$⊢ ((𝒫 z \subseteq U \land f \subseteq U \land i \in ⋃ f) \land (i \in v \land v \in f)) \to v \in f$
97	95 96	sseldd	$⊢ ((𝒫 z \subseteq U \land f \subseteq U \land i \in ⋃ f) \land (i \in v \land v \in f)) \to v \in U$
98		simprl	$⊢ ((𝒫 z \subseteq U \land f \subseteq U \land i \in ⋃ f) \land (i \in v \land v \in f)) \to i \in v$
99	97 98 96	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)$
100	99	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))$
101	100	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))$
102	94 101	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)$
103		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))$
104		3anass	$⊢ (v \in U \land i \in v \land v \in f) \leftrightarrow (v \in U \land (i \in v \land v \in f))$
105	104	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))$
106	103 105	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)$
107	102 106	sylibr	$⊢ (𝒫 z \subseteq U \land f \subseteq U \land i \in ⋃ f) \to \exists v \in U (i \in v \land v \in f)$
108	107	3expia	$⊢ (𝒫 z \subseteq U \land f \subseteq U) \to (i \in ⋃ f \to \exists v \in U (i \in v \land v \in f))$
109		elin	$⊢ u \in (f \cap 𝒫 𝒫 w) \leftrightarrow (u \in f \land u \in 𝒫 𝒫 w)$
110		vex	$⊢ u \in V$
111	110 55	mpbiran	$⊢ u \in 𝒫 𝒫 w \leftrightarrow ⋃ u \subseteq w$
112	111	anbi2i	$⊢ (u \in f \land u \in 𝒫 𝒫 w) \leftrightarrow (u \in f \land ⋃ u \subseteq w)$
113	109 112	bitri	$⊢ u \in (f \cap 𝒫 𝒫 w) \leftrightarrow (u \in f \land ⋃ u \subseteq w)$
114	113	anbi2i	$⊢ (i \in u \land u \in (f \cap 𝒫 𝒫 w)) \leftrightarrow (i \in u \land (u \in f \land ⋃ u \subseteq w))$
115		an12	$⊢ (u \in f \land (i \in u \land ⋃ u \subseteq w)) \leftrightarrow (i \in u \land (u \in f \land ⋃ u \subseteq w))$
116	114 115	bitr4i	$⊢ (i \in u \land u \in (f \cap 𝒫 𝒫 w)) \leftrightarrow (u \in f \land (i \in u \land ⋃ u \subseteq w))$
117	116	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))$
118		eluni	$⊢ i \in ⋃ (f \cap 𝒫 𝒫 w) \leftrightarrow \exists u (i \in u \land u \in (f \cap 𝒫 𝒫 w))$
119		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))$
120	117 118 119	3bitr4i	$⊢ i \in ⋃ (f \cap 𝒫 𝒫 w) \leftrightarrow \exists u \in f (i \in u \land ⋃ u \subseteq w)$
121	120	biimpri	$⊢ \exists u \in f (i \in u \land ⋃ u \subseteq w) \to i \in ⋃ (f \cap 𝒫 𝒫 w)$
122	121	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))$
123	108 122	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)))$
124	123	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)))$
125		elin	$⊢ i \in (z \cap ⋃ f) \leftrightarrow (i \in z \land i \in ⋃ f)$
126	125	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))$
127		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)))$
128	126 127	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)))$
129	128	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)))$
130		dfss2	$⊢ z \cap ⋃ f \subseteq ⋃ (f \cap 𝒫 𝒫 w) \leftrightarrow \forall i (i \in (z \cap ⋃ f) \to i \in ⋃ (f \cap 𝒫 𝒫 w))$
131		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)))$
132	129 130 131	3bitr4i	$⊢ z \cap ⋃ f \subseteq ⋃ (f \cap 𝒫 𝒫 w) \leftrightarrow \forall i \in z (i \in ⋃ f \to i \in ⋃ (f \cap 𝒫 𝒫 w))$
133	124 132	syl6ibr	$⊢ (𝒫 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))$
134	91 133	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)))$
135	134	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)))$
136	135	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))$
137	136	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))$
138	87 137	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))$
139	138	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))$
140	86 139	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))$
141	85 140	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))$
142	82 141	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