Theorem cmpfi 23441

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 4556	. . . 4 ⊢ (𝑦 ∈ 𝒫 𝐽 → 𝑦 ⊆ 𝐽)
2		0ss 4348	. . . . . . . . . . 11 ⊢ ∅ ⊆ 𝑦
3		0fi 9012	. . . . . . . . . . 11 ⊢ ∅ ∈ Fin
4		elfpw 9287	. . . . . . . . . . 11 ⊢ (∅ ∈ (𝒫 𝑦 ∩ Fin) ↔ (∅ ⊆ 𝑦 ∧ ∅ ∈ Fin))
5	2, 3, 4	mpbir2an 719	. . . . . . . . . 10 ⊢ ∅ ∈ (𝒫 𝑦 ∩ Fin)
6		simprr 780	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 = ∅ ∧ ∪ 𝐽 = ∪ 𝑦)) → ∪ 𝐽 = ∪ 𝑦)
7		simprl 778	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 = ∅ ∧ ∪ 𝐽 = ∪ 𝑦)) → 𝑦 = ∅)
8	7	unieqd 4872	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 = ∅ ∧ ∪ 𝐽 = ∪ 𝑦)) → ∪ 𝑦 = ∪ ∅)
9	6, 8	eqtrd 2791	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 = ∅ ∧ ∪ 𝐽 = ∪ 𝑦)) → ∪ 𝐽 = ∪ ∅)
10		unieq 4870	. . . . . . . . . . 11 ⊢ (𝑧 = ∅ → ∪ 𝑧 = ∪ ∅)
11	10	rspceeqv 3599	. . . . . . . . . 10 ⊢ ((∅ ∈ (𝒫 𝑦 ∩ Fin) ∧ ∪ 𝐽 = ∪ ∅) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧)
12	5, 9, 11	sylancr 595	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 = ∅ ∧ ∪ 𝐽 = ∪ 𝑦)) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧)
13	12	expr 459	. . . . . . . 8 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 = ∅) → (∪ 𝐽 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧))
14		vn0 4292	. . . . . . . . . 10 ⊢ V ≠ ∅
15		iineq1 4961	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ∅ → ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∩ 𝑟 ∈ ∅ (∪ 𝐽 ∖ 𝑟))
16	15	adantl 484	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 = ∅) → ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∩ 𝑟 ∈ ∅ (∪ 𝐽 ∖ 𝑟))
17		0iin 5015	. . . . . . . . . . . . 13 ⊢ ∩ 𝑟 ∈ ∅ (∪ 𝐽 ∖ 𝑟) = V
18	16, 17	eqtrdi 2807	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 = ∅) → ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = V)
19	18	eqeq1d 2758	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 = ∅) → (∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅ ↔ V = ∅))
20	19	necon3bbid 2988	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 = ∅) → (¬ ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅ ↔ V ≠ ∅))
21	14, 20	mpbiri 260	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 = ∅) → ¬ ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅)
22	21	pm2.21d 121	. . . . . . . 8 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 = ∅) → (∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅ → ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))))
23	13, 22	2thd 267	. . . . . . 7 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 = ∅) → ((∪ 𝐽 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧) ↔ (∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅ → ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))))
24		uniss 4867	. . . . . . . . . . . 12 ⊢ (𝑦 ⊆ 𝐽 → ∪ 𝑦 ⊆ ∪ 𝐽)
25	24	ad2antlr 735	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → ∪ 𝑦 ⊆ ∪ 𝐽)
26		eqss 3946	. . . . . . . . . . . 12 ⊢ (∪ 𝑦 = ∪ 𝐽 ↔ (∪ 𝑦 ⊆ ∪ 𝐽 ∧ ∪ 𝐽 ⊆ ∪ 𝑦))
27	26	baib 542	. . . . . . . . . . 11 ⊢ (∪ 𝑦 ⊆ ∪ 𝐽 → (∪ 𝑦 = ∪ 𝐽 ↔ ∪ 𝐽 ⊆ ∪ 𝑦))
28	25, 27	syl 17	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∪ 𝑦 = ∪ 𝐽 ↔ ∪ 𝐽 ⊆ ∪ 𝑦))
29		eqcom 2763	. . . . . . . . . 10 ⊢ (∪ 𝑦 = ∪ 𝐽 ↔ ∪ 𝐽 = ∪ 𝑦)
30		ssdif0 4313	. . . . . . . . . 10 ⊢ (∪ 𝐽 ⊆ ∪ 𝑦 ↔ (∪ 𝐽 ∖ ∪ 𝑦) = ∅)
31	28, 29, 30	3bitr3g 315	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∪ 𝐽 = ∪ 𝑦 ↔ (∪ 𝐽 ∖ ∪ 𝑦) = ∅))
32		iindif2 5028	. . . . . . . . . . . 12 ⊢ (𝑦 ≠ ∅ → ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = (∪ 𝐽 ∖ ∪ 𝑟 ∈ 𝑦 𝑟))
33	32	adantl 484	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = (∪ 𝐽 ∖ ∪ 𝑟 ∈ 𝑦 𝑟))
34		uniiun 5010	. . . . . . . . . . . 12 ⊢ ∪ 𝑦 = ∪ 𝑟 ∈ 𝑦 𝑟
35	34	difeq2i 4072	. . . . . . . . . . 11 ⊢ (∪ 𝐽 ∖ ∪ 𝑦) = (∪ 𝐽 ∖ ∪ 𝑟 ∈ 𝑦 𝑟)
36	33, 35	eqtr4di 2809	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = (∪ 𝐽 ∖ ∪ 𝑦))
37	36	eqeq1d 2758	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅ ↔ (∪ 𝐽 ∖ ∪ 𝑦) = ∅))
38	31, 37	bitr4d 284	. . . . . . . 8 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∪ 𝐽 = ∪ 𝑦 ↔ ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅))
39		imassrn 6050	. . . . . . . . . . . 12 ⊢ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ⊆ ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟))
40		df-ima 5653	. . . . . . . . . . . . . 14 ⊢ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) = ran ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) ↾ 𝑦)
41		resmpt 6016	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ⊆ 𝐽 → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) ↾ 𝑦) = (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
42	41	adantl 484	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) ↾ 𝑦) = (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
43	42	rneqd 5907	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ran ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) ↾ 𝑦) = ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
44	40, 43	eqtrid 2803	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) = ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
45	44	ad2antrr 734	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ (𝒫 𝑦 ∩ Fin)) → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) = ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
46	39, 45	sseqtrrid 3974	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ (𝒫 𝑦 ∩ Fin)) → ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ⊆ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))
47		funmpt 6548	. . . . . . . . . . . 12 ⊢ Fun (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟))
48		elinel2 4149	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (𝒫 𝑦 ∩ Fin) → 𝑧 ∈ Fin)
49	48	adantl 484	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ (𝒫 𝑦 ∩ Fin)) → 𝑧 ∈ Fin)
50		imafi 9248	. . . . . . . . . . . 12 ⊢ ((Fun (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) ∧ 𝑧 ∈ Fin) → ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ∈ Fin)
51	47, 49, 50	sylancr 595	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ (𝒫 𝑦 ∩ Fin)) → ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ∈ Fin)
52		elfpw 9287	. . . . . . . . . . 11 ⊢ (((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin) ↔ (((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ⊆ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∧ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ∈ Fin))
53	46, 51, 52	sylanbrc 591	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ (𝒫 𝑦 ∩ Fin)) → ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin))
54		eqid 2756	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝐽 = ∪ 𝐽
55	54	topopn 22939	. . . . . . . . . . . . . . . 16 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽)
56	55	difexd 5281	. . . . . . . . . . . . . . 15 ⊢ (𝐽 ∈ Top → (∪ 𝐽 ∖ 𝑟) ∈ V)
57	56	ralrimivw 3152	. . . . . . . . . . . . . 14 ⊢ (𝐽 ∈ Top → ∀𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) ∈ V)
58		eqid 2756	. . . . . . . . . . . . . . 15 ⊢ (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) = (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟))
59	58	fnmpt 6650	. . . . . . . . . . . . . 14 ⊢ (∀𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) ∈ V → (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) Fn 𝑦)
60	57, 59	syl 17	. . . . . . . . . . . . 13 ⊢ (𝐽 ∈ Top → (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) Fn 𝑦)
61	60	ad3antrrr 738	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)) → (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) Fn 𝑦)
62		elfpw 9287	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin) ↔ (𝑤 ⊆ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∧ 𝑤 ∈ Fin))
63	62	bilani 507	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)) → (𝑤 ⊆ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∧ 𝑤 ∈ Fin))
64	63	simpld 497	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)) → 𝑤 ⊆ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))
65	44	ad2antrr 734	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)) → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) = ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
66	64, 65	sseqtrd 3967	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)) → 𝑤 ⊆ ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
67	63	simprd 498	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)) → 𝑤 ∈ Fin)
68		fipreima 9291	. . . . . . . . . . . 12 ⊢ (((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) Fn 𝑦 ∧ 𝑤 ⊆ ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) ∧ 𝑤 ∈ Fin) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = 𝑤)
69	61, 66, 67, 68	syl3anc 1386	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = 𝑤)
70		eqcom 2763	. . . . . . . . . . . 12 ⊢ (((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = 𝑤 ↔ 𝑤 = ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧))
71	70	rexbii 3103	. . . . . . . . . . 11 ⊢ (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = 𝑤 ↔ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑤 = ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧))
72	69, 71	sylib 220	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑤 = ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧))
73		simpr 487	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 = ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)) → 𝑤 = ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧))
74	73	inteqd 4904	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 = ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)) → ∩ 𝑤 = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧))
75	74	eqeq2d 2767	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 = ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)) → (∅ = ∩ 𝑤 ↔ ∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)))
76	53, 72, 75	rexxfrd 5360	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∃𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)∅ = ∩ 𝑤 ↔ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)))
77		0ex 5251	. . . . . . . . . 10 ⊢ ∅ ∈ V
78		imassrn 6050	. . . . . . . . . . . . 13 ⊢ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ⊆ ran (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟))
79		eqid 2756	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) = (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟))
80	54, 79	opncldf1 23117	. . . . . . . . . . . . . . . 16 ⊢ (𝐽 ∈ Top → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)):𝐽–1-1-onto→(Clsd‘𝐽) ∧ ◡(𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) = (𝑣 ∈ (Clsd‘𝐽) ↦ (∪ 𝐽 ∖ 𝑣))))
81	80	simpld 497	. . . . . . . . . . . . . . 15 ⊢ (𝐽 ∈ Top → (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)):𝐽–1-1-onto→(Clsd‘𝐽))
82		f1ofo 6803	. . . . . . . . . . . . . . 15 ⊢ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)):𝐽–1-1-onto→(Clsd‘𝐽) → (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)):𝐽–onto→(Clsd‘𝐽))
83	81, 82	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝐽 ∈ Top → (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)):𝐽–onto→(Clsd‘𝐽))
84		forn 6770	. . . . . . . . . . . . . 14 ⊢ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)):𝐽–onto→(Clsd‘𝐽) → ran (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) = (Clsd‘𝐽))
85	83, 84	syl 17	. . . . . . . . . . . . 13 ⊢ (𝐽 ∈ Top → ran (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) = (Clsd‘𝐽))
86	78, 85	sseqtrid 3973	. . . . . . . . . . . 12 ⊢ (𝐽 ∈ Top → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ⊆ (Clsd‘𝐽))
87		fvex 6869	. . . . . . . . . . . . 13 ⊢ (Clsd‘𝐽) ∈ V
88	87	elpw2 5284	. . . . . . . . . . . 12 ⊢ (((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∈ 𝒫 (Clsd‘𝐽) ↔ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ⊆ (Clsd‘𝐽))
89	86, 88	sylibr 236	. . . . . . . . . . 11 ⊢ (𝐽 ∈ Top → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∈ 𝒫 (Clsd‘𝐽))
90	89	ad2antrr 734	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∈ 𝒫 (Clsd‘𝐽))
91		elfi 9349	. . . . . . . . . 10 ⊢ ((∅ ∈ V ∧ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∈ 𝒫 (Clsd‘𝐽)) → (∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) ↔ ∃𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)∅ = ∩ 𝑤))
92	77, 90, 91	sylancr 595	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) ↔ ∃𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)∅ = ∩ 𝑤))
93		inundif 4427	. . . . . . . . . . . . . 14 ⊢ (((𝒫 𝑦 ∩ Fin) ∩ {∅}) ∪ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) = (𝒫 𝑦 ∩ Fin)
94	93	rexeqi 3313	. . . . . . . . . . . . 13 ⊢ (∃𝑧 ∈ (((𝒫 𝑦 ∩ Fin) ∩ {∅}) ∪ ((𝒫 𝑦 ∩ Fin) ∖ {∅}))∪ 𝐽 = ∪ 𝑧 ↔ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧)
95		rexun 4143	. . . . . . . . . . . . 13 ⊢ (∃𝑧 ∈ (((𝒫 𝑦 ∩ Fin) ∩ {∅}) ∪ ((𝒫 𝑦 ∩ Fin) ∖ {∅}))∪ 𝐽 = ∪ 𝑧 ↔ (∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅})∪ 𝐽 = ∪ 𝑧 ∨ ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧))
96	94, 95	bitr3i 279	. . . . . . . . . . . 12 ⊢ (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧 ↔ (∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅})∪ 𝐽 = ∪ 𝑧 ∨ ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧))
97		elinel2 4149	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅}) → 𝑧 ∈ {∅})
98		elsni 4593	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ {∅} → 𝑧 = ∅)
99	97, 98	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅}) → 𝑧 = ∅)
100	99	unieqd 4872	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅}) → ∪ 𝑧 = ∪ ∅)
101		uni0 4888	. . . . . . . . . . . . . . . . . . 19 ⊢ ∪ ∅ = ∅
102	100, 101	eqtrdi 2807	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅}) → ∪ 𝑧 = ∅)
103	102	eqeq2d 2767	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅}) → (∪ 𝐽 = ∪ 𝑧 ↔ ∪ 𝐽 = ∅))
104	103	biimpd 231	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅}) → (∪ 𝐽 = ∪ 𝑧 → ∪ 𝐽 = ∅))
105	104	rexlimiv 3150	. . . . . . . . . . . . . . 15 ⊢ (∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅})∪ 𝐽 = ∪ 𝑧 → ∪ 𝐽 = ∅)
106		ssidd 3954	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → 𝑦 ⊆ 𝑦)
107		simprr 780	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → ∪ 𝐽 = ∅)
108		0ss 4348	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ∅ ⊆ ∪ 𝑦
109	107, 108	eqsstrdi 3975	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → ∪ 𝐽 ⊆ ∪ 𝑦)
110	24	ad2antlr 735	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → ∪ 𝑦 ⊆ ∪ 𝐽)
111	109, 110	eqssd 3948	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → ∪ 𝐽 = ∪ 𝑦)
112	111, 107	eqtr3d 2793	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → ∪ 𝑦 = ∅)
113	112, 3	eqeltrdi 2864	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → ∪ 𝑦 ∈ Fin)
114		pwfi 9252	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∪ 𝑦 ∈ Fin ↔ 𝒫 ∪ 𝑦 ∈ Fin)
115	113, 114	sylib 220	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → 𝒫 ∪ 𝑦 ∈ Fin)
116		pwuni 4898	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑦 ⊆ 𝒫 ∪ 𝑦
117		ssfi 9130	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝒫 ∪ 𝑦 ∈ Fin ∧ 𝑦 ⊆ 𝒫 ∪ 𝑦) → 𝑦 ∈ Fin)
118	115, 116, 117	sylancl 594	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → 𝑦 ∈ Fin)
119		elfpw 9287	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ (𝒫 𝑦 ∩ Fin) ↔ (𝑦 ⊆ 𝑦 ∧ 𝑦 ∈ Fin))
120	106, 118, 119	sylanbrc 591	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → 𝑦 ∈ (𝒫 𝑦 ∩ Fin))
121		simprl 778	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → 𝑦 ≠ ∅)
122		eldifsn 4740	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅}) ↔ (𝑦 ∈ (𝒫 𝑦 ∩ Fin) ∧ 𝑦 ≠ ∅))
123	120, 121, 122	sylanbrc 591	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → 𝑦 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅}))
124		unieq 4870	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑦 → ∪ 𝑧 = ∪ 𝑦)
125	124	rspceeqv 3599	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅}) ∧ ∪ 𝐽 = ∪ 𝑦) → ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧)
126	123, 111, 125	syl2anc 592	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧)
127	126	expr 459	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∪ 𝐽 = ∅ → ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧))
128	105, 127	syl5 34	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅})∪ 𝐽 = ∪ 𝑧 → ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧))
129		idd 24	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧 → ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧))
130	128, 129	jaod 868	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → ((∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅})∪ 𝐽 = ∪ 𝑧 ∨ ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧) → ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧))
131		olc 877	. . . . . . . . . . . . 13 ⊢ (∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧 → (∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅})∪ 𝐽 = ∪ 𝑧 ∨ ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧))
132	130, 131	impbid1 227	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → ((∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅})∪ 𝐽 = ∪ 𝑧 ∨ ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧) ↔ ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧))
133	96, 132	bitrid 285	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧 ↔ ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧))
134		eldifi 4079	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅}) → 𝑧 ∈ (𝒫 𝑦 ∩ Fin))
135	134	adantl 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → 𝑧 ∈ (𝒫 𝑦 ∩ Fin))
136		elfpw 9287	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ (𝒫 𝑦 ∩ Fin) ↔ (𝑧 ⊆ 𝑦 ∧ 𝑧 ∈ Fin))
137	135, 136	sylib 220	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → (𝑧 ⊆ 𝑦 ∧ 𝑧 ∈ Fin))
138	137	simpld 497	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → 𝑧 ⊆ 𝑦)
139		simpllr 783	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → 𝑦 ⊆ 𝐽)
140	138, 139	sstrd 3941	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → 𝑧 ⊆ 𝐽)
141	140	unissd 4869	. . . . . . . . . . . . . . 15 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ∪ 𝑧 ⊆ ∪ 𝐽)
142		eqss 3946	. . . . . . . . . . . . . . . 16 ⊢ (∪ 𝑧 = ∪ 𝐽 ↔ (∪ 𝑧 ⊆ ∪ 𝐽 ∧ ∪ 𝐽 ⊆ ∪ 𝑧))
143	142	baib 542	. . . . . . . . . . . . . . 15 ⊢ (∪ 𝑧 ⊆ ∪ 𝐽 → (∪ 𝑧 = ∪ 𝐽 ↔ ∪ 𝐽 ⊆ ∪ 𝑧))
144	141, 143	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → (∪ 𝑧 = ∪ 𝐽 ↔ ∪ 𝐽 ⊆ ∪ 𝑧))
145		eqcom 2763	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑧 = ∪ 𝐽 ↔ ∪ 𝐽 = ∪ 𝑧)
146		ssdif0 4313	. . . . . . . . . . . . . . 15 ⊢ (∪ 𝐽 ⊆ ∪ 𝑧 ↔ (∪ 𝐽 ∖ ∪ 𝑧) = ∅)
147		eqcom 2763	. . . . . . . . . . . . . . 15 ⊢ ((∪ 𝐽 ∖ ∪ 𝑧) = ∅ ↔ ∅ = (∪ 𝐽 ∖ ∪ 𝑧))
148	146, 147	bitri 277	. . . . . . . . . . . . . 14 ⊢ (∪ 𝐽 ⊆ ∪ 𝑧 ↔ ∅ = (∪ 𝐽 ∖ ∪ 𝑧))
149	144, 145, 148	3bitr3g 315	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → (∪ 𝐽 = ∪ 𝑧 ↔ ∅ = (∪ 𝐽 ∖ ∪ 𝑧)))
150		df-ima 5653	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = ran ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) ↾ 𝑧)
151	138	resmptd 6019	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) ↾ 𝑧) = (𝑟 ∈ 𝑧 ↦ (∪ 𝐽 ∖ 𝑟)))
152	151	rneqd 5907	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ran ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) ↾ 𝑧) = ran (𝑟 ∈ 𝑧 ↦ (∪ 𝐽 ∖ 𝑟)))
153	150, 152	eqtrid 2803	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = ran (𝑟 ∈ 𝑧 ↦ (∪ 𝐽 ∖ 𝑟)))
154	153	inteqd 4904	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = ∩ ran (𝑟 ∈ 𝑧 ↦ (∪ 𝐽 ∖ 𝑟)))
155	56	ralrimivw 3152	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐽 ∈ Top → ∀𝑟 ∈ 𝑧 (∪ 𝐽 ∖ 𝑟) ∈ V)
156	155	ad3antrrr 738	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ∀𝑟 ∈ 𝑧 (∪ 𝐽 ∖ 𝑟) ∈ V)
157		dfiin3g 5938	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑟 ∈ 𝑧 (∪ 𝐽 ∖ 𝑟) ∈ V → ∩ 𝑟 ∈ 𝑧 (∪ 𝐽 ∖ 𝑟) = ∩ ran (𝑟 ∈ 𝑧 ↦ (∪ 𝐽 ∖ 𝑟)))
158	156, 157	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ∩ 𝑟 ∈ 𝑧 (∪ 𝐽 ∖ 𝑟) = ∩ ran (𝑟 ∈ 𝑧 ↦ (∪ 𝐽 ∖ 𝑟)))
159		eldifsni 4744	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅}) → 𝑧 ≠ ∅)
160	159	adantl 484	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → 𝑧 ≠ ∅)
161		iindif2 5028	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ≠ ∅ → ∩ 𝑟 ∈ 𝑧 (∪ 𝐽 ∖ 𝑟) = (∪ 𝐽 ∖ ∪ 𝑟 ∈ 𝑧 𝑟))
162	160, 161	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ∩ 𝑟 ∈ 𝑧 (∪ 𝐽 ∖ 𝑟) = (∪ 𝐽 ∖ ∪ 𝑟 ∈ 𝑧 𝑟))
163	154, 158, 162	3eqtr2d 2797	. . . . . . . . . . . . . . 15 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = (∪ 𝐽 ∖ ∪ 𝑟 ∈ 𝑧 𝑟))
164		uniiun 5010	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑧 = ∪ 𝑟 ∈ 𝑧 𝑟
165	164	difeq2i 4072	. . . . . . . . . . . . . . 15 ⊢ (∪ 𝐽 ∖ ∪ 𝑧) = (∪ 𝐽 ∖ ∪ 𝑟 ∈ 𝑧 𝑟)
166	163, 165	eqtr4di 2809	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = (∪ 𝐽 ∖ ∪ 𝑧))
167	166	eqeq2d 2767	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → (∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ↔ ∅ = (∪ 𝐽 ∖ ∪ 𝑧)))
168	149, 167	bitr4d 284	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → (∪ 𝐽 = ∪ 𝑧 ↔ ∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)))
169	168	rexbidva 3178	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧 ↔ ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)))
170	133, 169	bitrd 281	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧 ↔ ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)))
171		imaeq2 6035	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = ∅ → ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ ∅))
172		ima0 6056	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ ∅) = ∅
173	171, 172	eqtrdi 2807	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = ∅ → ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = ∅)
174	173	inteqd 4904	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = ∅ → ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = ∩ ∅)
175		int0 4914	. . . . . . . . . . . . . . . . . 18 ⊢ ∩ ∅ = V
176	174, 175	eqtrdi 2807	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ∅ → ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = V)
177	176	neeq1d 3010	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = ∅ → (∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ≠ ∅ ↔ V ≠ ∅))
178	14, 177	mpbiri 260	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = ∅ → ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ≠ ∅)
179	178	necomd 3006	. . . . . . . . . . . . . 14 ⊢ (𝑧 = ∅ → ∅ ≠ ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧))
180	179	necon2i 2985	. . . . . . . . . . . . 13 ⊢ (∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) → 𝑧 ≠ ∅)
181		eldifsn 4740	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅}) ↔ (𝑧 ∈ (𝒫 𝑦 ∩ Fin) ∧ 𝑧 ≠ ∅))
182	181	rbaibr 544	. . . . . . . . . . . . 13 ⊢ (𝑧 ≠ ∅ → (𝑧 ∈ (𝒫 𝑦 ∩ Fin) ↔ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})))
183	180, 182	syl 17	. . . . . . . . . . . 12 ⊢ (∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) → (𝑧 ∈ (𝒫 𝑦 ∩ Fin) ↔ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})))
184	183	pm5.32ri 582	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ (𝒫 𝑦 ∩ Fin) ∧ ∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)) ↔ (𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅}) ∧ ∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)))
185	184	rexbii2 3099	. . . . . . . . . 10 ⊢ (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ↔ ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧))
186	170, 185	bitr4di 291	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧 ↔ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)))
187	76, 92, 186	3bitr4rd 314	. . . . . . . 8 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧 ↔ ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))))
188	38, 187	imbi12d 346	. . . . . . 7 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → ((∪ 𝐽 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧) ↔ (∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅ → ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))))
189	23, 188	pm2.61dane 3038	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ((∪ 𝐽 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧) ↔ (∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅ → ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))))
190	57	adantr 483	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ∀𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) ∈ V)
191		dfiin3g 5938	. . . . . . . . . . 11 ⊢ (∀𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) ∈ V → ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∩ ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
192	190, 191	syl 17	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∩ ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
193	44	inteqd 4904	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) = ∩ ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
194	192, 193	eqtr4d 2794	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))
195	194	eqeq1d 2758	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → (∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅ ↔ ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) = ∅))
196		nne 2955	. . . . . . . 8 ⊢ (¬ ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅ ↔ ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) = ∅)
197	195, 196	bitr4di 291	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → (∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅ ↔ ¬ ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅))
198	197	imbi1d 343	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ((∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅ → ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))) ↔ (¬ ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅ → ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))))
199	189, 198	bitrd 281	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ((∪ 𝐽 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧) ↔ (¬ ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅ → ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))))
200		con1b 360	. . . . 5 ⊢ ((¬ ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅ → ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))) ↔ (¬ ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅))
201	199, 200	bitrdi 289	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ((∪ 𝐽 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧) ↔ (¬ ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅)))
202	1, 201	sylan2 601	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ∈ 𝒫 𝐽) → ((∪ 𝐽 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧) ↔ (¬ ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅)))
203	202	ralbidva 3177	. 2 ⊢ (𝐽 ∈ Top → (∀𝑦 ∈ 𝒫 𝐽(∪ 𝐽 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧) ↔ ∀𝑦 ∈ 𝒫 𝐽(¬ ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅)))
204	54	iscmp 23421	. . 3 ⊢ (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝐽(∪ 𝐽 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧)))
205	204	baib 542	. 2 ⊢ (𝐽 ∈ Top → (𝐽 ∈ Comp ↔ ∀𝑦 ∈ 𝒫 𝐽(∪ 𝐽 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧)))
206	89	adantr 483	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ∈ 𝒫 𝐽) → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∈ 𝒫 (Clsd‘𝐽))
207		simpl 485	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) → 𝐽 ∈ Top)
208		funmpt 6548	. . . . . 6 ⊢ Fun (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟))
209	208	a1i 11	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) → Fun (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)))
210		elpwi 4556	. . . . . . 7 ⊢ (𝑥 ∈ 𝒫 (Clsd‘𝐽) → 𝑥 ⊆ (Clsd‘𝐽))
211		foima 6772	. . . . . . . . 9 ⊢ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)):𝐽–onto→(Clsd‘𝐽) → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝐽) = (Clsd‘𝐽))
212	83, 211	syl 17	. . . . . . . 8 ⊢ (𝐽 ∈ Top → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝐽) = (Clsd‘𝐽))
213	212	sseq2d 3963	. . . . . . 7 ⊢ (𝐽 ∈ Top → (𝑥 ⊆ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝐽) ↔ 𝑥 ⊆ (Clsd‘𝐽)))
214	210, 213	imbitrrid 248	. . . . . 6 ⊢ (𝐽 ∈ Top → (𝑥 ∈ 𝒫 (Clsd‘𝐽) → 𝑥 ⊆ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝐽)))
215	214	imp 409	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) → 𝑥 ⊆ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝐽))
216		ssimaexg 6942	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ Fun (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) ∧ 𝑥 ⊆ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝐽)) → ∃𝑦(𝑦 ⊆ 𝐽 ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))
217	207, 209, 215, 216	syl3anc 1386	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) → ∃𝑦(𝑦 ⊆ 𝐽 ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))
218		df-rex 3081	. . . . 5 ⊢ (∃𝑦 ∈ 𝒫 𝐽𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ↔ ∃𝑦(𝑦 ∈ 𝒫 𝐽 ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))
219		velpw 4554	. . . . . . 7 ⊢ (𝑦 ∈ 𝒫 𝐽 ↔ 𝑦 ⊆ 𝐽)
220	219	anbi1i 632	. . . . . 6 ⊢ ((𝑦 ∈ 𝒫 𝐽 ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) ↔ (𝑦 ⊆ 𝐽 ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))
221	220	exbii 1862	. . . . 5 ⊢ (∃𝑦(𝑦 ∈ 𝒫 𝐽 ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) ↔ ∃𝑦(𝑦 ⊆ 𝐽 ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))
222	218, 221	bitri 277	. . . 4 ⊢ (∃𝑦 ∈ 𝒫 𝐽𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ↔ ∃𝑦(𝑦 ⊆ 𝐽 ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))
223	217, 222	sylibr 236	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) → ∃𝑦 ∈ 𝒫 𝐽𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))
224		simpr 487	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))
225	224	fveq2d 6860	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → (fi‘𝑥) = (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))
226	225	eleq2d 2842	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → (∅ ∈ (fi‘𝑥) ↔ ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))))
227	226	notbid 320	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → (¬ ∅ ∈ (fi‘𝑥) ↔ ¬ ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))))
228	224	inteqd 4904	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → ∩ 𝑥 = ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))
229	228	neeq1d 3010	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → (∩ 𝑥 ≠ ∅ ↔ ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅))
230	227, 229	imbi12d 346	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → ((¬ ∅ ∈ (fi‘𝑥) → ∩ 𝑥 ≠ ∅) ↔ (¬ ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅)))
231	206, 223, 230	ralxfrd 5359	. 2 ⊢ (𝐽 ∈ Top → (∀𝑥 ∈ 𝒫 (Clsd‘𝐽)(¬ ∅ ∈ (fi‘𝑥) → ∩ 𝑥 ≠ ∅) ↔ ∀𝑦 ∈ 𝒫 𝐽(¬ ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅)))
232	203, 205, 231	3bitr4d 313	1 ⊢ (𝐽 ∈ Top → (𝐽 ∈ Comp ↔ ∀𝑥 ∈ 𝒫 (Clsd‘𝐽)(¬ ∅ ∈ (fi‘𝑥) → ∩ 𝑥 ≠ ∅)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∨ wo 856   = wceq 1554  ∃wex 1793   ∈ wcel 2136   ≠ wne 2951  ∀wral 3070  ∃wrex 3080  Vcvv 3448   ∖ cdif 3896   ∪ cun 3897   ∩ cin 3898   ⊆ wss 3899  ∅c0 4280  𝒫 cpw 4549  {csn 4576  ∪ cuni 4859  ∩ cint 4899  ∪ ciun 4943  ∩ ciin 4944   ↦ cmpt 5175  ^◡ccnv 5639  ran crn 5641   ↾ cres 5642   “ cima 5643  Fun wfun 6504   Fn wfn 6505  –onto→wfo 6508  –1-1-onto→wf1o 6509  ‘cfv 6510  Fincfn 8916  ficfi 9346  Topctop 22926  Clsdccld 23049  Compccmp 23419

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-10 2169  ax-11 2185  ax-12 2206  ax-ext 2728  ax-sep 5240  ax-nul 5250  ax-pow 5316  ax-pr 5384  ax-un 7707

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3or 1096  df-3an 1097  df-tru 1557  df-fal 1567  df-ex 1794  df-nf 1798  df-sb 2085  df-mo 2560  df-eu 2590  df-clab 2735  df-cleq 2748  df-clel 2831  df-nfc 2905  df-ne 2952  df-ral 3071  df-rex 3081  df-reu 3362  df-rab 3409  df-v 3450  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4281  df-if 4475  df-pw 4551  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-int 4900  df-iun 4945  df-iin 4946  df-br 5095  df-opab 5157  df-mpt 5176  df-tr 5202  df-id 5535  df-eprel 5540  df-po 5548  df-so 5549  df-fr 5593  df-we 5595  df-xp 5646  df-rel 5647  df-cnv 5648  df-co 5649  df-dm 5650  df-rn 5651  df-res 5652  df-ima 5653  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6466  df-fun 6512  df-fn 6513  df-f 6514  df-f1 6515  df-fo 6516  df-f1o 6517  df-fv 6518  df-om 7836  df-1o 8425  df-en 8917  df-dom 8918  df-fin 8920  df-fi 9347  df-top 22927  df-cld 23052  df-cmp 23420

This theorem is referenced by:  cmpfii  23442  fclscmp  24063  zarcmplem  34132  heibor1lem  38256