MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  alexsublem Structured version   Visualization version   GIF version

Theorem alexsublem 24052
Description: Lemma for alexsub 24053. (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.
StepHypRef Expression
1 eldif 3961 . . . . . . . . . 10 (𝑥 ∈ (𝑋 (𝐵𝐹)) ↔ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹)))
2 alexsub.3 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐽 = (topGen‘(fi‘𝐵)))
32eleq2d 2827 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑦𝐽𝑦 ∈ (topGen‘(fi‘𝐵))))
43anbi1d 631 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑦𝐽𝑥𝑦) ↔ (𝑦 ∈ (topGen‘(fi‘𝐵)) ∧ 𝑥𝑦)))
54biimpa 476 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑦𝐽𝑥𝑦)) → (𝑦 ∈ (topGen‘(fi‘𝐵)) ∧ 𝑥𝑦))
65adantlr 715 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦𝐽𝑥𝑦)) → (𝑦 ∈ (topGen‘(fi‘𝐵)) ∧ 𝑥𝑦))
7 tg2 22972 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ (topGen‘(fi‘𝐵)) ∧ 𝑥𝑦) → ∃𝑧 ∈ (fi‘𝐵)(𝑥𝑧𝑧𝑦))
86, 7syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦𝐽𝑥𝑦)) → ∃𝑧 ∈ (fi‘𝐵)(𝑥𝑧𝑧𝑦))
9 alexsub.5 . . . . . . . . . . . . . . . . . 18 (𝜑𝐹 ∈ (UFil‘𝑋))
10 ufilfil 23912 . . . . . . . . . . . . . . . . . 18 (𝐹 ∈ (UFil‘𝑋) → 𝐹 ∈ (Fil‘𝑋))
119, 10syl 17 . . . . . . . . . . . . . . . . 17 (𝜑𝐹 ∈ (Fil‘𝑋))
1211ad3antrrr 730 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦𝐽𝑥𝑦)) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥𝑧𝑧𝑦))) → 𝐹 ∈ (Fil‘𝑋))
13 alexsub.2 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑋 = 𝐵)
149elfvexd 6945 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑋 ∈ V)
1513, 14eqeltrrd 2842 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 𝐵 ∈ V)
16 uniexb 7784 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐵 ∈ V ↔ 𝐵 ∈ V)
1715, 16sylibr 234 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐵 ∈ V)
18 elfi2 9454 . . . . . . . . . . . . . . . . . . . . . 22 (𝐵 ∈ V → (𝑧 ∈ (fi‘𝐵) ↔ ∃𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})𝑧 = 𝑦))
1917, 18syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑧 ∈ (fi‘𝐵) ↔ ∃𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})𝑧 = 𝑦))
2019adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) → (𝑧 ∈ (fi‘𝐵) ↔ ∃𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})𝑧 = 𝑦))
2111ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦)) → 𝐹 ∈ (Fil‘𝑋))
22 simplrr 778 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦) ∧ 𝑧𝑦)) → ¬ 𝑥 (𝐵𝐹))
23 intss1 4963 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧𝑦 𝑦𝑧)
2423adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦) ∧ 𝑧𝑦) → 𝑦𝑧)
25 simplr 769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦) ∧ 𝑧𝑦) → 𝑥 𝑦)
2624, 25sseldd 3984 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦) ∧ 𝑧𝑦) → 𝑥𝑧)
2726ad2antlr 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦) ∧ 𝑧𝑦)) ∧ ¬ 𝑧𝐹) → 𝑥𝑧)
28 eldifsn 4786 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ↔ (𝑦 ∈ (𝒫 𝐵 ∩ Fin) ∧ 𝑦 ≠ ∅))
2928simplbi 497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) → 𝑦 ∈ (𝒫 𝐵 ∩ Fin))
3029ad2antrl 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦)) → 𝑦 ∈ (𝒫 𝐵 ∩ Fin))
31 elfpw 9394 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝑦𝐵𝑦 ∈ Fin))
3231simplbi 497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 ∈ (𝒫 𝐵 ∩ Fin) → 𝑦𝐵)
3330, 32syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦)) → 𝑦𝐵)
3433sselda 3983 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦)) ∧ 𝑧𝑦) → 𝑧𝐵)
3534anasss 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦) ∧ 𝑧𝑦)) → 𝑧𝐵)
3635anim1i 615 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦) ∧ 𝑧𝑦)) ∧ ¬ 𝑧𝐹) → (𝑧𝐵 ∧ ¬ 𝑧𝐹))
37 eldif 3961 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑧 ∈ (𝐵𝐹) ↔ (𝑧𝐵 ∧ ¬ 𝑧𝐹))
3836, 37sylibr 234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦) ∧ 𝑧𝑦)) ∧ ¬ 𝑧𝐹) → 𝑧 ∈ (𝐵𝐹))
39 elunii 4912 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑥𝑧𝑧 ∈ (𝐵𝐹)) → 𝑥 (𝐵𝐹))
4027, 38, 39syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦) ∧ 𝑧𝑦)) ∧ ¬ 𝑧𝐹) → 𝑥 (𝐵𝐹))
4140ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦) ∧ 𝑧𝑦)) → (¬ 𝑧𝐹𝑥 (𝐵𝐹)))
4222, 41mt3d 148 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦) ∧ 𝑧𝑦)) → 𝑧𝐹)
4342expr 456 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦)) → (𝑧𝑦𝑧𝐹))
4443ssrdv 3989 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦)) → 𝑦𝐹)
45 eldifsni 4790 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) → 𝑦 ≠ ∅)
4645ad2antrl 728 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦)) → 𝑦 ≠ ∅)
47 elinel2 4202 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ (𝒫 𝐵 ∩ Fin) → 𝑦 ∈ Fin)
4830, 47syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦)) → 𝑦 ∈ Fin)
49 elfir 9455 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑦𝐹𝑦 ≠ ∅ ∧ 𝑦 ∈ Fin)) → 𝑦 ∈ (fi‘𝐹))
5021, 44, 46, 48, 49syl13anc 1374 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦)) → 𝑦 ∈ (fi‘𝐹))
51 filfi 23867 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐹 ∈ (Fil‘𝑋) → (fi‘𝐹) = 𝐹)
5221, 51syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦)) → (fi‘𝐹) = 𝐹)
5350, 52eleqtrd 2843 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦)) → 𝑦𝐹)
5453expr 456 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ 𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})) → (𝑥 𝑦 𝑦𝐹))
55 eleq2 2830 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = 𝑦 → (𝑥𝑧𝑥 𝑦))
56 eleq1 2829 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = 𝑦 → (𝑧𝐹 𝑦𝐹))
5755, 56imbi12d 344 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = 𝑦 → ((𝑥𝑧𝑧𝐹) ↔ (𝑥 𝑦 𝑦𝐹)))
5854, 57syl5ibrcom 247 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ 𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})) → (𝑧 = 𝑦 → (𝑥𝑧𝑧𝐹)))
5958rexlimdva 3155 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) → (∃𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})𝑧 = 𝑦 → (𝑥𝑧𝑧𝐹)))
6020, 59sylbid 240 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) → (𝑧 ∈ (fi‘𝐵) → (𝑥𝑧𝑧𝐹)))
6160imp32 418 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑧 ∈ (fi‘𝐵) ∧ 𝑥𝑧)) → 𝑧𝐹)
6261adantrrr 725 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥𝑧𝑧𝑦))) → 𝑧𝐹)
6362adantlr 715 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦𝐽𝑥𝑦)) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥𝑧𝑧𝑦))) → 𝑧𝐹)
64 elssuni 4937 . . . . . . . . . . . . . . . . . . 19 (𝑦𝐽𝑦 𝐽)
6564ad2antrl 728 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦𝐽𝑥𝑦)) → 𝑦 𝐽)
66 fibas 22984 . . . . . . . . . . . . . . . . . . . . . . 23 (fi‘𝐵) ∈ TopBases
67 tgtopon 22978 . . . . . . . . . . . . . . . . . . . . . . 23 ((fi‘𝐵) ∈ TopBases → (topGen‘(fi‘𝐵)) ∈ (TopOn‘ (fi‘𝐵)))
6866, 67ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 (topGen‘(fi‘𝐵)) ∈ (TopOn‘ (fi‘𝐵))
692, 68eqeltrdi 2849 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐽 ∈ (TopOn‘ (fi‘𝐵)))
70 fiuni 9468 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐵 ∈ V → 𝐵 = (fi‘𝐵))
7117, 70syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 𝐵 = (fi‘𝐵))
7213, 71eqtrd 2777 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑋 = (fi‘𝐵))
7372fveq2d 6910 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (TopOn‘𝑋) = (TopOn‘ (fi‘𝐵)))
7469, 73eleqtrrd 2844 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐽 ∈ (TopOn‘𝑋))
75 toponuni 22920 . . . . . . . . . . . . . . . . . . . 20 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
7674, 75syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑋 = 𝐽)
7776ad2antrr 726 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦𝐽𝑥𝑦)) → 𝑋 = 𝐽)
7865, 77sseqtrrd 4021 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦𝐽𝑥𝑦)) → 𝑦𝑋)
7978adantr 480 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦𝐽𝑥𝑦)) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥𝑧𝑧𝑦))) → 𝑦𝑋)
80 simprrr 782 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦𝐽𝑥𝑦)) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥𝑧𝑧𝑦))) → 𝑧𝑦)
81 filss 23861 . . . . . . . . . . . . . . . 16 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑧𝐹𝑦𝑋𝑧𝑦)) → 𝑦𝐹)
8212, 63, 79, 80, 81syl13anc 1374 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦𝐽𝑥𝑦)) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥𝑧𝑧𝑦))) → 𝑦𝐹)
838, 82rexlimddv 3161 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦𝐽𝑥𝑦)) → 𝑦𝐹)
8483expr 456 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ 𝑦𝐽) → (𝑥𝑦𝑦𝐹))
8584ralrimiva 3146 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) → ∀𝑦𝐽 (𝑥𝑦𝑦𝐹))
8685expr 456 . . . . . . . . . . 11 ((𝜑𝑥𝑋) → (¬ 𝑥 (𝐵𝐹) → ∀𝑦𝐽 (𝑥𝑦𝑦𝐹)))
8786imdistanda 571 . . . . . . . . . 10 (𝜑 → ((𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹)) → (𝑥𝑋 ∧ ∀𝑦𝐽 (𝑥𝑦𝑦𝐹))))
881, 87biimtrid 242 . . . . . . . . 9 (𝜑 → (𝑥 ∈ (𝑋 (𝐵𝐹)) → (𝑥𝑋 ∧ ∀𝑦𝐽 (𝑥𝑦𝑦𝐹))))
89 flimopn 23983 . . . . . . . . . 10 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) → (𝑥 ∈ (𝐽 fLim 𝐹) ↔ (𝑥𝑋 ∧ ∀𝑦𝐽 (𝑥𝑦𝑦𝐹))))
9074, 11, 89syl2anc 584 . . . . . . . . 9 (𝜑 → (𝑥 ∈ (𝐽 fLim 𝐹) ↔ (𝑥𝑋 ∧ ∀𝑦𝐽 (𝑥𝑦𝑦𝐹))))
9188, 90sylibrd 259 . . . . . . . 8 (𝜑 → (𝑥 ∈ (𝑋 (𝐵𝐹)) → 𝑥 ∈ (𝐽 fLim 𝐹)))
9291ssrdv 3989 . . . . . . 7 (𝜑 → (𝑋 (𝐵𝐹)) ⊆ (𝐽 fLim 𝐹))
93 alexsub.6 . . . . . . 7 (𝜑 → (𝐽 fLim 𝐹) = ∅)
94 sseq0 4403 . . . . . . 7 (((𝑋 (𝐵𝐹)) ⊆ (𝐽 fLim 𝐹) ∧ (𝐽 fLim 𝐹) = ∅) → (𝑋 (𝐵𝐹)) = ∅)
9592, 93, 94syl2anc 584 . . . . . 6 (𝜑 → (𝑋 (𝐵𝐹)) = ∅)
96 ssdif0 4366 . . . . . 6 (𝑋 (𝐵𝐹) ↔ (𝑋 (𝐵𝐹)) = ∅)
9795, 96sylibr 234 . . . . 5 (𝜑𝑋 (𝐵𝐹))
98 difss 4136 . . . . . . 7 (𝐵𝐹) ⊆ 𝐵
9998unissi 4916 . . . . . 6 (𝐵𝐹) ⊆ 𝐵
10099, 13sseqtrrid 4027 . . . . 5 (𝜑 (𝐵𝐹) ⊆ 𝑋)
10197, 100eqssd 4001 . . . 4 (𝜑𝑋 = (𝐵𝐹))
102101, 98jctil 519 . . 3 (𝜑 → ((𝐵𝐹) ⊆ 𝐵𝑋 = (𝐵𝐹)))
10317difexd 5331 . . . . 5 (𝜑 → (𝐵𝐹) ∈ V)
104103adantr 480 . . . 4 ((𝜑 ∧ ((𝐵𝐹) ⊆ 𝐵𝑋 = (𝐵𝐹))) → (𝐵𝐹) ∈ V)
105 sseq1 4009 . . . . . . . 8 (𝑥 = (𝐵𝐹) → (𝑥𝐵 ↔ (𝐵𝐹) ⊆ 𝐵))
106 unieq 4918 . . . . . . . . 9 (𝑥 = (𝐵𝐹) → 𝑥 = (𝐵𝐹))
107106eqeq2d 2748 . . . . . . . 8 (𝑥 = (𝐵𝐹) → (𝑋 = 𝑥𝑋 = (𝐵𝐹)))
108105, 107anbi12d 632 . . . . . . 7 (𝑥 = (𝐵𝐹) → ((𝑥𝐵𝑋 = 𝑥) ↔ ((𝐵𝐹) ⊆ 𝐵𝑋 = (𝐵𝐹))))
109108anbi2d 630 . . . . . 6 (𝑥 = (𝐵𝐹) → ((𝜑 ∧ (𝑥𝐵𝑋 = 𝑥)) ↔ (𝜑 ∧ ((𝐵𝐹) ⊆ 𝐵𝑋 = (𝐵𝐹)))))
110 pweq 4614 . . . . . . . 8 (𝑥 = (𝐵𝐹) → 𝒫 𝑥 = 𝒫 (𝐵𝐹))
111110ineq1d 4219 . . . . . . 7 (𝑥 = (𝐵𝐹) → (𝒫 𝑥 ∩ Fin) = (𝒫 (𝐵𝐹) ∩ Fin))
112111rexeqdv 3327 . . . . . 6 (𝑥 = (𝐵𝐹) → (∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = 𝑦 ↔ ∃𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)𝑋 = 𝑦))
113109, 112imbi12d 344 . . . . 5 (𝑥 = (𝐵𝐹) → (((𝜑 ∧ (𝑥𝐵𝑋 = 𝑥)) → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = 𝑦) ↔ ((𝜑 ∧ ((𝐵𝐹) ⊆ 𝐵𝑋 = (𝐵𝐹))) → ∃𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)𝑋 = 𝑦)))
114 alexsub.4 . . . . 5 ((𝜑 ∧ (𝑥𝐵𝑋 = 𝑥)) → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = 𝑦)
115113, 114vtoclg 3554 . . . 4 ((𝐵𝐹) ∈ V → ((𝜑 ∧ ((𝐵𝐹) ⊆ 𝐵𝑋 = (𝐵𝐹))) → ∃𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)𝑋 = 𝑦))
116104, 115mpcom 38 . . 3 ((𝜑 ∧ ((𝐵𝐹) ⊆ 𝐵𝑋 = (𝐵𝐹))) → ∃𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)𝑋 = 𝑦)
117102, 116mpdan 687 . 2 (𝜑 → ∃𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)𝑋 = 𝑦)
118 unieq 4918 . . . . . . 7 (𝑦 = ∅ → 𝑦 = ∅)
119 uni0 4935 . . . . . . 7 ∅ = ∅
120118, 119eqtrdi 2793 . . . . . 6 (𝑦 = ∅ → 𝑦 = ∅)
121120neeq2d 3001 . . . . 5 (𝑦 = ∅ → (𝑋 𝑦𝑋 ≠ ∅))
122 difssd 4137 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) → (𝑋𝑧) ⊆ 𝑋)
123122ralrimivw 3150 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) → ∀𝑧𝑦 (𝑋𝑧) ⊆ 𝑋)
124 riinn0 5083 . . . . . . . . . 10 ((∀𝑧𝑦 (𝑋𝑧) ⊆ 𝑋𝑦 ≠ ∅) → (𝑋 𝑧𝑦 (𝑋𝑧)) = 𝑧𝑦 (𝑋𝑧))
125123, 124sylan 580 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑋 𝑧𝑦 (𝑋𝑧)) = 𝑧𝑦 (𝑋𝑧))
12614ad2antrr 726 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑋 ∈ V)
127126difexd 5331 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑋𝑧) ∈ V)
128127ralrimivw 3150 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ∀𝑧𝑦 (𝑋𝑧) ∈ V)
129 dfiin2g 5032 . . . . . . . . . . 11 (∀𝑧𝑦 (𝑋𝑧) ∈ V → 𝑧𝑦 (𝑋𝑧) = {𝑥 ∣ ∃𝑧𝑦 𝑥 = (𝑋𝑧)})
130128, 129syl 17 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑧𝑦 (𝑋𝑧) = {𝑥 ∣ ∃𝑧𝑦 𝑥 = (𝑋𝑧)})
131 eqid 2737 . . . . . . . . . . . 12 (𝑧𝑦 ↦ (𝑋𝑧)) = (𝑧𝑦 ↦ (𝑋𝑧))
132131rnmpt 5968 . . . . . . . . . . 11 ran (𝑧𝑦 ↦ (𝑋𝑧)) = {𝑥 ∣ ∃𝑧𝑦 𝑥 = (𝑋𝑧)}
133132inteqi 4950 . . . . . . . . . 10 ran (𝑧𝑦 ↦ (𝑋𝑧)) = {𝑥 ∣ ∃𝑧𝑦 𝑥 = (𝑋𝑧)}
134130, 133eqtr4di 2795 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑧𝑦 (𝑋𝑧) = ran (𝑧𝑦 ↦ (𝑋𝑧)))
135125, 134eqtrd 2777 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑋 𝑧𝑦 (𝑋𝑧)) = ran (𝑧𝑦 ↦ (𝑋𝑧)))
13611ad2antrr 726 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝐹 ∈ (Fil‘𝑋))
137 elfpw 9394 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin) ↔ (𝑦 ⊆ (𝐵𝐹) ∧ 𝑦 ∈ Fin))
138137simplbi 497 . . . . . . . . . . . . . . 15 (𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin) → 𝑦 ⊆ (𝐵𝐹))
139138ad2antlr 727 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑦 ⊆ (𝐵𝐹))
140139sselda 3983 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧𝑦) → 𝑧 ∈ (𝐵𝐹))
141140eldifbd 3964 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧𝑦) → ¬ 𝑧𝐹)
1429ad3antrrr 730 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧𝑦) → 𝐹 ∈ (UFil‘𝑋))
143139difss2d 4139 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑦𝐵)
144143sselda 3983 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧𝑦) → 𝑧𝐵)
145 elssuni 4937 . . . . . . . . . . . . . . 15 (𝑧𝐵𝑧 𝐵)
146144, 145syl 17 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧𝑦) → 𝑧 𝐵)
14713ad3antrrr 730 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧𝑦) → 𝑋 = 𝐵)
148146, 147sseqtrrd 4021 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧𝑦) → 𝑧𝑋)
149 ufilb 23914 . . . . . . . . . . . . 13 ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑧𝑋) → (¬ 𝑧𝐹 ↔ (𝑋𝑧) ∈ 𝐹))
150142, 148, 149syl2anc 584 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧𝑦) → (¬ 𝑧𝐹 ↔ (𝑋𝑧) ∈ 𝐹))
151141, 150mpbid 232 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧𝑦) → (𝑋𝑧) ∈ 𝐹)
152151fmpttd 7135 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑧𝑦 ↦ (𝑋𝑧)):𝑦𝐹)
153152frnd 6744 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ran (𝑧𝑦 ↦ (𝑋𝑧)) ⊆ 𝐹)
154131, 151dmmptd 6713 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → dom (𝑧𝑦 ↦ (𝑋𝑧)) = 𝑦)
155 simpr 484 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑦 ≠ ∅)
156154, 155eqnetrd 3008 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → dom (𝑧𝑦 ↦ (𝑋𝑧)) ≠ ∅)
157 dm0rn0 5935 . . . . . . . . . . 11 (dom (𝑧𝑦 ↦ (𝑋𝑧)) = ∅ ↔ ran (𝑧𝑦 ↦ (𝑋𝑧)) = ∅)
158157necon3bii 2993 . . . . . . . . . 10 (dom (𝑧𝑦 ↦ (𝑋𝑧)) ≠ ∅ ↔ ran (𝑧𝑦 ↦ (𝑋𝑧)) ≠ ∅)
159156, 158sylib 218 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ran (𝑧𝑦 ↦ (𝑋𝑧)) ≠ ∅)
160 elinel2 4202 . . . . . . . . . . 11 (𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin) → 𝑦 ∈ Fin)
161160ad2antlr 727 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑦 ∈ Fin)
162 abrexfi 9392 . . . . . . . . . . 11 (𝑦 ∈ Fin → {𝑥 ∣ ∃𝑧𝑦 𝑥 = (𝑋𝑧)} ∈ Fin)
163132, 162eqeltrid 2845 . . . . . . . . . 10 (𝑦 ∈ Fin → ran (𝑧𝑦 ↦ (𝑋𝑧)) ∈ Fin)
164161, 163syl 17 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ran (𝑧𝑦 ↦ (𝑋𝑧)) ∈ Fin)
165 filintn0 23869 . . . . . . . . 9 ((𝐹 ∈ (Fil‘𝑋) ∧ (ran (𝑧𝑦 ↦ (𝑋𝑧)) ⊆ 𝐹 ∧ ran (𝑧𝑦 ↦ (𝑋𝑧)) ≠ ∅ ∧ ran (𝑧𝑦 ↦ (𝑋𝑧)) ∈ Fin)) → ran (𝑧𝑦 ↦ (𝑋𝑧)) ≠ ∅)
166136, 153, 159, 164, 165syl13anc 1374 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ran (𝑧𝑦 ↦ (𝑋𝑧)) ≠ ∅)
167135, 166eqnetrd 3008 . . . . . . 7 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑋 𝑧𝑦 (𝑋𝑧)) ≠ ∅)
168 disj3 4454 . . . . . . . 8 ((𝑋 𝑧𝑦 (𝑋𝑧)) = ∅ ↔ 𝑋 = (𝑋 𝑧𝑦 (𝑋𝑧)))
169168necon3bii 2993 . . . . . . 7 ((𝑋 𝑧𝑦 (𝑋𝑧)) ≠ ∅ ↔ 𝑋 ≠ (𝑋 𝑧𝑦 (𝑋𝑧)))
170167, 169sylib 218 . . . . . 6 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑋 ≠ (𝑋 𝑧𝑦 (𝑋𝑧)))
171 iundif2 5074 . . . . . . 7 𝑧𝑦 (𝑋 ∖ (𝑋𝑧)) = (𝑋 𝑧𝑦 (𝑋𝑧))
172 dfss4 4269 . . . . . . . . . 10 (𝑧𝑋 ↔ (𝑋 ∖ (𝑋𝑧)) = 𝑧)
173148, 172sylib 218 . . . . . . . . 9 ((((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧𝑦) → (𝑋 ∖ (𝑋𝑧)) = 𝑧)
174173iuneq2dv 5016 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑧𝑦 (𝑋 ∖ (𝑋𝑧)) = 𝑧𝑦 𝑧)
175 uniiun 5058 . . . . . . . 8 𝑦 = 𝑧𝑦 𝑧
176174, 175eqtr4di 2795 . . . . . . 7 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑧𝑦 (𝑋 ∖ (𝑋𝑧)) = 𝑦)
177171, 176eqtr3id 2791 . . . . . 6 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑋 𝑧𝑦 (𝑋𝑧)) = 𝑦)
178170, 177neeqtrd 3010 . . . . 5 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑋 𝑦)
17911adantr 480 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) → 𝐹 ∈ (Fil‘𝑋))
180 filtop 23863 . . . . . 6 (𝐹 ∈ (Fil‘𝑋) → 𝑋𝐹)
181 fileln0 23858 . . . . . 6 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑋𝐹) → 𝑋 ≠ ∅)
182179, 180, 181syl2anc2 585 . . . . 5 ((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) → 𝑋 ≠ ∅)
183121, 178, 182pm2.61ne 3027 . . . 4 ((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) → 𝑋 𝑦)
184183neneqd 2945 . . 3 ((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) → ¬ 𝑋 = 𝑦)
185184nrexdv 3149 . 2 (𝜑 → ¬ ∃𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)𝑋 = 𝑦)
186117, 185pm2.65i 194 1 ¬ 𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395   = wceq 1540  wcel 2108  {cab 2714  wne 2940  wral 3061  wrex 3070  Vcvv 3480  cdif 3948  cin 3950  wss 3951  c0 4333  𝒫 cpw 4600  {csn 4626   cuni 4907   cint 4946   ciun 4991   ciin 4992  cmpt 5225  dom cdm 5685  ran crn 5686  cfv 6561  (class class class)co 7431  Fincfn 8985  ficfi 9450  topGenctg 17482  TopOnctopon 22916  TopBasesctb 22952  Filcfil 23853  UFilcufil 23907  UFLcufl 23908   fLim cflim 23942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-iin 4994  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-1o 8506  df-2o 8507  df-en 8986  df-dom 8987  df-fin 8989  df-fi 9451  df-topgen 17488  df-fbas 21361  df-top 22900  df-topon 22917  df-bases 22953  df-ntr 23028  df-nei 23106  df-fil 23854  df-ufil 23909  df-flim 23947
This theorem is referenced by:  alexsub  24053
  Copyright terms: Public domain W3C validator