Theorem cmpfi 22759

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 4567	. . . 4 ⊢ (𝑦 ∈ 𝒫 𝐽 → 𝑦 ⊆ 𝐽)
2		0ss 4356	. . . . . . . . . . 11 ⊢ ∅ ⊆ 𝑦
3		0fin 9115	. . . . . . . . . . 11 ⊢ ∅ ∈ Fin
4		elfpw 9298	. . . . . . . . . . 11 ⊢ (∅ ∈ (𝒫 𝑦 ∩ Fin) ↔ (∅ ⊆ 𝑦 ∧ ∅ ∈ Fin))
5	2, 3, 4	mpbir2an 709	. . . . . . . . . 10 ⊢ ∅ ∈ (𝒫 𝑦 ∩ Fin)
6		simprr 771	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 = ∅ ∧ ∪ 𝐽 = ∪ 𝑦)) → ∪ 𝐽 = ∪ 𝑦)
7		simprl 769	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 = ∅ ∧ ∪ 𝐽 = ∪ 𝑦)) → 𝑦 = ∅)
8	7	unieqd 4879	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 = ∅ ∧ ∪ 𝐽 = ∪ 𝑦)) → ∪ 𝑦 = ∪ ∅)
9	6, 8	eqtrd 2776	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 = ∅ ∧ ∪ 𝐽 = ∪ 𝑦)) → ∪ 𝐽 = ∪ ∅)
10		unieq 4876	. . . . . . . . . . 11 ⊢ (𝑧 = ∅ → ∪ 𝑧 = ∪ ∅)
11	10	rspceeqv 3595	. . . . . . . . . 10 ⊢ ((∅ ∈ (𝒫 𝑦 ∩ Fin) ∧ ∪ 𝐽 = ∪ ∅) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧)
12	5, 9, 11	sylancr 587	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 = ∅ ∧ ∪ 𝐽 = ∪ 𝑦)) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧)
13	12	expr 457	. . . . . . . 8 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 = ∅) → (∪ 𝐽 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧))
14		vn0 4298	. . . . . . . . . 10 ⊢ V ≠ ∅
15		iineq1 4971	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ∅ → ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∩ 𝑟 ∈ ∅ (∪ 𝐽 ∖ 𝑟))
16	15	adantl 482	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 = ∅) → ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∩ 𝑟 ∈ ∅ (∪ 𝐽 ∖ 𝑟))
17		0iin 5024	. . . . . . . . . . . . 13 ⊢ ∩ 𝑟 ∈ ∅ (∪ 𝐽 ∖ 𝑟) = V
18	16, 17	eqtrdi 2792	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 = ∅) → ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = V)
19	18	eqeq1d 2738	. . . . . . . . . . 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 4873	. . . . . . . . . . . 12 ⊢ (𝑦 ⊆ 𝐽 → ∪ 𝑦 ⊆ ∪ 𝐽)
25	24	ad2antlr 725	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → ∪ 𝑦 ⊆ ∪ 𝐽)
26		eqss 3959	. . . . . . . . . . . 12 ⊢ (∪ 𝑦 = ∪ 𝐽 ↔ (∪ 𝑦 ⊆ ∪ 𝐽 ∧ ∪ 𝐽 ⊆ ∪ 𝑦))
27	26	baib 536	. . . . . . . . . . 11 ⊢ (∪ 𝑦 ⊆ ∪ 𝐽 → (∪ 𝑦 = ∪ 𝐽 ↔ ∪ 𝐽 ⊆ ∪ 𝑦))
28	25, 27	syl 17	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∪ 𝑦 = ∪ 𝐽 ↔ ∪ 𝐽 ⊆ ∪ 𝑦))
29		eqcom 2743	. . . . . . . . . 10 ⊢ (∪ 𝑦 = ∪ 𝐽 ↔ ∪ 𝐽 = ∪ 𝑦)
30		ssdif0 4323	. . . . . . . . . 10 ⊢ (∪ 𝐽 ⊆ ∪ 𝑦 ↔ (∪ 𝐽 ∖ ∪ 𝑦) = ∅)
31	28, 29, 30	3bitr3g 312	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∪ 𝐽 = ∪ 𝑦 ↔ (∪ 𝐽 ∖ ∪ 𝑦) = ∅))
32		iindif2 5037	. . . . . . . . . . . 12 ⊢ (𝑦 ≠ ∅ → ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = (∪ 𝐽 ∖ ∪ 𝑟 ∈ 𝑦 𝑟))
33	32	adantl 482	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = (∪ 𝐽 ∖ ∪ 𝑟 ∈ 𝑦 𝑟))
34		uniiun 5018	. . . . . . . . . . . 12 ⊢ ∪ 𝑦 = ∪ 𝑟 ∈ 𝑦 𝑟
35	34	difeq2i 4079	. . . . . . . . . . 11 ⊢ (∪ 𝐽 ∖ ∪ 𝑦) = (∪ 𝐽 ∖ ∪ 𝑟 ∈ 𝑦 𝑟)
36	33, 35	eqtr4di 2794	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = (∪ 𝐽 ∖ ∪ 𝑦))
37	36	eqeq1d 2738	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅ ↔ (∪ 𝐽 ∖ ∪ 𝑦) = ∅))
38	31, 37	bitr4d 281	. . . . . . . 8 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∪ 𝐽 = ∪ 𝑦 ↔ ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅))
39		imassrn 6024	. . . . . . . . . . . 12 ⊢ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ⊆ ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟))
40		df-ima 5646	. . . . . . . . . . . . . 14 ⊢ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) = ran ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) ↾ 𝑦)
41		resmpt 5991	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ⊆ 𝐽 → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) ↾ 𝑦) = (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
42	41	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) ↾ 𝑦) = (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
43	42	rneqd 5893	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ran ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) ↾ 𝑦) = ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
44	40, 43	eqtrid 2788	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) = ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
45	44	ad2antrr 724	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ (𝒫 𝑦 ∩ Fin)) → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) = ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
46	39, 45	sseqtrrid 3997	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ (𝒫 𝑦 ∩ Fin)) → ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ⊆ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))
47		funmpt 6539	. . . . . . . . . . . 12 ⊢ Fun (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟))
48		elinel2 4156	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (𝒫 𝑦 ∩ Fin) → 𝑧 ∈ Fin)
49	48	adantl 482	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ (𝒫 𝑦 ∩ Fin)) → 𝑧 ∈ Fin)
50		imafi 9119	. . . . . . . . . . . 12 ⊢ ((Fun (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) ∧ 𝑧 ∈ Fin) → ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ∈ Fin)
51	47, 49, 50	sylancr 587	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ (𝒫 𝑦 ∩ Fin)) → ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ∈ Fin)
52		elfpw 9298	. . . . . . . . . . 11 ⊢ (((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin) ↔ (((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ⊆ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∧ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ∈ Fin))
53	46, 51, 52	sylanbrc 583	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ (𝒫 𝑦 ∩ Fin)) → ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin))
54		eqid 2736	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝐽 = ∪ 𝐽
55	54	topopn 22255	. . . . . . . . . . . . . . . 16 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽)
56	55	difexd 5286	. . . . . . . . . . . . . . 15 ⊢ (𝐽 ∈ Top → (∪ 𝐽 ∖ 𝑟) ∈ V)
57	56	ralrimivw 3147	. . . . . . . . . . . . . 14 ⊢ (𝐽 ∈ Top → ∀𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) ∈ V)
58		eqid 2736	. . . . . . . . . . . . . . 15 ⊢ (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) = (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟))
59	58	fnmpt 6641	. . . . . . . . . . . . . 14 ⊢ (∀𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) ∈ V → (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) Fn 𝑦)
60	57, 59	syl 17	. . . . . . . . . . . . 13 ⊢ (𝐽 ∈ Top → (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) Fn 𝑦)
61	60	ad3antrrr 728	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)) → (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) Fn 𝑦)
62		simpr 485	. . . . . . . . . . . . . . 15 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)) → 𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin))
63		elfpw 9298	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin) ↔ (𝑤 ⊆ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∧ 𝑤 ∈ Fin))
64	62, 63	sylib 217	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)) → (𝑤 ⊆ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∧ 𝑤 ∈ Fin))
65	64	simpld 495	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)) → 𝑤 ⊆ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))
66	44	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)) → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) = ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
67	65, 66	sseqtrd 3984	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)) → 𝑤 ⊆ ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
68	64	simprd 496	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)) → 𝑤 ∈ Fin)
69		fipreima 9302	. . . . . . . . . . . 12 ⊢ (((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) Fn 𝑦 ∧ 𝑤 ⊆ ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) ∧ 𝑤 ∈ Fin) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = 𝑤)
70	61, 67, 68, 69	syl3anc 1371	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = 𝑤)
71		eqcom 2743	. . . . . . . . . . . 12 ⊢ (((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = 𝑤 ↔ 𝑤 = ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧))
72	71	rexbii 3097	. . . . . . . . . . 11 ⊢ (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = 𝑤 ↔ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑤 = ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧))
73	70, 72	sylib 217	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑤 = ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧))
74		simpr 485	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 = ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)) → 𝑤 = ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧))
75	74	inteqd 4912	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 = ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)) → ∩ 𝑤 = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧))
76	75	eqeq2d 2747	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 = ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)) → (∅ = ∩ 𝑤 ↔ ∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)))
77	53, 73, 76	rexxfrd 5364	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∃𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)∅ = ∩ 𝑤 ↔ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)))
78		0ex 5264	. . . . . . . . . 10 ⊢ ∅ ∈ V
79		imassrn 6024	. . . . . . . . . . . . 13 ⊢ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ⊆ ran (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟))
80		eqid 2736	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) = (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟))
81	54, 80	opncldf1 22435	. . . . . . . . . . . . . . . 16 ⊢ (𝐽 ∈ Top → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)):𝐽–1-1-onto→(Clsd‘𝐽) ∧ ◡(𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) = (𝑣 ∈ (Clsd‘𝐽) ↦ (∪ 𝐽 ∖ 𝑣))))
82	81	simpld 495	. . . . . . . . . . . . . . 15 ⊢ (𝐽 ∈ Top → (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)):𝐽–1-1-onto→(Clsd‘𝐽))
83		f1ofo 6791	. . . . . . . . . . . . . . 15 ⊢ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)):𝐽–1-1-onto→(Clsd‘𝐽) → (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)):𝐽–onto→(Clsd‘𝐽))
84	82, 83	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝐽 ∈ Top → (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)):𝐽–onto→(Clsd‘𝐽))
85		forn 6759	. . . . . . . . . . . . . 14 ⊢ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)):𝐽–onto→(Clsd‘𝐽) → ran (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) = (Clsd‘𝐽))
86	84, 85	syl 17	. . . . . . . . . . . . 13 ⊢ (𝐽 ∈ Top → ran (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) = (Clsd‘𝐽))
87	79, 86	sseqtrid 3996	. . . . . . . . . . . 12 ⊢ (𝐽 ∈ Top → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ⊆ (Clsd‘𝐽))
88		fvex 6855	. . . . . . . . . . . . 13 ⊢ (Clsd‘𝐽) ∈ V
89	88	elpw2 5302	. . . . . . . . . . . 12 ⊢ (((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∈ 𝒫 (Clsd‘𝐽) ↔ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ⊆ (Clsd‘𝐽))
90	87, 89	sylibr 233	. . . . . . . . . . 11 ⊢ (𝐽 ∈ Top → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∈ 𝒫 (Clsd‘𝐽))
91	90	ad2antrr 724	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∈ 𝒫 (Clsd‘𝐽))
92		elfi 9349	. . . . . . . . . 10 ⊢ ((∅ ∈ V ∧ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∈ 𝒫 (Clsd‘𝐽)) → (∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) ↔ ∃𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)∅ = ∩ 𝑤))
93	78, 91, 92	sylancr 587	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) ↔ ∃𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)∅ = ∩ 𝑤))
94		inundif 4438	. . . . . . . . . . . . . 14 ⊢ (((𝒫 𝑦 ∩ Fin) ∩ {∅}) ∪ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) = (𝒫 𝑦 ∩ Fin)
95	94	rexeqi 3312	. . . . . . . . . . . . 13 ⊢ (∃𝑧 ∈ (((𝒫 𝑦 ∩ Fin) ∩ {∅}) ∪ ((𝒫 𝑦 ∩ Fin) ∖ {∅}))∪ 𝐽 = ∪ 𝑧 ↔ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧)
96		rexun 4150	. . . . . . . . . . . . 13 ⊢ (∃𝑧 ∈ (((𝒫 𝑦 ∩ Fin) ∩ {∅}) ∪ ((𝒫 𝑦 ∩ Fin) ∖ {∅}))∪ 𝐽 = ∪ 𝑧 ↔ (∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅})∪ 𝐽 = ∪ 𝑧 ∨ ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧))
97	95, 96	bitr3i 276	. . . . . . . . . . . 12 ⊢ (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧 ↔ (∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅})∪ 𝐽 = ∪ 𝑧 ∨ ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧))
98		elinel2 4156	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅}) → 𝑧 ∈ {∅})
99		elsni 4603	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ {∅} → 𝑧 = ∅)
100	98, 99	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅}) → 𝑧 = ∅)
101	100	unieqd 4879	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅}) → ∪ 𝑧 = ∪ ∅)
102		uni0 4896	. . . . . . . . . . . . . . . . . . 19 ⊢ ∪ ∅ = ∅
103	101, 102	eqtrdi 2792	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅}) → ∪ 𝑧 = ∅)
104	103	eqeq2d 2747	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅}) → (∪ 𝐽 = ∪ 𝑧 ↔ ∪ 𝐽 = ∅))
105	104	biimpd 228	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅}) → (∪ 𝐽 = ∪ 𝑧 → ∪ 𝐽 = ∅))
106	105	rexlimiv 3145	. . . . . . . . . . . . . . 15 ⊢ (∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅})∪ 𝐽 = ∪ 𝑧 → ∪ 𝐽 = ∅)
107		ssidd 3967	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → 𝑦 ⊆ 𝑦)
108		simprr 771	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → ∪ 𝐽 = ∅)
109		0ss 4356	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ∅ ⊆ ∪ 𝑦
110	108, 109	eqsstrdi 3998	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → ∪ 𝐽 ⊆ ∪ 𝑦)
111	24	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → ∪ 𝑦 ⊆ ∪ 𝐽)
112	110, 111	eqssd 3961	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → ∪ 𝐽 = ∪ 𝑦)
113	112, 108	eqtr3d 2778	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → ∪ 𝑦 = ∅)
114	113, 3	eqeltrdi 2846	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → ∪ 𝑦 ∈ Fin)
115		pwfi 9122	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∪ 𝑦 ∈ Fin ↔ 𝒫 ∪ 𝑦 ∈ Fin)
116	114, 115	sylib 217	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → 𝒫 ∪ 𝑦 ∈ Fin)
117		pwuni 4906	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑦 ⊆ 𝒫 ∪ 𝑦
118		ssfi 9117	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝒫 ∪ 𝑦 ∈ Fin ∧ 𝑦 ⊆ 𝒫 ∪ 𝑦) → 𝑦 ∈ Fin)
119	116, 117, 118	sylancl 586	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → 𝑦 ∈ Fin)
120		elfpw 9298	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ (𝒫 𝑦 ∩ Fin) ↔ (𝑦 ⊆ 𝑦 ∧ 𝑦 ∈ Fin))
121	107, 119, 120	sylanbrc 583	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → 𝑦 ∈ (𝒫 𝑦 ∩ Fin))
122		simprl 769	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → 𝑦 ≠ ∅)
123		eldifsn 4747	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅}) ↔ (𝑦 ∈ (𝒫 𝑦 ∩ Fin) ∧ 𝑦 ≠ ∅))
124	121, 122, 123	sylanbrc 583	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → 𝑦 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅}))
125		unieq 4876	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑦 → ∪ 𝑧 = ∪ 𝑦)
126	125	rspceeqv 3595	. . . . . . . . . . . . . . . . 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 857	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → ((∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅})∪ 𝐽 = ∪ 𝑧 ∨ ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧) → ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧))
132		olc 866	. . . . . . . . . . . . 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 4086	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅}) → 𝑧 ∈ (𝒫 𝑦 ∩ Fin))
136	135	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → 𝑧 ∈ (𝒫 𝑦 ∩ Fin))
137		elfpw 9298	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ (𝒫 𝑦 ∩ Fin) ↔ (𝑧 ⊆ 𝑦 ∧ 𝑧 ∈ Fin))
138	136, 137	sylib 217	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → (𝑧 ⊆ 𝑦 ∧ 𝑧 ∈ Fin))
139	138	simpld 495	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → 𝑧 ⊆ 𝑦)
140		simpllr 774	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → 𝑦 ⊆ 𝐽)
141	139, 140	sstrd 3954	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → 𝑧 ⊆ 𝐽)
142	141	unissd 4875	. . . . . . . . . . . . . . 15 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ∪ 𝑧 ⊆ ∪ 𝐽)
143		eqss 3959	. . . . . . . . . . . . . . . 16 ⊢ (∪ 𝑧 = ∪ 𝐽 ↔ (∪ 𝑧 ⊆ ∪ 𝐽 ∧ ∪ 𝐽 ⊆ ∪ 𝑧))
144	143	baib 536	. . . . . . . . . . . . . . 15 ⊢ (∪ 𝑧 ⊆ ∪ 𝐽 → (∪ 𝑧 = ∪ 𝐽 ↔ ∪ 𝐽 ⊆ ∪ 𝑧))
145	142, 144	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → (∪ 𝑧 = ∪ 𝐽 ↔ ∪ 𝐽 ⊆ ∪ 𝑧))
146		eqcom 2743	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑧 = ∪ 𝐽 ↔ ∪ 𝐽 = ∪ 𝑧)
147		ssdif0 4323	. . . . . . . . . . . . . . 15 ⊢ (∪ 𝐽 ⊆ ∪ 𝑧 ↔ (∪ 𝐽 ∖ ∪ 𝑧) = ∅)
148		eqcom 2743	. . . . . . . . . . . . . . 15 ⊢ ((∪ 𝐽 ∖ ∪ 𝑧) = ∅ ↔ ∅ = (∪ 𝐽 ∖ ∪ 𝑧))
149	147, 148	bitri 274	. . . . . . . . . . . . . 14 ⊢ (∪ 𝐽 ⊆ ∪ 𝑧 ↔ ∅ = (∪ 𝐽 ∖ ∪ 𝑧))
150	145, 146, 149	3bitr3g 312	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → (∪ 𝐽 = ∪ 𝑧 ↔ ∅ = (∪ 𝐽 ∖ ∪ 𝑧)))
151		df-ima 5646	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = ran ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) ↾ 𝑧)
152	139	resmptd 5994	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) ↾ 𝑧) = (𝑟 ∈ 𝑧 ↦ (∪ 𝐽 ∖ 𝑟)))
153	152	rneqd 5893	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ran ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) ↾ 𝑧) = ran (𝑟 ∈ 𝑧 ↦ (∪ 𝐽 ∖ 𝑟)))
154	151, 153	eqtrid 2788	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = ran (𝑟 ∈ 𝑧 ↦ (∪ 𝐽 ∖ 𝑟)))
155	154	inteqd 4912	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = ∩ ran (𝑟 ∈ 𝑧 ↦ (∪ 𝐽 ∖ 𝑟)))
156	56	ralrimivw 3147	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐽 ∈ Top → ∀𝑟 ∈ 𝑧 (∪ 𝐽 ∖ 𝑟) ∈ V)
157	156	ad3antrrr 728	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ∀𝑟 ∈ 𝑧 (∪ 𝐽 ∖ 𝑟) ∈ V)
158		dfiin3g 5920	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑟 ∈ 𝑧 (∪ 𝐽 ∖ 𝑟) ∈ V → ∩ 𝑟 ∈ 𝑧 (∪ 𝐽 ∖ 𝑟) = ∩ ran (𝑟 ∈ 𝑧 ↦ (∪ 𝐽 ∖ 𝑟)))
159	157, 158	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ∩ 𝑟 ∈ 𝑧 (∪ 𝐽 ∖ 𝑟) = ∩ ran (𝑟 ∈ 𝑧 ↦ (∪ 𝐽 ∖ 𝑟)))
160		eldifsni 4750	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅}) → 𝑧 ≠ ∅)
161	160	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → 𝑧 ≠ ∅)
162		iindif2 5037	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ≠ ∅ → ∩ 𝑟 ∈ 𝑧 (∪ 𝐽 ∖ 𝑟) = (∪ 𝐽 ∖ ∪ 𝑟 ∈ 𝑧 𝑟))
163	161, 162	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ∩ 𝑟 ∈ 𝑧 (∪ 𝐽 ∖ 𝑟) = (∪ 𝐽 ∖ ∪ 𝑟 ∈ 𝑧 𝑟))
164	155, 159, 163	3eqtr2d 2782	. . . . . . . . . . . . . . 15 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = (∪ 𝐽 ∖ ∪ 𝑟 ∈ 𝑧 𝑟))
165		uniiun 5018	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑧 = ∪ 𝑟 ∈ 𝑧 𝑟
166	165	difeq2i 4079	. . . . . . . . . . . . . . 15 ⊢ (∪ 𝐽 ∖ ∪ 𝑧) = (∪ 𝐽 ∖ ∪ 𝑟 ∈ 𝑧 𝑟)
167	164, 166	eqtr4di 2794	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = (∪ 𝐽 ∖ ∪ 𝑧))
168	167	eqeq2d 2747	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → (∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ↔ ∅ = (∪ 𝐽 ∖ ∪ 𝑧)))
169	150, 168	bitr4d 281	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → (∪ 𝐽 = ∪ 𝑧 ↔ ∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)))
170	169	rexbidva 3173	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧 ↔ ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)))
171	134, 170	bitrd 278	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧 ↔ ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)))
172		imaeq2 6009	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = ∅ → ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ ∅))
173		ima0 6029	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ ∅) = ∅
174	172, 173	eqtrdi 2792	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = ∅ → ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = ∅)
175	174	inteqd 4912	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = ∅ → ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = ∩ ∅)
176		int0 4923	. . . . . . . . . . . . . . . . . 18 ⊢ ∩ ∅ = V
177	175, 176	eqtrdi 2792	. . . . . . . . . . . . . . . . 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 4747	. . . . . . . . . . . . . 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 3093	. . . . . . . . . 10 ⊢ (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ↔ ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧))
187	171, 186	bitr4di 288	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧 ↔ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)))
188	77, 93, 187	3bitr4rd 311	. . . . . . . 8 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧 ↔ ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))))
189	38, 188	imbi12d 344	. . . . . . 7 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → ((∪ 𝐽 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧) ↔ (∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅ → ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))))
190	23, 189	pm2.61dane 3032	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ((∪ 𝐽 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧) ↔ (∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅ → ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))))
191	57	adantr 481	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ∀𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) ∈ V)
192		dfiin3g 5920	. . . . . . . . . . 11 ⊢ (∀𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) ∈ V → ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∩ ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
193	191, 192	syl 17	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∩ ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
194	44	inteqd 4912	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) = ∩ ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
195	193, 194	eqtr4d 2779	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))
196	195	eqeq1d 2738	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → (∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅ ↔ ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) = ∅))
197		nne 2947	. . . . . . . 8 ⊢ (¬ ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅ ↔ ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) = ∅)
198	196, 197	bitr4di 288	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → (∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅ ↔ ¬ ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅))
199	198	imbi1d 341	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ((∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅ → ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))) ↔ (¬ ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅ → ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))))
200	190, 199	bitrd 278	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ((∪ 𝐽 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧) ↔ (¬ ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅ → ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))))
201		con1b 358	. . . . 5 ⊢ ((¬ ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅ → ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))) ↔ (¬ ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅))
202	200, 201	bitrdi 286	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ((∪ 𝐽 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧) ↔ (¬ ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅)))
203	1, 202	sylan2 593	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ∈ 𝒫 𝐽) → ((∪ 𝐽 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧) ↔ (¬ ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅)))
204	203	ralbidva 3172	. 2 ⊢ (𝐽 ∈ Top → (∀𝑦 ∈ 𝒫 𝐽(∪ 𝐽 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧) ↔ ∀𝑦 ∈ 𝒫 𝐽(¬ ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅)))
205	54	iscmp 22739	. . 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 6539	. . . . . 6 ⊢ Fun (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟))
210	209	a1i 11	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) → Fun (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)))
211		elpwi 4567	. . . . . . 7 ⊢ (𝑥 ∈ 𝒫 (Clsd‘𝐽) → 𝑥 ⊆ (Clsd‘𝐽))
212		foima 6761	. . . . . . . . 9 ⊢ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)):𝐽–onto→(Clsd‘𝐽) → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝐽) = (Clsd‘𝐽))
213	84, 212	syl 17	. . . . . . . 8 ⊢ (𝐽 ∈ Top → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝐽) = (Clsd‘𝐽))
214	213	sseq2d 3976	. . . . . . 7 ⊢ (𝐽 ∈ Top → (𝑥 ⊆ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝐽) ↔ 𝑥 ⊆ (Clsd‘𝐽)))
215	211, 214	syl5ibr 245	. . . . . 6 ⊢ (𝐽 ∈ Top → (𝑥 ∈ 𝒫 (Clsd‘𝐽) → 𝑥 ⊆ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝐽)))
216	215	imp 407	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) → 𝑥 ⊆ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝐽))
217		ssimaexg 6927	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ Fun (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) ∧ 𝑥 ⊆ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝐽)) → ∃𝑦(𝑦 ⊆ 𝐽 ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))
218	208, 210, 216, 217	syl3anc 1371	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) → ∃𝑦(𝑦 ⊆ 𝐽 ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))
219		df-rex 3074	. . . . 5 ⊢ (∃𝑦 ∈ 𝒫 𝐽𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ↔ ∃𝑦(𝑦 ∈ 𝒫 𝐽 ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))
220		velpw 4565	. . . . . . 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 6846	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → (fi‘𝑥) = (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))
227	226	eleq2d 2823	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → (∅ ∈ (fi‘𝑥) ↔ ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))))
228	227	notbid 317	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → (¬ ∅ ∈ (fi‘𝑥) ↔ ¬ ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))))
229	225	inteqd 4912	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → ∩ 𝑥 = ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))
230	229	neeq1d 3003	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → (∩ 𝑥 ≠ ∅ ↔ ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅))
231	228, 230	imbi12d 344	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → ((¬ ∅ ∈ (fi‘𝑥) → ∩ 𝑥 ≠ ∅) ↔ (¬ ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅)))
232	207, 224, 231	ralxfrd 5363	. 2 ⊢ (𝐽 ∈ Top → (∀𝑥 ∈ 𝒫 (Clsd‘𝐽)(¬ ∅ ∈ (fi‘𝑥) → ∩ 𝑥 ≠ ∅) ↔ ∀𝑦 ∈ 𝒫 𝐽(¬ ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅)))
233	204, 206, 232	3bitr4d 310	1 ⊢ (𝐽 ∈ Top → (𝐽 ∈ Comp ↔ ∀𝑥 ∈ 𝒫 (Clsd‘𝐽)(¬ ∅ ∈ (fi‘𝑥) → ∩ 𝑥 ≠ ∅)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 845   = wceq 1541  ∃wex 1781   ∈ wcel 2106   ≠ wne 2943  ∀wral 3064  ∃wrex 3073  Vcvv 3445   ∖ cdif 3907   ∪ cun 3908   ∩ cin 3909   ⊆ wss 3910  ∅c0 4282  𝒫 cpw 4560  {csn 4586  ∪ cuni 4865  ∩ cint 4907  ∪ ciun 4954  ∩ ciin 4955   ↦ cmpt 5188  ^◡ccnv 5632  ran crn 5634   ↾ cres 5635   “ cima 5636  Fun wfun 6490   Fn wfn 6491  –onto→wfo 6494  –1-1-onto→wf1o 6495  ‘cfv 6496  Fincfn 8883  ficfi 9346  Topctop 22242  Clsdccld 22367  Compccmp 22737

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  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 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-iin 4957  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-om 7803  df-1o 8412  df-en 8884  df-fin 8887  df-fi 9347  df-top 22243  df-cld 22370  df-cmp 22738

This theorem is referenced by:  cmpfii  22760  fclscmp  23381  zarcmplem  32462  heibor1lem  36268