Theorem alexsublem 23960

Description: Lemma for alexsub 23961. (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 3908	. . . . . . . . . 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 22881	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ (topGen‘(fi‘𝐵)) ∧ 𝑥 ∈ 𝑦) → ∃𝑧 ∈ (fi‘𝐵)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦))
8	6, 7	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) → ∃𝑧 ∈ (fi‘𝐵)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦))
9		alexsub.5	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹 ∈ (UFil‘𝑋))
10		ufilfil 23820	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 ∈ (UFil‘𝑋) → 𝐹 ∈ (Fil‘𝑋))
11	9, 10	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐹 ∈ (Fil‘𝑋))
12	11	ad3antrrr 730	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦))) → 𝐹 ∈ (Fil‘𝑋))
13		alexsub.2	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑋 = ∪ 𝐵)
14	9	elfvexd 6864	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑋 ∈ V)
15	13, 14	eqeltrrd 2834	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ∪ 𝐵 ∈ V)
16		uniexb 7703	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐵 ∈ V ↔ ∪ 𝐵 ∈ V)
17	15, 16	sylibr 234	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐵 ∈ V)
18		elfi2 9305	. . . . . . . . . . . . . . . . . . . . . 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 4913	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑧 ∈ 𝑦 → ∩ 𝑦 ⊆ 𝑧)
24	23	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦) → ∩ 𝑦 ⊆ 𝑧)
25		simplr 768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦) → 𝑥 ∈ ∩ 𝑦)
26	24, 25	sseldd 3931	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦) → 𝑥 ∈ 𝑧)
27	26	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) ∧ ¬ 𝑧 ∈ 𝐹) → 𝑥 ∈ 𝑧)
28		eldifsn 4737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ↔ (𝑦 ∈ (𝒫 𝐵 ∩ Fin) ∧ 𝑦 ≠ ∅))
29	28	simplbi 497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) → 𝑦 ∈ (𝒫 𝐵 ∩ Fin))
30	29	ad2antrl 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦)) → 𝑦 ∈ (𝒫 𝐵 ∩ Fin))
31		elfpw 9245	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑦 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝑦 ⊆ 𝐵 ∧ 𝑦 ∈ Fin))
32	31	simplbi 497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑦 ∈ (𝒫 𝐵 ∩ Fin) → 𝑦 ⊆ 𝐵)
33	30, 32	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦)) → 𝑦 ⊆ 𝐵)
34	33	sselda 3930	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦)) ∧ 𝑧 ∈ 𝑦) → 𝑧 ∈ 𝐵)
35	34	anasss 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) → 𝑧 ∈ 𝐵)
36	35	anim1i 615	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) ∧ ¬ 𝑧 ∈ 𝐹) → (𝑧 ∈ 𝐵 ∧ ¬ 𝑧 ∈ 𝐹))
37		eldif 3908	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑧 ∈ (𝐵 ∖ 𝐹) ↔ (𝑧 ∈ 𝐵 ∧ ¬ 𝑧 ∈ 𝐹))
38	36, 37	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) ∧ ¬ 𝑧 ∈ 𝐹) → 𝑧 ∈ (𝐵 ∖ 𝐹))
39		elunii 4863	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3936	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦)) → 𝑦 ⊆ 𝐹)
45		eldifsni 4741	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) → 𝑦 ≠ ∅)
46	45	ad2antrl 728	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦)) → 𝑦 ≠ ∅)
47		elinel2 4151	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 ∈ (𝒫 𝐵 ∩ Fin) → 𝑦 ∈ Fin)
48	30, 47	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦)) → 𝑦 ∈ Fin)
49		elfir 9306	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑦 ⊆ 𝐹 ∧ 𝑦 ≠ ∅ ∧ 𝑦 ∈ Fin)) → ∩ 𝑦 ∈ (fi‘𝐹))
50	21, 44, 46, 48, 49	syl13anc 1374	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦)) → ∩ 𝑦 ∈ (fi‘𝐹))
51		filfi 23775	. . . . . . . . . . . . . . . . . . . . . . . . 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 3134	. . . . . . . . . . . . . . . . . . . 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 4889	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ 𝐽 → 𝑦 ⊆ ∪ 𝐽)
65	64	ad2antrl 728	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) → 𝑦 ⊆ ∪ 𝐽)
66		fibas 22893	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (fi‘𝐵) ∈ TopBases
67		tgtopon 22887	. . . . . . . . . . . . . . . . . . . . . . 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 9319	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐵 ∈ V → ∪ 𝐵 = ∪ (fi‘𝐵))
71	17, 70	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ∪ 𝐵 = ∪ (fi‘𝐵))
72	13, 71	eqtrd 2768	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑋 = ∪ (fi‘𝐵))
73	72	fveq2d 6832	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (TopOn‘𝑋) = (TopOn‘∪ (fi‘𝐵)))
74	69, 73	eleqtrrd 2836	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))
75		toponuni 22830	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽)
76	74, 75	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑋 = ∪ 𝐽)
77	76	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) → 𝑋 = ∪ 𝐽)
78	65, 77	sseqtrrd 3968	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) → 𝑦 ⊆ 𝑋)
79	78	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦))) → 𝑦 ⊆ 𝑋)
80		simprrr 781	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦))) → 𝑧 ⊆ 𝑦)
81		filss 23769	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑧 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑋 ∧ 𝑧 ⊆ 𝑦)) → 𝑦 ∈ 𝐹)
82	12, 63, 79, 80, 81	syl13anc 1374	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦))) → 𝑦 ∈ 𝐹)
83	8, 82	rexlimddv 3140	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) → 𝑦 ∈ 𝐹)
84	83	expr 456	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ 𝑦 ∈ 𝐽) → (𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹))
85	84	ralrimiva 3125	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) → ∀𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹))
86	85	expr 456	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹) → ∀𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹)))
87	86	imdistanda 571	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹)) → (𝑥 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹))))
88	1, 87	biimtrid 242	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (𝑋 ∖ ∪ (𝐵 ∖ 𝐹)) → (𝑥 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹))))
89		flimopn 23891	. . . . . . . . . 10 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) → (𝑥 ∈ (𝐽 fLim 𝐹) ↔ (𝑥 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹))))
90	74, 11, 89	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (𝐽 fLim 𝐹) ↔ (𝑥 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹))))
91	88, 90	sylibrd 259	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (𝑋 ∖ ∪ (𝐵 ∖ 𝐹)) → 𝑥 ∈ (𝐽 fLim 𝐹)))
92	91	ssrdv 3936	. . . . . . 7 ⊢ (𝜑 → (𝑋 ∖ ∪ (𝐵 ∖ 𝐹)) ⊆ (𝐽 fLim 𝐹))
93		alexsub.6	. . . . . . 7 ⊢ (𝜑 → (𝐽 fLim 𝐹) = ∅)
94		sseq0 4352	. . . . . . 7 ⊢ (((𝑋 ∖ ∪ (𝐵 ∖ 𝐹)) ⊆ (𝐽 fLim 𝐹) ∧ (𝐽 fLim 𝐹) = ∅) → (𝑋 ∖ ∪ (𝐵 ∖ 𝐹)) = ∅)
95	92, 93, 94	syl2anc 584	. . . . . 6 ⊢ (𝜑 → (𝑋 ∖ ∪ (𝐵 ∖ 𝐹)) = ∅)
96		ssdif0 4315	. . . . . 6 ⊢ (𝑋 ⊆ ∪ (𝐵 ∖ 𝐹) ↔ (𝑋 ∖ ∪ (𝐵 ∖ 𝐹)) = ∅)
97	95, 96	sylibr 234	. . . . 5 ⊢ (𝜑 → 𝑋 ⊆ ∪ (𝐵 ∖ 𝐹))
98		difss 4085	. . . . . . 7 ⊢ (𝐵 ∖ 𝐹) ⊆ 𝐵
99	98	unissi 4867	. . . . . 6 ⊢ ∪ (𝐵 ∖ 𝐹) ⊆ ∪ 𝐵
100	99, 13	sseqtrrid 3974	. . . . 5 ⊢ (𝜑 → ∪ (𝐵 ∖ 𝐹) ⊆ 𝑋)
101	97, 100	eqssd 3948	. . . 4 ⊢ (𝜑 → 𝑋 = ∪ (𝐵 ∖ 𝐹))
102	101, 98	jctil 519	. . 3 ⊢ (𝜑 → ((𝐵 ∖ 𝐹) ⊆ 𝐵 ∧ 𝑋 = ∪ (𝐵 ∖ 𝐹)))
103	17	difexd 5271	. . . . 5 ⊢ (𝜑 → (𝐵 ∖ 𝐹) ∈ V)
104	103	adantr 480	. . . 4 ⊢ ((𝜑 ∧ ((𝐵 ∖ 𝐹) ⊆ 𝐵 ∧ 𝑋 = ∪ (𝐵 ∖ 𝐹))) → (𝐵 ∖ 𝐹) ∈ V)
105		sseq1 3956	. . . . . . . 8 ⊢ (𝑥 = (𝐵 ∖ 𝐹) → (𝑥 ⊆ 𝐵 ↔ (𝐵 ∖ 𝐹) ⊆ 𝐵))
106		unieq 4869	. . . . . . . . 9 ⊢ (𝑥 = (𝐵 ∖ 𝐹) → ∪ 𝑥 = ∪ (𝐵 ∖ 𝐹))
107	106	eqeq2d 2744	. . . . . . . 8 ⊢ (𝑥 = (𝐵 ∖ 𝐹) → (𝑋 = ∪ 𝑥 ↔ 𝑋 = ∪ (𝐵 ∖ 𝐹)))
108	105, 107	anbi12d 632	. . . . . . 7 ⊢ (𝑥 = (𝐵 ∖ 𝐹) → ((𝑥 ⊆ 𝐵 ∧ 𝑋 = ∪ 𝑥) ↔ ((𝐵 ∖ 𝐹) ⊆ 𝐵 ∧ 𝑋 = ∪ (𝐵 ∖ 𝐹))))
109	108	anbi2d 630	. . . . . 6 ⊢ (𝑥 = (𝐵 ∖ 𝐹) → ((𝜑 ∧ (𝑥 ⊆ 𝐵 ∧ 𝑋 = ∪ 𝑥)) ↔ (𝜑 ∧ ((𝐵 ∖ 𝐹) ⊆ 𝐵 ∧ 𝑋 = ∪ (𝐵 ∖ 𝐹)))))
110		pweq 4563	. . . . . . . 8 ⊢ (𝑥 = (𝐵 ∖ 𝐹) → 𝒫 𝑥 = 𝒫 (𝐵 ∖ 𝐹))
111	110	ineq1d 4168	. . . . . . 7 ⊢ (𝑥 = (𝐵 ∖ 𝐹) → (𝒫 𝑥 ∩ Fin) = (𝒫 (𝐵 ∖ 𝐹) ∩ Fin))
112	111	rexeqdv 3294	. . . . . 6 ⊢ (𝑥 = (𝐵 ∖ 𝐹) → (∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦 ↔ ∃𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)𝑋 = ∪ 𝑦))
113	109, 112	imbi12d 344	. . . . 5 ⊢ (𝑥 = (𝐵 ∖ 𝐹) → (((𝜑 ∧ (𝑥 ⊆ 𝐵 ∧ 𝑋 = ∪ 𝑥)) → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦) ↔ ((𝜑 ∧ ((𝐵 ∖ 𝐹) ⊆ 𝐵 ∧ 𝑋 = ∪ (𝐵 ∖ 𝐹))) → ∃𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)𝑋 = ∪ 𝑦)))
114		alexsub.4	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐵 ∧ 𝑋 = ∪ 𝑥)) → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦)
115	113, 114	vtoclg 3508	. . . 4 ⊢ ((𝐵 ∖ 𝐹) ∈ V → ((𝜑 ∧ ((𝐵 ∖ 𝐹) ⊆ 𝐵 ∧ 𝑋 = ∪ (𝐵 ∖ 𝐹))) → ∃𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)𝑋 = ∪ 𝑦))
116	104, 115	mpcom 38	. . 3 ⊢ ((𝜑 ∧ ((𝐵 ∖ 𝐹) ⊆ 𝐵 ∧ 𝑋 = ∪ (𝐵 ∖ 𝐹))) → ∃𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)𝑋 = ∪ 𝑦)
117	102, 116	mpdan 687	. 2 ⊢ (𝜑 → ∃𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)𝑋 = ∪ 𝑦)
118		unieq 4869	. . . . . . 7 ⊢ (𝑦 = ∅ → ∪ 𝑦 = ∪ ∅)
119		uni0 4886	. . . . . . 7 ⊢ ∪ ∅ = ∅
120	118, 119	eqtrdi 2784	. . . . . 6 ⊢ (𝑦 = ∅ → ∪ 𝑦 = ∅)
121	120	neeq2d 2989	. . . . 5 ⊢ (𝑦 = ∅ → (𝑋 ≠ ∪ 𝑦 ↔ 𝑋 ≠ ∅))
122		difssd 4086	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) → (𝑋 ∖ 𝑧) ⊆ 𝑋)
123	122	ralrimivw 3129	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) → ∀𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧) ⊆ 𝑋)
124		riinn0 5033	. . . . . . . . . 10 ⊢ ((∀𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧) ⊆ 𝑋 ∧ 𝑦 ≠ ∅) → (𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)) = ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧))
125	123, 124	sylan 580	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)) = ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧))
126	14	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑋 ∈ V)
127	126	difexd 5271	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑋 ∖ 𝑧) ∈ V)
128	127	ralrimivw 3129	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ∀𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧) ∈ V)
129		dfiin2g 4981	. . . . . . . . . . 11 ⊢ (∀𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧) ∈ V → ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧) = ∩ {𝑥 ∣ ∃𝑧 ∈ 𝑦 𝑥 = (𝑋 ∖ 𝑧)})
130	128, 129	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧) = ∩ {𝑥 ∣ ∃𝑧 ∈ 𝑦 𝑥 = (𝑋 ∖ 𝑧)})
131		eqid 2733	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) = (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧))
132	131	rnmpt 5901	. . . . . . . . . . 11 ⊢ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) = {𝑥 ∣ ∃𝑧 ∈ 𝑦 𝑥 = (𝑋 ∖ 𝑧)}
133	132	inteqi 4901	. . . . . . . . . 10 ⊢ ∩ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) = ∩ {𝑥 ∣ ∃𝑧 ∈ 𝑦 𝑥 = (𝑋 ∖ 𝑧)}
134	130, 133	eqtr4di 2786	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧) = ∩ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)))
135	125, 134	eqtrd 2768	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)) = ∩ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)))
136	11	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝐹 ∈ (Fil‘𝑋))
137		elfpw 9245	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin) ↔ (𝑦 ⊆ (𝐵 ∖ 𝐹) ∧ 𝑦 ∈ Fin))
138	137	simplbi 497	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin) → 𝑦 ⊆ (𝐵 ∖ 𝐹))
139	138	ad2antlr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑦 ⊆ (𝐵 ∖ 𝐹))
140	139	sselda 3930	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → 𝑧 ∈ (𝐵 ∖ 𝐹))
141	140	eldifbd 3911	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → ¬ 𝑧 ∈ 𝐹)
142	9	ad3antrrr 730	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → 𝐹 ∈ (UFil‘𝑋))
143	139	difss2d 4088	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑦 ⊆ 𝐵)
144	143	sselda 3930	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → 𝑧 ∈ 𝐵)
145		elssuni 4889	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ 𝐵 → 𝑧 ⊆ ∪ 𝐵)
146	144, 145	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → 𝑧 ⊆ ∪ 𝐵)
147	13	ad3antrrr 730	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → 𝑋 = ∪ 𝐵)
148	146, 147	sseqtrrd 3968	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → 𝑧 ⊆ 𝑋)
149		ufilb 23822	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑧 ⊆ 𝑋) → (¬ 𝑧 ∈ 𝐹 ↔ (𝑋 ∖ 𝑧) ∈ 𝐹))
150	142, 148, 149	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → (¬ 𝑧 ∈ 𝐹 ↔ (𝑋 ∖ 𝑧) ∈ 𝐹))
151	141, 150	mpbid 232	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → (𝑋 ∖ 𝑧) ∈ 𝐹)
152	151	fmpttd 7054	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)):𝑦⟶𝐹)
153	152	frnd 6664	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ⊆ 𝐹)
154	131, 151	dmmptd 6631	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → dom (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) = 𝑦)
155		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑦 ≠ ∅)
156	154, 155	eqnetrd 2996	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → dom (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ≠ ∅)
157		dm0rn0 5868	. . . . . . . . . . 11 ⊢ (dom (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) = ∅ ↔ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) = ∅)
158	157	necon3bii 2981	. . . . . . . . . 10 ⊢ (dom (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ≠ ∅ ↔ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ≠ ∅)
159	156, 158	sylib 218	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ≠ ∅)
160		elinel2 4151	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin) → 𝑦 ∈ Fin)
161	160	ad2antlr 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑦 ∈ Fin)
162		abrexfi 9243	. . . . . . . . . . 11 ⊢ (𝑦 ∈ Fin → {𝑥 ∣ ∃𝑧 ∈ 𝑦 𝑥 = (𝑋 ∖ 𝑧)} ∈ Fin)
163	132, 162	eqeltrid 2837	. . . . . . . . . 10 ⊢ (𝑦 ∈ Fin → ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ∈ Fin)
164	161, 163	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ∈ Fin)
165		filintn0 23777	. . . . . . . . 9 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ⊆ 𝐹 ∧ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ≠ ∅ ∧ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ∈ Fin)) → ∩ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ≠ ∅)
166	136, 153, 159, 164, 165	syl13anc 1374	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ∩ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ≠ ∅)
167	135, 166	eqnetrd 2996	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)) ≠ ∅)
168		disj3 4403	. . . . . . . 8 ⊢ ((𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)) = ∅ ↔ 𝑋 = (𝑋 ∖ ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)))
169	168	necon3bii 2981	. . . . . . 7 ⊢ ((𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)) ≠ ∅ ↔ 𝑋 ≠ (𝑋 ∖ ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)))
170	167, 169	sylib 218	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑋 ≠ (𝑋 ∖ ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)))
171		iundif2 5024	. . . . . . 7 ⊢ ∪ 𝑧 ∈ 𝑦 (𝑋 ∖ (𝑋 ∖ 𝑧)) = (𝑋 ∖ ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧))
172		dfss4 4218	. . . . . . . . . 10 ⊢ (𝑧 ⊆ 𝑋 ↔ (𝑋 ∖ (𝑋 ∖ 𝑧)) = 𝑧)
173	148, 172	sylib 218	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → (𝑋 ∖ (𝑋 ∖ 𝑧)) = 𝑧)
174	173	iuneq2dv 4966	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ∪ 𝑧 ∈ 𝑦 (𝑋 ∖ (𝑋 ∖ 𝑧)) = ∪ 𝑧 ∈ 𝑦 𝑧)
175		uniiun 5009	. . . . . . . 8 ⊢ ∪ 𝑦 = ∪ 𝑧 ∈ 𝑦 𝑧
176	174, 175	eqtr4di 2786	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ∪ 𝑧 ∈ 𝑦 (𝑋 ∖ (𝑋 ∖ 𝑧)) = ∪ 𝑦)
177	171, 176	eqtr3id 2782	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑋 ∖ ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)) = ∪ 𝑦)
178	170, 177	neeqtrd 2998	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑋 ≠ ∪ 𝑦)
179	11	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) → 𝐹 ∈ (Fil‘𝑋))
180		filtop 23771	. . . . . 6 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐹)
181		fileln0 23766	. . . . . 6 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑋 ∈ 𝐹) → 𝑋 ≠ ∅)
182	179, 180, 181	syl2anc2 585	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) → 𝑋 ≠ ∅)
183	121, 178, 182	pm2.61ne 3014	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) → 𝑋 ≠ ∪ 𝑦)
184	183	neneqd 2934	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) → ¬ 𝑋 = ∪ 𝑦)
185	184	nrexdv 3128	. 2 ⊢ (𝜑 → ¬ ∃𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)𝑋 = ∪ 𝑦)
186	117, 185	pm2.65i 194	1 ⊢ ¬ 𝜑

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113  {cab 2711   ≠ wne 2929  ∀wral 3048  ∃wrex 3057  Vcvv 3437   ∖ cdif 3895   ∩ cin 3897   ⊆ wss 3898  ∅c0 4282  𝒫 cpw 4549  {csn 4575  ∪ cuni 4858  ∩ cint 4897  ∪ ciun 4941  ∩ ciin 4942   ↦ cmpt 5174  dom cdm 5619  ran crn 5620  ‘cfv 6486  (class class class)co 7352  Fincfn 8875  ficfi 9301  topGenctg 17343  TopOnctopon 22826  TopBasesctb 22861  Filcfil 23761  UFilcufil 23815  UFLcufl 23816   fLim cflim 23850

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 2182  ax-ext 2705  ax-rep 5219  ax-sep 5236  ax-nul 5246  ax-pow 5305  ax-pr 5372  ax-un 7674

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 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-int 4898  df-iun 4943  df-iin 4944  df-br 5094  df-opab 5156  df-mpt 5175  df-tr 5201  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-ov 7355  df-oprab 7356  df-mpo 7357  df-om 7803  df-1st 7927  df-2nd 7928  df-1o 8391  df-2o 8392  df-en 8876  df-dom 8877  df-fin 8879  df-fi 9302  df-topgen 17349  df-fbas 21290  df-top 22810  df-topon 22827  df-bases 22862  df-ntr 22936  df-nei 23014  df-fil 23762  df-ufil 23817  df-flim 23855

This theorem is referenced by:  alexsub  23961