Theorem ismnushort 44011

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

Assertion

Ref	Expression
ismnushort	⊢ (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ (𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))

Distinct variable groups:   𝑣,𝑈   𝑓,𝑖,𝑤,𝑧   𝑣,𝑓,𝑖,𝑧   𝑈,𝑓,𝑖,𝑢,𝑤

Allowed substitution hint:   𝑈(𝑧)

Proof of Theorem ismnushort

Dummy variable 𝑔 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpl 481	. . . . . 6 ⊢ ((𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) → 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤))
2	1	reximi 3074	. . . . 5 ⊢ (∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) → ∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤))
3	2	ralimi 3073	. . . 4 ⊢ (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) → ∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤))
4		0elpw 5352	. . . . . . 7 ⊢ ∅ ∈ 𝒫 𝑈
5	4	a1i 11	. . . . . 6 ⊢ (⊤ → ∅ ∈ 𝒫 𝑈)
6		biidd 261	. . . . . 6 ⊢ ((⊤ ∧ 𝑓 = ∅) → (∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ↔ ∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤)))
7	5, 6	rspcdv 3601	. . . . 5 ⊢ (⊤ → (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) → ∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤)))
8	7	mptru 1541	. . . 4 ⊢ (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) → ∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤))
9		inss1 4229	. . . . . 6 ⊢ (𝑈 ∩ 𝑤) ⊆ 𝑈
10		sstr2 3987	. . . . . 6 ⊢ (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) → ((𝑈 ∩ 𝑤) ⊆ 𝑈 → 𝒫 𝑧 ⊆ 𝑈))
11	9, 10	mpi 20	. . . . 5 ⊢ (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) → 𝒫 𝑧 ⊆ 𝑈)
12	11	reximi 3074	. . . 4 ⊢ (∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) → ∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ 𝑈)
13		rexex 3066	. . . . 5 ⊢ (∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ 𝑈 → ∃𝑤𝒫 𝑧 ⊆ 𝑈)
14		ax5e 1908	. . . . 5 ⊢ (∃𝑤𝒫 𝑧 ⊆ 𝑈 → 𝒫 𝑧 ⊆ 𝑈)
15	13, 14	syl 17	. . . 4 ⊢ (∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ 𝑈 → 𝒫 𝑧 ⊆ 𝑈)
16	3, 8, 12, 15	4syl 19	. . 3 ⊢ (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) → 𝒫 𝑧 ⊆ 𝑈)
17		inss1 4229	. . . . . . . 8 ⊢ (𝑈 ∩ 𝑔) ⊆ 𝑈
18		vex 3468	. . . . . . . . . 10 ⊢ 𝑔 ∈ V
19	18	inex2 5315	. . . . . . . . 9 ⊢ (𝑈 ∩ 𝑔) ∈ V
20	19	elpw 4603	. . . . . . . 8 ⊢ ((𝑈 ∩ 𝑔) ∈ 𝒫 𝑈 ↔ (𝑈 ∩ 𝑔) ⊆ 𝑈)
21	17, 20	mpbir 230	. . . . . . 7 ⊢ (𝑈 ∩ 𝑔) ∈ 𝒫 𝑈
22		unieq 4918	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑈 ∩ 𝑔) → ∪ 𝑓 = ∪ (𝑈 ∩ 𝑔))
23	22	ineq2d 4212	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑈 ∩ 𝑔) → (𝑧 ∩ ∪ 𝑓) = (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)))
24		ineq1 4205	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑈 ∩ 𝑔) → (𝑓 ∩ 𝒫 𝒫 𝑤) = ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤))
25	24	unieqd 4920	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑈 ∩ 𝑔) → ∪ (𝑓 ∩ 𝒫 𝒫 𝑤) = ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤))
26	23, 25	sseq12d 4014	. . . . . . . . . 10 ⊢ (𝑓 = (𝑈 ∩ 𝑔) → ((𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤) ↔ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)))
27	26	anbi2d 628	. . . . . . . . 9 ⊢ (𝑓 = (𝑈 ∩ 𝑔) → ((𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤))))
28	27	rexbidv 3169	. . . . . . . 8 ⊢ (𝑓 = (𝑈 ∩ 𝑔) → (∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤))))
29	28	rspcv 3605	. . . . . . 7 ⊢ ((𝑈 ∩ 𝑔) ∈ 𝒫 𝑈 → (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤))))
30	21, 29	ax-mp 5	. . . . . 6 ⊢ (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)))
31	30	alrimiv 1923	. . . . 5 ⊢ (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) → ∀𝑔∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)))
32		inss2 4230	. . . . . . . 8 ⊢ (𝑈 ∩ 𝑤) ⊆ 𝑤
33		sstr2 3987	. . . . . . . 8 ⊢ (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) → ((𝑈 ∩ 𝑤) ⊆ 𝑤 → 𝒫 𝑧 ⊆ 𝑤))
34	32, 33	mpi 20	. . . . . . 7 ⊢ (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) → 𝒫 𝑧 ⊆ 𝑤)
35		an12 643	. . . . . . . . . . . 12 ⊢ ((𝑣 ∈ 𝑈 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔)) ↔ (𝑖 ∈ 𝑣 ∧ (𝑣 ∈ 𝑈 ∧ 𝑣 ∈ 𝑔)))
36		elin 3964	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ (𝑈 ∩ 𝑔) ↔ (𝑣 ∈ 𝑈 ∧ 𝑣 ∈ 𝑔))
37	36	bicomi 223	. . . . . . . . . . . . 13 ⊢ ((𝑣 ∈ 𝑈 ∧ 𝑣 ∈ 𝑔) ↔ 𝑣 ∈ (𝑈 ∩ 𝑔))
38	37	anbi2i 621	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ 𝑣 ∧ (𝑣 ∈ 𝑈 ∧ 𝑣 ∈ 𝑔)) ↔ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ (𝑈 ∩ 𝑔)))
39	35, 38	bitri 274	. . . . . . . . . . 11 ⊢ ((𝑣 ∈ 𝑈 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔)) ↔ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ (𝑈 ∩ 𝑔)))
40	39	exbii 1843	. . . . . . . . . 10 ⊢ (∃𝑣(𝑣 ∈ 𝑈 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔)) ↔ ∃𝑣(𝑖 ∈ 𝑣 ∧ 𝑣 ∈ (𝑈 ∩ 𝑔)))
41		df-rex 3061	. . . . . . . . . 10 ⊢ (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) ↔ ∃𝑣(𝑣 ∈ 𝑈 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔)))
42		eluni 4910	. . . . . . . . . 10 ⊢ (𝑖 ∈ ∪ (𝑈 ∩ 𝑔) ↔ ∃𝑣(𝑖 ∈ 𝑣 ∧ 𝑣 ∈ (𝑈 ∩ 𝑔)))
43	40, 41, 42	3bitr4i 302	. . . . . . . . 9 ⊢ (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) ↔ 𝑖 ∈ ∪ (𝑈 ∩ 𝑔))
44		simp1 1133	. . . . . . . . . . . . 13 ⊢ (((𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) ∧ 𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ (𝑈 ∩ 𝑔)) → (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤))
45		elin 3964	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ↔ (𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ (𝑈 ∩ 𝑔)))
46	45	biimpri 227	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ (𝑈 ∩ 𝑔)) → 𝑖 ∈ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)))
47	46	3adant1 1127	. . . . . . . . . . . . 13 ⊢ (((𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) ∧ 𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ (𝑈 ∩ 𝑔)) → 𝑖 ∈ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)))
48	44, 47	sseldd 3981	. . . . . . . . . . . 12 ⊢ (((𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) ∧ 𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ (𝑈 ∩ 𝑔)) → 𝑖 ∈ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤))
49		eluni 4910	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) ↔ ∃𝑢(𝑖 ∈ 𝑢 ∧ 𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)))
50	48, 49	sylib 217	. . . . . . . . . . 11 ⊢ (((𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) ∧ 𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ (𝑈 ∩ 𝑔)) → ∃𝑢(𝑖 ∈ 𝑢 ∧ 𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)))
51		elinel1 4195	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) → 𝑢 ∈ (𝑈 ∩ 𝑔))
52	51	elin2d 4199	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) → 𝑢 ∈ 𝑔)
53		elinel2 4196	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) → 𝑢 ∈ 𝒫 𝒫 𝑤)
54		elpwpw 5104	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 ∈ 𝒫 𝒫 𝑤 ↔ (𝑢 ∈ V ∧ ∪ 𝑢 ⊆ 𝑤))
55	54	simprbi 495	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 ∈ 𝒫 𝒫 𝑤 → ∪ 𝑢 ⊆ 𝑤)
56	53, 55	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) → ∪ 𝑢 ⊆ 𝑤)
57	52, 56	jca 510	. . . . . . . . . . . . . . 15 ⊢ (𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) → (𝑢 ∈ 𝑔 ∧ ∪ 𝑢 ⊆ 𝑤))
58	57	anim2i 615	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∈ 𝑢 ∧ 𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)) → (𝑖 ∈ 𝑢 ∧ (𝑢 ∈ 𝑔 ∧ ∪ 𝑢 ⊆ 𝑤)))
59		an12 643	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∈ 𝑢 ∧ (𝑢 ∈ 𝑔 ∧ ∪ 𝑢 ⊆ 𝑤)) ↔ (𝑢 ∈ 𝑔 ∧ (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
60	58, 59	sylib 217	. . . . . . . . . . . . 13 ⊢ ((𝑖 ∈ 𝑢 ∧ 𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)) → (𝑢 ∈ 𝑔 ∧ (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
61	60	eximi 1830	. . . . . . . . . . . 12 ⊢ (∃𝑢(𝑖 ∈ 𝑢 ∧ 𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)) → ∃𝑢(𝑢 ∈ 𝑔 ∧ (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
62		df-rex 3061	. . . . . . . . . . . 12 ⊢ (∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ ∃𝑢(𝑢 ∈ 𝑔 ∧ (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
63	61, 62	sylibr 233	. . . . . . . . . . 11 ⊢ (∃𝑢(𝑖 ∈ 𝑢 ∧ 𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))
64	50, 63	syl 17	. . . . . . . . . 10 ⊢ (((𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) ∧ 𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ (𝑈 ∩ 𝑔)) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))
65	64	3expia 1118	. . . . . . . . 9 ⊢ (((𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) ∧ 𝑖 ∈ 𝑧) → (𝑖 ∈ ∪ (𝑈 ∩ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
66	43, 65	biimtrid 241	. . . . . . . 8 ⊢ (((𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) ∧ 𝑖 ∈ 𝑧) → (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
67	66	ralrimiva 3136	. . . . . . 7 ⊢ ((𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) → ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
68	34, 67	anim12i 611	. . . . . 6 ⊢ ((𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)) → (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
69	68	reximi 3074	. . . . 5 ⊢ (∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
70	31, 69	sylg 1818	. . . 4 ⊢ (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) → ∀𝑔∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
71		elequ2 2114	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑔 → (𝑣 ∈ 𝑓 ↔ 𝑣 ∈ 𝑔))
72	71	anbi2d 628	. . . . . . . . . 10 ⊢ (𝑓 = 𝑔 → ((𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) ↔ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔)))
73	72	rexbidv 3169	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) ↔ ∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔)))
74		rexeq 3311	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → (∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
75	73, 74	imbi12d 343	. . . . . . . 8 ⊢ (𝑓 = 𝑔 → ((∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) ↔ (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
76	75	ralbidv 3168	. . . . . . 7 ⊢ (𝑓 = 𝑔 → (∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) ↔ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
77	76	anbi2d 628	. . . . . 6 ⊢ (𝑓 = 𝑔 → ((𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) ↔ (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))
78	77	rexbidv 3169	. . . . 5 ⊢ (𝑓 = 𝑔 → (∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) ↔ ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))
79	78	cbvalvw 2032	. . . 4 ⊢ (∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) ↔ ∀𝑔∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
80	70, 79	sylibr 233	. . 3 ⊢ (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) → ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
81	16, 80	jca 510	. 2 ⊢ (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) → (𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))
82		nfv 1910	. . . 4 ⊢ Ⅎ𝑓𝒫 𝑧 ⊆ 𝑈
83		nfa1 2141	. . . 4 ⊢ Ⅎ𝑓∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
84	82, 83	nfan 1895	. . 3 ⊢ Ⅎ𝑓(𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
85		elpwi 4606	. . . 4 ⊢ (𝑓 ∈ 𝒫 𝑈 → 𝑓 ⊆ 𝑈)
86		sp 2172	. . . . . 6 ⊢ (∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
87		ssin 4231	. . . . . . . . . . . . 13 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝒫 𝑧 ⊆ 𝑤) ↔ 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤))
88	87	biimpi 215	. . . . . . . . . . . 12 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝒫 𝑧 ⊆ 𝑤) → 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤))
89	88	ex 411	. . . . . . . . . . 11 ⊢ (𝒫 𝑧 ⊆ 𝑈 → (𝒫 𝑧 ⊆ 𝑤 → 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤)))
90	89	adantr 479	. . . . . . . . . 10 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈) → (𝒫 𝑧 ⊆ 𝑤 → 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤)))
91		simp3 1135	. . . . . . . . . . . . . . . . 17 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) → 𝑖 ∈ ∪ 𝑓)
92		eluni 4910	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ ∪ 𝑓 ↔ ∃𝑣(𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓))
93	91, 92	sylib 217	. . . . . . . . . . . . . . . 16 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) → ∃𝑣(𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓))
94		simpl2 1189	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) → 𝑓 ⊆ 𝑈)
95		simprr 771	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) → 𝑣 ∈ 𝑓)
96	94, 95	sseldd 3981	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) → 𝑣 ∈ 𝑈)
97		simprl 769	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) → 𝑖 ∈ 𝑣)
98	96, 97, 95	3jca 1125	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) → (𝑣 ∈ 𝑈 ∧ 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓))
99	98	ex 411	. . . . . . . . . . . . . . . . 17 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) → ((𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → (𝑣 ∈ 𝑈 ∧ 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)))
100	99	eximdv 1913	. . . . . . . . . . . . . . . 16 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) → (∃𝑣(𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑣(𝑣 ∈ 𝑈 ∧ 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)))
101	93, 100	mpd 15	. . . . . . . . . . . . . . 15 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) → ∃𝑣(𝑣 ∈ 𝑈 ∧ 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓))
102		df-rex 3061	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) ↔ ∃𝑣(𝑣 ∈ 𝑈 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)))
103		3anass 1092	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑣 ∈ 𝑈 ∧ 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) ↔ (𝑣 ∈ 𝑈 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)))
104	103	exbii 1843	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑣(𝑣 ∈ 𝑈 ∧ 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) ↔ ∃𝑣(𝑣 ∈ 𝑈 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)))
105	102, 104	bitr4i 277	. . . . . . . . . . . . . . 15 ⊢ (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) ↔ ∃𝑣(𝑣 ∈ 𝑈 ∧ 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓))
106	101, 105	sylibr 233	. . . . . . . . . . . . . 14 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) → ∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓))
107	106	3expia 1118	. . . . . . . . . . . . 13 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈) → (𝑖 ∈ ∪ 𝑓 → ∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)))
108		elin 3964	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 ∈ (𝑓 ∩ 𝒫 𝒫 𝑤) ↔ (𝑢 ∈ 𝑓 ∧ 𝑢 ∈ 𝒫 𝒫 𝑤))
109		vex 3468	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑢 ∈ V
110	109, 54	mpbiran 707	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ 𝒫 𝒫 𝑤 ↔ ∪ 𝑢 ⊆ 𝑤)
111	110	anbi2i 621	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑢 ∈ 𝑓 ∧ 𝑢 ∈ 𝒫 𝒫 𝑤) ↔ (𝑢 ∈ 𝑓 ∧ ∪ 𝑢 ⊆ 𝑤))
112	108, 111	bitri 274	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 ∈ (𝑓 ∩ 𝒫 𝒫 𝑤) ↔ (𝑢 ∈ 𝑓 ∧ ∪ 𝑢 ⊆ 𝑤))
113	112	anbi2i 621	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ 𝑢 ∧ 𝑢 ∈ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ (𝑖 ∈ 𝑢 ∧ (𝑢 ∈ 𝑓 ∧ ∪ 𝑢 ⊆ 𝑤)))
114		an12 643	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ∈ 𝑓 ∧ (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) ↔ (𝑖 ∈ 𝑢 ∧ (𝑢 ∈ 𝑓 ∧ ∪ 𝑢 ⊆ 𝑤)))
115	113, 114	bitr4i 277	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ 𝑢 ∧ 𝑢 ∈ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ (𝑢 ∈ 𝑓 ∧ (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
116	115	exbii 1843	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑢(𝑖 ∈ 𝑢 ∧ 𝑢 ∈ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ ∃𝑢(𝑢 ∈ 𝑓 ∧ (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
117		eluni 4910	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤) ↔ ∃𝑢(𝑖 ∈ 𝑢 ∧ 𝑢 ∈ (𝑓 ∩ 𝒫 𝒫 𝑤)))
118		df-rex 3061	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ ∃𝑢(𝑢 ∈ 𝑓 ∧ (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
119	116, 117, 118	3bitr4i 302	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤) ↔ ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))
120	119	biimpri 227	. . . . . . . . . . . . . 14 ⊢ (∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤))
121	120	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈) → (∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))
122	107, 121	imim12d 81	. . . . . . . . . . . 12 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈) → ((∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) → (𝑖 ∈ ∪ 𝑓 → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤))))
123	122	ralimdv 3159	. . . . . . . . . . 11 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈) → (∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) → ∀𝑖 ∈ 𝑧 (𝑖 ∈ ∪ 𝑓 → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤))))
124		elin 3964	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (𝑧 ∩ ∪ 𝑓) ↔ (𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ 𝑓))
125	124	imbi1i 348	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∈ (𝑧 ∩ ∪ 𝑓) → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ ((𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ 𝑓) → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))
126		impexp 449	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ 𝑓) → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ (𝑖 ∈ 𝑧 → (𝑖 ∈ ∪ 𝑓 → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤))))
127	125, 126	bitri 274	. . . . . . . . . . . . 13 ⊢ ((𝑖 ∈ (𝑧 ∩ ∪ 𝑓) → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ (𝑖 ∈ 𝑧 → (𝑖 ∈ ∪ 𝑓 → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤))))
128	127	albii 1814	. . . . . . . . . . . 12 ⊢ (∀𝑖(𝑖 ∈ (𝑧 ∩ ∪ 𝑓) → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ ∀𝑖(𝑖 ∈ 𝑧 → (𝑖 ∈ ∪ 𝑓 → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤))))
129		df-ss 3965	. . . . . . . . . . . 12 ⊢ ((𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤) ↔ ∀𝑖(𝑖 ∈ (𝑧 ∩ ∪ 𝑓) → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))
130		df-ral 3052	. . . . . . . . . . . 12 ⊢ (∀𝑖 ∈ 𝑧 (𝑖 ∈ ∪ 𝑓 → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ ∀𝑖(𝑖 ∈ 𝑧 → (𝑖 ∈ ∪ 𝑓 → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤))))
131	128, 129, 130	3bitr4i 302	. . . . . . . . . . 11 ⊢ ((𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤) ↔ ∀𝑖 ∈ 𝑧 (𝑖 ∈ ∪ 𝑓 → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))
132	123, 131	imbitrrdi 251	. . . . . . . . . 10 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈) → (∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) → (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))
133	90, 132	anim12d 607	. . . . . . . . 9 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈) → ((𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) → (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤))))
134	133	reximdv 3160	. . . . . . . 8 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈) → (∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤))))
135	134	3impia 1114	. . . . . . 7 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))
136	135	3com23 1123	. . . . . 6 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) ∧ 𝑓 ⊆ 𝑈) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))
137	86, 136	syl3an2 1161	. . . . 5 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) ∧ 𝑓 ⊆ 𝑈) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))
138	137	3expa 1115	. . . 4 ⊢ (((𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) ∧ 𝑓 ⊆ 𝑈) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))
139	85, 138	sylan2 591	. . 3 ⊢ (((𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) ∧ 𝑓 ∈ 𝒫 𝑈) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))
140	84, 139	ralrimia 3246	. 2 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → ∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))
141	81, 140	impbii 208	1 ⊢ (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ (𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1084  ∀wal 1532   = wceq 1534  ⊤wtru 1535  ∃wex 1774   ∈ wcel 2099  ∀wral 3051  ∃wrex 3060  Vcvv 3464   ∩ cin 3947   ⊆ wss 3948  ∅c0 4324  𝒫 cpw 4599  ∪ cuni 4907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-12 2167  ax-ext 2697  ax-sep 5296  ax-nul 5303

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-ral 3052  df-rex 3061  df-rab 3421  df-v 3466  df-dif 3951  df-in 3955  df-ss 3965  df-nul 4325  df-pw 4601  df-uni 4908

This theorem is referenced by:  dfuniv2  44012