Theorem alexsublem 23998

Description: Lemma for alexsub 23999. (Contributed by Mario Carneiro, 26-Aug-2015.)

Hypotheses

Ref	Expression
alexsub.1	⊢ (𝜑 → 𝑋 ∈ UFL)
alexsub.2	⊢ (𝜑 → 𝑋 = ∪ 𝐵)
alexsub.3	⊢ (𝜑 → 𝐽 = (topGen‘(fi‘𝐵)))
alexsub.4	⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐵 ∧ 𝑋 = ∪ 𝑥)) → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦)
alexsub.5	⊢ (𝜑 → 𝐹 ∈ (UFil‘𝑋))
alexsub.6	⊢ (𝜑 → (𝐽 fLim 𝐹) = ∅)

Assertion

Ref	Expression
alexsublem	⊢ ¬ 𝜑

Distinct variable groups:   𝑥,𝑦,𝐵   𝑥,𝐽,𝑦   𝜑,𝑥,𝑦   𝑥,𝑋,𝑦   𝑥,𝐹,𝑦

Proof of Theorem alexsublem

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eldif 3941	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝑋 ∖ ∪ (𝐵 ∖ 𝐹)) ↔ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹)))
2		alexsub.3	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐽 = (topGen‘(fi‘𝐵)))
3	2	eleq2d 2819	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑦 ∈ 𝐽 ↔ 𝑦 ∈ (topGen‘(fi‘𝐵))))
4	3	anbi1d 631	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦) ↔ (𝑦 ∈ (topGen‘(fi‘𝐵)) ∧ 𝑥 ∈ 𝑦)))
5	4	biimpa 476	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) → (𝑦 ∈ (topGen‘(fi‘𝐵)) ∧ 𝑥 ∈ 𝑦))
6	5	adantlr 715	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) → (𝑦 ∈ (topGen‘(fi‘𝐵)) ∧ 𝑥 ∈ 𝑦))
7		tg2 22919	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ (topGen‘(fi‘𝐵)) ∧ 𝑥 ∈ 𝑦) → ∃𝑧 ∈ (fi‘𝐵)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦))
8	6, 7	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) → ∃𝑧 ∈ (fi‘𝐵)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦))
9		alexsub.5	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹 ∈ (UFil‘𝑋))
10		ufilfil 23858	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 ∈ (UFil‘𝑋) → 𝐹 ∈ (Fil‘𝑋))
11	9, 10	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐹 ∈ (Fil‘𝑋))
12	11	ad3antrrr 730	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦))) → 𝐹 ∈ (Fil‘𝑋))
13		alexsub.2	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑋 = ∪ 𝐵)
14	9	elfvexd 6925	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑋 ∈ V)
15	13, 14	eqeltrrd 2834	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ∪ 𝐵 ∈ V)
16		uniexb 7766	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐵 ∈ V ↔ ∪ 𝐵 ∈ V)
17	15, 16	sylibr 234	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐵 ∈ V)
18		elfi2 9436	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐵 ∈ V → (𝑧 ∈ (fi‘𝐵) ↔ ∃𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})𝑧 = ∩ 𝑦))
19	17, 18	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑧 ∈ (fi‘𝐵) ↔ ∃𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})𝑧 = ∩ 𝑦))
20	19	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) → (𝑧 ∈ (fi‘𝐵) ↔ ∃𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})𝑧 = ∩ 𝑦))
21	11	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦)) → 𝐹 ∈ (Fil‘𝑋))
22		simplrr 777	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) → ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))
23		intss1 4943	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑧 ∈ 𝑦 → ∩ 𝑦 ⊆ 𝑧)
24	23	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦) → ∩ 𝑦 ⊆ 𝑧)
25		simplr 768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦) → 𝑥 ∈ ∩ 𝑦)
26	24, 25	sseldd 3964	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦) → 𝑥 ∈ 𝑧)
27	26	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) ∧ ¬ 𝑧 ∈ 𝐹) → 𝑥 ∈ 𝑧)
28		eldifsn 4766	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ↔ (𝑦 ∈ (𝒫 𝐵 ∩ Fin) ∧ 𝑦 ≠ ∅))
29	28	simplbi 497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) → 𝑦 ∈ (𝒫 𝐵 ∩ Fin))
30	29	ad2antrl 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦)) → 𝑦 ∈ (𝒫 𝐵 ∩ Fin))
31		elfpw 9376	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑦 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝑦 ⊆ 𝐵 ∧ 𝑦 ∈ Fin))
32	31	simplbi 497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑦 ∈ (𝒫 𝐵 ∩ Fin) → 𝑦 ⊆ 𝐵)
33	30, 32	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦)) → 𝑦 ⊆ 𝐵)
34	33	sselda 3963	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦)) ∧ 𝑧 ∈ 𝑦) → 𝑧 ∈ 𝐵)
35	34	anasss 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) → 𝑧 ∈ 𝐵)
36	35	anim1i 615	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) ∧ ¬ 𝑧 ∈ 𝐹) → (𝑧 ∈ 𝐵 ∧ ¬ 𝑧 ∈ 𝐹))
37		eldif 3941	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑧 ∈ (𝐵 ∖ 𝐹) ↔ (𝑧 ∈ 𝐵 ∧ ¬ 𝑧 ∈ 𝐹))
38	36, 37	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) ∧ ¬ 𝑧 ∈ 𝐹) → 𝑧 ∈ (𝐵 ∖ 𝐹))
39		elunii 4892	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑥 ∈ 𝑧 ∧ 𝑧 ∈ (𝐵 ∖ 𝐹)) → 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))
40	27, 38, 39	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) ∧ ¬ 𝑧 ∈ 𝐹) → 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))
41	40	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) → (¬ 𝑧 ∈ 𝐹 → 𝑥 ∈ ∪ (𝐵 ∖ 𝐹)))
42	22, 41	mt3d 148	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) → 𝑧 ∈ 𝐹)
43	42	expr 456	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦)) → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝐹))
44	43	ssrdv 3969	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦)) → 𝑦 ⊆ 𝐹)
45		eldifsni 4770	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) → 𝑦 ≠ ∅)
46	45	ad2antrl 728	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦)) → 𝑦 ≠ ∅)
47		elinel2 4182	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 ∈ (𝒫 𝐵 ∩ Fin) → 𝑦 ∈ Fin)
48	30, 47	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦)) → 𝑦 ∈ Fin)
49		elfir 9437	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑦 ⊆ 𝐹 ∧ 𝑦 ≠ ∅ ∧ 𝑦 ∈ Fin)) → ∩ 𝑦 ∈ (fi‘𝐹))
50	21, 44, 46, 48, 49	syl13anc 1373	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦)) → ∩ 𝑦 ∈ (fi‘𝐹))
51		filfi 23813	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐹 ∈ (Fil‘𝑋) → (fi‘𝐹) = 𝐹)
52	21, 51	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦)) → (fi‘𝐹) = 𝐹)
53	50, 52	eleqtrd 2835	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦)) → ∩ 𝑦 ∈ 𝐹)
54	53	expr 456	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ 𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})) → (𝑥 ∈ ∩ 𝑦 → ∩ 𝑦 ∈ 𝐹))
55		eleq2 2822	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 = ∩ 𝑦 → (𝑥 ∈ 𝑧 ↔ 𝑥 ∈ ∩ 𝑦))
56		eleq1 2821	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 = ∩ 𝑦 → (𝑧 ∈ 𝐹 ↔ ∩ 𝑦 ∈ 𝐹))
57	55, 56	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = ∩ 𝑦 → ((𝑥 ∈ 𝑧 → 𝑧 ∈ 𝐹) ↔ (𝑥 ∈ ∩ 𝑦 → ∩ 𝑦 ∈ 𝐹)))
58	54, 57	syl5ibrcom 247	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ 𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})) → (𝑧 = ∩ 𝑦 → (𝑥 ∈ 𝑧 → 𝑧 ∈ 𝐹)))
59	58	rexlimdva 3142	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) → (∃𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})𝑧 = ∩ 𝑦 → (𝑥 ∈ 𝑧 → 𝑧 ∈ 𝐹)))
60	20, 59	sylbid 240	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) → (𝑧 ∈ (fi‘𝐵) → (𝑥 ∈ 𝑧 → 𝑧 ∈ 𝐹)))
61	60	imp32 418	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑧 ∈ (fi‘𝐵) ∧ 𝑥 ∈ 𝑧)) → 𝑧 ∈ 𝐹)
62	61	adantrrr 725	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦))) → 𝑧 ∈ 𝐹)
63	62	adantlr 715	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦))) → 𝑧 ∈ 𝐹)
64		elssuni 4917	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ 𝐽 → 𝑦 ⊆ ∪ 𝐽)
65	64	ad2antrl 728	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) → 𝑦 ⊆ ∪ 𝐽)
66		fibas 22931	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (fi‘𝐵) ∈ TopBases
67		tgtopon 22925	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((fi‘𝐵) ∈ TopBases → (topGen‘(fi‘𝐵)) ∈ (TopOn‘∪ (fi‘𝐵)))
68	66, 67	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (topGen‘(fi‘𝐵)) ∈ (TopOn‘∪ (fi‘𝐵))
69	2, 68	eqeltrdi 2841	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘∪ (fi‘𝐵)))
70		fiuni 9450	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐵 ∈ V → ∪ 𝐵 = ∪ (fi‘𝐵))
71	17, 70	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ∪ 𝐵 = ∪ (fi‘𝐵))
72	13, 71	eqtrd 2769	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑋 = ∪ (fi‘𝐵))
73	72	fveq2d 6890	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (TopOn‘𝑋) = (TopOn‘∪ (fi‘𝐵)))
74	69, 73	eleqtrrd 2836	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))
75		toponuni 22868	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽)
76	74, 75	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑋 = ∪ 𝐽)
77	76	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) → 𝑋 = ∪ 𝐽)
78	65, 77	sseqtrrd 4001	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) → 𝑦 ⊆ 𝑋)
79	78	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦))) → 𝑦 ⊆ 𝑋)
80		simprrr 781	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦))) → 𝑧 ⊆ 𝑦)
81		filss 23807	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑧 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑋 ∧ 𝑧 ⊆ 𝑦)) → 𝑦 ∈ 𝐹)
82	12, 63, 79, 80, 81	syl13anc 1373	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦))) → 𝑦 ∈ 𝐹)
83	8, 82	rexlimddv 3148	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) → 𝑦 ∈ 𝐹)
84	83	expr 456	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ 𝑦 ∈ 𝐽) → (𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹))
85	84	ralrimiva 3133	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) → ∀𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹))
86	85	expr 456	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹) → ∀𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹)))
87	86	imdistanda 571	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹)) → (𝑥 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹))))
88	1, 87	biimtrid 242	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (𝑋 ∖ ∪ (𝐵 ∖ 𝐹)) → (𝑥 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹))))
89		flimopn 23929	. . . . . . . . . 10 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) → (𝑥 ∈ (𝐽 fLim 𝐹) ↔ (𝑥 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹))))
90	74, 11, 89	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (𝐽 fLim 𝐹) ↔ (𝑥 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹))))
91	88, 90	sylibrd 259	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (𝑋 ∖ ∪ (𝐵 ∖ 𝐹)) → 𝑥 ∈ (𝐽 fLim 𝐹)))
92	91	ssrdv 3969	. . . . . . 7 ⊢ (𝜑 → (𝑋 ∖ ∪ (𝐵 ∖ 𝐹)) ⊆ (𝐽 fLim 𝐹))
93		alexsub.6	. . . . . . 7 ⊢ (𝜑 → (𝐽 fLim 𝐹) = ∅)
94		sseq0 4383	. . . . . . 7 ⊢ (((𝑋 ∖ ∪ (𝐵 ∖ 𝐹)) ⊆ (𝐽 fLim 𝐹) ∧ (𝐽 fLim 𝐹) = ∅) → (𝑋 ∖ ∪ (𝐵 ∖ 𝐹)) = ∅)
95	92, 93, 94	syl2anc 584	. . . . . 6 ⊢ (𝜑 → (𝑋 ∖ ∪ (𝐵 ∖ 𝐹)) = ∅)
96		ssdif0 4346	. . . . . 6 ⊢ (𝑋 ⊆ ∪ (𝐵 ∖ 𝐹) ↔ (𝑋 ∖ ∪ (𝐵 ∖ 𝐹)) = ∅)
97	95, 96	sylibr 234	. . . . 5 ⊢ (𝜑 → 𝑋 ⊆ ∪ (𝐵 ∖ 𝐹))
98		difss 4116	. . . . . . 7 ⊢ (𝐵 ∖ 𝐹) ⊆ 𝐵
99	98	unissi 4896	. . . . . 6 ⊢ ∪ (𝐵 ∖ 𝐹) ⊆ ∪ 𝐵
100	99, 13	sseqtrrid 4007	. . . . 5 ⊢ (𝜑 → ∪ (𝐵 ∖ 𝐹) ⊆ 𝑋)
101	97, 100	eqssd 3981	. . . 4 ⊢ (𝜑 → 𝑋 = ∪ (𝐵 ∖ 𝐹))
102	101, 98	jctil 519	. . 3 ⊢ (𝜑 → ((𝐵 ∖ 𝐹) ⊆ 𝐵 ∧ 𝑋 = ∪ (𝐵 ∖ 𝐹)))
103	17	difexd 5311	. . . . 5 ⊢ (𝜑 → (𝐵 ∖ 𝐹) ∈ V)
104	103	adantr 480	. . . 4 ⊢ ((𝜑 ∧ ((𝐵 ∖ 𝐹) ⊆ 𝐵 ∧ 𝑋 = ∪ (𝐵 ∖ 𝐹))) → (𝐵 ∖ 𝐹) ∈ V)
105		sseq1 3989	. . . . . . . 8 ⊢ (𝑥 = (𝐵 ∖ 𝐹) → (𝑥 ⊆ 𝐵 ↔ (𝐵 ∖ 𝐹) ⊆ 𝐵))
106		unieq 4898	. . . . . . . . 9 ⊢ (𝑥 = (𝐵 ∖ 𝐹) → ∪ 𝑥 = ∪ (𝐵 ∖ 𝐹))
107	106	eqeq2d 2745	. . . . . . . 8 ⊢ (𝑥 = (𝐵 ∖ 𝐹) → (𝑋 = ∪ 𝑥 ↔ 𝑋 = ∪ (𝐵 ∖ 𝐹)))
108	105, 107	anbi12d 632	. . . . . . 7 ⊢ (𝑥 = (𝐵 ∖ 𝐹) → ((𝑥 ⊆ 𝐵 ∧ 𝑋 = ∪ 𝑥) ↔ ((𝐵 ∖ 𝐹) ⊆ 𝐵 ∧ 𝑋 = ∪ (𝐵 ∖ 𝐹))))
109	108	anbi2d 630	. . . . . 6 ⊢ (𝑥 = (𝐵 ∖ 𝐹) → ((𝜑 ∧ (𝑥 ⊆ 𝐵 ∧ 𝑋 = ∪ 𝑥)) ↔ (𝜑 ∧ ((𝐵 ∖ 𝐹) ⊆ 𝐵 ∧ 𝑋 = ∪ (𝐵 ∖ 𝐹)))))
110		pweq 4594	. . . . . . . 8 ⊢ (𝑥 = (𝐵 ∖ 𝐹) → 𝒫 𝑥 = 𝒫 (𝐵 ∖ 𝐹))
111	110	ineq1d 4199	. . . . . . 7 ⊢ (𝑥 = (𝐵 ∖ 𝐹) → (𝒫 𝑥 ∩ Fin) = (𝒫 (𝐵 ∖ 𝐹) ∩ Fin))
112	111	rexeqdv 3310	. . . . . 6 ⊢ (𝑥 = (𝐵 ∖ 𝐹) → (∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦 ↔ ∃𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)𝑋 = ∪ 𝑦))
113	109, 112	imbi12d 344	. . . . 5 ⊢ (𝑥 = (𝐵 ∖ 𝐹) → (((𝜑 ∧ (𝑥 ⊆ 𝐵 ∧ 𝑋 = ∪ 𝑥)) → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦) ↔ ((𝜑 ∧ ((𝐵 ∖ 𝐹) ⊆ 𝐵 ∧ 𝑋 = ∪ (𝐵 ∖ 𝐹))) → ∃𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)𝑋 = ∪ 𝑦)))
114		alexsub.4	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐵 ∧ 𝑋 = ∪ 𝑥)) → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦)
115	113, 114	vtoclg 3537	. . . 4 ⊢ ((𝐵 ∖ 𝐹) ∈ V → ((𝜑 ∧ ((𝐵 ∖ 𝐹) ⊆ 𝐵 ∧ 𝑋 = ∪ (𝐵 ∖ 𝐹))) → ∃𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)𝑋 = ∪ 𝑦))
116	104, 115	mpcom 38	. . 3 ⊢ ((𝜑 ∧ ((𝐵 ∖ 𝐹) ⊆ 𝐵 ∧ 𝑋 = ∪ (𝐵 ∖ 𝐹))) → ∃𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)𝑋 = ∪ 𝑦)
117	102, 116	mpdan 687	. 2 ⊢ (𝜑 → ∃𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)𝑋 = ∪ 𝑦)
118		unieq 4898	. . . . . . 7 ⊢ (𝑦 = ∅ → ∪ 𝑦 = ∪ ∅)
119		uni0 4915	. . . . . . 7 ⊢ ∪ ∅ = ∅
120	118, 119	eqtrdi 2785	. . . . . 6 ⊢ (𝑦 = ∅ → ∪ 𝑦 = ∅)
121	120	neeq2d 2991	. . . . 5 ⊢ (𝑦 = ∅ → (𝑋 ≠ ∪ 𝑦 ↔ 𝑋 ≠ ∅))
122		difssd 4117	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) → (𝑋 ∖ 𝑧) ⊆ 𝑋)
123	122	ralrimivw 3137	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) → ∀𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧) ⊆ 𝑋)
124		riinn0 5063	. . . . . . . . . 10 ⊢ ((∀𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧) ⊆ 𝑋 ∧ 𝑦 ≠ ∅) → (𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)) = ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧))
125	123, 124	sylan 580	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)) = ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧))
126	14	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑋 ∈ V)
127	126	difexd 5311	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑋 ∖ 𝑧) ∈ V)
128	127	ralrimivw 3137	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ∀𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧) ∈ V)
129		dfiin2g 5012	. . . . . . . . . . 11 ⊢ (∀𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧) ∈ V → ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧) = ∩ {𝑥 ∣ ∃𝑧 ∈ 𝑦 𝑥 = (𝑋 ∖ 𝑧)})
130	128, 129	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧) = ∩ {𝑥 ∣ ∃𝑧 ∈ 𝑦 𝑥 = (𝑋 ∖ 𝑧)})
131		eqid 2734	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) = (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧))
132	131	rnmpt 5948	. . . . . . . . . . 11 ⊢ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) = {𝑥 ∣ ∃𝑧 ∈ 𝑦 𝑥 = (𝑋 ∖ 𝑧)}
133	132	inteqi 4930	. . . . . . . . . 10 ⊢ ∩ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) = ∩ {𝑥 ∣ ∃𝑧 ∈ 𝑦 𝑥 = (𝑋 ∖ 𝑧)}
134	130, 133	eqtr4di 2787	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧) = ∩ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)))
135	125, 134	eqtrd 2769	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)) = ∩ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)))
136	11	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝐹 ∈ (Fil‘𝑋))
137		elfpw 9376	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin) ↔ (𝑦 ⊆ (𝐵 ∖ 𝐹) ∧ 𝑦 ∈ Fin))
138	137	simplbi 497	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin) → 𝑦 ⊆ (𝐵 ∖ 𝐹))
139	138	ad2antlr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑦 ⊆ (𝐵 ∖ 𝐹))
140	139	sselda 3963	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → 𝑧 ∈ (𝐵 ∖ 𝐹))
141	140	eldifbd 3944	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → ¬ 𝑧 ∈ 𝐹)
142	9	ad3antrrr 730	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → 𝐹 ∈ (UFil‘𝑋))
143	139	difss2d 4119	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑦 ⊆ 𝐵)
144	143	sselda 3963	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → 𝑧 ∈ 𝐵)
145		elssuni 4917	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ 𝐵 → 𝑧 ⊆ ∪ 𝐵)
146	144, 145	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → 𝑧 ⊆ ∪ 𝐵)
147	13	ad3antrrr 730	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → 𝑋 = ∪ 𝐵)
148	146, 147	sseqtrrd 4001	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → 𝑧 ⊆ 𝑋)
149		ufilb 23860	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑧 ⊆ 𝑋) → (¬ 𝑧 ∈ 𝐹 ↔ (𝑋 ∖ 𝑧) ∈ 𝐹))
150	142, 148, 149	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → (¬ 𝑧 ∈ 𝐹 ↔ (𝑋 ∖ 𝑧) ∈ 𝐹))
151	141, 150	mpbid 232	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → (𝑋 ∖ 𝑧) ∈ 𝐹)
152	151	fmpttd 7115	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)):𝑦⟶𝐹)
153	152	frnd 6724	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ⊆ 𝐹)
154	131, 151	dmmptd 6693	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → dom (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) = 𝑦)
155		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑦 ≠ ∅)
156	154, 155	eqnetrd 2998	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → dom (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ≠ ∅)
157		dm0rn0 5915	. . . . . . . . . . 11 ⊢ (dom (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) = ∅ ↔ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) = ∅)
158	157	necon3bii 2983	. . . . . . . . . 10 ⊢ (dom (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ≠ ∅ ↔ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ≠ ∅)
159	156, 158	sylib 218	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ≠ ∅)
160		elinel2 4182	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin) → 𝑦 ∈ Fin)
161	160	ad2antlr 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑦 ∈ Fin)
162		abrexfi 9374	. . . . . . . . . . 11 ⊢ (𝑦 ∈ Fin → {𝑥 ∣ ∃𝑧 ∈ 𝑦 𝑥 = (𝑋 ∖ 𝑧)} ∈ Fin)
163	132, 162	eqeltrid 2837	. . . . . . . . . 10 ⊢ (𝑦 ∈ Fin → ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ∈ Fin)
164	161, 163	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ∈ Fin)
165		filintn0 23815	. . . . . . . . 9 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ⊆ 𝐹 ∧ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ≠ ∅ ∧ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ∈ Fin)) → ∩ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ≠ ∅)
166	136, 153, 159, 164, 165	syl13anc 1373	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ∩ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ≠ ∅)
167	135, 166	eqnetrd 2998	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)) ≠ ∅)
168		disj3 4434	. . . . . . . 8 ⊢ ((𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)) = ∅ ↔ 𝑋 = (𝑋 ∖ ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)))
169	168	necon3bii 2983	. . . . . . 7 ⊢ ((𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)) ≠ ∅ ↔ 𝑋 ≠ (𝑋 ∖ ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)))
170	167, 169	sylib 218	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑋 ≠ (𝑋 ∖ ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)))
171		iundif2 5054	. . . . . . 7 ⊢ ∪ 𝑧 ∈ 𝑦 (𝑋 ∖ (𝑋 ∖ 𝑧)) = (𝑋 ∖ ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧))
172		dfss4 4249	. . . . . . . . . 10 ⊢ (𝑧 ⊆ 𝑋 ↔ (𝑋 ∖ (𝑋 ∖ 𝑧)) = 𝑧)
173	148, 172	sylib 218	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → (𝑋 ∖ (𝑋 ∖ 𝑧)) = 𝑧)
174	173	iuneq2dv 4996	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ∪ 𝑧 ∈ 𝑦 (𝑋 ∖ (𝑋 ∖ 𝑧)) = ∪ 𝑧 ∈ 𝑦 𝑧)
175		uniiun 5038	. . . . . . . 8 ⊢ ∪ 𝑦 = ∪ 𝑧 ∈ 𝑦 𝑧
176	174, 175	eqtr4di 2787	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ∪ 𝑧 ∈ 𝑦 (𝑋 ∖ (𝑋 ∖ 𝑧)) = ∪ 𝑦)
177	171, 176	eqtr3id 2783	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑋 ∖ ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)) = ∪ 𝑦)
178	170, 177	neeqtrd 3000	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑋 ≠ ∪ 𝑦)
179	11	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) → 𝐹 ∈ (Fil‘𝑋))
180		filtop 23809	. . . . . 6 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐹)
181		fileln0 23804	. . . . . 6 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑋 ∈ 𝐹) → 𝑋 ≠ ∅)
182	179, 180, 181	syl2anc2 585	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) → 𝑋 ≠ ∅)
183	121, 178, 182	pm2.61ne 3016	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) → 𝑋 ≠ ∪ 𝑦)
184	183	neneqd 2936	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) → ¬ 𝑋 = ∪ 𝑦)
185	184	nrexdv 3136	. 2 ⊢ (𝜑 → ¬ ∃𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)𝑋 = ∪ 𝑦)
186	117, 185	pm2.65i 194	1 ⊢ ¬ 𝜑

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1539   ∈ wcel 2107  {cab 2712   ≠ wne 2931  ∀wral 3050  ∃wrex 3059  Vcvv 3463   ∖ cdif 3928   ∩ cin 3930   ⊆ wss 3931  ∅c0 4313  𝒫 cpw 4580  {csn 4606  ∪ cuni 4887  ∩ cint 4926  ∪ ciun 4971  ∩ ciin 4972   ↦ cmpt 5205  dom cdm 5665  ran crn 5666  ‘cfv 6541  (class class class)co 7413  Fincfn 8967  ficfi 9432  topGenctg 17453  TopOnctopon 22864  TopBasesctb 22899  Filcfil 23799  UFilcufil 23853  UFLcufl 23854   fLim cflim 23888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-rep 5259  ax-sep 5276  ax-nul 5286  ax-pow 5345  ax-pr 5412  ax-un 7737

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-reu 3364  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-int 4927  df-iun 4973  df-iin 4974  df-br 5124  df-opab 5186  df-mpt 5206  df-tr 5240  df-id 5558  df-eprel 5564  df-po 5572  df-so 5573  df-fr 5617  df-we 5619  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-res 5677  df-ima 5678  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7870  df-1st 7996  df-2nd 7997  df-1o 8488  df-2o 8489  df-en 8968  df-dom 8969  df-fin 8971  df-fi 9433  df-topgen 17459  df-fbas 21323  df-top 22848  df-topon 22865  df-bases 22900  df-ntr 22974  df-nei 23052  df-fil 23800  df-ufil 23855  df-flim 23893

This theorem is referenced by:  alexsub  23999