Theorem alexsublem 23903

Description: Lemma for alexsub 23904. (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 3953	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝑋 ∖ ∪ (𝐵 ∖ 𝐹)) ↔ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹)))
2		alexsub.3	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐽 = (topGen‘(fi‘𝐵)))
3	2	eleq2d 2813	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑦 ∈ 𝐽 ↔ 𝑦 ∈ (topGen‘(fi‘𝐵))))
4	3	anbi1d 629	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦) ↔ (𝑦 ∈ (topGen‘(fi‘𝐵)) ∧ 𝑥 ∈ 𝑦)))
5	4	biimpa 476	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) → (𝑦 ∈ (topGen‘(fi‘𝐵)) ∧ 𝑥 ∈ 𝑦))
6	5	adantlr 712	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) → (𝑦 ∈ (topGen‘(fi‘𝐵)) ∧ 𝑥 ∈ 𝑦))
7		tg2 22823	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ (topGen‘(fi‘𝐵)) ∧ 𝑥 ∈ 𝑦) → ∃𝑧 ∈ (fi‘𝐵)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦))
8	6, 7	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) → ∃𝑧 ∈ (fi‘𝐵)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦))
9		alexsub.5	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹 ∈ (UFil‘𝑋))
10		ufilfil 23763	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 ∈ (UFil‘𝑋) → 𝐹 ∈ (Fil‘𝑋))
11	9, 10	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐹 ∈ (Fil‘𝑋))
12	11	ad3antrrr 727	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦))) → 𝐹 ∈ (Fil‘𝑋))
13		alexsub.2	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑋 = ∪ 𝐵)
14	9	elfvexd 6924	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑋 ∈ V)
15	13, 14	eqeltrrd 2828	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ∪ 𝐵 ∈ V)
16		uniexb 7748	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐵 ∈ V ↔ ∪ 𝐵 ∈ V)
17	15, 16	sylibr 233	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐵 ∈ V)
18		elfi2 9411	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐵 ∈ V → (𝑧 ∈ (fi‘𝐵) ↔ ∃𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})𝑧 = ∩ 𝑦))
19	17, 18	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑧 ∈ (fi‘𝐵) ↔ ∃𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})𝑧 = ∩ 𝑦))
20	19	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) → (𝑧 ∈ (fi‘𝐵) ↔ ∃𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})𝑧 = ∩ 𝑦))
21	11	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦)) → 𝐹 ∈ (Fil‘𝑋))
22		simplrr 775	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) → ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))
23		intss1 4960	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑧 ∈ 𝑦 → ∩ 𝑦 ⊆ 𝑧)
24	23	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦) → ∩ 𝑦 ⊆ 𝑧)
25		simplr 766	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦) → 𝑥 ∈ ∩ 𝑦)
26	24, 25	sseldd 3978	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦) → 𝑥 ∈ 𝑧)
27	26	ad2antlr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) ∧ ¬ 𝑧 ∈ 𝐹) → 𝑥 ∈ 𝑧)
28		eldifsn 4785	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ↔ (𝑦 ∈ (𝒫 𝐵 ∩ Fin) ∧ 𝑦 ≠ ∅))
29	28	simplbi 497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) → 𝑦 ∈ (𝒫 𝐵 ∩ Fin))
30	29	ad2antrl 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦)) → 𝑦 ∈ (𝒫 𝐵 ∩ Fin))
31		elfpw 9356	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑦 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝑦 ⊆ 𝐵 ∧ 𝑦 ∈ Fin))
32	31	simplbi 497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑦 ∈ (𝒫 𝐵 ∩ Fin) → 𝑦 ⊆ 𝐵)
33	30, 32	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦)) → 𝑦 ⊆ 𝐵)
34	33	sselda 3977	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦)) ∧ 𝑧 ∈ 𝑦) → 𝑧 ∈ 𝐵)
35	34	anasss 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) → 𝑧 ∈ 𝐵)
36	35	anim1i 614	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) ∧ ¬ 𝑧 ∈ 𝐹) → (𝑧 ∈ 𝐵 ∧ ¬ 𝑧 ∈ 𝐹))
37		eldif 3953	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑧 ∈ (𝐵 ∖ 𝐹) ↔ (𝑧 ∈ 𝐵 ∧ ¬ 𝑧 ∈ 𝐹))
38	36, 37	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) ∧ ¬ 𝑧 ∈ 𝐹) → 𝑧 ∈ (𝐵 ∖ 𝐹))
39		elunii 4907	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑥 ∈ 𝑧 ∧ 𝑧 ∈ (𝐵 ∖ 𝐹)) → 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))
40	27, 38, 39	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) ∧ ¬ 𝑧 ∈ 𝐹) → 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))
41	40	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) → (¬ 𝑧 ∈ 𝐹 → 𝑥 ∈ ∪ (𝐵 ∖ 𝐹)))
42	22, 41	mt3d 148	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦) ∧ 𝑧 ∈ 𝑦)) → 𝑧 ∈ 𝐹)
43	42	expr 456	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦)) → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝐹))
44	43	ssrdv 3983	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦)) → 𝑦 ⊆ 𝐹)
45		eldifsni 4788	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) → 𝑦 ≠ ∅)
46	45	ad2antrl 725	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦)) → 𝑦 ≠ ∅)
47		elinel2 4191	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 ∈ (𝒫 𝐵 ∩ Fin) → 𝑦 ∈ Fin)
48	30, 47	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦)) → 𝑦 ∈ Fin)
49		elfir 9412	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑦 ⊆ 𝐹 ∧ 𝑦 ≠ ∅ ∧ 𝑦 ∈ Fin)) → ∩ 𝑦 ∈ (fi‘𝐹))
50	21, 44, 46, 48, 49	syl13anc 1369	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦)) → ∩ 𝑦 ∈ (fi‘𝐹))
51		filfi 23718	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐹 ∈ (Fil‘𝑋) → (fi‘𝐹) = 𝐹)
52	21, 51	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦)) → (fi‘𝐹) = 𝐹)
53	50, 52	eleqtrd 2829	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦)) → ∩ 𝑦 ∈ 𝐹)
54	53	expr 456	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ 𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})) → (𝑥 ∈ ∩ 𝑦 → ∩ 𝑦 ∈ 𝐹))
55		eleq2 2816	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 = ∩ 𝑦 → (𝑥 ∈ 𝑧 ↔ 𝑥 ∈ ∩ 𝑦))
56		eleq1 2815	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 = ∩ 𝑦 → (𝑧 ∈ 𝐹 ↔ ∩ 𝑦 ∈ 𝐹))
57	55, 56	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = ∩ 𝑦 → ((𝑥 ∈ 𝑧 → 𝑧 ∈ 𝐹) ↔ (𝑥 ∈ ∩ 𝑦 → ∩ 𝑦 ∈ 𝐹)))
58	54, 57	syl5ibrcom 246	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ 𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})) → (𝑧 = ∩ 𝑦 → (𝑥 ∈ 𝑧 → 𝑧 ∈ 𝐹)))
59	58	rexlimdva 3149	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) → (∃𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})𝑧 = ∩ 𝑦 → (𝑥 ∈ 𝑧 → 𝑧 ∈ 𝐹)))
60	20, 59	sylbid 239	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) → (𝑧 ∈ (fi‘𝐵) → (𝑥 ∈ 𝑧 → 𝑧 ∈ 𝐹)))
61	60	imp32 418	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑧 ∈ (fi‘𝐵) ∧ 𝑥 ∈ 𝑧)) → 𝑧 ∈ 𝐹)
62	61	adantrrr 722	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦))) → 𝑧 ∈ 𝐹)
63	62	adantlr 712	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦))) → 𝑧 ∈ 𝐹)
64		elssuni 4934	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ 𝐽 → 𝑦 ⊆ ∪ 𝐽)
65	64	ad2antrl 725	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) → 𝑦 ⊆ ∪ 𝐽)
66		fibas 22835	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (fi‘𝐵) ∈ TopBases
67		tgtopon 22829	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((fi‘𝐵) ∈ TopBases → (topGen‘(fi‘𝐵)) ∈ (TopOn‘∪ (fi‘𝐵)))
68	66, 67	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (topGen‘(fi‘𝐵)) ∈ (TopOn‘∪ (fi‘𝐵))
69	2, 68	eqeltrdi 2835	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘∪ (fi‘𝐵)))
70		fiuni 9425	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐵 ∈ V → ∪ 𝐵 = ∪ (fi‘𝐵))
71	17, 70	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ∪ 𝐵 = ∪ (fi‘𝐵))
72	13, 71	eqtrd 2766	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑋 = ∪ (fi‘𝐵))
73	72	fveq2d 6889	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (TopOn‘𝑋) = (TopOn‘∪ (fi‘𝐵)))
74	69, 73	eleqtrrd 2830	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))
75		toponuni 22771	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽)
76	74, 75	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑋 = ∪ 𝐽)
77	76	ad2antrr 723	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) → 𝑋 = ∪ 𝐽)
78	65, 77	sseqtrrd 4018	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) → 𝑦 ⊆ 𝑋)
79	78	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦))) → 𝑦 ⊆ 𝑋)
80		simprrr 779	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦))) → 𝑧 ⊆ 𝑦)
81		filss 23712	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑧 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑋 ∧ 𝑧 ⊆ 𝑦)) → 𝑦 ∈ 𝐹)
82	12, 63, 79, 80, 81	syl13anc 1369	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦))) → 𝑦 ∈ 𝐹)
83	8, 82	rexlimddv 3155	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) → 𝑦 ∈ 𝐹)
84	83	expr 456	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ 𝑦 ∈ 𝐽) → (𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹))
85	84	ralrimiva 3140	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) → ∀𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹))
86	85	expr 456	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹) → ∀𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹)))
87	86	imdistanda 571	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹)) → (𝑥 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹))))
88	1, 87	biimtrid 241	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (𝑋 ∖ ∪ (𝐵 ∖ 𝐹)) → (𝑥 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹))))
89		flimopn 23834	. . . . . . . . . 10 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) → (𝑥 ∈ (𝐽 fLim 𝐹) ↔ (𝑥 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹))))
90	74, 11, 89	syl2anc 583	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (𝐽 fLim 𝐹) ↔ (𝑥 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹))))
91	88, 90	sylibrd 259	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (𝑋 ∖ ∪ (𝐵 ∖ 𝐹)) → 𝑥 ∈ (𝐽 fLim 𝐹)))
92	91	ssrdv 3983	. . . . . . 7 ⊢ (𝜑 → (𝑋 ∖ ∪ (𝐵 ∖ 𝐹)) ⊆ (𝐽 fLim 𝐹))
93		alexsub.6	. . . . . . 7 ⊢ (𝜑 → (𝐽 fLim 𝐹) = ∅)
94		sseq0 4394	. . . . . . 7 ⊢ (((𝑋 ∖ ∪ (𝐵 ∖ 𝐹)) ⊆ (𝐽 fLim 𝐹) ∧ (𝐽 fLim 𝐹) = ∅) → (𝑋 ∖ ∪ (𝐵 ∖ 𝐹)) = ∅)
95	92, 93, 94	syl2anc 583	. . . . . 6 ⊢ (𝜑 → (𝑋 ∖ ∪ (𝐵 ∖ 𝐹)) = ∅)
96		ssdif0 4358	. . . . . 6 ⊢ (𝑋 ⊆ ∪ (𝐵 ∖ 𝐹) ↔ (𝑋 ∖ ∪ (𝐵 ∖ 𝐹)) = ∅)
97	95, 96	sylibr 233	. . . . 5 ⊢ (𝜑 → 𝑋 ⊆ ∪ (𝐵 ∖ 𝐹))
98		difss 4126	. . . . . . 7 ⊢ (𝐵 ∖ 𝐹) ⊆ 𝐵
99	98	unissi 4911	. . . . . 6 ⊢ ∪ (𝐵 ∖ 𝐹) ⊆ ∪ 𝐵
100	99, 13	sseqtrrid 4030	. . . . 5 ⊢ (𝜑 → ∪ (𝐵 ∖ 𝐹) ⊆ 𝑋)
101	97, 100	eqssd 3994	. . . 4 ⊢ (𝜑 → 𝑋 = ∪ (𝐵 ∖ 𝐹))
102	101, 98	jctil 519	. . 3 ⊢ (𝜑 → ((𝐵 ∖ 𝐹) ⊆ 𝐵 ∧ 𝑋 = ∪ (𝐵 ∖ 𝐹)))
103	17	difexd 5322	. . . . 5 ⊢ (𝜑 → (𝐵 ∖ 𝐹) ∈ V)
104	103	adantr 480	. . . 4 ⊢ ((𝜑 ∧ ((𝐵 ∖ 𝐹) ⊆ 𝐵 ∧ 𝑋 = ∪ (𝐵 ∖ 𝐹))) → (𝐵 ∖ 𝐹) ∈ V)
105		sseq1 4002	. . . . . . . 8 ⊢ (𝑥 = (𝐵 ∖ 𝐹) → (𝑥 ⊆ 𝐵 ↔ (𝐵 ∖ 𝐹) ⊆ 𝐵))
106		unieq 4913	. . . . . . . . 9 ⊢ (𝑥 = (𝐵 ∖ 𝐹) → ∪ 𝑥 = ∪ (𝐵 ∖ 𝐹))
107	106	eqeq2d 2737	. . . . . . . 8 ⊢ (𝑥 = (𝐵 ∖ 𝐹) → (𝑋 = ∪ 𝑥 ↔ 𝑋 = ∪ (𝐵 ∖ 𝐹)))
108	105, 107	anbi12d 630	. . . . . . 7 ⊢ (𝑥 = (𝐵 ∖ 𝐹) → ((𝑥 ⊆ 𝐵 ∧ 𝑋 = ∪ 𝑥) ↔ ((𝐵 ∖ 𝐹) ⊆ 𝐵 ∧ 𝑋 = ∪ (𝐵 ∖ 𝐹))))
109	108	anbi2d 628	. . . . . 6 ⊢ (𝑥 = (𝐵 ∖ 𝐹) → ((𝜑 ∧ (𝑥 ⊆ 𝐵 ∧ 𝑋 = ∪ 𝑥)) ↔ (𝜑 ∧ ((𝐵 ∖ 𝐹) ⊆ 𝐵 ∧ 𝑋 = ∪ (𝐵 ∖ 𝐹)))))
110		pweq 4611	. . . . . . . 8 ⊢ (𝑥 = (𝐵 ∖ 𝐹) → 𝒫 𝑥 = 𝒫 (𝐵 ∖ 𝐹))
111	110	ineq1d 4206	. . . . . . 7 ⊢ (𝑥 = (𝐵 ∖ 𝐹) → (𝒫 𝑥 ∩ Fin) = (𝒫 (𝐵 ∖ 𝐹) ∩ Fin))
112	111	rexeqdv 3320	. . . . . 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 684	. 2 ⊢ (𝜑 → ∃𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)𝑋 = ∪ 𝑦)
118		unieq 4913	. . . . . . 7 ⊢ (𝑦 = ∅ → ∪ 𝑦 = ∪ ∅)
119		uni0 4932	. . . . . . 7 ⊢ ∪ ∅ = ∅
120	118, 119	eqtrdi 2782	. . . . . 6 ⊢ (𝑦 = ∅ → ∪ 𝑦 = ∅)
121	120	neeq2d 2995	. . . . 5 ⊢ (𝑦 = ∅ → (𝑋 ≠ ∪ 𝑦 ↔ 𝑋 ≠ ∅))
122		difssd 4127	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) → (𝑋 ∖ 𝑧) ⊆ 𝑋)
123	122	ralrimivw 3144	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) → ∀𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧) ⊆ 𝑋)
124		riinn0 5079	. . . . . . . . . 10 ⊢ ((∀𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧) ⊆ 𝑋 ∧ 𝑦 ≠ ∅) → (𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)) = ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧))
125	123, 124	sylan 579	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)) = ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧))
126	14	ad2antrr 723	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑋 ∈ V)
127	126	difexd 5322	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑋 ∖ 𝑧) ∈ V)
128	127	ralrimivw 3144	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ∀𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧) ∈ V)
129		dfiin2g 5028	. . . . . . . . . . 11 ⊢ (∀𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧) ∈ V → ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧) = ∩ {𝑥 ∣ ∃𝑧 ∈ 𝑦 𝑥 = (𝑋 ∖ 𝑧)})
130	128, 129	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧) = ∩ {𝑥 ∣ ∃𝑧 ∈ 𝑦 𝑥 = (𝑋 ∖ 𝑧)})
131		eqid 2726	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) = (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧))
132	131	rnmpt 5948	. . . . . . . . . . 11 ⊢ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) = {𝑥 ∣ ∃𝑧 ∈ 𝑦 𝑥 = (𝑋 ∖ 𝑧)}
133	132	inteqi 4947	. . . . . . . . . 10 ⊢ ∩ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) = ∩ {𝑥 ∣ ∃𝑧 ∈ 𝑦 𝑥 = (𝑋 ∖ 𝑧)}
134	130, 133	eqtr4di 2784	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧) = ∩ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)))
135	125, 134	eqtrd 2766	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)) = ∩ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)))
136	11	ad2antrr 723	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝐹 ∈ (Fil‘𝑋))
137		elfpw 9356	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin) ↔ (𝑦 ⊆ (𝐵 ∖ 𝐹) ∧ 𝑦 ∈ Fin))
138	137	simplbi 497	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin) → 𝑦 ⊆ (𝐵 ∖ 𝐹))
139	138	ad2antlr 724	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑦 ⊆ (𝐵 ∖ 𝐹))
140	139	sselda 3977	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → 𝑧 ∈ (𝐵 ∖ 𝐹))
141	140	eldifbd 3956	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → ¬ 𝑧 ∈ 𝐹)
142	9	ad3antrrr 727	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → 𝐹 ∈ (UFil‘𝑋))
143	139	difss2d 4129	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑦 ⊆ 𝐵)
144	143	sselda 3977	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → 𝑧 ∈ 𝐵)
145		elssuni 4934	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ 𝐵 → 𝑧 ⊆ ∪ 𝐵)
146	144, 145	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → 𝑧 ⊆ ∪ 𝐵)
147	13	ad3antrrr 727	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → 𝑋 = ∪ 𝐵)
148	146, 147	sseqtrrd 4018	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → 𝑧 ⊆ 𝑋)
149		ufilb 23765	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑧 ⊆ 𝑋) → (¬ 𝑧 ∈ 𝐹 ↔ (𝑋 ∖ 𝑧) ∈ 𝐹))
150	142, 148, 149	syl2anc 583	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → (¬ 𝑧 ∈ 𝐹 ↔ (𝑋 ∖ 𝑧) ∈ 𝐹))
151	141, 150	mpbid 231	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → (𝑋 ∖ 𝑧) ∈ 𝐹)
152	151	fmpttd 7110	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)):𝑦⟶𝐹)
153	152	frnd 6719	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ⊆ 𝐹)
154	131, 151	dmmptd 6689	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → dom (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) = 𝑦)
155		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑦 ≠ ∅)
156	154, 155	eqnetrd 3002	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → dom (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ≠ ∅)
157		dm0rn0 5918	. . . . . . . . . . 11 ⊢ (dom (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) = ∅ ↔ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) = ∅)
158	157	necon3bii 2987	. . . . . . . . . 10 ⊢ (dom (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ≠ ∅ ↔ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ≠ ∅)
159	156, 158	sylib 217	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ≠ ∅)
160		elinel2 4191	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin) → 𝑦 ∈ Fin)
161	160	ad2antlr 724	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑦 ∈ Fin)
162		abrexfi 9354	. . . . . . . . . . 11 ⊢ (𝑦 ∈ Fin → {𝑥 ∣ ∃𝑧 ∈ 𝑦 𝑥 = (𝑋 ∖ 𝑧)} ∈ Fin)
163	132, 162	eqeltrid 2831	. . . . . . . . . 10 ⊢ (𝑦 ∈ Fin → ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ∈ Fin)
164	161, 163	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ∈ Fin)
165		filintn0 23720	. . . . . . . . 9 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ⊆ 𝐹 ∧ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ≠ ∅ ∧ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ∈ Fin)) → ∩ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ≠ ∅)
166	136, 153, 159, 164, 165	syl13anc 1369	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ∩ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ≠ ∅)
167	135, 166	eqnetrd 3002	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)) ≠ ∅)
168		disj3 4448	. . . . . . . 8 ⊢ ((𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)) = ∅ ↔ 𝑋 = (𝑋 ∖ ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)))
169	168	necon3bii 2987	. . . . . . 7 ⊢ ((𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)) ≠ ∅ ↔ 𝑋 ≠ (𝑋 ∖ ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)))
170	167, 169	sylib 217	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑋 ≠ (𝑋 ∖ ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)))
171		iundif2 5070	. . . . . . 7 ⊢ ∪ 𝑧 ∈ 𝑦 (𝑋 ∖ (𝑋 ∖ 𝑧)) = (𝑋 ∖ ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧))
172		dfss4 4253	. . . . . . . . . 10 ⊢ (𝑧 ⊆ 𝑋 ↔ (𝑋 ∖ (𝑋 ∖ 𝑧)) = 𝑧)
173	148, 172	sylib 217	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → (𝑋 ∖ (𝑋 ∖ 𝑧)) = 𝑧)
174	173	iuneq2dv 5014	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ∪ 𝑧 ∈ 𝑦 (𝑋 ∖ (𝑋 ∖ 𝑧)) = ∪ 𝑧 ∈ 𝑦 𝑧)
175		uniiun 5054	. . . . . . . 8 ⊢ ∪ 𝑦 = ∪ 𝑧 ∈ 𝑦 𝑧
176	174, 175	eqtr4di 2784	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ∪ 𝑧 ∈ 𝑦 (𝑋 ∖ (𝑋 ∖ 𝑧)) = ∪ 𝑦)
177	171, 176	eqtr3id 2780	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑋 ∖ ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)) = ∪ 𝑦)
178	170, 177	neeqtrd 3004	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑋 ≠ ∪ 𝑦)
179	11	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) → 𝐹 ∈ (Fil‘𝑋))
180		filtop 23714	. . . . . 6 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐹)
181		fileln0 23709	. . . . . 6 ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑋 ∈ 𝐹) → 𝑋 ≠ ∅)
182	179, 180, 181	syl2anc2 584	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) → 𝑋 ≠ ∅)
183	121, 178, 182	pm2.61ne 3021	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) → 𝑋 ≠ ∪ 𝑦)
184	183	neneqd 2939	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) → ¬ 𝑋 = ∪ 𝑦)
185	184	nrexdv 3143	. 2 ⊢ (𝜑 → ¬ ∃𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)𝑋 = ∪ 𝑦)
186	117, 185	pm2.65i 193	1 ⊢ ¬ 𝜑

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1533   ∈ wcel 2098  {cab 2703   ≠ wne 2934  ∀wral 3055  ∃wrex 3064  Vcvv 3468   ∖ cdif 3940   ∩ cin 3942   ⊆ wss 3943  ∅c0 4317  𝒫 cpw 4597  {csn 4623  ∪ cuni 4902  ∩ cint 4943  ∪ ciun 4990  ∩ ciin 4991   ↦ cmpt 5224  dom cdm 5669  ran crn 5670  ‘cfv 6537  (class class class)co 7405  Fincfn 8941  ficfi 9407  topGenctg 17392  TopOnctopon 22767  TopBasesctb 22803  Filcfil 23704  UFilcufil 23758  UFLcufl 23759   fLim cflim 23793

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7722

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-nel 3041  df-ral 3056  df-rex 3065  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-int 4944  df-iun 4992  df-iin 4993  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-ord 6361  df-on 6362  df-lim 6363  df-suc 6364  df-iota 6489  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7853  df-1st 7974  df-2nd 7975  df-1o 8467  df-er 8705  df-en 8942  df-dom 8943  df-fin 8945  df-fi 9408  df-topgen 17398  df-fbas 21237  df-top 22751  df-topon 22768  df-bases 22804  df-ntr 22879  df-nei 22957  df-fil 23705  df-ufil 23760  df-flim 23798

This theorem is referenced by:  alexsub  23904