Theorem ismnushort 44815

Description: Express the predicate on 𝑈 and 𝑧 in ismnu 44775 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 485	. . . . . 6 ⊢ ((𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) → 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤))
2	1	reximi 3090	. . . . 5 ⊢ (∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) → ∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤))
3	2	ralimi 3089	. . . 4 ⊢ (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) → ∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤))
4		0elpw 5302	. . . . . . 7 ⊢ ∅ ∈ 𝒫 𝑈
5	4	a1i 11	. . . . . 6 ⊢ (⊤ → ∅ ∈ 𝒫 𝑈)
6		biidd 264	. . . . . 6 ⊢ ((⊤ ∧ 𝑓 = ∅) → (∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ↔ ∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤)))
7	5, 6	rspcdv 3564	. . . . 5 ⊢ (⊤ → (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) → ∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤)))
8	7	mptru 1557	. . . 4 ⊢ (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) → ∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤))
9		inss1 4179	. . . . . 6 ⊢ (𝑈 ∩ 𝑤) ⊆ 𝑈
10		sstr2 3934	. . . . . 6 ⊢ (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) → ((𝑈 ∩ 𝑤) ⊆ 𝑈 → 𝒫 𝑧 ⊆ 𝑈))
11	9, 10	mpi 20	. . . . 5 ⊢ (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) → 𝒫 𝑧 ⊆ 𝑈)
12	11	reximi 3090	. . . 4 ⊢ (∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) → ∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ 𝑈)
13		rexex 3082	. . . . 5 ⊢ (∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ 𝑈 → ∃𝑤𝒫 𝑧 ⊆ 𝑈)
14		ax5e 1922	. . . . 5 ⊢ (∃𝑤𝒫 𝑧 ⊆ 𝑈 → 𝒫 𝑧 ⊆ 𝑈)
15	13, 14	syl 17	. . . 4 ⊢ (∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ 𝑈 → 𝒫 𝑧 ⊆ 𝑈)
16	3, 8, 12, 15	4syl 19	. . 3 ⊢ (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) → 𝒫 𝑧 ⊆ 𝑈)
17		inss1 4179	. . . . . . . 8 ⊢ (𝑈 ∩ 𝑔) ⊆ 𝑈
18		vex 3448	. . . . . . . . . 10 ⊢ 𝑔 ∈ V
19	18	inex2 5264	. . . . . . . . 9 ⊢ (𝑈 ∩ 𝑔) ∈ V
20	19	elpw 4549	. . . . . . . 8 ⊢ ((𝑈 ∩ 𝑔) ∈ 𝒫 𝑈 ↔ (𝑈 ∩ 𝑔) ⊆ 𝑈)
21	17, 20	mpbir 233	. . . . . . 7 ⊢ (𝑈 ∩ 𝑔) ∈ 𝒫 𝑈
22		unieq 4866	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑈 ∩ 𝑔) → ∪ 𝑓 = ∪ (𝑈 ∩ 𝑔))
23	22	ineq2d 4163	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑈 ∩ 𝑔) → (𝑧 ∩ ∪ 𝑓) = (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)))
24		ineq1 4156	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑈 ∩ 𝑔) → (𝑓 ∩ 𝒫 𝒫 𝑤) = ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤))
25	24	unieqd 4868	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑈 ∩ 𝑔) → ∪ (𝑓 ∩ 𝒫 𝒫 𝑤) = ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤))
26	23, 25	sseq12d 3960	. . . . . . . . . 10 ⊢ (𝑓 = (𝑈 ∩ 𝑔) → ((𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤) ↔ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)))
27	26	anbi2d 638	. . . . . . . . 9 ⊢ (𝑓 = (𝑈 ∩ 𝑔) → ((𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤))))
28	27	rexbidv 3176	. . . . . . . 8 ⊢ (𝑓 = (𝑈 ∩ 𝑔) → (∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤))))
29	28	rspcv 3568	. . . . . . 7 ⊢ ((𝑈 ∩ 𝑔) ∈ 𝒫 𝑈 → (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤))))
30	21, 29	ax-mp 5	. . . . . 6 ⊢ (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)))
31	30	alrimiv 1937	. . . . 5 ⊢ (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) → ∀𝑔∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)))
32		inss2 4180	. . . . . . . 8 ⊢ (𝑈 ∩ 𝑤) ⊆ 𝑤
33		sstr2 3934	. . . . . . . 8 ⊢ (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) → ((𝑈 ∩ 𝑤) ⊆ 𝑤 → 𝒫 𝑧 ⊆ 𝑤))
34	32, 33	mpi 20	. . . . . . 7 ⊢ (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) → 𝒫 𝑧 ⊆ 𝑤)
35		an12 653	. . . . . . . . . . . 12 ⊢ ((𝑣 ∈ 𝑈 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔)) ↔ (𝑖 ∈ 𝑣 ∧ (𝑣 ∈ 𝑈 ∧ 𝑣 ∈ 𝑔)))
36		elin 3911	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ (𝑈 ∩ 𝑔) ↔ (𝑣 ∈ 𝑈 ∧ 𝑣 ∈ 𝑔))
37	36	bicomi 226	. . . . . . . . . . . . 13 ⊢ ((𝑣 ∈ 𝑈 ∧ 𝑣 ∈ 𝑔) ↔ 𝑣 ∈ (𝑈 ∩ 𝑔))
38	37	anbi2i 631	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ 𝑣 ∧ (𝑣 ∈ 𝑈 ∧ 𝑣 ∈ 𝑔)) ↔ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ (𝑈 ∩ 𝑔)))
39	35, 38	bitri 277	. . . . . . . . . . 11 ⊢ ((𝑣 ∈ 𝑈 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔)) ↔ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ (𝑈 ∩ 𝑔)))
40	39	exbii 1858	. . . . . . . . . 10 ⊢ (∃𝑣(𝑣 ∈ 𝑈 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔)) ↔ ∃𝑣(𝑖 ∈ 𝑣 ∧ 𝑣 ∈ (𝑈 ∩ 𝑔)))
41		df-rex 3077	. . . . . . . . . 10 ⊢ (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) ↔ ∃𝑣(𝑣 ∈ 𝑈 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔)))
42		eluni 4858	. . . . . . . . . 10 ⊢ (𝑖 ∈ ∪ (𝑈 ∩ 𝑔) ↔ ∃𝑣(𝑖 ∈ 𝑣 ∧ 𝑣 ∈ (𝑈 ∩ 𝑔)))
43	40, 41, 42	3bitr4i 305	. . . . . . . . 9 ⊢ (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) ↔ 𝑖 ∈ ∪ (𝑈 ∩ 𝑔))
44		simp1 1145	. . . . . . . . . . . . 13 ⊢ (((𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) ∧ 𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ (𝑈 ∩ 𝑔)) → (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤))
45		elin 3911	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ↔ (𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ (𝑈 ∩ 𝑔)))
46	45	biimpri 230	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ (𝑈 ∩ 𝑔)) → 𝑖 ∈ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)))
47	46	3adant1 1139	. . . . . . . . . . . . 13 ⊢ (((𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) ∧ 𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ (𝑈 ∩ 𝑔)) → 𝑖 ∈ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)))
48	44, 47	sseldd 3928	. . . . . . . . . . . 12 ⊢ (((𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) ∧ 𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ (𝑈 ∩ 𝑔)) → 𝑖 ∈ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤))
49		eluni 4858	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) ↔ ∃𝑢(𝑖 ∈ 𝑢 ∧ 𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)))
50	48, 49	sylib 220	. . . . . . . . . . 11 ⊢ (((𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) ∧ 𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ (𝑈 ∩ 𝑔)) → ∃𝑢(𝑖 ∈ 𝑢 ∧ 𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)))
51		elinel1 4144	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) → 𝑢 ∈ (𝑈 ∩ 𝑔))
52	51	elin2d 4148	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) → 𝑢 ∈ 𝑔)
53		elinel2 4145	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) → 𝑢 ∈ 𝒫 𝒫 𝑤)
54		elpwpw 5049	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 ∈ 𝒫 𝒫 𝑤 ↔ (𝑢 ∈ V ∧ ∪ 𝑢 ⊆ 𝑤))
55	54	simprbi 500	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 ∈ 𝒫 𝒫 𝑤 → ∪ 𝑢 ⊆ 𝑤)
56	53, 55	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) → ∪ 𝑢 ⊆ 𝑤)
57	52, 56	jca 518	. . . . . . . . . . . . . . 15 ⊢ (𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) → (𝑢 ∈ 𝑔 ∧ ∪ 𝑢 ⊆ 𝑤))
58	57	anim2i 625	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∈ 𝑢 ∧ 𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)) → (𝑖 ∈ 𝑢 ∧ (𝑢 ∈ 𝑔 ∧ ∪ 𝑢 ⊆ 𝑤)))
59		an12 653	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∈ 𝑢 ∧ (𝑢 ∈ 𝑔 ∧ ∪ 𝑢 ⊆ 𝑤)) ↔ (𝑢 ∈ 𝑔 ∧ (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
60	58, 59	sylib 220	. . . . . . . . . . . . 13 ⊢ ((𝑖 ∈ 𝑢 ∧ 𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)) → (𝑢 ∈ 𝑔 ∧ (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
61	60	eximi 1845	. . . . . . . . . . . 12 ⊢ (∃𝑢(𝑖 ∈ 𝑢 ∧ 𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)) → ∃𝑢(𝑢 ∈ 𝑔 ∧ (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
62		df-rex 3077	. . . . . . . . . . . 12 ⊢ (∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ ∃𝑢(𝑢 ∈ 𝑔 ∧ (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
63	61, 62	sylibr 236	. . . . . . . . . . 11 ⊢ (∃𝑢(𝑖 ∈ 𝑢 ∧ 𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))
64	50, 63	syl 17	. . . . . . . . . 10 ⊢ (((𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) ∧ 𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ (𝑈 ∩ 𝑔)) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))
65	64	3expia 1130	. . . . . . . . 9 ⊢ (((𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) ∧ 𝑖 ∈ 𝑧) → (𝑖 ∈ ∪ (𝑈 ∩ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
66	43, 65	biimtrid 244	. . . . . . . 8 ⊢ (((𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) ∧ 𝑖 ∈ 𝑧) → (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
67	66	ralrimiva 3144	. . . . . . 7 ⊢ ((𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) → ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
68	34, 67	anim12i 621	. . . . . 6 ⊢ ((𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)) → (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
69	68	reximi 3090	. . . . 5 ⊢ (∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
70	31, 69	sylg 1833	. . . 4 ⊢ (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) → ∀𝑔∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
71		elequ2 2147	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑔 → (𝑣 ∈ 𝑓 ↔ 𝑣 ∈ 𝑔))
72	71	anbi2d 638	. . . . . . . . . 10 ⊢ (𝑓 = 𝑔 → ((𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) ↔ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔)))
73	72	rexbidv 3176	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) ↔ ∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔)))
74		rexeq 3306	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → (∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
75	73, 74	imbi12d 346	. . . . . . . 8 ⊢ (𝑓 = 𝑔 → ((∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) ↔ (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
76	75	ralbidv 3175	. . . . . . 7 ⊢ (𝑓 = 𝑔 → (∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) ↔ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
77	76	anbi2d 638	. . . . . 6 ⊢ (𝑓 = 𝑔 → ((𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) ↔ (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))
78	77	rexbidv 3176	. . . . 5 ⊢ (𝑓 = 𝑔 → (∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) ↔ ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))
79	78	cbvalvw 2046	. . . 4 ⊢ (∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) ↔ ∀𝑔∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
80	70, 79	sylibr 236	. . 3 ⊢ (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) → ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
81	16, 80	jca 518	. 2 ⊢ (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) → (𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))
82		nfv 1924	. . . 4 ⊢ Ⅎ𝑓𝒫 𝑧 ⊆ 𝑈
83		nfa1 2175	. . . 4 ⊢ Ⅎ𝑓∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
84	82, 83	nfan 1909	. . 3 ⊢ Ⅎ𝑓(𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
85		elpwi 4552	. . . 4 ⊢ (𝑓 ∈ 𝒫 𝑈 → 𝑓 ⊆ 𝑈)
86		sp 2208	. . . . . 6 ⊢ (∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
87		ssin 4181	. . . . . . . . . . . . 13 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝒫 𝑧 ⊆ 𝑤) ↔ 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤))
88	87	biimpi 218	. . . . . . . . . . . 12 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝒫 𝑧 ⊆ 𝑤) → 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤))
89	88	ex 415	. . . . . . . . . . 11 ⊢ (𝒫 𝑧 ⊆ 𝑈 → (𝒫 𝑧 ⊆ 𝑤 → 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤)))
90	89	adantr 483	. . . . . . . . . 10 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈) → (𝒫 𝑧 ⊆ 𝑤 → 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤)))
91		simp3 1147	. . . . . . . . . . . . . . . . 17 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) → 𝑖 ∈ ∪ 𝑓)
92		eluni 4858	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ ∪ 𝑓 ↔ ∃𝑣(𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓))
93	91, 92	sylib 220	. . . . . . . . . . . . . . . 16 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) → ∃𝑣(𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓))
94		simpl2 1202	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) → 𝑓 ⊆ 𝑈)
95		simprr 780	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) → 𝑣 ∈ 𝑓)
96	94, 95	sseldd 3928	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) → 𝑣 ∈ 𝑈)
97		simprl 778	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) → 𝑖 ∈ 𝑣)
98	96, 97, 95	3jca 1137	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) → (𝑣 ∈ 𝑈 ∧ 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓))
99	98	ex 415	. . . . . . . . . . . . . . . . 17 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) → ((𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → (𝑣 ∈ 𝑈 ∧ 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)))
100	99	eximdv 1927	. . . . . . . . . . . . . . . 16 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) → (∃𝑣(𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑣(𝑣 ∈ 𝑈 ∧ 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)))
101	93, 100	mpd 15	. . . . . . . . . . . . . . 15 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) → ∃𝑣(𝑣 ∈ 𝑈 ∧ 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓))
102		df-rex 3077	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) ↔ ∃𝑣(𝑣 ∈ 𝑈 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)))
103		3anass 1103	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑣 ∈ 𝑈 ∧ 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) ↔ (𝑣 ∈ 𝑈 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)))
104	103	exbii 1858	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑣(𝑣 ∈ 𝑈 ∧ 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) ↔ ∃𝑣(𝑣 ∈ 𝑈 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)))
105	102, 104	bitr4i 280	. . . . . . . . . . . . . . 15 ⊢ (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) ↔ ∃𝑣(𝑣 ∈ 𝑈 ∧ 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓))
106	101, 105	sylibr 236	. . . . . . . . . . . . . 14 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) → ∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓))
107	106	3expia 1130	. . . . . . . . . . . . 13 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈) → (𝑖 ∈ ∪ 𝑓 → ∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)))
108		elin 3911	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 ∈ (𝑓 ∩ 𝒫 𝒫 𝑤) ↔ (𝑢 ∈ 𝑓 ∧ 𝑢 ∈ 𝒫 𝒫 𝑤))
109		vex 3448	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑢 ∈ V
110	109, 54	mpbiran 717	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ 𝒫 𝒫 𝑤 ↔ ∪ 𝑢 ⊆ 𝑤)
111	110	anbi2i 631	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑢 ∈ 𝑓 ∧ 𝑢 ∈ 𝒫 𝒫 𝑤) ↔ (𝑢 ∈ 𝑓 ∧ ∪ 𝑢 ⊆ 𝑤))
112	108, 111	bitri 277	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 ∈ (𝑓 ∩ 𝒫 𝒫 𝑤) ↔ (𝑢 ∈ 𝑓 ∧ ∪ 𝑢 ⊆ 𝑤))
113	112	anbi2i 631	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ 𝑢 ∧ 𝑢 ∈ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ (𝑖 ∈ 𝑢 ∧ (𝑢 ∈ 𝑓 ∧ ∪ 𝑢 ⊆ 𝑤)))
114		an12 653	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ∈ 𝑓 ∧ (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) ↔ (𝑖 ∈ 𝑢 ∧ (𝑢 ∈ 𝑓 ∧ ∪ 𝑢 ⊆ 𝑤)))
115	113, 114	bitr4i 280	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ 𝑢 ∧ 𝑢 ∈ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ (𝑢 ∈ 𝑓 ∧ (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
116	115	exbii 1858	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑢(𝑖 ∈ 𝑢 ∧ 𝑢 ∈ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ ∃𝑢(𝑢 ∈ 𝑓 ∧ (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
117		eluni 4858	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤) ↔ ∃𝑢(𝑖 ∈ 𝑢 ∧ 𝑢 ∈ (𝑓 ∩ 𝒫 𝒫 𝑤)))
118		df-rex 3077	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ ∃𝑢(𝑢 ∈ 𝑓 ∧ (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
119	116, 117, 118	3bitr4i 305	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤) ↔ ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))
120	119	biimpri 230	. . . . . . . . . . . . . 14 ⊢ (∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤))
121	120	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈) → (∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))
122	107, 121	imim12d 81	. . . . . . . . . . . 12 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈) → ((∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) → (𝑖 ∈ ∪ 𝑓 → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤))))
123	122	ralimdv 3166	. . . . . . . . . . 11 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈) → (∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) → ∀𝑖 ∈ 𝑧 (𝑖 ∈ ∪ 𝑓 → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤))))
124		elin 3911	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (𝑧 ∩ ∪ 𝑓) ↔ (𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ 𝑓))
125	124	imbi1i 351	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∈ (𝑧 ∩ ∪ 𝑓) → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ ((𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ 𝑓) → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))
126		impexp 453	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ 𝑓) → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ (𝑖 ∈ 𝑧 → (𝑖 ∈ ∪ 𝑓 → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤))))
127	125, 126	bitri 277	. . . . . . . . . . . . 13 ⊢ ((𝑖 ∈ (𝑧 ∩ ∪ 𝑓) → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ (𝑖 ∈ 𝑧 → (𝑖 ∈ ∪ 𝑓 → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤))))
128	127	albii 1829	. . . . . . . . . . . 12 ⊢ (∀𝑖(𝑖 ∈ (𝑧 ∩ ∪ 𝑓) → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ ∀𝑖(𝑖 ∈ 𝑧 → (𝑖 ∈ ∪ 𝑓 → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤))))
129		df-ss 3912	. . . . . . . . . . . 12 ⊢ ((𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤) ↔ ∀𝑖(𝑖 ∈ (𝑧 ∩ ∪ 𝑓) → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))
130		df-ral 3067	. . . . . . . . . . . 12 ⊢ (∀𝑖 ∈ 𝑧 (𝑖 ∈ ∪ 𝑓 → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ ∀𝑖(𝑖 ∈ 𝑧 → (𝑖 ∈ ∪ 𝑓 → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤))))
131	128, 129, 130	3bitr4i 305	. . . . . . . . . . 11 ⊢ ((𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤) ↔ ∀𝑖 ∈ 𝑧 (𝑖 ∈ ∪ 𝑓 → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))
132	123, 131	imbitrrdi 254	. . . . . . . . . 10 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈) → (∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) → (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))
133	90, 132	anim12d 617	. . . . . . . . 9 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈) → ((𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) → (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤))))
134	133	reximdv 3167	. . . . . . . 8 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈) → (∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤))))
135	134	3impia 1126	. . . . . . 7 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))
136	135	3com23 1135	. . . . . 6 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) ∧ 𝑓 ⊆ 𝑈) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))
137	86, 136	syl3an2 1173	. . . . 5 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) ∧ 𝑓 ⊆ 𝑈) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))
138	137	3expa 1127	. . . 4 ⊢ (((𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) ∧ 𝑓 ⊆ 𝑈) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))
139	85, 138	sylan2 601	. . 3 ⊢ (((𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) ∧ 𝑓 ∈ 𝒫 𝑈) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))
140	84, 139	ralrimia 3251	. 2 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → ∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))
141	81, 140	impbii 211	1 ⊢ (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ (𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1095  ∀wal 1548   = wceq 1550  ⊤wtru 1551  ∃wex 1789   ∈ wcel 2132  ∀wral 3066  ∃wrex 3076  Vcvv 3444   ∩ cin 3894   ⊆ wss 3895  ∅c0 4276  𝒫 cpw 4545  ∪ cuni 4855

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-10 2165  ax-12 2202  ax-ext 2724  ax-sep 5236  ax-nul 5246

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-nf 1794  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-ral 3067  df-rex 3077  df-rab 3405  df-v 3446  df-dif 3898  df-in 3902  df-ss 3912  df-nul 4277  df-pw 4547  df-uni 4856

This theorem is referenced by:  dfuniv2  44816