Theorem ismnushort 43641

Description: Express the predicate on 𝑈 and 𝑧 in ismnu 43601 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 482	. . . . . 6 ⊢ ((𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) → 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤))
2	1	reximi 3078	. . . . 5 ⊢ (∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) → ∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤))
3	2	ralimi 3077	. . . 4 ⊢ (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) → ∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤))
4		0elpw 5347	. . . . . . . 8 ⊢ ∅ ∈ 𝒫 𝑈
5	4	a1i 11	. . . . . . 7 ⊢ (⊤ → ∅ ∈ 𝒫 𝑈)
6		biidd 262	. . . . . . 7 ⊢ ((⊤ ∧ 𝑓 = ∅) → (∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ↔ ∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤)))
7	5, 6	rspcdv 3598	. . . . . 6 ⊢ (⊤ → (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) → ∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤)))
8	7	mptru 1540	. . . . 5 ⊢ (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) → ∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤))
9		inss1 4223	. . . . . . 7 ⊢ (𝑈 ∩ 𝑤) ⊆ 𝑈
10		sstr2 3984	. . . . . . 7 ⊢ (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) → ((𝑈 ∩ 𝑤) ⊆ 𝑈 → 𝒫 𝑧 ⊆ 𝑈))
11	9, 10	mpi 20	. . . . . 6 ⊢ (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) → 𝒫 𝑧 ⊆ 𝑈)
12	11	reximi 3078	. . . . 5 ⊢ (∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) → ∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ 𝑈)
13	8, 12	syl 17	. . . 4 ⊢ (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) → ∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ 𝑈)
14		rexex 3070	. . . . 5 ⊢ (∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ 𝑈 → ∃𝑤𝒫 𝑧 ⊆ 𝑈)
15		ax5e 1907	. . . . 5 ⊢ (∃𝑤𝒫 𝑧 ⊆ 𝑈 → 𝒫 𝑧 ⊆ 𝑈)
16	14, 15	syl 17	. . . 4 ⊢ (∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ 𝑈 → 𝒫 𝑧 ⊆ 𝑈)
17	3, 13, 16	3syl 18	. . 3 ⊢ (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) → 𝒫 𝑧 ⊆ 𝑈)
18		inss1 4223	. . . . . . . 8 ⊢ (𝑈 ∩ 𝑔) ⊆ 𝑈
19		vex 3472	. . . . . . . . . 10 ⊢ 𝑔 ∈ V
20	19	inex2 5311	. . . . . . . . 9 ⊢ (𝑈 ∩ 𝑔) ∈ V
21	20	elpw 4601	. . . . . . . 8 ⊢ ((𝑈 ∩ 𝑔) ∈ 𝒫 𝑈 ↔ (𝑈 ∩ 𝑔) ⊆ 𝑈)
22	18, 21	mpbir 230	. . . . . . 7 ⊢ (𝑈 ∩ 𝑔) ∈ 𝒫 𝑈
23		unieq 4913	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑈 ∩ 𝑔) → ∪ 𝑓 = ∪ (𝑈 ∩ 𝑔))
24	23	ineq2d 4207	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑈 ∩ 𝑔) → (𝑧 ∩ ∪ 𝑓) = (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)))
25		ineq1 4200	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑈 ∩ 𝑔) → (𝑓 ∩ 𝒫 𝒫 𝑤) = ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤))
26	25	unieqd 4915	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑈 ∩ 𝑔) → ∪ (𝑓 ∩ 𝒫 𝒫 𝑤) = ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤))
27	24, 26	sseq12d 4010	. . . . . . . . . 10 ⊢ (𝑓 = (𝑈 ∩ 𝑔) → ((𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤) ↔ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)))
28	27	anbi2d 628	. . . . . . . . 9 ⊢ (𝑓 = (𝑈 ∩ 𝑔) → ((𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤))))
29	28	rexbidv 3172	. . . . . . . 8 ⊢ (𝑓 = (𝑈 ∩ 𝑔) → (∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤))))
30	29	rspcv 3602	. . . . . . 7 ⊢ ((𝑈 ∩ 𝑔) ∈ 𝒫 𝑈 → (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤))))
31	22, 30	ax-mp 5	. . . . . 6 ⊢ (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)))
32	31	alrimiv 1922	. . . . 5 ⊢ (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) → ∀𝑔∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)))
33		inss2 4224	. . . . . . . 8 ⊢ (𝑈 ∩ 𝑤) ⊆ 𝑤
34		sstr2 3984	. . . . . . . 8 ⊢ (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) → ((𝑈 ∩ 𝑤) ⊆ 𝑤 → 𝒫 𝑧 ⊆ 𝑤))
35	33, 34	mpi 20	. . . . . . 7 ⊢ (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) → 𝒫 𝑧 ⊆ 𝑤)
36		an12 642	. . . . . . . . . . . 12 ⊢ ((𝑣 ∈ 𝑈 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔)) ↔ (𝑖 ∈ 𝑣 ∧ (𝑣 ∈ 𝑈 ∧ 𝑣 ∈ 𝑔)))
37		elin 3959	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ (𝑈 ∩ 𝑔) ↔ (𝑣 ∈ 𝑈 ∧ 𝑣 ∈ 𝑔))
38	37	bicomi 223	. . . . . . . . . . . . 13 ⊢ ((𝑣 ∈ 𝑈 ∧ 𝑣 ∈ 𝑔) ↔ 𝑣 ∈ (𝑈 ∩ 𝑔))
39	38	anbi2i 622	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ 𝑣 ∧ (𝑣 ∈ 𝑈 ∧ 𝑣 ∈ 𝑔)) ↔ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ (𝑈 ∩ 𝑔)))
40	36, 39	bitri 275	. . . . . . . . . . 11 ⊢ ((𝑣 ∈ 𝑈 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔)) ↔ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ (𝑈 ∩ 𝑔)))
41	40	exbii 1842	. . . . . . . . . 10 ⊢ (∃𝑣(𝑣 ∈ 𝑈 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔)) ↔ ∃𝑣(𝑖 ∈ 𝑣 ∧ 𝑣 ∈ (𝑈 ∩ 𝑔)))
42		df-rex 3065	. . . . . . . . . 10 ⊢ (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) ↔ ∃𝑣(𝑣 ∈ 𝑈 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔)))
43		eluni 4905	. . . . . . . . . 10 ⊢ (𝑖 ∈ ∪ (𝑈 ∩ 𝑔) ↔ ∃𝑣(𝑖 ∈ 𝑣 ∧ 𝑣 ∈ (𝑈 ∩ 𝑔)))
44	41, 42, 43	3bitr4i 303	. . . . . . . . 9 ⊢ (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) ↔ 𝑖 ∈ ∪ (𝑈 ∩ 𝑔))
45		simp1 1133	. . . . . . . . . . . . 13 ⊢ (((𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) ∧ 𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ (𝑈 ∩ 𝑔)) → (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤))
46		elin 3959	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ↔ (𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ (𝑈 ∩ 𝑔)))
47	46	biimpri 227	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ (𝑈 ∩ 𝑔)) → 𝑖 ∈ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)))
48	47	3adant1 1127	. . . . . . . . . . . . 13 ⊢ (((𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) ∧ 𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ (𝑈 ∩ 𝑔)) → 𝑖 ∈ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)))
49	45, 48	sseldd 3978	. . . . . . . . . . . 12 ⊢ (((𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) ∧ 𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ (𝑈 ∩ 𝑔)) → 𝑖 ∈ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤))
50		eluni 4905	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) ↔ ∃𝑢(𝑖 ∈ 𝑢 ∧ 𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)))
51	49, 50	sylib 217	. . . . . . . . . . 11 ⊢ (((𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) ∧ 𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ (𝑈 ∩ 𝑔)) → ∃𝑢(𝑖 ∈ 𝑢 ∧ 𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)))
52		elinel1 4190	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) → 𝑢 ∈ (𝑈 ∩ 𝑔))
53	52	elin2d 4194	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) → 𝑢 ∈ 𝑔)
54		elinel2 4191	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) → 𝑢 ∈ 𝒫 𝒫 𝑤)
55		elpwpw 5098	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 ∈ 𝒫 𝒫 𝑤 ↔ (𝑢 ∈ V ∧ ∪ 𝑢 ⊆ 𝑤))
56	55	simprbi 496	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 ∈ 𝒫 𝒫 𝑤 → ∪ 𝑢 ⊆ 𝑤)
57	54, 56	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) → ∪ 𝑢 ⊆ 𝑤)
58	53, 57	jca 511	. . . . . . . . . . . . . . 15 ⊢ (𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) → (𝑢 ∈ 𝑔 ∧ ∪ 𝑢 ⊆ 𝑤))
59	58	anim2i 616	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∈ 𝑢 ∧ 𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)) → (𝑖 ∈ 𝑢 ∧ (𝑢 ∈ 𝑔 ∧ ∪ 𝑢 ⊆ 𝑤)))
60		an12 642	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∈ 𝑢 ∧ (𝑢 ∈ 𝑔 ∧ ∪ 𝑢 ⊆ 𝑤)) ↔ (𝑢 ∈ 𝑔 ∧ (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
61	59, 60	sylib 217	. . . . . . . . . . . . 13 ⊢ ((𝑖 ∈ 𝑢 ∧ 𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)) → (𝑢 ∈ 𝑔 ∧ (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
62	61	eximi 1829	. . . . . . . . . . . 12 ⊢ (∃𝑢(𝑖 ∈ 𝑢 ∧ 𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)) → ∃𝑢(𝑢 ∈ 𝑔 ∧ (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
63		df-rex 3065	. . . . . . . . . . . 12 ⊢ (∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ ∃𝑢(𝑢 ∈ 𝑔 ∧ (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
64	62, 63	sylibr 233	. . . . . . . . . . 11 ⊢ (∃𝑢(𝑖 ∈ 𝑢 ∧ 𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))
65	51, 64	syl 17	. . . . . . . . . 10 ⊢ (((𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) ∧ 𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ (𝑈 ∩ 𝑔)) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))
66	65	3expia 1118	. . . . . . . . 9 ⊢ (((𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) ∧ 𝑖 ∈ 𝑧) → (𝑖 ∈ ∪ (𝑈 ∩ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
67	44, 66	biimtrid 241	. . . . . . . 8 ⊢ (((𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) ∧ 𝑖 ∈ 𝑧) → (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
68	67	ralrimiva 3140	. . . . . . 7 ⊢ ((𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) → ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
69	35, 68	anim12i 612	. . . . . 6 ⊢ ((𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)) → (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
70	69	reximi 3078	. . . . 5 ⊢ (∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
71	32, 70	sylg 1817	. . . 4 ⊢ (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) → ∀𝑔∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
72		elequ2 2113	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑔 → (𝑣 ∈ 𝑓 ↔ 𝑣 ∈ 𝑔))
73	72	anbi2d 628	. . . . . . . . . 10 ⊢ (𝑓 = 𝑔 → ((𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) ↔ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔)))
74	73	rexbidv 3172	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) ↔ ∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔)))
75		rexeq 3315	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → (∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
76	74, 75	imbi12d 344	. . . . . . . 8 ⊢ (𝑓 = 𝑔 → ((∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) ↔ (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
77	76	ralbidv 3171	. . . . . . 7 ⊢ (𝑓 = 𝑔 → (∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) ↔ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
78	77	anbi2d 628	. . . . . 6 ⊢ (𝑓 = 𝑔 → ((𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) ↔ (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))
79	78	rexbidv 3172	. . . . 5 ⊢ (𝑓 = 𝑔 → (∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) ↔ ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))
80	79	cbvalvw 2031	. . . 4 ⊢ (∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) ↔ ∀𝑔∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
81	71, 80	sylibr 233	. . 3 ⊢ (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) → ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
82	17, 81	jca 511	. 2 ⊢ (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) → (𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))
83		nfv 1909	. . . 4 ⊢ Ⅎ𝑓𝒫 𝑧 ⊆ 𝑈
84		nfa1 2140	. . . 4 ⊢ Ⅎ𝑓∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
85	83, 84	nfan 1894	. . 3 ⊢ Ⅎ𝑓(𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
86		elpwi 4604	. . . 4 ⊢ (𝑓 ∈ 𝒫 𝑈 → 𝑓 ⊆ 𝑈)
87		sp 2168	. . . . . 6 ⊢ (∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
88		ssin 4225	. . . . . . . . . . . . 13 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝒫 𝑧 ⊆ 𝑤) ↔ 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤))
89	88	biimpi 215	. . . . . . . . . . . 12 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝒫 𝑧 ⊆ 𝑤) → 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤))
90	89	ex 412	. . . . . . . . . . 11 ⊢ (𝒫 𝑧 ⊆ 𝑈 → (𝒫 𝑧 ⊆ 𝑤 → 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤)))
91	90	adantr 480	. . . . . . . . . 10 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈) → (𝒫 𝑧 ⊆ 𝑤 → 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤)))
92		simp3 1135	. . . . . . . . . . . . . . . . 17 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) → 𝑖 ∈ ∪ 𝑓)
93		eluni 4905	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ ∪ 𝑓 ↔ ∃𝑣(𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓))
94	92, 93	sylib 217	. . . . . . . . . . . . . . . 16 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) → ∃𝑣(𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓))
95		simpl2 1189	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) → 𝑓 ⊆ 𝑈)
96		simprr 770	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) → 𝑣 ∈ 𝑓)
97	95, 96	sseldd 3978	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) → 𝑣 ∈ 𝑈)
98		simprl 768	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) → 𝑖 ∈ 𝑣)
99	97, 98, 96	3jca 1125	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) → (𝑣 ∈ 𝑈 ∧ 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓))
100	99	ex 412	. . . . . . . . . . . . . . . . 17 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) → ((𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → (𝑣 ∈ 𝑈 ∧ 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)))
101	100	eximdv 1912	. . . . . . . . . . . . . . . 16 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) → (∃𝑣(𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑣(𝑣 ∈ 𝑈 ∧ 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)))
102	94, 101	mpd 15	. . . . . . . . . . . . . . 15 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) → ∃𝑣(𝑣 ∈ 𝑈 ∧ 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓))
103		df-rex 3065	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) ↔ ∃𝑣(𝑣 ∈ 𝑈 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)))
104		3anass 1092	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑣 ∈ 𝑈 ∧ 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) ↔ (𝑣 ∈ 𝑈 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)))
105	104	exbii 1842	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑣(𝑣 ∈ 𝑈 ∧ 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) ↔ ∃𝑣(𝑣 ∈ 𝑈 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)))
106	103, 105	bitr4i 278	. . . . . . . . . . . . . . 15 ⊢ (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) ↔ ∃𝑣(𝑣 ∈ 𝑈 ∧ 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓))
107	102, 106	sylibr 233	. . . . . . . . . . . . . 14 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) → ∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓))
108	107	3expia 1118	. . . . . . . . . . . . 13 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈) → (𝑖 ∈ ∪ 𝑓 → ∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)))
109		elin 3959	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 ∈ (𝑓 ∩ 𝒫 𝒫 𝑤) ↔ (𝑢 ∈ 𝑓 ∧ 𝑢 ∈ 𝒫 𝒫 𝑤))
110		vex 3472	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑢 ∈ V
111	110, 55	mpbiran 706	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ 𝒫 𝒫 𝑤 ↔ ∪ 𝑢 ⊆ 𝑤)
112	111	anbi2i 622	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑢 ∈ 𝑓 ∧ 𝑢 ∈ 𝒫 𝒫 𝑤) ↔ (𝑢 ∈ 𝑓 ∧ ∪ 𝑢 ⊆ 𝑤))
113	109, 112	bitri 275	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 ∈ (𝑓 ∩ 𝒫 𝒫 𝑤) ↔ (𝑢 ∈ 𝑓 ∧ ∪ 𝑢 ⊆ 𝑤))
114	113	anbi2i 622	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ 𝑢 ∧ 𝑢 ∈ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ (𝑖 ∈ 𝑢 ∧ (𝑢 ∈ 𝑓 ∧ ∪ 𝑢 ⊆ 𝑤)))
115		an12 642	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ∈ 𝑓 ∧ (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) ↔ (𝑖 ∈ 𝑢 ∧ (𝑢 ∈ 𝑓 ∧ ∪ 𝑢 ⊆ 𝑤)))
116	114, 115	bitr4i 278	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ 𝑢 ∧ 𝑢 ∈ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ (𝑢 ∈ 𝑓 ∧ (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
117	116	exbii 1842	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑢(𝑖 ∈ 𝑢 ∧ 𝑢 ∈ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ ∃𝑢(𝑢 ∈ 𝑓 ∧ (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
118		eluni 4905	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤) ↔ ∃𝑢(𝑖 ∈ 𝑢 ∧ 𝑢 ∈ (𝑓 ∩ 𝒫 𝒫 𝑤)))
119		df-rex 3065	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ ∃𝑢(𝑢 ∈ 𝑓 ∧ (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
120	117, 118, 119	3bitr4i 303	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤) ↔ ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))
121	120	biimpri 227	. . . . . . . . . . . . . 14 ⊢ (∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤))
122	121	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈) → (∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))
123	108, 122	imim12d 81	. . . . . . . . . . . 12 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈) → ((∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) → (𝑖 ∈ ∪ 𝑓 → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤))))
124	123	ralimdv 3163	. . . . . . . . . . 11 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈) → (∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) → ∀𝑖 ∈ 𝑧 (𝑖 ∈ ∪ 𝑓 → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤))))
125		elin 3959	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (𝑧 ∩ ∪ 𝑓) ↔ (𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ 𝑓))
126	125	imbi1i 349	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∈ (𝑧 ∩ ∪ 𝑓) → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ ((𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ 𝑓) → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))
127		impexp 450	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ 𝑓) → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ (𝑖 ∈ 𝑧 → (𝑖 ∈ ∪ 𝑓 → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤))))
128	126, 127	bitri 275	. . . . . . . . . . . . 13 ⊢ ((𝑖 ∈ (𝑧 ∩ ∪ 𝑓) → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ (𝑖 ∈ 𝑧 → (𝑖 ∈ ∪ 𝑓 → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤))))
129	128	albii 1813	. . . . . . . . . . . 12 ⊢ (∀𝑖(𝑖 ∈ (𝑧 ∩ ∪ 𝑓) → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ ∀𝑖(𝑖 ∈ 𝑧 → (𝑖 ∈ ∪ 𝑓 → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤))))
130		dfss2 3963	. . . . . . . . . . . 12 ⊢ ((𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤) ↔ ∀𝑖(𝑖 ∈ (𝑧 ∩ ∪ 𝑓) → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))
131		df-ral 3056	. . . . . . . . . . . 12 ⊢ (∀𝑖 ∈ 𝑧 (𝑖 ∈ ∪ 𝑓 → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ ∀𝑖(𝑖 ∈ 𝑧 → (𝑖 ∈ ∪ 𝑓 → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤))))
132	129, 130, 131	3bitr4i 303	. . . . . . . . . . 11 ⊢ ((𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤) ↔ ∀𝑖 ∈ 𝑧 (𝑖 ∈ ∪ 𝑓 → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))
133	124, 132	imbitrrdi 251	. . . . . . . . . 10 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈) → (∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) → (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))
134	91, 133	anim12d 608	. . . . . . . . 9 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈) → ((𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) → (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤))))
135	134	reximdv 3164	. . . . . . . 8 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈) → (∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤))))
136	135	3impia 1114	. . . . . . 7 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))
137	136	3com23 1123	. . . . . 6 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) ∧ 𝑓 ⊆ 𝑈) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))
138	87, 137	syl3an2 1161	. . . . 5 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) ∧ 𝑓 ⊆ 𝑈) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))
139	138	3expa 1115	. . . 4 ⊢ (((𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) ∧ 𝑓 ⊆ 𝑈) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))
140	86, 139	sylan2 592	. . 3 ⊢ (((𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) ∧ 𝑓 ∈ 𝒫 𝑈) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))
141	85, 140	ralrimia 3249	. 2 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → ∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))
142	82, 141	impbii 208	1 ⊢ (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ (𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1084  ∀wal 1531   = wceq 1533  ⊤wtru 1534  ∃wex 1773   ∈ wcel 2098  ∀wral 3055  ∃wrex 3064  Vcvv 3468   ∩ cin 3942   ⊆ wss 3943  ∅c0 4317  𝒫 cpw 4597  ∪ cuni 4902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-12 2163  ax-ext 2697  ax-sep 5292  ax-nul 5299

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-clab 2704  df-cleq 2718  df-clel 2804  df-ral 3056  df-rex 3065  df-rab 3427  df-v 3470  df-dif 3946  df-in 3950  df-ss 3960  df-nul 4318  df-pw 4599  df-uni 4903

This theorem is referenced by:  dfuniv2  43642