Theorem ismnushort 41533

Description: Express the predicate on 𝑈 and 𝑧 in ismnu 41493 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 486	. . . . . 6 ⊢ ((𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) → 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤))
2	1	reximi 3156	. . . . 5 ⊢ (∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) → ∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤))
3	2	ralimi 3073	. . . 4 ⊢ (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) → ∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤))
4		0elpw 5232	. . . . . . . 8 ⊢ ∅ ∈ 𝒫 𝑈
5	4	a1i 11	. . . . . . 7 ⊢ (⊤ → ∅ ∈ 𝒫 𝑈)
6		biidd 265	. . . . . . 7 ⊢ ((⊤ ∧ 𝑓 = ∅) → (∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ↔ ∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤)))
7	5, 6	rspcdv 3519	. . . . . 6 ⊢ (⊤ → (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) → ∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤)))
8	7	mptru 1550	. . . . 5 ⊢ (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) → ∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤))
9		inss1 4129	. . . . . . 7 ⊢ (𝑈 ∩ 𝑤) ⊆ 𝑈
10		sstr2 3894	. . . . . . 7 ⊢ (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) → ((𝑈 ∩ 𝑤) ⊆ 𝑈 → 𝒫 𝑧 ⊆ 𝑈))
11	9, 10	mpi 20	. . . . . 6 ⊢ (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) → 𝒫 𝑧 ⊆ 𝑈)
12	11	reximi 3156	. . . . 5 ⊢ (∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) → ∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ 𝑈)
13	8, 12	syl 17	. . . 4 ⊢ (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) → ∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ 𝑈)
14		rexex 3152	. . . . 5 ⊢ (∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ 𝑈 → ∃𝑤𝒫 𝑧 ⊆ 𝑈)
15		ax5e 1920	. . . . 5 ⊢ (∃𝑤𝒫 𝑧 ⊆ 𝑈 → 𝒫 𝑧 ⊆ 𝑈)
16	14, 15	syl 17	. . . 4 ⊢ (∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ 𝑈 → 𝒫 𝑧 ⊆ 𝑈)
17	3, 13, 16	3syl 18	. . 3 ⊢ (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) → 𝒫 𝑧 ⊆ 𝑈)
18		inss1 4129	. . . . . . . 8 ⊢ (𝑈 ∩ 𝑔) ⊆ 𝑈
19		vex 3402	. . . . . . . . . 10 ⊢ 𝑔 ∈ V
20	19	inex2 5196	. . . . . . . . 9 ⊢ (𝑈 ∩ 𝑔) ∈ V
21	20	elpw 4503	. . . . . . . 8 ⊢ ((𝑈 ∩ 𝑔) ∈ 𝒫 𝑈 ↔ (𝑈 ∩ 𝑔) ⊆ 𝑈)
22	18, 21	mpbir 234	. . . . . . 7 ⊢ (𝑈 ∩ 𝑔) ∈ 𝒫 𝑈
23		unieq 4816	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑈 ∩ 𝑔) → ∪ 𝑓 = ∪ (𝑈 ∩ 𝑔))
24	23	ineq2d 4113	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑈 ∩ 𝑔) → (𝑧 ∩ ∪ 𝑓) = (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)))
25		ineq1 4106	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑈 ∩ 𝑔) → (𝑓 ∩ 𝒫 𝒫 𝑤) = ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤))
26	25	unieqd 4819	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑈 ∩ 𝑔) → ∪ (𝑓 ∩ 𝒫 𝒫 𝑤) = ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤))
27	24, 26	sseq12d 3920	. . . . . . . . . 10 ⊢ (𝑓 = (𝑈 ∩ 𝑔) → ((𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤) ↔ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)))
28	27	anbi2d 632	. . . . . . . . 9 ⊢ (𝑓 = (𝑈 ∩ 𝑔) → ((𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤))))
29	28	rexbidv 3206	. . . . . . . 8 ⊢ (𝑓 = (𝑈 ∩ 𝑔) → (∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤))))
30	29	rspcv 3522	. . . . . . 7 ⊢ ((𝑈 ∩ 𝑔) ∈ 𝒫 𝑈 → (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤))))
31	22, 30	ax-mp 5	. . . . . 6 ⊢ (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)))
32	31	alrimiv 1935	. . . . 5 ⊢ (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) → ∀𝑔∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)))
33		inss2 4130	. . . . . . . 8 ⊢ (𝑈 ∩ 𝑤) ⊆ 𝑤
34		sstr2 3894	. . . . . . . 8 ⊢ (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) → ((𝑈 ∩ 𝑤) ⊆ 𝑤 → 𝒫 𝑧 ⊆ 𝑤))
35	33, 34	mpi 20	. . . . . . 7 ⊢ (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) → 𝒫 𝑧 ⊆ 𝑤)
36		an12 645	. . . . . . . . . . . 12 ⊢ ((𝑣 ∈ 𝑈 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔)) ↔ (𝑖 ∈ 𝑣 ∧ (𝑣 ∈ 𝑈 ∧ 𝑣 ∈ 𝑔)))
37		elin 3869	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ (𝑈 ∩ 𝑔) ↔ (𝑣 ∈ 𝑈 ∧ 𝑣 ∈ 𝑔))
38	37	bicomi 227	. . . . . . . . . . . . 13 ⊢ ((𝑣 ∈ 𝑈 ∧ 𝑣 ∈ 𝑔) ↔ 𝑣 ∈ (𝑈 ∩ 𝑔))
39	38	anbi2i 626	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ 𝑣 ∧ (𝑣 ∈ 𝑈 ∧ 𝑣 ∈ 𝑔)) ↔ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ (𝑈 ∩ 𝑔)))
40	36, 39	bitri 278	. . . . . . . . . . 11 ⊢ ((𝑣 ∈ 𝑈 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔)) ↔ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ (𝑈 ∩ 𝑔)))
41	40	exbii 1855	. . . . . . . . . 10 ⊢ (∃𝑣(𝑣 ∈ 𝑈 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔)) ↔ ∃𝑣(𝑖 ∈ 𝑣 ∧ 𝑣 ∈ (𝑈 ∩ 𝑔)))
42		df-rex 3057	. . . . . . . . . 10 ⊢ (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) ↔ ∃𝑣(𝑣 ∈ 𝑈 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔)))
43		eluni 4808	. . . . . . . . . 10 ⊢ (𝑖 ∈ ∪ (𝑈 ∩ 𝑔) ↔ ∃𝑣(𝑖 ∈ 𝑣 ∧ 𝑣 ∈ (𝑈 ∩ 𝑔)))
44	41, 42, 43	3bitr4i 306	. . . . . . . . 9 ⊢ (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) ↔ 𝑖 ∈ ∪ (𝑈 ∩ 𝑔))
45		simp1 1138	. . . . . . . . . . . . 13 ⊢ (((𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) ∧ 𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ (𝑈 ∩ 𝑔)) → (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤))
46		elin 3869	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ↔ (𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ (𝑈 ∩ 𝑔)))
47	46	biimpri 231	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ (𝑈 ∩ 𝑔)) → 𝑖 ∈ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)))
48	47	3adant1 1132	. . . . . . . . . . . . 13 ⊢ (((𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) ∧ 𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ (𝑈 ∩ 𝑔)) → 𝑖 ∈ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)))
49	45, 48	sseldd 3888	. . . . . . . . . . . 12 ⊢ (((𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) ∧ 𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ (𝑈 ∩ 𝑔)) → 𝑖 ∈ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤))
50		eluni 4808	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) ↔ ∃𝑢(𝑖 ∈ 𝑢 ∧ 𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)))
51	49, 50	sylib 221	. . . . . . . . . . 11 ⊢ (((𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) ∧ 𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ (𝑈 ∩ 𝑔)) → ∃𝑢(𝑖 ∈ 𝑢 ∧ 𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)))
52		elinel1 4095	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) → 𝑢 ∈ (𝑈 ∩ 𝑔))
53	52	elin2d 4099	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) → 𝑢 ∈ 𝑔)
54		elinel2 4096	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) → 𝑢 ∈ 𝒫 𝒫 𝑤)
55		elpwpw 4996	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 ∈ 𝒫 𝒫 𝑤 ↔ (𝑢 ∈ V ∧ ∪ 𝑢 ⊆ 𝑤))
56	55	simprbi 500	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 ∈ 𝒫 𝒫 𝑤 → ∪ 𝑢 ⊆ 𝑤)
57	54, 56	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) → ∪ 𝑢 ⊆ 𝑤)
58	53, 57	jca 515	. . . . . . . . . . . . . . 15 ⊢ (𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) → (𝑢 ∈ 𝑔 ∧ ∪ 𝑢 ⊆ 𝑤))
59	58	anim2i 620	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∈ 𝑢 ∧ 𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)) → (𝑖 ∈ 𝑢 ∧ (𝑢 ∈ 𝑔 ∧ ∪ 𝑢 ⊆ 𝑤)))
60		an12 645	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∈ 𝑢 ∧ (𝑢 ∈ 𝑔 ∧ ∪ 𝑢 ⊆ 𝑤)) ↔ (𝑢 ∈ 𝑔 ∧ (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
61	59, 60	sylib 221	. . . . . . . . . . . . 13 ⊢ ((𝑖 ∈ 𝑢 ∧ 𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)) → (𝑢 ∈ 𝑔 ∧ (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
62	61	eximi 1842	. . . . . . . . . . . 12 ⊢ (∃𝑢(𝑖 ∈ 𝑢 ∧ 𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)) → ∃𝑢(𝑢 ∈ 𝑔 ∧ (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
63		df-rex 3057	. . . . . . . . . . . 12 ⊢ (∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ ∃𝑢(𝑢 ∈ 𝑔 ∧ (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
64	62, 63	sylibr 237	. . . . . . . . . . 11 ⊢ (∃𝑢(𝑖 ∈ 𝑢 ∧ 𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))
65	51, 64	syl 17	. . . . . . . . . 10 ⊢ (((𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) ∧ 𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ (𝑈 ∩ 𝑔)) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))
66	65	3expia 1123	. . . . . . . . 9 ⊢ (((𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) ∧ 𝑖 ∈ 𝑧) → (𝑖 ∈ ∪ (𝑈 ∩ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
67	44, 66	syl5bi 245	. . . . . . . 8 ⊢ (((𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) ∧ 𝑖 ∈ 𝑧) → (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
68	67	ralrimiva 3095	. . . . . . 7 ⊢ ((𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) → ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
69	35, 68	anim12i 616	. . . . . 6 ⊢ ((𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)) → (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
70	69	reximi 3156	. . . . 5 ⊢ (∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
71	32, 70	sylg 1830	. . . 4 ⊢ (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) → ∀𝑔∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
72		elequ2 2127	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑔 → (𝑣 ∈ 𝑓 ↔ 𝑣 ∈ 𝑔))
73	72	anbi2d 632	. . . . . . . . . 10 ⊢ (𝑓 = 𝑔 → ((𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) ↔ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔)))
74	73	rexbidv 3206	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) ↔ ∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔)))
75		rexeq 3310	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → (∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
76	74, 75	imbi12d 348	. . . . . . . 8 ⊢ (𝑓 = 𝑔 → ((∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) ↔ (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
77	76	ralbidv 3108	. . . . . . 7 ⊢ (𝑓 = 𝑔 → (∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) ↔ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
78	77	anbi2d 632	. . . . . 6 ⊢ (𝑓 = 𝑔 → ((𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) ↔ (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))
79	78	rexbidv 3206	. . . . 5 ⊢ (𝑓 = 𝑔 → (∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) ↔ ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))
80	79	cbvalvw 2046	. . . 4 ⊢ (∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) ↔ ∀𝑔∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
81	71, 80	sylibr 237	. . 3 ⊢ (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) → ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
82	17, 81	jca 515	. 2 ⊢ (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) → (𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))
83		nfv 1922	. . . 4 ⊢ Ⅎ𝑓𝒫 𝑧 ⊆ 𝑈
84		nfa1 2154	. . . 4 ⊢ Ⅎ𝑓∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
85	83, 84	nfan 1907	. . 3 ⊢ Ⅎ𝑓(𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
86		elpwi 4508	. . . 4 ⊢ (𝑓 ∈ 𝒫 𝑈 → 𝑓 ⊆ 𝑈)
87		sp 2182	. . . . . 6 ⊢ (∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
88		ssin 4131	. . . . . . . . . . . . 13 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝒫 𝑧 ⊆ 𝑤) ↔ 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤))
89	88	biimpi 219	. . . . . . . . . . . 12 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝒫 𝑧 ⊆ 𝑤) → 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤))
90	89	ex 416	. . . . . . . . . . 11 ⊢ (𝒫 𝑧 ⊆ 𝑈 → (𝒫 𝑧 ⊆ 𝑤 → 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤)))
91	90	adantr 484	. . . . . . . . . 10 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈) → (𝒫 𝑧 ⊆ 𝑤 → 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤)))
92		simp3 1140	. . . . . . . . . . . . . . . . 17 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) → 𝑖 ∈ ∪ 𝑓)
93		eluni 4808	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ ∪ 𝑓 ↔ ∃𝑣(𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓))
94	92, 93	sylib 221	. . . . . . . . . . . . . . . 16 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) → ∃𝑣(𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓))
95		simpl2 1194	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) → 𝑓 ⊆ 𝑈)
96		simprr 773	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) → 𝑣 ∈ 𝑓)
97	95, 96	sseldd 3888	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) → 𝑣 ∈ 𝑈)
98		simprl 771	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) → 𝑖 ∈ 𝑣)
99	97, 98, 96	3jca 1130	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) → (𝑣 ∈ 𝑈 ∧ 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓))
100	99	ex 416	. . . . . . . . . . . . . . . . 17 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) → ((𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → (𝑣 ∈ 𝑈 ∧ 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)))
101	100	eximdv 1925	. . . . . . . . . . . . . . . 16 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) → (∃𝑣(𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑣(𝑣 ∈ 𝑈 ∧ 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)))
102	94, 101	mpd 15	. . . . . . . . . . . . . . 15 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) → ∃𝑣(𝑣 ∈ 𝑈 ∧ 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓))
103		df-rex 3057	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) ↔ ∃𝑣(𝑣 ∈ 𝑈 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)))
104		3anass 1097	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑣 ∈ 𝑈 ∧ 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) ↔ (𝑣 ∈ 𝑈 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)))
105	104	exbii 1855	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑣(𝑣 ∈ 𝑈 ∧ 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) ↔ ∃𝑣(𝑣 ∈ 𝑈 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)))
106	103, 105	bitr4i 281	. . . . . . . . . . . . . . 15 ⊢ (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) ↔ ∃𝑣(𝑣 ∈ 𝑈 ∧ 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓))
107	102, 106	sylibr 237	. . . . . . . . . . . . . 14 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) → ∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓))
108	107	3expia 1123	. . . . . . . . . . . . 13 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈) → (𝑖 ∈ ∪ 𝑓 → ∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)))
109		elin 3869	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 ∈ (𝑓 ∩ 𝒫 𝒫 𝑤) ↔ (𝑢 ∈ 𝑓 ∧ 𝑢 ∈ 𝒫 𝒫 𝑤))
110		vex 3402	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑢 ∈ V
111	110, 55	mpbiran 709	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ 𝒫 𝒫 𝑤 ↔ ∪ 𝑢 ⊆ 𝑤)
112	111	anbi2i 626	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑢 ∈ 𝑓 ∧ 𝑢 ∈ 𝒫 𝒫 𝑤) ↔ (𝑢 ∈ 𝑓 ∧ ∪ 𝑢 ⊆ 𝑤))
113	109, 112	bitri 278	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 ∈ (𝑓 ∩ 𝒫 𝒫 𝑤) ↔ (𝑢 ∈ 𝑓 ∧ ∪ 𝑢 ⊆ 𝑤))
114	113	anbi2i 626	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ 𝑢 ∧ 𝑢 ∈ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ (𝑖 ∈ 𝑢 ∧ (𝑢 ∈ 𝑓 ∧ ∪ 𝑢 ⊆ 𝑤)))
115		an12 645	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ∈ 𝑓 ∧ (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) ↔ (𝑖 ∈ 𝑢 ∧ (𝑢 ∈ 𝑓 ∧ ∪ 𝑢 ⊆ 𝑤)))
116	114, 115	bitr4i 281	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ 𝑢 ∧ 𝑢 ∈ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ (𝑢 ∈ 𝑓 ∧ (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
117	116	exbii 1855	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑢(𝑖 ∈ 𝑢 ∧ 𝑢 ∈ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ ∃𝑢(𝑢 ∈ 𝑓 ∧ (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
118		eluni 4808	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤) ↔ ∃𝑢(𝑖 ∈ 𝑢 ∧ 𝑢 ∈ (𝑓 ∩ 𝒫 𝒫 𝑤)))
119		df-rex 3057	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ ∃𝑢(𝑢 ∈ 𝑓 ∧ (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
120	117, 118, 119	3bitr4i 306	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤) ↔ ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))
121	120	biimpri 231	. . . . . . . . . . . . . 14 ⊢ (∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤))
122	121	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈) → (∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))
123	108, 122	imim12d 81	. . . . . . . . . . . 12 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈) → ((∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) → (𝑖 ∈ ∪ 𝑓 → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤))))
124	123	ralimdv 3091	. . . . . . . . . . 11 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈) → (∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) → ∀𝑖 ∈ 𝑧 (𝑖 ∈ ∪ 𝑓 → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤))))
125		elin 3869	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (𝑧 ∩ ∪ 𝑓) ↔ (𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ 𝑓))
126	125	imbi1i 353	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∈ (𝑧 ∩ ∪ 𝑓) → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ ((𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ 𝑓) → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))
127		impexp 454	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ 𝑓) → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ (𝑖 ∈ 𝑧 → (𝑖 ∈ ∪ 𝑓 → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤))))
128	126, 127	bitri 278	. . . . . . . . . . . . 13 ⊢ ((𝑖 ∈ (𝑧 ∩ ∪ 𝑓) → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ (𝑖 ∈ 𝑧 → (𝑖 ∈ ∪ 𝑓 → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤))))
129	128	albii 1827	. . . . . . . . . . . 12 ⊢ (∀𝑖(𝑖 ∈ (𝑧 ∩ ∪ 𝑓) → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ ∀𝑖(𝑖 ∈ 𝑧 → (𝑖 ∈ ∪ 𝑓 → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤))))
130		dfss2 3873	. . . . . . . . . . . 12 ⊢ ((𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤) ↔ ∀𝑖(𝑖 ∈ (𝑧 ∩ ∪ 𝑓) → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))
131		df-ral 3056	. . . . . . . . . . . 12 ⊢ (∀𝑖 ∈ 𝑧 (𝑖 ∈ ∪ 𝑓 → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ ∀𝑖(𝑖 ∈ 𝑧 → (𝑖 ∈ ∪ 𝑓 → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤))))
132	129, 130, 131	3bitr4i 306	. . . . . . . . . . 11 ⊢ ((𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤) ↔ ∀𝑖 ∈ 𝑧 (𝑖 ∈ ∪ 𝑓 → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))
133	124, 132	syl6ibr 255	. . . . . . . . . 10 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈) → (∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) → (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))
134	91, 133	anim12d 612	. . . . . . . . 9 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈) → ((𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) → (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤))))
135	134	reximdv 3182	. . . . . . . 8 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈) → (∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤))))
136	135	3impia 1119	. . . . . . 7 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))
137	136	3com23 1128	. . . . . 6 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) ∧ 𝑓 ⊆ 𝑈) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))
138	87, 137	syl3an2 1166	. . . . 5 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) ∧ 𝑓 ⊆ 𝑈) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))
139	138	3expa 1120	. . . 4 ⊢ (((𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) ∧ 𝑓 ⊆ 𝑈) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))
140	86, 139	sylan2 596	. . 3 ⊢ (((𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) ∧ 𝑓 ∈ 𝒫 𝑈) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))
141	85, 140	ralrimia 3396	. 2 ⊢ ((𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → ∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))
142	82, 141	impbii 212	1 ⊢ (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ (𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1089  ∀wal 1541   = wceq 1543  ⊤wtru 1544  ∃wex 1787   ∈ wcel 2112  ∀wral 3051  ∃wrex 3052  Vcvv 3398   ∩ cin 3852   ⊆ wss 3853  ∅c0 4223  𝒫 cpw 4499  ∪ cuni 4805

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-sep 5177  ax-nul 5184

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3400  df-dif 3856  df-in 3860  df-ss 3870  df-nul 4224  df-pw 4501  df-uni 4806

This theorem is referenced by:  dfuniv2  41534