Theorem cmpfi 23351

Description: If a topology is compact and a collection of closed sets has the finite intersection property, its intersection is nonempty. (Contributed by Jeff Hankins, 25-Aug-2009.) (Proof shortened by Mario Carneiro, 1-Sep-2015.)

Assertion

Ref	Expression
cmpfi	⊢ (𝐽 ∈ Top → (𝐽 ∈ Comp ↔ ∀𝑥 ∈ 𝒫 (Clsd‘𝐽)(¬ ∅ ∈ (fi‘𝑥) → ∩ 𝑥 ≠ ∅)))

Distinct variable group:   𝑥,𝐽

Proof of Theorem cmpfi

Dummy variables 𝑣 𝑟 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elpwi 4587	. . . 4 ⊢ (𝑦 ∈ 𝒫 𝐽 → 𝑦 ⊆ 𝐽)
2		0ss 4380	. . . . . . . . . . 11 ⊢ ∅ ⊆ 𝑦
3		0fi 9061	. . . . . . . . . . 11 ⊢ ∅ ∈ Fin
4		elfpw 9371	. . . . . . . . . . 11 ⊢ (∅ ∈ (𝒫 𝑦 ∩ Fin) ↔ (∅ ⊆ 𝑦 ∧ ∅ ∈ Fin))
5	2, 3, 4	mpbir2an 711	. . . . . . . . . 10 ⊢ ∅ ∈ (𝒫 𝑦 ∩ Fin)
6		simprr 772	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 = ∅ ∧ ∪ 𝐽 = ∪ 𝑦)) → ∪ 𝐽 = ∪ 𝑦)
7		simprl 770	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 = ∅ ∧ ∪ 𝐽 = ∪ 𝑦)) → 𝑦 = ∅)
8	7	unieqd 4901	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 = ∅ ∧ ∪ 𝐽 = ∪ 𝑦)) → ∪ 𝑦 = ∪ ∅)
9	6, 8	eqtrd 2771	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 = ∅ ∧ ∪ 𝐽 = ∪ 𝑦)) → ∪ 𝐽 = ∪ ∅)
10		unieq 4899	. . . . . . . . . . 11 ⊢ (𝑧 = ∅ → ∪ 𝑧 = ∪ ∅)
11	10	rspceeqv 3629	. . . . . . . . . 10 ⊢ ((∅ ∈ (𝒫 𝑦 ∩ Fin) ∧ ∪ 𝐽 = ∪ ∅) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧)
12	5, 9, 11	sylancr 587	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 = ∅ ∧ ∪ 𝐽 = ∪ 𝑦)) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧)
13	12	expr 456	. . . . . . . 8 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 = ∅) → (∪ 𝐽 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧))
14		vn0 4325	. . . . . . . . . 10 ⊢ V ≠ ∅
15		iineq1 4990	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ∅ → ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∩ 𝑟 ∈ ∅ (∪ 𝐽 ∖ 𝑟))
16	15	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 = ∅) → ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∩ 𝑟 ∈ ∅ (∪ 𝐽 ∖ 𝑟))
17		0iin 5045	. . . . . . . . . . . . 13 ⊢ ∩ 𝑟 ∈ ∅ (∪ 𝐽 ∖ 𝑟) = V
18	16, 17	eqtrdi 2787	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 = ∅) → ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = V)
19	18	eqeq1d 2738	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 = ∅) → (∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅ ↔ V = ∅))
20	19	necon3bbid 2970	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 = ∅) → (¬ ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅ ↔ V ≠ ∅))
21	14, 20	mpbiri 258	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 = ∅) → ¬ ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅)
22	21	pm2.21d 121	. . . . . . . 8 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 = ∅) → (∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅ → ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))))
23	13, 22	2thd 265	. . . . . . 7 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 = ∅) → ((∪ 𝐽 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧) ↔ (∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅ → ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))))
24		uniss 4896	. . . . . . . . . . . 12 ⊢ (𝑦 ⊆ 𝐽 → ∪ 𝑦 ⊆ ∪ 𝐽)
25	24	ad2antlr 727	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → ∪ 𝑦 ⊆ ∪ 𝐽)
26		eqss 3979	. . . . . . . . . . . 12 ⊢ (∪ 𝑦 = ∪ 𝐽 ↔ (∪ 𝑦 ⊆ ∪ 𝐽 ∧ ∪ 𝐽 ⊆ ∪ 𝑦))
27	26	baib 535	. . . . . . . . . . 11 ⊢ (∪ 𝑦 ⊆ ∪ 𝐽 → (∪ 𝑦 = ∪ 𝐽 ↔ ∪ 𝐽 ⊆ ∪ 𝑦))
28	25, 27	syl 17	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∪ 𝑦 = ∪ 𝐽 ↔ ∪ 𝐽 ⊆ ∪ 𝑦))
29		eqcom 2743	. . . . . . . . . 10 ⊢ (∪ 𝑦 = ∪ 𝐽 ↔ ∪ 𝐽 = ∪ 𝑦)
30		ssdif0 4346	. . . . . . . . . 10 ⊢ (∪ 𝐽 ⊆ ∪ 𝑦 ↔ (∪ 𝐽 ∖ ∪ 𝑦) = ∅)
31	28, 29, 30	3bitr3g 313	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∪ 𝐽 = ∪ 𝑦 ↔ (∪ 𝐽 ∖ ∪ 𝑦) = ∅))
32		iindif2 5058	. . . . . . . . . . . 12 ⊢ (𝑦 ≠ ∅ → ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = (∪ 𝐽 ∖ ∪ 𝑟 ∈ 𝑦 𝑟))
33	32	adantl 481	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = (∪ 𝐽 ∖ ∪ 𝑟 ∈ 𝑦 𝑟))
34		uniiun 5039	. . . . . . . . . . . 12 ⊢ ∪ 𝑦 = ∪ 𝑟 ∈ 𝑦 𝑟
35	34	difeq2i 4103	. . . . . . . . . . 11 ⊢ (∪ 𝐽 ∖ ∪ 𝑦) = (∪ 𝐽 ∖ ∪ 𝑟 ∈ 𝑦 𝑟)
36	33, 35	eqtr4di 2789	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = (∪ 𝐽 ∖ ∪ 𝑦))
37	36	eqeq1d 2738	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅ ↔ (∪ 𝐽 ∖ ∪ 𝑦) = ∅))
38	31, 37	bitr4d 282	. . . . . . . 8 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∪ 𝐽 = ∪ 𝑦 ↔ ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅))
39		imassrn 6063	. . . . . . . . . . . 12 ⊢ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ⊆ ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟))
40		df-ima 5672	. . . . . . . . . . . . . 14 ⊢ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) = ran ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) ↾ 𝑦)
41		resmpt 6029	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ⊆ 𝐽 → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) ↾ 𝑦) = (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
42	41	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) ↾ 𝑦) = (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
43	42	rneqd 5923	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ran ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) ↾ 𝑦) = ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
44	40, 43	eqtrid 2783	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) = ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
45	44	ad2antrr 726	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ (𝒫 𝑦 ∩ Fin)) → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) = ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
46	39, 45	sseqtrrid 4007	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ (𝒫 𝑦 ∩ Fin)) → ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ⊆ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))
47		funmpt 6579	. . . . . . . . . . . 12 ⊢ Fun (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟))
48		elinel2 4182	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (𝒫 𝑦 ∩ Fin) → 𝑧 ∈ Fin)
49	48	adantl 481	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ (𝒫 𝑦 ∩ Fin)) → 𝑧 ∈ Fin)
50		imafi 9330	. . . . . . . . . . . 12 ⊢ ((Fun (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) ∧ 𝑧 ∈ Fin) → ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ∈ Fin)
51	47, 49, 50	sylancr 587	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ (𝒫 𝑦 ∩ Fin)) → ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ∈ Fin)
52		elfpw 9371	. . . . . . . . . . 11 ⊢ (((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin) ↔ (((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ⊆ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∧ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ∈ Fin))
53	46, 51, 52	sylanbrc 583	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ (𝒫 𝑦 ∩ Fin)) → ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin))
54		eqid 2736	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝐽 = ∪ 𝐽
55	54	topopn 22849	. . . . . . . . . . . . . . . 16 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽)
56	55	difexd 5306	. . . . . . . . . . . . . . 15 ⊢ (𝐽 ∈ Top → (∪ 𝐽 ∖ 𝑟) ∈ V)
57	56	ralrimivw 3137	. . . . . . . . . . . . . 14 ⊢ (𝐽 ∈ Top → ∀𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) ∈ V)
58		eqid 2736	. . . . . . . . . . . . . . 15 ⊢ (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) = (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟))
59	58	fnmpt 6683	. . . . . . . . . . . . . 14 ⊢ (∀𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) ∈ V → (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) Fn 𝑦)
60	57, 59	syl 17	. . . . . . . . . . . . 13 ⊢ (𝐽 ∈ Top → (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) Fn 𝑦)
61	60	ad3antrrr 730	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)) → (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) Fn 𝑦)
62		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)) → 𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin))
63		elfpw 9371	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin) ↔ (𝑤 ⊆ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∧ 𝑤 ∈ Fin))
64	62, 63	sylib 218	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)) → (𝑤 ⊆ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∧ 𝑤 ∈ Fin))
65	64	simpld 494	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)) → 𝑤 ⊆ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))
66	44	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)) → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) = ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
67	65, 66	sseqtrd 4000	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)) → 𝑤 ⊆ ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
68	64	simprd 495	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)) → 𝑤 ∈ Fin)
69		fipreima 9375	. . . . . . . . . . . 12 ⊢ (((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) Fn 𝑦 ∧ 𝑤 ⊆ ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) ∧ 𝑤 ∈ Fin) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = 𝑤)
70	61, 67, 68, 69	syl3anc 1373	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = 𝑤)
71		eqcom 2743	. . . . . . . . . . . 12 ⊢ (((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = 𝑤 ↔ 𝑤 = ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧))
72	71	rexbii 3084	. . . . . . . . . . 11 ⊢ (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = 𝑤 ↔ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑤 = ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧))
73	70, 72	sylib 218	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑤 = ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧))
74		simpr 484	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 = ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)) → 𝑤 = ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧))
75	74	inteqd 4932	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 = ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)) → ∩ 𝑤 = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧))
76	75	eqeq2d 2747	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 = ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)) → (∅ = ∩ 𝑤 ↔ ∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)))
77	53, 73, 76	rexxfrd 5384	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∃𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)∅ = ∩ 𝑤 ↔ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)))
78		0ex 5282	. . . . . . . . . 10 ⊢ ∅ ∈ V
79		imassrn 6063	. . . . . . . . . . . . 13 ⊢ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ⊆ ran (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟))
80		eqid 2736	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) = (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟))
81	54, 80	opncldf1 23027	. . . . . . . . . . . . . . . 16 ⊢ (𝐽 ∈ Top → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)):𝐽–1-1-onto→(Clsd‘𝐽) ∧ ◡(𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) = (𝑣 ∈ (Clsd‘𝐽) ↦ (∪ 𝐽 ∖ 𝑣))))
82	81	simpld 494	. . . . . . . . . . . . . . 15 ⊢ (𝐽 ∈ Top → (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)):𝐽–1-1-onto→(Clsd‘𝐽))
83		f1ofo 6830	. . . . . . . . . . . . . . 15 ⊢ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)):𝐽–1-1-onto→(Clsd‘𝐽) → (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)):𝐽–onto→(Clsd‘𝐽))
84	82, 83	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝐽 ∈ Top → (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)):𝐽–onto→(Clsd‘𝐽))
85		forn 6798	. . . . . . . . . . . . . 14 ⊢ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)):𝐽–onto→(Clsd‘𝐽) → ran (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) = (Clsd‘𝐽))
86	84, 85	syl 17	. . . . . . . . . . . . 13 ⊢ (𝐽 ∈ Top → ran (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) = (Clsd‘𝐽))
87	79, 86	sseqtrid 4006	. . . . . . . . . . . 12 ⊢ (𝐽 ∈ Top → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ⊆ (Clsd‘𝐽))
88		fvex 6894	. . . . . . . . . . . . 13 ⊢ (Clsd‘𝐽) ∈ V
89	88	elpw2 5309	. . . . . . . . . . . 12 ⊢ (((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∈ 𝒫 (Clsd‘𝐽) ↔ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ⊆ (Clsd‘𝐽))
90	87, 89	sylibr 234	. . . . . . . . . . 11 ⊢ (𝐽 ∈ Top → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∈ 𝒫 (Clsd‘𝐽))
91	90	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∈ 𝒫 (Clsd‘𝐽))
92		elfi 9430	. . . . . . . . . 10 ⊢ ((∅ ∈ V ∧ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∈ 𝒫 (Clsd‘𝐽)) → (∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) ↔ ∃𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)∅ = ∩ 𝑤))
93	78, 91, 92	sylancr 587	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) ↔ ∃𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)∅ = ∩ 𝑤))
94		inundif 4459	. . . . . . . . . . . . . 14 ⊢ (((𝒫 𝑦 ∩ Fin) ∩ {∅}) ∪ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) = (𝒫 𝑦 ∩ Fin)
95	94	rexeqi 3308	. . . . . . . . . . . . 13 ⊢ (∃𝑧 ∈ (((𝒫 𝑦 ∩ Fin) ∩ {∅}) ∪ ((𝒫 𝑦 ∩ Fin) ∖ {∅}))∪ 𝐽 = ∪ 𝑧 ↔ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧)
96		rexun 4176	. . . . . . . . . . . . 13 ⊢ (∃𝑧 ∈ (((𝒫 𝑦 ∩ Fin) ∩ {∅}) ∪ ((𝒫 𝑦 ∩ Fin) ∖ {∅}))∪ 𝐽 = ∪ 𝑧 ↔ (∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅})∪ 𝐽 = ∪ 𝑧 ∨ ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧))
97	95, 96	bitr3i 277	. . . . . . . . . . . 12 ⊢ (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧 ↔ (∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅})∪ 𝐽 = ∪ 𝑧 ∨ ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧))
98		elinel2 4182	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅}) → 𝑧 ∈ {∅})
99		elsni 4623	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ {∅} → 𝑧 = ∅)
100	98, 99	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅}) → 𝑧 = ∅)
101	100	unieqd 4901	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅}) → ∪ 𝑧 = ∪ ∅)
102		uni0 4916	. . . . . . . . . . . . . . . . . . 19 ⊢ ∪ ∅ = ∅
103	101, 102	eqtrdi 2787	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅}) → ∪ 𝑧 = ∅)
104	103	eqeq2d 2747	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅}) → (∪ 𝐽 = ∪ 𝑧 ↔ ∪ 𝐽 = ∅))
105	104	biimpd 229	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅}) → (∪ 𝐽 = ∪ 𝑧 → ∪ 𝐽 = ∅))
106	105	rexlimiv 3135	. . . . . . . . . . . . . . 15 ⊢ (∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅})∪ 𝐽 = ∪ 𝑧 → ∪ 𝐽 = ∅)
107		ssidd 3987	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → 𝑦 ⊆ 𝑦)
108		simprr 772	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → ∪ 𝐽 = ∅)
109		0ss 4380	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ∅ ⊆ ∪ 𝑦
110	108, 109	eqsstrdi 4008	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → ∪ 𝐽 ⊆ ∪ 𝑦)
111	24	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → ∪ 𝑦 ⊆ ∪ 𝐽)
112	110, 111	eqssd 3981	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → ∪ 𝐽 = ∪ 𝑦)
113	112, 108	eqtr3d 2773	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → ∪ 𝑦 = ∅)
114	113, 3	eqeltrdi 2843	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → ∪ 𝑦 ∈ Fin)
115		pwfi 9334	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∪ 𝑦 ∈ Fin ↔ 𝒫 ∪ 𝑦 ∈ Fin)
116	114, 115	sylib 218	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → 𝒫 ∪ 𝑦 ∈ Fin)
117		pwuni 4926	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑦 ⊆ 𝒫 ∪ 𝑦
118		ssfi 9192	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝒫 ∪ 𝑦 ∈ Fin ∧ 𝑦 ⊆ 𝒫 ∪ 𝑦) → 𝑦 ∈ Fin)
119	116, 117, 118	sylancl 586	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → 𝑦 ∈ Fin)
120		elfpw 9371	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ (𝒫 𝑦 ∩ Fin) ↔ (𝑦 ⊆ 𝑦 ∧ 𝑦 ∈ Fin))
121	107, 119, 120	sylanbrc 583	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → 𝑦 ∈ (𝒫 𝑦 ∩ Fin))
122		simprl 770	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → 𝑦 ≠ ∅)
123		eldifsn 4767	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅}) ↔ (𝑦 ∈ (𝒫 𝑦 ∩ Fin) ∧ 𝑦 ≠ ∅))
124	121, 122, 123	sylanbrc 583	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → 𝑦 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅}))
125		unieq 4899	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑦 → ∪ 𝑧 = ∪ 𝑦)
126	125	rspceeqv 3629	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅}) ∧ ∪ 𝐽 = ∪ 𝑦) → ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧)
127	124, 112, 126	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧)
128	127	expr 456	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∪ 𝐽 = ∅ → ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧))
129	106, 128	syl5 34	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅})∪ 𝐽 = ∪ 𝑧 → ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧))
130		idd 24	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧 → ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧))
131	129, 130	jaod 859	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → ((∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅})∪ 𝐽 = ∪ 𝑧 ∨ ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧) → ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧))
132		olc 868	. . . . . . . . . . . . 13 ⊢ (∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧 → (∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅})∪ 𝐽 = ∪ 𝑧 ∨ ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧))
133	131, 132	impbid1 225	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → ((∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅})∪ 𝐽 = ∪ 𝑧 ∨ ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧) ↔ ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧))
134	97, 133	bitrid 283	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧 ↔ ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧))
135		eldifi 4111	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅}) → 𝑧 ∈ (𝒫 𝑦 ∩ Fin))
136	135	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → 𝑧 ∈ (𝒫 𝑦 ∩ Fin))
137		elfpw 9371	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ (𝒫 𝑦 ∩ Fin) ↔ (𝑧 ⊆ 𝑦 ∧ 𝑧 ∈ Fin))
138	136, 137	sylib 218	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → (𝑧 ⊆ 𝑦 ∧ 𝑧 ∈ Fin))
139	138	simpld 494	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → 𝑧 ⊆ 𝑦)
140		simpllr 775	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → 𝑦 ⊆ 𝐽)
141	139, 140	sstrd 3974	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → 𝑧 ⊆ 𝐽)
142	141	unissd 4898	. . . . . . . . . . . . . . 15 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ∪ 𝑧 ⊆ ∪ 𝐽)
143		eqss 3979	. . . . . . . . . . . . . . . 16 ⊢ (∪ 𝑧 = ∪ 𝐽 ↔ (∪ 𝑧 ⊆ ∪ 𝐽 ∧ ∪ 𝐽 ⊆ ∪ 𝑧))
144	143	baib 535	. . . . . . . . . . . . . . 15 ⊢ (∪ 𝑧 ⊆ ∪ 𝐽 → (∪ 𝑧 = ∪ 𝐽 ↔ ∪ 𝐽 ⊆ ∪ 𝑧))
145	142, 144	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → (∪ 𝑧 = ∪ 𝐽 ↔ ∪ 𝐽 ⊆ ∪ 𝑧))
146		eqcom 2743	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑧 = ∪ 𝐽 ↔ ∪ 𝐽 = ∪ 𝑧)
147		ssdif0 4346	. . . . . . . . . . . . . . 15 ⊢ (∪ 𝐽 ⊆ ∪ 𝑧 ↔ (∪ 𝐽 ∖ ∪ 𝑧) = ∅)
148		eqcom 2743	. . . . . . . . . . . . . . 15 ⊢ ((∪ 𝐽 ∖ ∪ 𝑧) = ∅ ↔ ∅ = (∪ 𝐽 ∖ ∪ 𝑧))
149	147, 148	bitri 275	. . . . . . . . . . . . . 14 ⊢ (∪ 𝐽 ⊆ ∪ 𝑧 ↔ ∅ = (∪ 𝐽 ∖ ∪ 𝑧))
150	145, 146, 149	3bitr3g 313	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → (∪ 𝐽 = ∪ 𝑧 ↔ ∅ = (∪ 𝐽 ∖ ∪ 𝑧)))
151		df-ima 5672	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = ran ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) ↾ 𝑧)
152	139	resmptd 6032	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) ↾ 𝑧) = (𝑟 ∈ 𝑧 ↦ (∪ 𝐽 ∖ 𝑟)))
153	152	rneqd 5923	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ran ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) ↾ 𝑧) = ran (𝑟 ∈ 𝑧 ↦ (∪ 𝐽 ∖ 𝑟)))
154	151, 153	eqtrid 2783	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = ran (𝑟 ∈ 𝑧 ↦ (∪ 𝐽 ∖ 𝑟)))
155	154	inteqd 4932	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = ∩ ran (𝑟 ∈ 𝑧 ↦ (∪ 𝐽 ∖ 𝑟)))
156	56	ralrimivw 3137	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐽 ∈ Top → ∀𝑟 ∈ 𝑧 (∪ 𝐽 ∖ 𝑟) ∈ V)
157	156	ad3antrrr 730	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ∀𝑟 ∈ 𝑧 (∪ 𝐽 ∖ 𝑟) ∈ V)
158		dfiin3g 5953	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑟 ∈ 𝑧 (∪ 𝐽 ∖ 𝑟) ∈ V → ∩ 𝑟 ∈ 𝑧 (∪ 𝐽 ∖ 𝑟) = ∩ ran (𝑟 ∈ 𝑧 ↦ (∪ 𝐽 ∖ 𝑟)))
159	157, 158	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ∩ 𝑟 ∈ 𝑧 (∪ 𝐽 ∖ 𝑟) = ∩ ran (𝑟 ∈ 𝑧 ↦ (∪ 𝐽 ∖ 𝑟)))
160		eldifsni 4771	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅}) → 𝑧 ≠ ∅)
161	160	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → 𝑧 ≠ ∅)
162		iindif2 5058	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ≠ ∅ → ∩ 𝑟 ∈ 𝑧 (∪ 𝐽 ∖ 𝑟) = (∪ 𝐽 ∖ ∪ 𝑟 ∈ 𝑧 𝑟))
163	161, 162	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ∩ 𝑟 ∈ 𝑧 (∪ 𝐽 ∖ 𝑟) = (∪ 𝐽 ∖ ∪ 𝑟 ∈ 𝑧 𝑟))
164	155, 159, 163	3eqtr2d 2777	. . . . . . . . . . . . . . 15 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = (∪ 𝐽 ∖ ∪ 𝑟 ∈ 𝑧 𝑟))
165		uniiun 5039	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑧 = ∪ 𝑟 ∈ 𝑧 𝑟
166	165	difeq2i 4103	. . . . . . . . . . . . . . 15 ⊢ (∪ 𝐽 ∖ ∪ 𝑧) = (∪ 𝐽 ∖ ∪ 𝑟 ∈ 𝑧 𝑟)
167	164, 166	eqtr4di 2789	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = (∪ 𝐽 ∖ ∪ 𝑧))
168	167	eqeq2d 2747	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → (∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ↔ ∅ = (∪ 𝐽 ∖ ∪ 𝑧)))
169	150, 168	bitr4d 282	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → (∪ 𝐽 = ∪ 𝑧 ↔ ∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)))
170	169	rexbidva 3163	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧 ↔ ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)))
171	134, 170	bitrd 279	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧 ↔ ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)))
172		imaeq2 6048	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = ∅ → ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ ∅))
173		ima0 6069	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ ∅) = ∅
174	172, 173	eqtrdi 2787	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = ∅ → ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = ∅)
175	174	inteqd 4932	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = ∅ → ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = ∩ ∅)
176		int0 4943	. . . . . . . . . . . . . . . . . 18 ⊢ ∩ ∅ = V
177	175, 176	eqtrdi 2787	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ∅ → ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = V)
178	177	neeq1d 2992	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = ∅ → (∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ≠ ∅ ↔ V ≠ ∅))
179	14, 178	mpbiri 258	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = ∅ → ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ≠ ∅)
180	179	necomd 2988	. . . . . . . . . . . . . 14 ⊢ (𝑧 = ∅ → ∅ ≠ ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧))
181	180	necon2i 2967	. . . . . . . . . . . . 13 ⊢ (∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) → 𝑧 ≠ ∅)
182		eldifsn 4767	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅}) ↔ (𝑧 ∈ (𝒫 𝑦 ∩ Fin) ∧ 𝑧 ≠ ∅))
183	182	rbaibr 537	. . . . . . . . . . . . 13 ⊢ (𝑧 ≠ ∅ → (𝑧 ∈ (𝒫 𝑦 ∩ Fin) ↔ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})))
184	181, 183	syl 17	. . . . . . . . . . . 12 ⊢ (∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) → (𝑧 ∈ (𝒫 𝑦 ∩ Fin) ↔ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})))
185	184	pm5.32ri 575	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ (𝒫 𝑦 ∩ Fin) ∧ ∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)) ↔ (𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅}) ∧ ∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)))
186	185	rexbii2 3080	. . . . . . . . . 10 ⊢ (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ↔ ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧))
187	171, 186	bitr4di 289	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧 ↔ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)))
188	77, 93, 187	3bitr4rd 312	. . . . . . . 8 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧 ↔ ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))))
189	38, 188	imbi12d 344	. . . . . . 7 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → ((∪ 𝐽 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧) ↔ (∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅ → ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))))
190	23, 189	pm2.61dane 3020	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ((∪ 𝐽 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧) ↔ (∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅ → ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))))
191	57	adantr 480	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ∀𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) ∈ V)
192		dfiin3g 5953	. . . . . . . . . . 11 ⊢ (∀𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) ∈ V → ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∩ ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
193	191, 192	syl 17	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∩ ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
194	44	inteqd 4932	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) = ∩ ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
195	193, 194	eqtr4d 2774	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))
196	195	eqeq1d 2738	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → (∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅ ↔ ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) = ∅))
197		nne 2937	. . . . . . . 8 ⊢ (¬ ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅ ↔ ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) = ∅)
198	196, 197	bitr4di 289	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → (∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅ ↔ ¬ ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅))
199	198	imbi1d 341	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ((∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅ → ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))) ↔ (¬ ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅ → ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))))
200	190, 199	bitrd 279	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ((∪ 𝐽 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧) ↔ (¬ ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅ → ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))))
201		con1b 358	. . . . 5 ⊢ ((¬ ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅ → ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))) ↔ (¬ ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅))
202	200, 201	bitrdi 287	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ((∪ 𝐽 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧) ↔ (¬ ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅)))
203	1, 202	sylan2 593	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ∈ 𝒫 𝐽) → ((∪ 𝐽 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧) ↔ (¬ ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅)))
204	203	ralbidva 3162	. 2 ⊢ (𝐽 ∈ Top → (∀𝑦 ∈ 𝒫 𝐽(∪ 𝐽 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧) ↔ ∀𝑦 ∈ 𝒫 𝐽(¬ ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅)))
205	54	iscmp 23331	. . 3 ⊢ (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝐽(∪ 𝐽 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧)))
206	205	baib 535	. 2 ⊢ (𝐽 ∈ Top → (𝐽 ∈ Comp ↔ ∀𝑦 ∈ 𝒫 𝐽(∪ 𝐽 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧)))
207	90	adantr 480	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ∈ 𝒫 𝐽) → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∈ 𝒫 (Clsd‘𝐽))
208		simpl 482	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) → 𝐽 ∈ Top)
209		funmpt 6579	. . . . . 6 ⊢ Fun (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟))
210	209	a1i 11	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) → Fun (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)))
211		elpwi 4587	. . . . . . 7 ⊢ (𝑥 ∈ 𝒫 (Clsd‘𝐽) → 𝑥 ⊆ (Clsd‘𝐽))
212		foima 6800	. . . . . . . . 9 ⊢ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)):𝐽–onto→(Clsd‘𝐽) → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝐽) = (Clsd‘𝐽))
213	84, 212	syl 17	. . . . . . . 8 ⊢ (𝐽 ∈ Top → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝐽) = (Clsd‘𝐽))
214	213	sseq2d 3996	. . . . . . 7 ⊢ (𝐽 ∈ Top → (𝑥 ⊆ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝐽) ↔ 𝑥 ⊆ (Clsd‘𝐽)))
215	211, 214	imbitrrid 246	. . . . . 6 ⊢ (𝐽 ∈ Top → (𝑥 ∈ 𝒫 (Clsd‘𝐽) → 𝑥 ⊆ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝐽)))
216	215	imp 406	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) → 𝑥 ⊆ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝐽))
217		ssimaexg 6970	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ Fun (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) ∧ 𝑥 ⊆ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝐽)) → ∃𝑦(𝑦 ⊆ 𝐽 ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))
218	208, 210, 216, 217	syl3anc 1373	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) → ∃𝑦(𝑦 ⊆ 𝐽 ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))
219		df-rex 3062	. . . . 5 ⊢ (∃𝑦 ∈ 𝒫 𝐽𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ↔ ∃𝑦(𝑦 ∈ 𝒫 𝐽 ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))
220		velpw 4585	. . . . . . 7 ⊢ (𝑦 ∈ 𝒫 𝐽 ↔ 𝑦 ⊆ 𝐽)
221	220	anbi1i 624	. . . . . 6 ⊢ ((𝑦 ∈ 𝒫 𝐽 ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) ↔ (𝑦 ⊆ 𝐽 ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))
222	221	exbii 1848	. . . . 5 ⊢ (∃𝑦(𝑦 ∈ 𝒫 𝐽 ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) ↔ ∃𝑦(𝑦 ⊆ 𝐽 ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))
223	219, 222	bitri 275	. . . 4 ⊢ (∃𝑦 ∈ 𝒫 𝐽𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ↔ ∃𝑦(𝑦 ⊆ 𝐽 ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))
224	218, 223	sylibr 234	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) → ∃𝑦 ∈ 𝒫 𝐽𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))
225		simpr 484	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))
226	225	fveq2d 6885	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → (fi‘𝑥) = (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))
227	226	eleq2d 2821	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → (∅ ∈ (fi‘𝑥) ↔ ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))))
228	227	notbid 318	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → (¬ ∅ ∈ (fi‘𝑥) ↔ ¬ ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))))
229	225	inteqd 4932	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → ∩ 𝑥 = ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))
230	229	neeq1d 2992	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → (∩ 𝑥 ≠ ∅ ↔ ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅))
231	228, 230	imbi12d 344	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → ((¬ ∅ ∈ (fi‘𝑥) → ∩ 𝑥 ≠ ∅) ↔ (¬ ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅)))
232	207, 224, 231	ralxfrd 5383	. 2 ⊢ (𝐽 ∈ Top → (∀𝑥 ∈ 𝒫 (Clsd‘𝐽)(¬ ∅ ∈ (fi‘𝑥) → ∩ 𝑥 ≠ ∅) ↔ ∀𝑦 ∈ 𝒫 𝐽(¬ ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅)))
233	204, 206, 232	3bitr4d 311	1 ⊢ (𝐽 ∈ Top → (𝐽 ∈ Comp ↔ ∀𝑥 ∈ 𝒫 (Clsd‘𝐽)(¬ ∅ ∈ (fi‘𝑥) → ∩ 𝑥 ≠ ∅)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1540  ∃wex 1779   ∈ wcel 2109   ≠ wne 2933  ∀wral 3052  ∃wrex 3061  Vcvv 3464   ∖ cdif 3928   ∪ cun 3929   ∩ cin 3930   ⊆ wss 3931  ∅c0 4313  𝒫 cpw 4580  {csn 4606  ∪ cuni 4888  ∩ cint 4927  ∪ ciun 4972  ∩ ciin 4973   ↦ cmpt 5206  ^◡ccnv 5658  ran crn 5660   ↾ cres 5661   “ cima 5662  Fun wfun 6530   Fn wfn 6531  –onto→wfo 6534  –1-1-onto→wf1o 6535  ‘cfv 6536  Fincfn 8964  ficfi 9427  Topctop 22836  Clsdccld 22959  Compccmp 23329

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-int 4928  df-iun 4974  df-iin 4975  df-br 5125  df-opab 5187  df-mpt 5207  df-tr 5235  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-om 7867  df-1o 8485  df-en 8965  df-dom 8966  df-fin 8968  df-fi 9428  df-top 22837  df-cld 22962  df-cmp 23330

This theorem is referenced by:  cmpfii  23352  fclscmp  23973  zarcmplem  33917  heibor1lem  37838