Theorem cmpfi 22559

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 4542	. . . 4 ⊢ (𝑦 ∈ 𝒫 𝐽 → 𝑦 ⊆ 𝐽)
2		0ss 4330	. . . . . . . . . . 11 ⊢ ∅ ⊆ 𝑦
3		0fin 8954	. . . . . . . . . . 11 ⊢ ∅ ∈ Fin
4		elfpw 9121	. . . . . . . . . . 11 ⊢ (∅ ∈ (𝒫 𝑦 ∩ Fin) ↔ (∅ ⊆ 𝑦 ∧ ∅ ∈ Fin))
5	2, 3, 4	mpbir2an 708	. . . . . . . . . 10 ⊢ ∅ ∈ (𝒫 𝑦 ∩ Fin)
6		simprr 770	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 = ∅ ∧ ∪ 𝐽 = ∪ 𝑦)) → ∪ 𝐽 = ∪ 𝑦)
7		simprl 768	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 = ∅ ∧ ∪ 𝐽 = ∪ 𝑦)) → 𝑦 = ∅)
8	7	unieqd 4853	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 = ∅ ∧ ∪ 𝐽 = ∪ 𝑦)) → ∪ 𝑦 = ∪ ∅)
9	6, 8	eqtrd 2778	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 = ∅ ∧ ∪ 𝐽 = ∪ 𝑦)) → ∪ 𝐽 = ∪ ∅)
10		unieq 4850	. . . . . . . . . . 11 ⊢ (𝑧 = ∅ → ∪ 𝑧 = ∪ ∅)
11	10	rspceeqv 3575	. . . . . . . . . 10 ⊢ ((∅ ∈ (𝒫 𝑦 ∩ Fin) ∧ ∪ 𝐽 = ∪ ∅) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧)
12	5, 9, 11	sylancr 587	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 = ∅ ∧ ∪ 𝐽 = ∪ 𝑦)) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧)
13	12	expr 457	. . . . . . . 8 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 = ∅) → (∪ 𝐽 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧))
14		vn0 4272	. . . . . . . . . 10 ⊢ V ≠ ∅
15		iineq1 4941	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ∅ → ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∩ 𝑟 ∈ ∅ (∪ 𝐽 ∖ 𝑟))
16	15	adantl 482	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 = ∅) → ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∩ 𝑟 ∈ ∅ (∪ 𝐽 ∖ 𝑟))
17		0iin 4993	. . . . . . . . . . . . 13 ⊢ ∩ 𝑟 ∈ ∅ (∪ 𝐽 ∖ 𝑟) = V
18	16, 17	eqtrdi 2794	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 = ∅) → ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = V)
19	18	eqeq1d 2740	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 = ∅) → (∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅ ↔ V = ∅))
20	19	necon3bbid 2981	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 = ∅) → (¬ ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅ ↔ V ≠ ∅))
21	14, 20	mpbiri 257	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 = ∅) → ¬ ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅)
22	21	pm2.21d 121	. . . . . . . 8 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 = ∅) → (∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅ → ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))))
23	13, 22	2thd 264	. . . . . . 7 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 = ∅) → ((∪ 𝐽 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧) ↔ (∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅ → ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))))
24		uniss 4847	. . . . . . . . . . . 12 ⊢ (𝑦 ⊆ 𝐽 → ∪ 𝑦 ⊆ ∪ 𝐽)
25	24	ad2antlr 724	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → ∪ 𝑦 ⊆ ∪ 𝐽)
26		eqss 3936	. . . . . . . . . . . 12 ⊢ (∪ 𝑦 = ∪ 𝐽 ↔ (∪ 𝑦 ⊆ ∪ 𝐽 ∧ ∪ 𝐽 ⊆ ∪ 𝑦))
27	26	baib 536	. . . . . . . . . . 11 ⊢ (∪ 𝑦 ⊆ ∪ 𝐽 → (∪ 𝑦 = ∪ 𝐽 ↔ ∪ 𝐽 ⊆ ∪ 𝑦))
28	25, 27	syl 17	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∪ 𝑦 = ∪ 𝐽 ↔ ∪ 𝐽 ⊆ ∪ 𝑦))
29		eqcom 2745	. . . . . . . . . 10 ⊢ (∪ 𝑦 = ∪ 𝐽 ↔ ∪ 𝐽 = ∪ 𝑦)
30		ssdif0 4297	. . . . . . . . . 10 ⊢ (∪ 𝐽 ⊆ ∪ 𝑦 ↔ (∪ 𝐽 ∖ ∪ 𝑦) = ∅)
31	28, 29, 30	3bitr3g 313	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∪ 𝐽 = ∪ 𝑦 ↔ (∪ 𝐽 ∖ ∪ 𝑦) = ∅))
32		iindif2 5006	. . . . . . . . . . . 12 ⊢ (𝑦 ≠ ∅ → ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = (∪ 𝐽 ∖ ∪ 𝑟 ∈ 𝑦 𝑟))
33	32	adantl 482	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = (∪ 𝐽 ∖ ∪ 𝑟 ∈ 𝑦 𝑟))
34		uniiun 4988	. . . . . . . . . . . 12 ⊢ ∪ 𝑦 = ∪ 𝑟 ∈ 𝑦 𝑟
35	34	difeq2i 4054	. . . . . . . . . . 11 ⊢ (∪ 𝐽 ∖ ∪ 𝑦) = (∪ 𝐽 ∖ ∪ 𝑟 ∈ 𝑦 𝑟)
36	33, 35	eqtr4di 2796	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = (∪ 𝐽 ∖ ∪ 𝑦))
37	36	eqeq1d 2740	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅ ↔ (∪ 𝐽 ∖ ∪ 𝑦) = ∅))
38	31, 37	bitr4d 281	. . . . . . . 8 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∪ 𝐽 = ∪ 𝑦 ↔ ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅))
39		imassrn 5980	. . . . . . . . . . . 12 ⊢ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ⊆ ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟))
40		df-ima 5602	. . . . . . . . . . . . . 14 ⊢ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) = ran ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) ↾ 𝑦)
41		resmpt 5945	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ⊆ 𝐽 → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) ↾ 𝑦) = (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
42	41	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) ↾ 𝑦) = (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
43	42	rneqd 5847	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ran ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) ↾ 𝑦) = ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
44	40, 43	eqtrid 2790	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) = ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
45	44	ad2antrr 723	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ (𝒫 𝑦 ∩ Fin)) → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) = ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
46	39, 45	sseqtrrid 3974	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ (𝒫 𝑦 ∩ Fin)) → ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ⊆ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))
47		funmpt 6472	. . . . . . . . . . . 12 ⊢ Fun (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟))
48		elinel2 4130	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (𝒫 𝑦 ∩ Fin) → 𝑧 ∈ Fin)
49	48	adantl 482	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ (𝒫 𝑦 ∩ Fin)) → 𝑧 ∈ Fin)
50		imafi 8958	. . . . . . . . . . . 12 ⊢ ((Fun (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) ∧ 𝑧 ∈ Fin) → ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ∈ Fin)
51	47, 49, 50	sylancr 587	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ (𝒫 𝑦 ∩ Fin)) → ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ∈ Fin)
52		elfpw 9121	. . . . . . . . . . 11 ⊢ (((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin) ↔ (((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ⊆ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∧ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ∈ Fin))
53	46, 51, 52	sylanbrc 583	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ (𝒫 𝑦 ∩ Fin)) → ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin))
54		eqid 2738	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝐽 = ∪ 𝐽
55	54	topopn 22055	. . . . . . . . . . . . . . . 16 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽)
56	55	difexd 5253	. . . . . . . . . . . . . . 15 ⊢ (𝐽 ∈ Top → (∪ 𝐽 ∖ 𝑟) ∈ V)
57	56	ralrimivw 3104	. . . . . . . . . . . . . 14 ⊢ (𝐽 ∈ Top → ∀𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) ∈ V)
58		eqid 2738	. . . . . . . . . . . . . . 15 ⊢ (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) = (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟))
59	58	fnmpt 6573	. . . . . . . . . . . . . 14 ⊢ (∀𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) ∈ V → (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) Fn 𝑦)
60	57, 59	syl 17	. . . . . . . . . . . . 13 ⊢ (𝐽 ∈ Top → (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) Fn 𝑦)
61	60	ad3antrrr 727	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)) → (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) Fn 𝑦)
62		simpr 485	. . . . . . . . . . . . . . 15 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)) → 𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin))
63		elfpw 9121	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin) ↔ (𝑤 ⊆ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∧ 𝑤 ∈ Fin))
64	62, 63	sylib 217	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)) → (𝑤 ⊆ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∧ 𝑤 ∈ Fin))
65	64	simpld 495	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)) → 𝑤 ⊆ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))
66	44	ad2antrr 723	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)) → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) = ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
67	65, 66	sseqtrd 3961	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)) → 𝑤 ⊆ ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
68	64	simprd 496	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)) → 𝑤 ∈ Fin)
69		fipreima 9125	. . . . . . . . . . . 12 ⊢ (((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) Fn 𝑦 ∧ 𝑤 ⊆ ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) ∧ 𝑤 ∈ Fin) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = 𝑤)
70	61, 67, 68, 69	syl3anc 1370	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = 𝑤)
71		eqcom 2745	. . . . . . . . . . . 12 ⊢ (((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = 𝑤 ↔ 𝑤 = ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧))
72	71	rexbii 3181	. . . . . . . . . . 11 ⊢ (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = 𝑤 ↔ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑤 = ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧))
73	70, 72	sylib 217	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑤 = ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧))
74		simpr 485	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 = ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)) → 𝑤 = ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧))
75	74	inteqd 4884	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 = ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)) → ∩ 𝑤 = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧))
76	75	eqeq2d 2749	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 = ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)) → (∅ = ∩ 𝑤 ↔ ∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)))
77	53, 73, 76	rexxfrd 5332	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∃𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)∅ = ∩ 𝑤 ↔ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)))
78		0ex 5231	. . . . . . . . . 10 ⊢ ∅ ∈ V
79		imassrn 5980	. . . . . . . . . . . . 13 ⊢ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ⊆ ran (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟))
80		eqid 2738	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) = (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟))
81	54, 80	opncldf1 22235	. . . . . . . . . . . . . . . 16 ⊢ (𝐽 ∈ Top → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)):𝐽–1-1-onto→(Clsd‘𝐽) ∧ ◡(𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) = (𝑣 ∈ (Clsd‘𝐽) ↦ (∪ 𝐽 ∖ 𝑣))))
82	81	simpld 495	. . . . . . . . . . . . . . 15 ⊢ (𝐽 ∈ Top → (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)):𝐽–1-1-onto→(Clsd‘𝐽))
83		f1ofo 6723	. . . . . . . . . . . . . . 15 ⊢ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)):𝐽–1-1-onto→(Clsd‘𝐽) → (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)):𝐽–onto→(Clsd‘𝐽))
84	82, 83	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝐽 ∈ Top → (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)):𝐽–onto→(Clsd‘𝐽))
85		forn 6691	. . . . . . . . . . . . . 14 ⊢ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)):𝐽–onto→(Clsd‘𝐽) → ran (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) = (Clsd‘𝐽))
86	84, 85	syl 17	. . . . . . . . . . . . 13 ⊢ (𝐽 ∈ Top → ran (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) = (Clsd‘𝐽))
87	79, 86	sseqtrid 3973	. . . . . . . . . . . 12 ⊢ (𝐽 ∈ Top → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ⊆ (Clsd‘𝐽))
88		fvex 6787	. . . . . . . . . . . . 13 ⊢ (Clsd‘𝐽) ∈ V
89	88	elpw2 5269	. . . . . . . . . . . 12 ⊢ (((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∈ 𝒫 (Clsd‘𝐽) ↔ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ⊆ (Clsd‘𝐽))
90	87, 89	sylibr 233	. . . . . . . . . . 11 ⊢ (𝐽 ∈ Top → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∈ 𝒫 (Clsd‘𝐽))
91	90	ad2antrr 723	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∈ 𝒫 (Clsd‘𝐽))
92		elfi 9172	. . . . . . . . . 10 ⊢ ((∅ ∈ V ∧ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∈ 𝒫 (Clsd‘𝐽)) → (∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) ↔ ∃𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)∅ = ∩ 𝑤))
93	78, 91, 92	sylancr 587	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) ↔ ∃𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)∅ = ∩ 𝑤))
94		inundif 4412	. . . . . . . . . . . . . 14 ⊢ (((𝒫 𝑦 ∩ Fin) ∩ {∅}) ∪ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) = (𝒫 𝑦 ∩ Fin)
95	94	rexeqi 3347	. . . . . . . . . . . . 13 ⊢ (∃𝑧 ∈ (((𝒫 𝑦 ∩ Fin) ∩ {∅}) ∪ ((𝒫 𝑦 ∩ Fin) ∖ {∅}))∪ 𝐽 = ∪ 𝑧 ↔ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧)
96		rexun 4124	. . . . . . . . . . . . 13 ⊢ (∃𝑧 ∈ (((𝒫 𝑦 ∩ Fin) ∩ {∅}) ∪ ((𝒫 𝑦 ∩ Fin) ∖ {∅}))∪ 𝐽 = ∪ 𝑧 ↔ (∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅})∪ 𝐽 = ∪ 𝑧 ∨ ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧))
97	95, 96	bitr3i 276	. . . . . . . . . . . 12 ⊢ (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧 ↔ (∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅})∪ 𝐽 = ∪ 𝑧 ∨ ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧))
98		elinel2 4130	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅}) → 𝑧 ∈ {∅})
99		elsni 4578	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ {∅} → 𝑧 = ∅)
100	98, 99	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅}) → 𝑧 = ∅)
101	100	unieqd 4853	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅}) → ∪ 𝑧 = ∪ ∅)
102		uni0 4869	. . . . . . . . . . . . . . . . . . 19 ⊢ ∪ ∅ = ∅
103	101, 102	eqtrdi 2794	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅}) → ∪ 𝑧 = ∅)
104	103	eqeq2d 2749	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅}) → (∪ 𝐽 = ∪ 𝑧 ↔ ∪ 𝐽 = ∅))
105	104	biimpd 228	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅}) → (∪ 𝐽 = ∪ 𝑧 → ∪ 𝐽 = ∅))
106	105	rexlimiv 3209	. . . . . . . . . . . . . . 15 ⊢ (∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅})∪ 𝐽 = ∪ 𝑧 → ∪ 𝐽 = ∅)
107		ssidd 3944	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → 𝑦 ⊆ 𝑦)
108		simprr 770	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → ∪ 𝐽 = ∅)
109		0ss 4330	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ∅ ⊆ ∪ 𝑦
110	108, 109	eqsstrdi 3975	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → ∪ 𝐽 ⊆ ∪ 𝑦)
111	24	ad2antlr 724	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → ∪ 𝑦 ⊆ ∪ 𝐽)
112	110, 111	eqssd 3938	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → ∪ 𝐽 = ∪ 𝑦)
113	112, 108	eqtr3d 2780	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → ∪ 𝑦 = ∅)
114	113, 3	eqeltrdi 2847	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → ∪ 𝑦 ∈ Fin)
115		pwfi 8961	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∪ 𝑦 ∈ Fin ↔ 𝒫 ∪ 𝑦 ∈ Fin)
116	114, 115	sylib 217	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → 𝒫 ∪ 𝑦 ∈ Fin)
117		pwuni 4878	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑦 ⊆ 𝒫 ∪ 𝑦
118		ssfi 8956	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝒫 ∪ 𝑦 ∈ Fin ∧ 𝑦 ⊆ 𝒫 ∪ 𝑦) → 𝑦 ∈ Fin)
119	116, 117, 118	sylancl 586	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → 𝑦 ∈ Fin)
120		elfpw 9121	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ (𝒫 𝑦 ∩ Fin) ↔ (𝑦 ⊆ 𝑦 ∧ 𝑦 ∈ Fin))
121	107, 119, 120	sylanbrc 583	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → 𝑦 ∈ (𝒫 𝑦 ∩ Fin))
122		simprl 768	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → 𝑦 ≠ ∅)
123		eldifsn 4720	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅}) ↔ (𝑦 ∈ (𝒫 𝑦 ∩ Fin) ∧ 𝑦 ≠ ∅))
124	121, 122, 123	sylanbrc 583	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → 𝑦 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅}))
125		unieq 4850	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑦 → ∪ 𝑧 = ∪ 𝑦)
126	125	rspceeqv 3575	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅}) ∧ ∪ 𝐽 = ∪ 𝑦) → ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧)
127	124, 112, 126	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧)
128	127	expr 457	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∪ 𝐽 = ∅ → ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧))
129	106, 128	syl5 34	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅})∪ 𝐽 = ∪ 𝑧 → ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧))
130		idd 24	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧 → ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧))
131	129, 130	jaod 856	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → ((∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅})∪ 𝐽 = ∪ 𝑧 ∨ ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧) → ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧))
132		olc 865	. . . . . . . . . . . . 13 ⊢ (∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧 → (∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅})∪ 𝐽 = ∪ 𝑧 ∨ ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧))
133	131, 132	impbid1 224	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → ((∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅})∪ 𝐽 = ∪ 𝑧 ∨ ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧) ↔ ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧))
134	97, 133	bitrid 282	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧 ↔ ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧))
135		eldifi 4061	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅}) → 𝑧 ∈ (𝒫 𝑦 ∩ Fin))
136	135	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → 𝑧 ∈ (𝒫 𝑦 ∩ Fin))
137		elfpw 9121	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ (𝒫 𝑦 ∩ Fin) ↔ (𝑧 ⊆ 𝑦 ∧ 𝑧 ∈ Fin))
138	136, 137	sylib 217	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → (𝑧 ⊆ 𝑦 ∧ 𝑧 ∈ Fin))
139	138	simpld 495	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → 𝑧 ⊆ 𝑦)
140		simpllr 773	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → 𝑦 ⊆ 𝐽)
141	139, 140	sstrd 3931	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → 𝑧 ⊆ 𝐽)
142	141	unissd 4849	. . . . . . . . . . . . . . 15 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ∪ 𝑧 ⊆ ∪ 𝐽)
143		eqss 3936	. . . . . . . . . . . . . . . 16 ⊢ (∪ 𝑧 = ∪ 𝐽 ↔ (∪ 𝑧 ⊆ ∪ 𝐽 ∧ ∪ 𝐽 ⊆ ∪ 𝑧))
144	143	baib 536	. . . . . . . . . . . . . . 15 ⊢ (∪ 𝑧 ⊆ ∪ 𝐽 → (∪ 𝑧 = ∪ 𝐽 ↔ ∪ 𝐽 ⊆ ∪ 𝑧))
145	142, 144	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → (∪ 𝑧 = ∪ 𝐽 ↔ ∪ 𝐽 ⊆ ∪ 𝑧))
146		eqcom 2745	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑧 = ∪ 𝐽 ↔ ∪ 𝐽 = ∪ 𝑧)
147		ssdif0 4297	. . . . . . . . . . . . . . 15 ⊢ (∪ 𝐽 ⊆ ∪ 𝑧 ↔ (∪ 𝐽 ∖ ∪ 𝑧) = ∅)
148		eqcom 2745	. . . . . . . . . . . . . . 15 ⊢ ((∪ 𝐽 ∖ ∪ 𝑧) = ∅ ↔ ∅ = (∪ 𝐽 ∖ ∪ 𝑧))
149	147, 148	bitri 274	. . . . . . . . . . . . . 14 ⊢ (∪ 𝐽 ⊆ ∪ 𝑧 ↔ ∅ = (∪ 𝐽 ∖ ∪ 𝑧))
150	145, 146, 149	3bitr3g 313	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → (∪ 𝐽 = ∪ 𝑧 ↔ ∅ = (∪ 𝐽 ∖ ∪ 𝑧)))
151		df-ima 5602	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = ran ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) ↾ 𝑧)
152	139	resmptd 5948	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) ↾ 𝑧) = (𝑟 ∈ 𝑧 ↦ (∪ 𝐽 ∖ 𝑟)))
153	152	rneqd 5847	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ran ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) ↾ 𝑧) = ran (𝑟 ∈ 𝑧 ↦ (∪ 𝐽 ∖ 𝑟)))
154	151, 153	eqtrid 2790	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = ran (𝑟 ∈ 𝑧 ↦ (∪ 𝐽 ∖ 𝑟)))
155	154	inteqd 4884	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = ∩ ran (𝑟 ∈ 𝑧 ↦ (∪ 𝐽 ∖ 𝑟)))
156	56	ralrimivw 3104	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐽 ∈ Top → ∀𝑟 ∈ 𝑧 (∪ 𝐽 ∖ 𝑟) ∈ V)
157	156	ad3antrrr 727	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ∀𝑟 ∈ 𝑧 (∪ 𝐽 ∖ 𝑟) ∈ V)
158		dfiin3g 5874	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑟 ∈ 𝑧 (∪ 𝐽 ∖ 𝑟) ∈ V → ∩ 𝑟 ∈ 𝑧 (∪ 𝐽 ∖ 𝑟) = ∩ ran (𝑟 ∈ 𝑧 ↦ (∪ 𝐽 ∖ 𝑟)))
159	157, 158	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ∩ 𝑟 ∈ 𝑧 (∪ 𝐽 ∖ 𝑟) = ∩ ran (𝑟 ∈ 𝑧 ↦ (∪ 𝐽 ∖ 𝑟)))
160		eldifsni 4723	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅}) → 𝑧 ≠ ∅)
161	160	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → 𝑧 ≠ ∅)
162		iindif2 5006	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ≠ ∅ → ∩ 𝑟 ∈ 𝑧 (∪ 𝐽 ∖ 𝑟) = (∪ 𝐽 ∖ ∪ 𝑟 ∈ 𝑧 𝑟))
163	161, 162	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ∩ 𝑟 ∈ 𝑧 (∪ 𝐽 ∖ 𝑟) = (∪ 𝐽 ∖ ∪ 𝑟 ∈ 𝑧 𝑟))
164	155, 159, 163	3eqtr2d 2784	. . . . . . . . . . . . . . 15 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = (∪ 𝐽 ∖ ∪ 𝑟 ∈ 𝑧 𝑟))
165		uniiun 4988	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑧 = ∪ 𝑟 ∈ 𝑧 𝑟
166	165	difeq2i 4054	. . . . . . . . . . . . . . 15 ⊢ (∪ 𝐽 ∖ ∪ 𝑧) = (∪ 𝐽 ∖ ∪ 𝑟 ∈ 𝑧 𝑟)
167	164, 166	eqtr4di 2796	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = (∪ 𝐽 ∖ ∪ 𝑧))
168	167	eqeq2d 2749	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → (∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ↔ ∅ = (∪ 𝐽 ∖ ∪ 𝑧)))
169	150, 168	bitr4d 281	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → (∪ 𝐽 = ∪ 𝑧 ↔ ∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)))
170	169	rexbidva 3225	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧 ↔ ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)))
171	134, 170	bitrd 278	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧 ↔ ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)))
172		imaeq2 5965	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = ∅ → ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ ∅))
173		ima0 5985	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ ∅) = ∅
174	172, 173	eqtrdi 2794	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = ∅ → ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = ∅)
175	174	inteqd 4884	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = ∅ → ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = ∩ ∅)
176		int0 4893	. . . . . . . . . . . . . . . . . 18 ⊢ ∩ ∅ = V
177	175, 176	eqtrdi 2794	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ∅ → ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = V)
178	177	neeq1d 3003	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = ∅ → (∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ≠ ∅ ↔ V ≠ ∅))
179	14, 178	mpbiri 257	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = ∅ → ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ≠ ∅)
180	179	necomd 2999	. . . . . . . . . . . . . 14 ⊢ (𝑧 = ∅ → ∅ ≠ ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧))
181	180	necon2i 2978	. . . . . . . . . . . . 13 ⊢ (∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) → 𝑧 ≠ ∅)
182		eldifsn 4720	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅}) ↔ (𝑧 ∈ (𝒫 𝑦 ∩ Fin) ∧ 𝑧 ≠ ∅))
183	182	rbaibr 538	. . . . . . . . . . . . 13 ⊢ (𝑧 ≠ ∅ → (𝑧 ∈ (𝒫 𝑦 ∩ Fin) ↔ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})))
184	181, 183	syl 17	. . . . . . . . . . . 12 ⊢ (∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) → (𝑧 ∈ (𝒫 𝑦 ∩ Fin) ↔ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})))
185	184	pm5.32ri 576	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ (𝒫 𝑦 ∩ Fin) ∧ ∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)) ↔ (𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅}) ∧ ∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)))
186	185	rexbii2 3179	. . . . . . . . . 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 345	. . . . . . 7 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → ((∪ 𝐽 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧) ↔ (∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅ → ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))))
190	23, 189	pm2.61dane 3032	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ((∪ 𝐽 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧) ↔ (∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅ → ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))))
191	57	adantr 481	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ∀𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) ∈ V)
192		dfiin3g 5874	. . . . . . . . . . 11 ⊢ (∀𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) ∈ V → ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∩ ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
193	191, 192	syl 17	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∩ ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
194	44	inteqd 4884	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) = ∩ ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
195	193, 194	eqtr4d 2781	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))
196	195	eqeq1d 2740	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → (∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅ ↔ ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) = ∅))
197		nne 2947	. . . . . . . 8 ⊢ (¬ ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅ ↔ ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) = ∅)
198	196, 197	bitr4di 289	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → (∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅ ↔ ¬ ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅))
199	198	imbi1d 342	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ((∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅ → ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))) ↔ (¬ ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅ → ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))))
200	190, 199	bitrd 278	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ((∪ 𝐽 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧) ↔ (¬ ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅ → ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))))
201		con1b 359	. . . . 5 ⊢ ((¬ ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅ → ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))) ↔ (¬ ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅))
202	200, 201	bitrdi 287	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ((∪ 𝐽 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧) ↔ (¬ ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅)))
203	1, 202	sylan2 593	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ∈ 𝒫 𝐽) → ((∪ 𝐽 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧) ↔ (¬ ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅)))
204	203	ralbidva 3111	. 2 ⊢ (𝐽 ∈ Top → (∀𝑦 ∈ 𝒫 𝐽(∪ 𝐽 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧) ↔ ∀𝑦 ∈ 𝒫 𝐽(¬ ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅)))
205	54	iscmp 22539	. . 3 ⊢ (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝐽(∪ 𝐽 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧)))
206	205	baib 536	. 2 ⊢ (𝐽 ∈ Top → (𝐽 ∈ Comp ↔ ∀𝑦 ∈ 𝒫 𝐽(∪ 𝐽 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧)))
207	90	adantr 481	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ∈ 𝒫 𝐽) → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∈ 𝒫 (Clsd‘𝐽))
208		simpl 483	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) → 𝐽 ∈ Top)
209		funmpt 6472	. . . . . 6 ⊢ Fun (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟))
210	209	a1i 11	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) → Fun (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)))
211		elpwi 4542	. . . . . . 7 ⊢ (𝑥 ∈ 𝒫 (Clsd‘𝐽) → 𝑥 ⊆ (Clsd‘𝐽))
212		foima 6693	. . . . . . . . 9 ⊢ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)):𝐽–onto→(Clsd‘𝐽) → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝐽) = (Clsd‘𝐽))
213	84, 212	syl 17	. . . . . . . 8 ⊢ (𝐽 ∈ Top → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝐽) = (Clsd‘𝐽))
214	213	sseq2d 3953	. . . . . . 7 ⊢ (𝐽 ∈ Top → (𝑥 ⊆ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝐽) ↔ 𝑥 ⊆ (Clsd‘𝐽)))
215	211, 214	syl5ibr 245	. . . . . 6 ⊢ (𝐽 ∈ Top → (𝑥 ∈ 𝒫 (Clsd‘𝐽) → 𝑥 ⊆ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝐽)))
216	215	imp 407	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) → 𝑥 ⊆ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝐽))
217		ssimaexg 6854	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ Fun (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) ∧ 𝑥 ⊆ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝐽)) → ∃𝑦(𝑦 ⊆ 𝐽 ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))
218	208, 210, 216, 217	syl3anc 1370	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) → ∃𝑦(𝑦 ⊆ 𝐽 ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))
219		df-rex 3070	. . . . 5 ⊢ (∃𝑦 ∈ 𝒫 𝐽𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ↔ ∃𝑦(𝑦 ∈ 𝒫 𝐽 ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))
220		velpw 4538	. . . . . . 7 ⊢ (𝑦 ∈ 𝒫 𝐽 ↔ 𝑦 ⊆ 𝐽)
221	220	anbi1i 624	. . . . . 6 ⊢ ((𝑦 ∈ 𝒫 𝐽 ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) ↔ (𝑦 ⊆ 𝐽 ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))
222	221	exbii 1850	. . . . 5 ⊢ (∃𝑦(𝑦 ∈ 𝒫 𝐽 ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) ↔ ∃𝑦(𝑦 ⊆ 𝐽 ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))
223	219, 222	bitri 274	. . . 4 ⊢ (∃𝑦 ∈ 𝒫 𝐽𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ↔ ∃𝑦(𝑦 ⊆ 𝐽 ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))
224	218, 223	sylibr 233	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) → ∃𝑦 ∈ 𝒫 𝐽𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))
225		simpr 485	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))
226	225	fveq2d 6778	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → (fi‘𝑥) = (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))
227	226	eleq2d 2824	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → (∅ ∈ (fi‘𝑥) ↔ ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))))
228	227	notbid 318	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → (¬ ∅ ∈ (fi‘𝑥) ↔ ¬ ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))))
229	225	inteqd 4884	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → ∩ 𝑥 = ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))
230	229	neeq1d 3003	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → (∩ 𝑥 ≠ ∅ ↔ ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅))
231	228, 230	imbi12d 345	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → ((¬ ∅ ∈ (fi‘𝑥) → ∩ 𝑥 ≠ ∅) ↔ (¬ ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅)))
232	207, 224, 231	ralxfrd 5331	. 2 ⊢ (𝐽 ∈ Top → (∀𝑥 ∈ 𝒫 (Clsd‘𝐽)(¬ ∅ ∈ (fi‘𝑥) → ∩ 𝑥 ≠ ∅) ↔ ∀𝑦 ∈ 𝒫 𝐽(¬ ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅)))
233	204, 206, 232	3bitr4d 311	1 ⊢ (𝐽 ∈ Top → (𝐽 ∈ Comp ↔ ∀𝑥 ∈ 𝒫 (Clsd‘𝐽)(¬ ∅ ∈ (fi‘𝑥) → ∩ 𝑥 ≠ ∅)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 844   = wceq 1539  ∃wex 1782   ∈ wcel 2106   ≠ wne 2943  ∀wral 3064  ∃wrex 3065  Vcvv 3432   ∖ cdif 3884   ∪ cun 3885   ∩ cin 3886   ⊆ wss 3887  ∅c0 4256  𝒫 cpw 4533  {csn 4561  ∪ cuni 4839  ∩ cint 4879  ∪ ciun 4924  ∩ ciin 4925   ↦ cmpt 5157  ^◡ccnv 5588  ran crn 5590   ↾ cres 5591   “ cima 5592  Fun wfun 6427   Fn wfn 6428  –onto→wfo 6431  –1-1-onto→wf1o 6432  ‘cfv 6433  Fincfn 8733  ficfi 9169  Topctop 22042  Clsdccld 22167  Compccmp 22537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-int 4880  df-iun 4926  df-iin 4927  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-om 7713  df-1o 8297  df-en 8734  df-fin 8737  df-fi 9170  df-top 22043  df-cld 22170  df-cmp 22538

This theorem is referenced by:  cmpfii  22560  fclscmp  23181  zarcmplem  31831  heibor1lem  35967