Theorem cmpfi 23544

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 4568	. . . 4 ⊢ (𝑦 ∈ 𝒫 𝐽 → 𝑦 ⊆ 𝐽)
2		0ss 4356	. . . . . . . . . . 11 ⊢ ∅ ⊆ 𝑦
3		0fi 9038	. . . . . . . . . . 11 ⊢ ∅ ∈ Fin
4		elfpw 9310	. . . . . . . . . . 11 ⊢ (∅ ∈ (𝒫 𝑦 ∩ Fin) ↔ (∅ ⊆ 𝑦 ∧ ∅ ∈ Fin))
5	2, 3, 4	mpbir2an 723	. . . . . . . . . 10 ⊢ ∅ ∈ (𝒫 𝑦 ∩ Fin)
6		simprr 784	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 = ∅ ∧ ∪ 𝐽 = ∪ 𝑦)) → ∪ 𝐽 = ∪ 𝑦)
7		simprl 782	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 = ∅ ∧ ∪ 𝐽 = ∪ 𝑦)) → 𝑦 = ∅)
8	7	unieqd 4884	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 = ∅ ∧ ∪ 𝐽 = ∪ 𝑦)) → ∪ 𝑦 = ∪ ∅)
9	6, 8	eqtrd 2796	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 = ∅ ∧ ∪ 𝐽 = ∪ 𝑦)) → ∪ 𝐽 = ∪ ∅)
10		unieq 4882	. . . . . . . . . . 11 ⊢ (𝑧 = ∅ → ∪ 𝑧 = ∪ ∅)
11	10	rspceeqv 3603	. . . . . . . . . 10 ⊢ ((∅ ∈ (𝒫 𝑦 ∩ Fin) ∧ ∪ 𝐽 = ∪ ∅) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧)
12	5, 9, 11	sylancr 598	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 = ∅ ∧ ∪ 𝐽 = ∪ 𝑦)) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧)
13	12	expr 461	. . . . . . . 8 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 = ∅) → (∪ 𝐽 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧))
14		vn0 4297	. . . . . . . . . 10 ⊢ V ≠ ∅
15		iineq1 4973	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ∅ → ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∩ 𝑟 ∈ ∅ (∪ 𝐽 ∖ 𝑟))
16	15	adantl 486	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 = ∅) → ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∩ 𝑟 ∈ ∅ (∪ 𝐽 ∖ 𝑟))
17		0iin 5027	. . . . . . . . . . . . 13 ⊢ ∩ 𝑟 ∈ ∅ (∪ 𝐽 ∖ 𝑟) = V
18	16, 17	eqtrdi 2812	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 = ∅) → ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = V)
19	18	eqeq1d 2763	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 = ∅) → (∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅ ↔ V = ∅))
20	19	necon3bbid 2993	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 = ∅) → (¬ ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅ ↔ V ≠ ∅))
21	14, 20	mpbiri 261	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 = ∅) → ¬ ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅)
22	21	pm2.21d 122	. . . . . . . 8 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 = ∅) → (∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅ → ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))))
23	13, 22	2thd 268	. . . . . . 7 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 = ∅) → ((∪ 𝐽 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧) ↔ (∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅ → ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))))
24		uniss 4879	. . . . . . . . . . . 12 ⊢ (𝑦 ⊆ 𝐽 → ∪ 𝑦 ⊆ ∪ 𝐽)
25	24	ad2antlr 739	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → ∪ 𝑦 ⊆ ∪ 𝐽)
26		eqss 3951	. . . . . . . . . . . 12 ⊢ (∪ 𝑦 = ∪ 𝐽 ↔ (∪ 𝑦 ⊆ ∪ 𝐽 ∧ ∪ 𝐽 ⊆ ∪ 𝑦))
27	26	baib 544	. . . . . . . . . . 11 ⊢ (∪ 𝑦 ⊆ ∪ 𝐽 → (∪ 𝑦 = ∪ 𝐽 ↔ ∪ 𝐽 ⊆ ∪ 𝑦))
28	25, 27	syl 18	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∪ 𝑦 = ∪ 𝐽 ↔ ∪ 𝐽 ⊆ ∪ 𝑦))
29		eqcom 2768	. . . . . . . . . 10 ⊢ (∪ 𝑦 = ∪ 𝐽 ↔ ∪ 𝐽 = ∪ 𝑦)
30		ssdif0 4320	. . . . . . . . . 10 ⊢ (∪ 𝐽 ⊆ ∪ 𝑦 ↔ (∪ 𝐽 ∖ ∪ 𝑦) = ∅)
31	28, 29, 30	3bitr3g 316	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∪ 𝐽 = ∪ 𝑦 ↔ (∪ 𝐽 ∖ ∪ 𝑦) = ∅))
32		iindif2 5042	. . . . . . . . . . . 12 ⊢ (𝑦 ≠ ∅ → ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = (∪ 𝐽 ∖ ∪ 𝑟 ∈ 𝑦 𝑟))
33	32	adantl 486	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = (∪ 𝐽 ∖ ∪ 𝑟 ∈ 𝑦 𝑟))
34		uniiun 5022	. . . . . . . . . . . 12 ⊢ ∪ 𝑦 = ∪ 𝑟 ∈ 𝑦 𝑟
35	34	difeq2i 4077	. . . . . . . . . . 11 ⊢ (∪ 𝐽 ∖ ∪ 𝑦) = (∪ 𝐽 ∖ ∪ 𝑟 ∈ 𝑦 𝑟)
36	33, 35	eqtr4di 2814	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = (∪ 𝐽 ∖ ∪ 𝑦))
37	36	eqeq1d 2763	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅ ↔ (∪ 𝐽 ∖ ∪ 𝑦) = ∅))
38	31, 37	bitr4d 285	. . . . . . . 8 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∪ 𝐽 = ∪ 𝑦 ↔ ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅))
39		imassrn 6073	. . . . . . . . . . . 12 ⊢ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ⊆ ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟))
40		df-ima 5674	. . . . . . . . . . . . . 14 ⊢ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) = ran ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) ↾ 𝑦)
41		resmpt 6039	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ⊆ 𝐽 → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) ↾ 𝑦) = (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
42	41	adantl 486	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) ↾ 𝑦) = (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
43	42	rneqd 5928	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ran ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) ↾ 𝑦) = ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
44	40, 43	eqtrid 2808	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) = ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
45	44	ad2antrr 738	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ (𝒫 𝑦 ∩ Fin)) → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) = ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
46	39, 45	sseqtrrid 3979	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ (𝒫 𝑦 ∩ Fin)) → ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ⊆ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))
47		funmpt 6574	. . . . . . . . . . . 12 ⊢ Fun (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟))
48		elinel2 4154	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (𝒫 𝑦 ∩ Fin) → 𝑧 ∈ Fin)
49	48	adantl 486	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ (𝒫 𝑦 ∩ Fin)) → 𝑧 ∈ Fin)
50		imafi 9274	. . . . . . . . . . . 12 ⊢ ((Fun (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) ∧ 𝑧 ∈ Fin) → ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ∈ Fin)
51	47, 49, 50	sylancr 598	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ (𝒫 𝑦 ∩ Fin)) → ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ∈ Fin)
52		elfpw 9310	. . . . . . . . . . 11 ⊢ (((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin) ↔ (((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ⊆ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∧ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ∈ Fin))
53	46, 51, 52	sylanbrc 594	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ (𝒫 𝑦 ∩ Fin)) → ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin))
54		eqid 2761	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝐽 = ∪ 𝐽
55	54	topopn 23042	. . . . . . . . . . . . . . . 16 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽)
56	55	difexd 5301	. . . . . . . . . . . . . . 15 ⊢ (𝐽 ∈ Top → (∪ 𝐽 ∖ 𝑟) ∈ V)
57	56	ralrimivw 3159	. . . . . . . . . . . . . 14 ⊢ (𝐽 ∈ Top → ∀𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) ∈ V)
58		eqid 2761	. . . . . . . . . . . . . . 15 ⊢ (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) = (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟))
59	58	fnmpt 6675	. . . . . . . . . . . . . 14 ⊢ (∀𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) ∈ V → (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) Fn 𝑦)
60	57, 59	syl 18	. . . . . . . . . . . . 13 ⊢ (𝐽 ∈ Top → (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) Fn 𝑦)
61	60	ad3antrrr 742	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)) → (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) Fn 𝑦)
62		elfpw 9310	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin) ↔ (𝑤 ⊆ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∧ 𝑤 ∈ Fin))
63	62	bilani 509	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)) → (𝑤 ⊆ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∧ 𝑤 ∈ Fin))
64	63	simpld 499	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)) → 𝑤 ⊆ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))
65	44	ad2antrr 738	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)) → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) = ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
66	64, 65	sseqtrd 3972	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)) → 𝑤 ⊆ ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
67	63	simprd 500	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)) → 𝑤 ∈ Fin)
68		fipreima 9314	. . . . . . . . . . . 12 ⊢ (((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) Fn 𝑦 ∧ 𝑤 ⊆ ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) ∧ 𝑤 ∈ Fin) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = 𝑤)
69	61, 66, 67, 68	syl3anc 1396	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = 𝑤)
70		eqcom 2768	. . . . . . . . . . . 12 ⊢ (((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = 𝑤 ↔ 𝑤 = ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧))
71	70	rexbii 3110	. . . . . . . . . . 11 ⊢ (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = 𝑤 ↔ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑤 = ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧))
72	69, 71	sylib 221	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑤 = ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧))
73		simpr 489	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 = ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)) → 𝑤 = ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧))
74	73	inteqd 4916	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 = ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)) → ∩ 𝑤 = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧))
75	74	eqeq2d 2772	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑤 = ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)) → (∅ = ∩ 𝑤 ↔ ∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)))
76	53, 72, 75	rexxfrd 5380	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∃𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)∅ = ∩ 𝑤 ↔ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)))
77		0ex 5269	. . . . . . . . . 10 ⊢ ∅ ∈ V
78		imassrn 6073	. . . . . . . . . . . . 13 ⊢ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ⊆ ran (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟))
79		eqid 2761	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) = (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟))
80	54, 79	opncldf1 23220	. . . . . . . . . . . . . . . 16 ⊢ (𝐽 ∈ Top → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)):𝐽–1-1-onto→(Clsd‘𝐽) ∧ ◡(𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) = (𝑣 ∈ (Clsd‘𝐽) ↦ (∪ 𝐽 ∖ 𝑣))))
81	80	simpld 499	. . . . . . . . . . . . . . 15 ⊢ (𝐽 ∈ Top → (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)):𝐽–1-1-onto→(Clsd‘𝐽))
82		f1ofo 6828	. . . . . . . . . . . . . . 15 ⊢ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)):𝐽–1-1-onto→(Clsd‘𝐽) → (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)):𝐽–onto→(Clsd‘𝐽))
83	81, 82	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝐽 ∈ Top → (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)):𝐽–onto→(Clsd‘𝐽))
84		forn 6795	. . . . . . . . . . . . . 14 ⊢ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)):𝐽–onto→(Clsd‘𝐽) → ran (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) = (Clsd‘𝐽))
85	83, 84	syl 18	. . . . . . . . . . . . 13 ⊢ (𝐽 ∈ Top → ran (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) = (Clsd‘𝐽))
86	78, 85	sseqtrid 3978	. . . . . . . . . . . 12 ⊢ (𝐽 ∈ Top → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ⊆ (Clsd‘𝐽))
87		fvex 6894	. . . . . . . . . . . . 13 ⊢ (Clsd‘𝐽) ∈ V
88	87	elpw2 5304	. . . . . . . . . . . 12 ⊢ (((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∈ 𝒫 (Clsd‘𝐽) ↔ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ⊆ (Clsd‘𝐽))
89	86, 88	sylibr 237	. . . . . . . . . . 11 ⊢ (𝐽 ∈ Top → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∈ 𝒫 (Clsd‘𝐽))
90	89	ad2antrr 738	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∈ 𝒫 (Clsd‘𝐽))
91		elfi 9372	. . . . . . . . . 10 ⊢ ((∅ ∈ V ∧ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∈ 𝒫 (Clsd‘𝐽)) → (∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) ↔ ∃𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)∅ = ∩ 𝑤))
92	77, 90, 91	sylancr 598	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) ↔ ∃𝑤 ∈ (𝒫 ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∩ Fin)∅ = ∩ 𝑤))
93		inundif 4439	. . . . . . . . . . . . . 14 ⊢ (((𝒫 𝑦 ∩ Fin) ∩ {∅}) ∪ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) = (𝒫 𝑦 ∩ Fin)
94	93	rexeqi 3320	. . . . . . . . . . . . 13 ⊢ (∃𝑧 ∈ (((𝒫 𝑦 ∩ Fin) ∩ {∅}) ∪ ((𝒫 𝑦 ∩ Fin) ∖ {∅}))∪ 𝐽 = ∪ 𝑧 ↔ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧)
95		rexun 4148	. . . . . . . . . . . . 13 ⊢ (∃𝑧 ∈ (((𝒫 𝑦 ∩ Fin) ∩ {∅}) ∪ ((𝒫 𝑦 ∩ Fin) ∖ {∅}))∪ 𝐽 = ∪ 𝑧 ↔ (∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅})∪ 𝐽 = ∪ 𝑧 ∨ ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧))
96	94, 95	bitr3i 280	. . . . . . . . . . . 12 ⊢ (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧 ↔ (∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅})∪ 𝐽 = ∪ 𝑧 ∨ ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧))
97		elinel2 4154	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅}) → 𝑧 ∈ {∅})
98		elsni 4605	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ {∅} → 𝑧 = ∅)
99	97, 98	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅}) → 𝑧 = ∅)
100	99	unieqd 4884	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅}) → ∪ 𝑧 = ∪ ∅)
101		uni0 4900	. . . . . . . . . . . . . . . . . . 19 ⊢ ∪ ∅ = ∅
102	100, 101	eqtrdi 2812	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅}) → ∪ 𝑧 = ∅)
103	102	eqeq2d 2772	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅}) → (∪ 𝐽 = ∪ 𝑧 ↔ ∪ 𝐽 = ∅))
104	103	biimpd 232	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅}) → (∪ 𝐽 = ∪ 𝑧 → ∪ 𝐽 = ∅))
105	104	rexlimiv 3157	. . . . . . . . . . . . . . 15 ⊢ (∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅})∪ 𝐽 = ∪ 𝑧 → ∪ 𝐽 = ∅)
106		ssidd 3959	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → 𝑦 ⊆ 𝑦)
107		simprr 784	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → ∪ 𝐽 = ∅)
108		0ss 4356	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ∅ ⊆ ∪ 𝑦
109	107, 108	eqsstrdi 3980	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → ∪ 𝐽 ⊆ ∪ 𝑦)
110	24	ad2antlr 739	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → ∪ 𝑦 ⊆ ∪ 𝐽)
111	109, 110	eqssd 3953	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → ∪ 𝐽 = ∪ 𝑦)
112	111, 107	eqtr3d 2798	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → ∪ 𝑦 = ∅)
113	112, 3	eqeltrdi 2869	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → ∪ 𝑦 ∈ Fin)
114		pwfi 9277	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∪ 𝑦 ∈ Fin ↔ 𝒫 ∪ 𝑦 ∈ Fin)
115	113, 114	sylib 221	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → 𝒫 ∪ 𝑦 ∈ Fin)
116		pwuni 4910	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑦 ⊆ 𝒫 ∪ 𝑦
117		ssfi 9156	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝒫 ∪ 𝑦 ∈ Fin ∧ 𝑦 ⊆ 𝒫 ∪ 𝑦) → 𝑦 ∈ Fin)
118	115, 116, 117	sylancl 597	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → 𝑦 ∈ Fin)
119		elfpw 9310	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ (𝒫 𝑦 ∩ Fin) ↔ (𝑦 ⊆ 𝑦 ∧ 𝑦 ∈ Fin))
120	106, 118, 119	sylanbrc 594	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → 𝑦 ∈ (𝒫 𝑦 ∩ Fin))
121		simprl 782	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → 𝑦 ≠ ∅)
122		eldifsn 4752	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅}) ↔ (𝑦 ∈ (𝒫 𝑦 ∩ Fin) ∧ 𝑦 ≠ ∅))
123	120, 121, 122	sylanbrc 594	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → 𝑦 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅}))
124		unieq 4882	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑦 → ∪ 𝑧 = ∪ 𝑦)
125	124	rspceeqv 3603	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅}) ∧ ∪ 𝐽 = ∪ 𝑦) → ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧)
126	123, 111, 125	syl2anc 595	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ (𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅)) → ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧)
127	126	expr 461	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∪ 𝐽 = ∅ → ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧))
128	105, 127	syl5 35	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅})∪ 𝐽 = ∪ 𝑧 → ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧))
129		idd 25	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧 → ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧))
130	128, 129	jaod 872	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → ((∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅})∪ 𝐽 = ∪ 𝑧 ∨ ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧) → ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧))
131		olc 881	. . . . . . . . . . . . 13 ⊢ (∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧 → (∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅})∪ 𝐽 = ∪ 𝑧 ∨ ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧))
132	130, 131	impbid1 228	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → ((∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∩ {∅})∪ 𝐽 = ∪ 𝑧 ∨ ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧) ↔ ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧))
133	96, 132	bitrid 286	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧 ↔ ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧))
134		eldifi 4084	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅}) → 𝑧 ∈ (𝒫 𝑦 ∩ Fin))
135	134	adantl 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → 𝑧 ∈ (𝒫 𝑦 ∩ Fin))
136		elfpw 9310	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ (𝒫 𝑦 ∩ Fin) ↔ (𝑧 ⊆ 𝑦 ∧ 𝑧 ∈ Fin))
137	135, 136	sylib 221	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → (𝑧 ⊆ 𝑦 ∧ 𝑧 ∈ Fin))
138	137	simpld 499	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → 𝑧 ⊆ 𝑦)
139		simpllr 787	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → 𝑦 ⊆ 𝐽)
140	138, 139	sstrd 3946	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → 𝑧 ⊆ 𝐽)
141	140	unissd 4881	. . . . . . . . . . . . . . 15 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ∪ 𝑧 ⊆ ∪ 𝐽)
142		eqss 3951	. . . . . . . . . . . . . . . 16 ⊢ (∪ 𝑧 = ∪ 𝐽 ↔ (∪ 𝑧 ⊆ ∪ 𝐽 ∧ ∪ 𝐽 ⊆ ∪ 𝑧))
143	142	baib 544	. . . . . . . . . . . . . . 15 ⊢ (∪ 𝑧 ⊆ ∪ 𝐽 → (∪ 𝑧 = ∪ 𝐽 ↔ ∪ 𝐽 ⊆ ∪ 𝑧))
144	141, 143	syl 18	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → (∪ 𝑧 = ∪ 𝐽 ↔ ∪ 𝐽 ⊆ ∪ 𝑧))
145		eqcom 2768	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑧 = ∪ 𝐽 ↔ ∪ 𝐽 = ∪ 𝑧)
146		ssdif0 4320	. . . . . . . . . . . . . . 15 ⊢ (∪ 𝐽 ⊆ ∪ 𝑧 ↔ (∪ 𝐽 ∖ ∪ 𝑧) = ∅)
147		eqcom 2768	. . . . . . . . . . . . . . 15 ⊢ ((∪ 𝐽 ∖ ∪ 𝑧) = ∅ ↔ ∅ = (∪ 𝐽 ∖ ∪ 𝑧))
148	146, 147	bitri 278	. . . . . . . . . . . . . 14 ⊢ (∪ 𝐽 ⊆ ∪ 𝑧 ↔ ∅ = (∪ 𝐽 ∖ ∪ 𝑧))
149	144, 145, 148	3bitr3g 316	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → (∪ 𝐽 = ∪ 𝑧 ↔ ∅ = (∪ 𝐽 ∖ ∪ 𝑧)))
150		df-ima 5674	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = ran ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) ↾ 𝑧)
151	138	resmptd 6042	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) ↾ 𝑧) = (𝑟 ∈ 𝑧 ↦ (∪ 𝐽 ∖ 𝑟)))
152	151	rneqd 5928	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ran ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) ↾ 𝑧) = ran (𝑟 ∈ 𝑧 ↦ (∪ 𝐽 ∖ 𝑟)))
153	150, 152	eqtrid 2808	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = ran (𝑟 ∈ 𝑧 ↦ (∪ 𝐽 ∖ 𝑟)))
154	153	inteqd 4916	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = ∩ ran (𝑟 ∈ 𝑧 ↦ (∪ 𝐽 ∖ 𝑟)))
155	56	ralrimivw 3159	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐽 ∈ Top → ∀𝑟 ∈ 𝑧 (∪ 𝐽 ∖ 𝑟) ∈ V)
156	155	ad3antrrr 742	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ∀𝑟 ∈ 𝑧 (∪ 𝐽 ∖ 𝑟) ∈ V)
157		dfiin3g 5959	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑟 ∈ 𝑧 (∪ 𝐽 ∖ 𝑟) ∈ V → ∩ 𝑟 ∈ 𝑧 (∪ 𝐽 ∖ 𝑟) = ∩ ran (𝑟 ∈ 𝑧 ↦ (∪ 𝐽 ∖ 𝑟)))
158	156, 157	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ∩ 𝑟 ∈ 𝑧 (∪ 𝐽 ∖ 𝑟) = ∩ ran (𝑟 ∈ 𝑧 ↦ (∪ 𝐽 ∖ 𝑟)))
159		eldifsni 4757	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅}) → 𝑧 ≠ ∅)
160	159	adantl 486	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → 𝑧 ≠ ∅)
161		iindif2 5042	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ≠ ∅ → ∩ 𝑟 ∈ 𝑧 (∪ 𝐽 ∖ 𝑟) = (∪ 𝐽 ∖ ∪ 𝑟 ∈ 𝑧 𝑟))
162	160, 161	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ∩ 𝑟 ∈ 𝑧 (∪ 𝐽 ∖ 𝑟) = (∪ 𝐽 ∖ ∪ 𝑟 ∈ 𝑧 𝑟))
163	154, 158, 162	3eqtr2d 2802	. . . . . . . . . . . . . . 15 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = (∪ 𝐽 ∖ ∪ 𝑟 ∈ 𝑧 𝑟))
164		uniiun 5022	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑧 = ∪ 𝑟 ∈ 𝑧 𝑟
165	164	difeq2i 4077	. . . . . . . . . . . . . . 15 ⊢ (∪ 𝐽 ∖ ∪ 𝑧) = (∪ 𝐽 ∖ ∪ 𝑟 ∈ 𝑧 𝑟)
166	163, 165	eqtr4di 2814	. . . . . . . . . . . . . 14 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = (∪ 𝐽 ∖ ∪ 𝑧))
167	166	eqeq2d 2772	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → (∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ↔ ∅ = (∪ 𝐽 ∖ ∪ 𝑧)))
168	149, 167	bitr4d 285	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})) → (∪ 𝐽 = ∪ 𝑧 ↔ ∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)))
169	168	rexbidva 3185	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∪ 𝐽 = ∪ 𝑧 ↔ ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)))
170	133, 169	bitrd 282	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧 ↔ ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)))
171		imaeq2 6058	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = ∅ → ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ ∅))
172		ima0 6079	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ ∅) = ∅
173	171, 172	eqtrdi 2812	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = ∅ → ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = ∅)
174	173	inteqd 4916	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = ∅ → ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = ∩ ∅)
175		int0 4926	. . . . . . . . . . . . . . . . . 18 ⊢ ∩ ∅ = V
176	174, 175	eqtrdi 2812	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ∅ → ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) = V)
177	176	neeq1d 3015	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = ∅ → (∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ≠ ∅ ↔ V ≠ ∅))
178	14, 177	mpbiri 261	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = ∅ → ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ≠ ∅)
179	178	necomd 3011	. . . . . . . . . . . . . 14 ⊢ (𝑧 = ∅ → ∅ ≠ ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧))
180	179	necon2i 2990	. . . . . . . . . . . . 13 ⊢ (∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) → 𝑧 ≠ ∅)
181		eldifsn 4752	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅}) ↔ (𝑧 ∈ (𝒫 𝑦 ∩ Fin) ∧ 𝑧 ≠ ∅))
182	181	rbaibr 546	. . . . . . . . . . . . 13 ⊢ (𝑧 ≠ ∅ → (𝑧 ∈ (𝒫 𝑦 ∩ Fin) ↔ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})))
183	180, 182	syl 18	. . . . . . . . . . . 12 ⊢ (∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) → (𝑧 ∈ (𝒫 𝑦 ∩ Fin) ↔ 𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})))
184	183	pm5.32ri 585	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ (𝒫 𝑦 ∩ Fin) ∧ ∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)) ↔ (𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅}) ∧ ∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)))
185	184	rexbii2 3106	. . . . . . . . . 10 ⊢ (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧) ↔ ∃𝑧 ∈ ((𝒫 𝑦 ∩ Fin) ∖ {∅})∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧))
186	170, 185	bitr4di 292	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧 ↔ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∅ = ∩ ((𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑧)))
187	76, 92, 186	3bitr4rd 315	. . . . . . . 8 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧 ↔ ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))))
188	38, 187	imbi12d 347	. . . . . . 7 ⊢ (((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) ∧ 𝑦 ≠ ∅) → ((∪ 𝐽 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧) ↔ (∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅ → ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))))
189	23, 188	pm2.61dane 3043	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ((∪ 𝐽 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧) ↔ (∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅ → ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))))
190	57	adantr 485	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ∀𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) ∈ V)
191		dfiin3g 5959	. . . . . . . . . . 11 ⊢ (∀𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) ∈ V → ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∩ ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
192	190, 191	syl 18	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∩ ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
193	44	inteqd 4916	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) = ∩ ran (𝑟 ∈ 𝑦 ↦ (∪ 𝐽 ∖ 𝑟)))
194	192, 193	eqtr4d 2799	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))
195	194	eqeq1d 2763	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → (∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅ ↔ ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) = ∅))
196		nne 2960	. . . . . . . 8 ⊢ (¬ ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅ ↔ ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) = ∅)
197	195, 196	bitr4di 292	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → (∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅ ↔ ¬ ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅))
198	197	imbi1d 344	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ((∩ 𝑟 ∈ 𝑦 (∪ 𝐽 ∖ 𝑟) = ∅ → ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))) ↔ (¬ ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅ → ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))))
199	189, 198	bitrd 282	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ((∪ 𝐽 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧) ↔ (¬ ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅ → ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))))
200		con1b 361	. . . . 5 ⊢ ((¬ ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅ → ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))) ↔ (¬ ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅))
201	199, 200	bitrdi 290	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽) → ((∪ 𝐽 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧) ↔ (¬ ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅)))
202	1, 201	sylan2 604	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ∈ 𝒫 𝐽) → ((∪ 𝐽 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧) ↔ (¬ ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅)))
203	202	ralbidva 3184	. 2 ⊢ (𝐽 ∈ Top → (∀𝑦 ∈ 𝒫 𝐽(∪ 𝐽 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧) ↔ ∀𝑦 ∈ 𝒫 𝐽(¬ ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅)))
204	54	iscmp 23524	. . 3 ⊢ (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝐽(∪ 𝐽 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧)))
205	204	baib 544	. 2 ⊢ (𝐽 ∈ Top → (𝐽 ∈ Comp ↔ ∀𝑦 ∈ 𝒫 𝐽(∪ 𝐽 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝐽 = ∪ 𝑧)))
206	89	adantr 485	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝑦 ∈ 𝒫 𝐽) → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ∈ 𝒫 (Clsd‘𝐽))
207		simpl 487	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) → 𝐽 ∈ Top)
208		funmpt 6574	. . . . . 6 ⊢ Fun (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟))
209	208	a1i 11	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) → Fun (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)))
210		elpwi 4568	. . . . . . 7 ⊢ (𝑥 ∈ 𝒫 (Clsd‘𝐽) → 𝑥 ⊆ (Clsd‘𝐽))
211		foima 6797	. . . . . . . . 9 ⊢ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)):𝐽–onto→(Clsd‘𝐽) → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝐽) = (Clsd‘𝐽))
212	83, 211	syl 18	. . . . . . . 8 ⊢ (𝐽 ∈ Top → ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝐽) = (Clsd‘𝐽))
213	212	sseq2d 3968	. . . . . . 7 ⊢ (𝐽 ∈ Top → (𝑥 ⊆ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝐽) ↔ 𝑥 ⊆ (Clsd‘𝐽)))
214	210, 213	imbitrrid 249	. . . . . 6 ⊢ (𝐽 ∈ Top → (𝑥 ∈ 𝒫 (Clsd‘𝐽) → 𝑥 ⊆ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝐽)))
215	214	imp 411	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) → 𝑥 ⊆ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝐽))
216		ssimaexg 6967	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ Fun (𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) ∧ 𝑥 ⊆ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝐽)) → ∃𝑦(𝑦 ⊆ 𝐽 ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))
217	207, 209, 215, 216	syl3anc 1396	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) → ∃𝑦(𝑦 ⊆ 𝐽 ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))
218		df-rex 3088	. . . . 5 ⊢ (∃𝑦 ∈ 𝒫 𝐽𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ↔ ∃𝑦(𝑦 ∈ 𝒫 𝐽 ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))
219		velpw 4566	. . . . . . 7 ⊢ (𝑦 ∈ 𝒫 𝐽 ↔ 𝑦 ⊆ 𝐽)
220	219	anbi1i 635	. . . . . 6 ⊢ ((𝑦 ∈ 𝒫 𝐽 ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) ↔ (𝑦 ⊆ 𝐽 ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))
221	220	exbii 1876	. . . . 5 ⊢ (∃𝑦(𝑦 ∈ 𝒫 𝐽 ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) ↔ ∃𝑦(𝑦 ⊆ 𝐽 ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))
222	218, 221	bitri 278	. . . 4 ⊢ (∃𝑦 ∈ 𝒫 𝐽𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ↔ ∃𝑦(𝑦 ⊆ 𝐽 ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))
223	217, 222	sylibr 237	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ 𝒫 (Clsd‘𝐽)) → ∃𝑦 ∈ 𝒫 𝐽𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))
224		simpr 489	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))
225	224	fveq2d 6885	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → (fi‘𝑥) = (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)))
226	225	eleq2d 2847	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → (∅ ∈ (fi‘𝑥) ↔ ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))))
227	226	notbid 321	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → (¬ ∅ ∈ (fi‘𝑥) ↔ ¬ ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))))
228	224	inteqd 4916	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → ∩ 𝑥 = ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦))
229	228	neeq1d 3015	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → (∩ 𝑥 ≠ ∅ ↔ ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅))
230	227, 229	imbi12d 347	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝑥 = ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → ((¬ ∅ ∈ (fi‘𝑥) → ∩ 𝑥 ≠ ∅) ↔ (¬ ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅)))
231	206, 223, 230	ralxfrd 5379	. 2 ⊢ (𝐽 ∈ Top → (∀𝑥 ∈ 𝒫 (Clsd‘𝐽)(¬ ∅ ∈ (fi‘𝑥) → ∩ 𝑥 ≠ ∅) ↔ ∀𝑦 ∈ 𝒫 𝐽(¬ ∅ ∈ (fi‘((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦)) → ∩ ((𝑟 ∈ 𝐽 ↦ (∪ 𝐽 ∖ 𝑟)) “ 𝑦) ≠ ∅)))
232	203, 205, 231	3bitr4d 314	1 ⊢ (𝐽 ∈ Top → (𝐽 ∈ Comp ↔ ∀𝑥 ∈ 𝒫 (Clsd‘𝐽)(¬ ∅ ∈ (fi‘𝑥) → ∩ 𝑥 ≠ ∅)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860   = wceq 1568  ∃wex 1807   ∈ wcel 2141   ≠ wne 2956  ∀wral 3077  ∃wrex 3087  Vcvv 3453   ∖ cdif 3901   ∪ cun 3902   ∩ cin 3903   ⊆ wss 3904  ∅c0 4285  𝒫 cpw 4561  {csn 4588  ∪ cuni 4871  ∩ cint 4911  ∪ ciun 4955  ∩ ciin 4956   ↦ cmpt 5191  ^◡ccnv 5660  ran crn 5662   ↾ cres 5663   “ cima 5664  Fun wfun 6530   Fn wfn 6531  –onto→wfo 6534  –1-1-onto→wf1o 6535  ‘cfv 6536  Fincfn 8942  ficfi 9369  Topctop 23029  Clsdccld 23152  Compccmp 23522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5256  ax-nul 5268  ax-pow 5336  ax-pr 5404  ax-un 7732

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-nf 1812  df-sb 2095  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3744  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-int 4912  df-iun 4957  df-iin 4958  df-br 5109  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-om 7862  df-1o 8452  df-en 8943  df-dom 8944  df-fin 8946  df-fi 9370  df-top 23030  df-cld 23155  df-cmp 23523

This theorem is referenced by:  cmpfii  23545  fclscmp  24166  zarcmplem  34237  heibor1lem  38426