Theorem alexsublem 23988

Description: Lemma for alexsub 23989. (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 3911	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝑋 ∖ ∪ (𝐵 ∖ 𝐹)) ↔ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹)))
2		alexsub.3	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐽 = (topGen‘(fi‘𝐵)))
3	2	eleq2d 2822	. . . . . . . . . . . . . . . . . . 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 22909	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ (topGen‘(fi‘𝐵)) ∧ 𝑥 ∈ 𝑦) → ∃𝑧 ∈ (fi‘𝐵)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦))
8	6, 7	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) → ∃𝑧 ∈ (fi‘𝐵)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦))
9		alexsub.5	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹 ∈ (UFil‘𝑋))
10		ufilfil 23848	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 ∈ (UFil‘𝑋) → 𝐹 ∈ (Fil‘𝑋))
11	9, 10	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐹 ∈ (Fil‘𝑋))
12	11	ad3antrrr 730	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦))) → 𝐹 ∈ (Fil‘𝑋))
13		alexsub.2	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑋 = ∪ 𝐵)
14	9	elfvexd 6870	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑋 ∈ V)
15	13, 14	eqeltrrd 2837	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ∪ 𝐵 ∈ V)
16		uniexb 7709	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐵 ∈ V ↔ ∪ 𝐵 ∈ V)
17	15, 16	sylibr 234	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐵 ∈ V)
18		elfi2 9317	. . . . . . . . . . . . . . . . . . . . . 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 4918	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑧 ∈ 𝑦 → ∩ 𝑦 ⊆ 𝑧)
24	23	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦) → ∩ 𝑦 ⊆ 𝑧)
25		simplr 768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦) → 𝑥 ∈ ∩ 𝑦)
26	24, 25	sseldd 3934	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦) → 𝑥 ∈ 𝑧)
27	26	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) ∧ ¬ 𝑧 ∈ 𝐹) → 𝑥 ∈ 𝑧)
28		eldifsn 4742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ↔ (𝑦 ∈ (𝒫 𝐵 ∩ Fin) ∧ 𝑦 ≠ ∅))
29	28	simplbi 497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) → 𝑦 ∈ (𝒫 𝐵 ∩ Fin))
30	29	ad2antrl 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦)) → 𝑦 ∈ (𝒫 𝐵 ∩ Fin))
31		elfpw 9254	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑦 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝑦 ⊆ 𝐵 ∧ 𝑦 ∈ Fin))
32	31	simplbi 497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑦 ∈ (𝒫 𝐵 ∩ Fin) → 𝑦 ⊆ 𝐵)
33	30, 32	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦)) → 𝑦 ⊆ 𝐵)
34	33	sselda 3933	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦)) ∧ 𝑧 ∈ 𝑦) → 𝑧 ∈ 𝐵)
35	34	anasss 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) → 𝑧 ∈ 𝐵)
36	35	anim1i 615	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) ∧ ¬ 𝑧 ∈ 𝐹) → (𝑧 ∈ 𝐵 ∧ ¬ 𝑧 ∈ 𝐹))
37		eldif 3911	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑧 ∈ (𝐵 ∖ 𝐹) ↔ (𝑧 ∈ 𝐵 ∧ ¬ 𝑧 ∈ 𝐹))
38	36, 37	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) ∧ ¬ 𝑧 ∈ 𝐹) → 𝑧 ∈ (𝐵 ∖ 𝐹))
39		elunii 4868	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3939	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦)) → 𝑦 ⊆ 𝐹)
45		eldifsni 4746	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) → 𝑦 ≠ ∅)
46	45	ad2antrl 728	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦)) → 𝑦 ≠ ∅)
47		elinel2 4154	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 ∈ (𝒫 𝐵 ∩ Fin) → 𝑦 ∈ Fin)
48	30, 47	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦)) → 𝑦 ∈ Fin)
49		elfir 9318	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑦 ⊆ 𝐹 ∧ 𝑦 ≠ ∅ ∧ 𝑦 ∈ Fin)) → ∩ 𝑦 ∈ (fi‘𝐹))
50	21, 44, 46, 48, 49	syl13anc 1374	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦)) → ∩ 𝑦 ∈ (fi‘𝐹))
51		filfi 23803	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐹 ∈ (Fil‘𝑋) → (fi‘𝐹) = 𝐹)
52	21, 51	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦)) → (fi‘𝐹) = 𝐹)
53	50, 52	eleqtrd 2838	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦)) → ∩ 𝑦 ∈ 𝐹)
54	53	expr 456	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ 𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})) → (𝑥 ∈ ∩ 𝑦 → ∩ 𝑦 ∈ 𝐹))
55		eleq2 2825	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 = ∩ 𝑦 → (𝑥 ∈ 𝑧 ↔ 𝑥 ∈ ∩ 𝑦))
56		eleq1 2824	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 = ∩ 𝑦 → (𝑧 ∈ 𝐹 ↔ ∩ 𝑦 ∈ 𝐹))
57	55, 56	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = ∩ 𝑦 → ((𝑥 ∈ 𝑧 → 𝑧 ∈ 𝐹) ↔ (𝑥 ∈ ∩ 𝑦 → ∩ 𝑦 ∈ 𝐹)))
58	54, 57	syl5ibrcom 247	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ 𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})) → (𝑧 = ∩ 𝑦 → (𝑥 ∈ 𝑧 → 𝑧 ∈ 𝐹)))
59	58	rexlimdva 3137	. . . . . . . . . . . . . . . . . . . 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 4894	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ 𝐽 → 𝑦 ⊆ ∪ 𝐽)
65	64	ad2antrl 728	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) → 𝑦 ⊆ ∪ 𝐽)
66		fibas 22921	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (fi‘𝐵) ∈ TopBases
67		tgtopon 22915	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((fi‘𝐵) ∈ TopBases → (topGen‘(fi‘𝐵)) ∈ (TopOn‘∪ (fi‘𝐵)))
68	66, 67	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (topGen‘(fi‘𝐵)) ∈ (TopOn‘∪ (fi‘𝐵))
69	2, 68	eqeltrdi 2844	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘∪ (fi‘𝐵)))
70		fiuni 9331	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐵 ∈ V → ∪ 𝐵 = ∪ (fi‘𝐵))
71	17, 70	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ∪ 𝐵 = ∪ (fi‘𝐵))
72	13, 71	eqtrd 2771	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑋 = ∪ (fi‘𝐵))
73	72	fveq2d 6838	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (TopOn‘𝑋) = (TopOn‘∪ (fi‘𝐵)))
74	69, 73	eleqtrrd 2839	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))
75		toponuni 22858	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽)
76	74, 75	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑋 = ∪ 𝐽)
77	76	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) → 𝑋 = ∪ 𝐽)
78	65, 77	sseqtrrd 3971	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) → 𝑦 ⊆ 𝑋)
79	78	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦))) → 𝑦 ⊆ 𝑋)
80		simprrr 781	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦))) → 𝑧 ⊆ 𝑦)
81		filss 23797	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑧 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑋 ∧ 𝑧 ⊆ 𝑦)) → 𝑦 ∈ 𝐹)
82	12, 63, 79, 80, 81	syl13anc 1374	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦))) → 𝑦 ∈ 𝐹)
83	8, 82	rexlimddv 3143	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) → 𝑦 ∈ 𝐹)
84	83	expr 456	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ 𝑦 ∈ 𝐽) → (𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹))
85	84	ralrimiva 3128	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) → ∀𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹))
86	85	expr 456	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹) → ∀𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹)))
87	86	imdistanda 571	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹)) → (𝑥 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹))))
88	1, 87	biimtrid 242	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (𝑋 ∖ ∪ (𝐵 ∖ 𝐹)) → (𝑥 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹))))
89		flimopn 23919	. . . . . . . . . 10 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) → (𝑥 ∈ (𝐽 fLim 𝐹) ↔ (𝑥 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹))))
90	74, 11, 89	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (𝐽 fLim 𝐹) ↔ (𝑥 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹))))
91	88, 90	sylibrd 259	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (𝑋 ∖ ∪ (𝐵 ∖ 𝐹)) → 𝑥 ∈ (𝐽 fLim 𝐹)))
92	91	ssrdv 3939	. . . . . . 7 ⊢ (𝜑 → (𝑋 ∖ ∪ (𝐵 ∖ 𝐹)) ⊆ (𝐽 fLim 𝐹))
93		alexsub.6	. . . . . . 7 ⊢ (𝜑 → (𝐽 fLim 𝐹) = ∅)
94		sseq0 4355	. . . . . . 7 ⊢ (((𝑋 ∖ ∪ (𝐵 ∖ 𝐹)) ⊆ (𝐽 fLim 𝐹) ∧ (𝐽 fLim 𝐹) = ∅) → (𝑋 ∖ ∪ (𝐵 ∖ 𝐹)) = ∅)
95	92, 93, 94	syl2anc 584	. . . . . 6 ⊢ (𝜑 → (𝑋 ∖ ∪ (𝐵 ∖ 𝐹)) = ∅)
96		ssdif0 4318	. . . . . 6 ⊢ (𝑋 ⊆ ∪ (𝐵 ∖ 𝐹) ↔ (𝑋 ∖ ∪ (𝐵 ∖ 𝐹)) = ∅)
97	95, 96	sylibr 234	. . . . 5 ⊢ (𝜑 → 𝑋 ⊆ ∪ (𝐵 ∖ 𝐹))
98		difss 4088	. . . . . . 7 ⊢ (𝐵 ∖ 𝐹) ⊆ 𝐵
99	98	unissi 4872	. . . . . 6 ⊢ ∪ (𝐵 ∖ 𝐹) ⊆ ∪ 𝐵
100	99, 13	sseqtrrid 3977	. . . . 5 ⊢ (𝜑 → ∪ (𝐵 ∖ 𝐹) ⊆ 𝑋)
101	97, 100	eqssd 3951	. . . 4 ⊢ (𝜑 → 𝑋 = ∪ (𝐵 ∖ 𝐹))
102	101, 98	jctil 519	. . 3 ⊢ (𝜑 → ((𝐵 ∖ 𝐹) ⊆ 𝐵 ∧ 𝑋 = ∪ (𝐵 ∖ 𝐹)))
103	17	difexd 5276	. . . . 5 ⊢ (𝜑 → (𝐵 ∖ 𝐹) ∈ V)
104	103	adantr 480	. . . 4 ⊢ ((𝜑 ∧ ((𝐵 ∖ 𝐹) ⊆ 𝐵 ∧ 𝑋 = ∪ (𝐵 ∖ 𝐹))) → (𝐵 ∖ 𝐹) ∈ V)
105		sseq1 3959	. . . . . . . 8 ⊢ (𝑥 = (𝐵 ∖ 𝐹) → (𝑥 ⊆ 𝐵 ↔ (𝐵 ∖ 𝐹) ⊆ 𝐵))
106		unieq 4874	. . . . . . . . 9 ⊢ (𝑥 = (𝐵 ∖ 𝐹) → ∪ 𝑥 = ∪ (𝐵 ∖ 𝐹))
107	106	eqeq2d 2747	. . . . . . . 8 ⊢ (𝑥 = (𝐵 ∖ 𝐹) → (𝑋 = ∪ 𝑥 ↔ 𝑋 = ∪ (𝐵 ∖ 𝐹)))
108	105, 107	anbi12d 632	. . . . . . 7 ⊢ (𝑥 = (𝐵 ∖ 𝐹) → ((𝑥 ⊆ 𝐵 ∧ 𝑋 = ∪ 𝑥) ↔ ((𝐵 ∖ 𝐹) ⊆ 𝐵 ∧ 𝑋 = ∪ (𝐵 ∖ 𝐹))))
109	108	anbi2d 630	. . . . . 6 ⊢ (𝑥 = (𝐵 ∖ 𝐹) → ((𝜑 ∧ (𝑥 ⊆ 𝐵 ∧ 𝑋 = ∪ 𝑥)) ↔ (𝜑 ∧ ((𝐵 ∖ 𝐹) ⊆ 𝐵 ∧ 𝑋 = ∪ (𝐵 ∖ 𝐹)))))
110		pweq 4568	. . . . . . . 8 ⊢ (𝑥 = (𝐵 ∖ 𝐹) → 𝒫 𝑥 = 𝒫 (𝐵 ∖ 𝐹))
111	110	ineq1d 4171	. . . . . . 7 ⊢ (𝑥 = (𝐵 ∖ 𝐹) → (𝒫 𝑥 ∩ Fin) = (𝒫 (𝐵 ∖ 𝐹) ∩ Fin))
112	111	rexeqdv 3297	. . . . . 6 ⊢ (𝑥 = (𝐵 ∖ 𝐹) → (∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦 ↔ ∃𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)𝑋 = ∪ 𝑦))
113	109, 112	imbi12d 344	. . . . 5 ⊢ (𝑥 = (𝐵 ∖ 𝐹) → (((𝜑 ∧ (𝑥 ⊆ 𝐵 ∧ 𝑋 = ∪ 𝑥)) → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦) ↔ ((𝜑 ∧ ((𝐵 ∖ 𝐹) ⊆ 𝐵 ∧ 𝑋 = ∪ (𝐵 ∖ 𝐹))) → ∃𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)𝑋 = ∪ 𝑦)))
114		alexsub.4	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐵 ∧ 𝑋 = ∪ 𝑥)) → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦)
115	113, 114	vtoclg 3511	. . . 4 ⊢ ((𝐵 ∖ 𝐹) ∈ V → ((𝜑 ∧ ((𝐵 ∖ 𝐹) ⊆ 𝐵 ∧ 𝑋 = ∪ (𝐵 ∖ 𝐹))) → ∃𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)𝑋 = ∪ 𝑦))
116	104, 115	mpcom 38	. . 3 ⊢ ((𝜑 ∧ ((𝐵 ∖ 𝐹) ⊆ 𝐵 ∧ 𝑋 = ∪ (𝐵 ∖ 𝐹))) → ∃𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)𝑋 = ∪ 𝑦)
117	102, 116	mpdan 687	. 2 ⊢ (𝜑 → ∃𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)𝑋 = ∪ 𝑦)
118		unieq 4874	. . . . . . 7 ⊢ (𝑦 = ∅ → ∪ 𝑦 = ∪ ∅)
119		uni0 4891	. . . . . . 7 ⊢ ∪ ∅ = ∅
120	118, 119	eqtrdi 2787	. . . . . 6 ⊢ (𝑦 = ∅ → ∪ 𝑦 = ∅)
121	120	neeq2d 2992	. . . . 5 ⊢ (𝑦 = ∅ → (𝑋 ≠ ∪ 𝑦 ↔ 𝑋 ≠ ∅))
122		difssd 4089	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) → (𝑋 ∖ 𝑧) ⊆ 𝑋)
123	122	ralrimivw 3132	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) → ∀𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧) ⊆ 𝑋)
124		riinn0 5038	. . . . . . . . . 10 ⊢ ((∀𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧) ⊆ 𝑋 ∧ 𝑦 ≠ ∅) → (𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)) = ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧))
125	123, 124	sylan 580	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)) = ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧))
126	14	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑋 ∈ V)
127	126	difexd 5276	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑋 ∖ 𝑧) ∈ V)
128	127	ralrimivw 3132	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ∀𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧) ∈ V)
129		dfiin2g 4986	. . . . . . . . . . 11 ⊢ (∀𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧) ∈ V → ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧) = ∩ {𝑥 ∣ ∃𝑧 ∈ 𝑦 𝑥 = (𝑋 ∖ 𝑧)})
130	128, 129	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧) = ∩ {𝑥 ∣ ∃𝑧 ∈ 𝑦 𝑥 = (𝑋 ∖ 𝑧)})
131		eqid 2736	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) = (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧))
132	131	rnmpt 5906	. . . . . . . . . . 11 ⊢ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) = {𝑥 ∣ ∃𝑧 ∈ 𝑦 𝑥 = (𝑋 ∖ 𝑧)}
133	132	inteqi 4906	. . . . . . . . . 10 ⊢ ∩ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) = ∩ {𝑥 ∣ ∃𝑧 ∈ 𝑦 𝑥 = (𝑋 ∖ 𝑧)}
134	130, 133	eqtr4di 2789	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧) = ∩ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)))
135	125, 134	eqtrd 2771	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)) = ∩ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)))
136	11	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝐹 ∈ (Fil‘𝑋))
137		elfpw 9254	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin) ↔ (𝑦 ⊆ (𝐵 ∖ 𝐹) ∧ 𝑦 ∈ Fin))
138	137	simplbi 497	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin) → 𝑦 ⊆ (𝐵 ∖ 𝐹))
139	138	ad2antlr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑦 ⊆ (𝐵 ∖ 𝐹))
140	139	sselda 3933	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → 𝑧 ∈ (𝐵 ∖ 𝐹))
141	140	eldifbd 3914	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → ¬ 𝑧 ∈ 𝐹)
142	9	ad3antrrr 730	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → 𝐹 ∈ (UFil‘𝑋))
143	139	difss2d 4091	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑦 ⊆ 𝐵)
144	143	sselda 3933	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → 𝑧 ∈ 𝐵)
145		elssuni 4894	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ 𝐵 → 𝑧 ⊆ ∪ 𝐵)
146	144, 145	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → 𝑧 ⊆ ∪ 𝐵)
147	13	ad3antrrr 730	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → 𝑋 = ∪ 𝐵)
148	146, 147	sseqtrrd 3971	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → 𝑧 ⊆ 𝑋)
149		ufilb 23850	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑧 ⊆ 𝑋) → (¬ 𝑧 ∈ 𝐹 ↔ (𝑋 ∖ 𝑧) ∈ 𝐹))
150	142, 148, 149	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → (¬ 𝑧 ∈ 𝐹 ↔ (𝑋 ∖ 𝑧) ∈ 𝐹))
151	141, 150	mpbid 232	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → (𝑋 ∖ 𝑧) ∈ 𝐹)
152	151	fmpttd 7060	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)):𝑦⟶𝐹)
153	152	frnd 6670	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ⊆ 𝐹)
154	131, 151	dmmptd 6637	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → dom (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) = 𝑦)
155		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑦 ≠ ∅)
156	154, 155	eqnetrd 2999	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → dom (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ≠ ∅)
157		dm0rn0 5873	. . . . . . . . . . 11 ⊢ (dom (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) = ∅ ↔ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) = ∅)
158	157	necon3bii 2984	. . . . . . . . . 10 ⊢ (dom (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ≠ ∅ ↔ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ≠ ∅)
159	156, 158	sylib 218	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ≠ ∅)
160		elinel2 4154	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin) → 𝑦 ∈ Fin)
161	160	ad2antlr 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑦 ∈ Fin)
162		abrexfi 9252	. . . . . . . . . . 11 ⊢ (𝑦 ∈ Fin → {𝑥 ∣ ∃𝑧 ∈ 𝑦 𝑥 = (𝑋 ∖ 𝑧)} ∈ Fin)
163	132, 162	eqeltrid 2840	. . . . . . . . . 10 ⊢ (𝑦 ∈ Fin → ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ∈ Fin)
164	161, 163	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ∈ Fin)
165		filintn0 23805	. . . . . . . . 9 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ⊆ 𝐹 ∧ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ≠ ∅ ∧ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ∈ Fin)) → ∩ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ≠ ∅)
166	136, 153, 159, 164, 165	syl13anc 1374	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ∩ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ≠ ∅)
167	135, 166	eqnetrd 2999	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)) ≠ ∅)
168		disj3 4406	. . . . . . . 8 ⊢ ((𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)) = ∅ ↔ 𝑋 = (𝑋 ∖ ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)))
169	168	necon3bii 2984	. . . . . . 7 ⊢ ((𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)) ≠ ∅ ↔ 𝑋 ≠ (𝑋 ∖ ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)))
170	167, 169	sylib 218	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑋 ≠ (𝑋 ∖ ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)))
171		iundif2 5029	. . . . . . 7 ⊢ ∪ 𝑧 ∈ 𝑦 (𝑋 ∖ (𝑋 ∖ 𝑧)) = (𝑋 ∖ ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧))
172		dfss4 4221	. . . . . . . . . 10 ⊢ (𝑧 ⊆ 𝑋 ↔ (𝑋 ∖ (𝑋 ∖ 𝑧)) = 𝑧)
173	148, 172	sylib 218	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → (𝑋 ∖ (𝑋 ∖ 𝑧)) = 𝑧)
174	173	iuneq2dv 4971	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ∪ 𝑧 ∈ 𝑦 (𝑋 ∖ (𝑋 ∖ 𝑧)) = ∪ 𝑧 ∈ 𝑦 𝑧)
175		uniiun 5014	. . . . . . . 8 ⊢ ∪ 𝑦 = ∪ 𝑧 ∈ 𝑦 𝑧
176	174, 175	eqtr4di 2789	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ∪ 𝑧 ∈ 𝑦 (𝑋 ∖ (𝑋 ∖ 𝑧)) = ∪ 𝑦)
177	171, 176	eqtr3id 2785	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑋 ∖ ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)) = ∪ 𝑦)
178	170, 177	neeqtrd 3001	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑋 ≠ ∪ 𝑦)
179	11	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) → 𝐹 ∈ (Fil‘𝑋))
180		filtop 23799	. . . . . 6 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐹)
181		fileln0 23794	. . . . . 6 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑋 ∈ 𝐹) → 𝑋 ≠ ∅)
182	179, 180, 181	syl2anc2 585	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) → 𝑋 ≠ ∅)
183	121, 178, 182	pm2.61ne 3017	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) → 𝑋 ≠ ∪ 𝑦)
184	183	neneqd 2937	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) → ¬ 𝑋 = ∪ 𝑦)
185	184	nrexdv 3131	. 2 ⊢ (𝜑 → ¬ ∃𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)𝑋 = ∪ 𝑦)
186	117, 185	pm2.65i 194	1 ⊢ ¬ 𝜑

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113  {cab 2714   ≠ wne 2932  ∀wral 3051  ∃wrex 3060  Vcvv 3440   ∖ cdif 3898   ∩ cin 3900   ⊆ wss 3901  ∅c0 4285  𝒫 cpw 4554  {csn 4580  ∪ cuni 4863  ∩ cint 4902  ∪ ciun 4946  ∩ ciin 4947   ↦ cmpt 5179  dom cdm 5624  ran crn 5625  ‘cfv 6492  (class class class)co 7358  Fincfn 8883  ficfi 9313  topGenctg 17357  TopOnctopon 22854  TopBasesctb 22889  Filcfil 23789  UFilcufil 23843  UFLcufl 23844   fLim cflim 23878

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-rep 5224  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-int 4903  df-iun 4948  df-iin 4949  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7809  df-1st 7933  df-2nd 7934  df-1o 8397  df-2o 8398  df-en 8884  df-dom 8885  df-fin 8887  df-fi 9314  df-topgen 17363  df-fbas 21306  df-top 22838  df-topon 22855  df-bases 22890  df-ntr 22964  df-nei 23042  df-fil 23790  df-ufil 23845  df-flim 23883

This theorem is referenced by:  alexsub  23989