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

Theorem alexsublem 24067
Description: Lemma for alexsub 24068. (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 3972 . . . . . . . . . 10 (𝑥 ∈ (𝑋 (𝐵𝐹)) ↔ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹)))
2 alexsub.3 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐽 = (topGen‘(fi‘𝐵)))
32eleq2d 2824 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑦𝐽𝑦 ∈ (topGen‘(fi‘𝐵))))
43anbi1d 631 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑦𝐽𝑥𝑦) ↔ (𝑦 ∈ (topGen‘(fi‘𝐵)) ∧ 𝑥𝑦)))
54biimpa 476 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑦𝐽𝑥𝑦)) → (𝑦 ∈ (topGen‘(fi‘𝐵)) ∧ 𝑥𝑦))
65adantlr 715 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦𝐽𝑥𝑦)) → (𝑦 ∈ (topGen‘(fi‘𝐵)) ∧ 𝑥𝑦))
7 tg2 22987 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ (topGen‘(fi‘𝐵)) ∧ 𝑥𝑦) → ∃𝑧 ∈ (fi‘𝐵)(𝑥𝑧𝑧𝑦))
86, 7syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦𝐽𝑥𝑦)) → ∃𝑧 ∈ (fi‘𝐵)(𝑥𝑧𝑧𝑦))
9 alexsub.5 . . . . . . . . . . . . . . . . . 18 (𝜑𝐹 ∈ (UFil‘𝑋))
10 ufilfil 23927 . . . . . . . . . . . . . . . . . 18 (𝐹 ∈ (UFil‘𝑋) → 𝐹 ∈ (Fil‘𝑋))
119, 10syl 17 . . . . . . . . . . . . . . . . 17 (𝜑𝐹 ∈ (Fil‘𝑋))
1211ad3antrrr 730 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦𝐽𝑥𝑦)) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥𝑧𝑧𝑦))) → 𝐹 ∈ (Fil‘𝑋))
13 alexsub.2 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑋 = 𝐵)
149elfvexd 6945 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑋 ∈ V)
1513, 14eqeltrrd 2839 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 𝐵 ∈ V)
16 uniexb 7782 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐵 ∈ V ↔ 𝐵 ∈ V)
1715, 16sylibr 234 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐵 ∈ V)
18 elfi2 9451 . . . . . . . . . . . . . . . . . . . . . 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 4967 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧𝑦 𝑦𝑧)
2423adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦) ∧ 𝑧𝑦) → 𝑦𝑧)
25 simplr 769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦) ∧ 𝑧𝑦) → 𝑥 𝑦)
2624, 25sseldd 3995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦) ∧ 𝑧𝑦) → 𝑥𝑧)
2726ad2antlr 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦) ∧ 𝑧𝑦)) ∧ ¬ 𝑧𝐹) → 𝑥𝑧)
28 eldifsn 4790 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ↔ (𝑦 ∈ (𝒫 𝐵 ∩ Fin) ∧ 𝑦 ≠ ∅))
2928simplbi 497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) → 𝑦 ∈ (𝒫 𝐵 ∩ Fin))
3029ad2antrl 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦)) → 𝑦 ∈ (𝒫 𝐵 ∩ Fin))
31 elfpw 9391 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝑦𝐵𝑦 ∈ Fin))
3231simplbi 497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 ∈ (𝒫 𝐵 ∩ Fin) → 𝑦𝐵)
3330, 32syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦)) → 𝑦𝐵)
3433sselda 3994 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦)) ∧ 𝑧𝑦) → 𝑧𝐵)
3534anasss 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦) ∧ 𝑧𝑦)) → 𝑧𝐵)
3635anim1i 615 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦) ∧ 𝑧𝑦)) ∧ ¬ 𝑧𝐹) → (𝑧𝐵 ∧ ¬ 𝑧𝐹))
37 eldif 3972 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑧 ∈ (𝐵𝐹) ↔ (𝑧𝐵 ∧ ¬ 𝑧𝐹))
3836, 37sylibr 234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦) ∧ 𝑧𝑦)) ∧ ¬ 𝑧𝐹) → 𝑧 ∈ (𝐵𝐹))
39 elunii 4916 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑥𝑧𝑧 ∈ (𝐵𝐹)) → 𝑥 (𝐵𝐹))
4027, 38, 39syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦) ∧ 𝑧𝑦)) ∧ ¬ 𝑧𝐹) → 𝑥 (𝐵𝐹))
4140ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦) ∧ 𝑧𝑦)) → (¬ 𝑧𝐹𝑥 (𝐵𝐹)))
4222, 41mt3d 148 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦) ∧ 𝑧𝑦)) → 𝑧𝐹)
4342expr 456 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦)) → (𝑧𝑦𝑧𝐹))
4443ssrdv 4000 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦)) → 𝑦𝐹)
45 eldifsni 4794 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) → 𝑦 ≠ ∅)
4645ad2antrl 728 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦)) → 𝑦 ≠ ∅)
47 elinel2 4211 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ (𝒫 𝐵 ∩ Fin) → 𝑦 ∈ Fin)
4830, 47syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦)) → 𝑦 ∈ Fin)
49 elfir 9452 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑦𝐹𝑦 ≠ ∅ ∧ 𝑦 ∈ Fin)) → 𝑦 ∈ (fi‘𝐹))
5021, 44, 46, 48, 49syl13anc 1371 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦)) → 𝑦 ∈ (fi‘𝐹))
51 filfi 23882 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐹 ∈ (Fil‘𝑋) → (fi‘𝐹) = 𝐹)
5221, 51syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦)) → (fi‘𝐹) = 𝐹)
5350, 52eleqtrd 2840 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦)) → 𝑦𝐹)
5453expr 456 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ 𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})) → (𝑥 𝑦 𝑦𝐹))
55 eleq2 2827 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = 𝑦 → (𝑥𝑧𝑥 𝑦))
56 eleq1 2826 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = 𝑦 → (𝑧𝐹 𝑦𝐹))
5755, 56imbi12d 344 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = 𝑦 → ((𝑥𝑧𝑧𝐹) ↔ (𝑥 𝑦 𝑦𝐹)))
5854, 57syl5ibrcom 247 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ 𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})) → (𝑧 = 𝑦 → (𝑥𝑧𝑧𝐹)))
5958rexlimdva 3152 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) → (∃𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})𝑧 = 𝑦 → (𝑥𝑧𝑧𝐹)))
6020, 59sylbid 240 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) → (𝑧 ∈ (fi‘𝐵) → (𝑥𝑧𝑧𝐹)))
6160imp32 418 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑧 ∈ (fi‘𝐵) ∧ 𝑥𝑧)) → 𝑧𝐹)
6261adantrrr 725 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥𝑧𝑧𝑦))) → 𝑧𝐹)
6362adantlr 715 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦𝐽𝑥𝑦)) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥𝑧𝑧𝑦))) → 𝑧𝐹)
64 elssuni 4941 . . . . . . . . . . . . . . . . . . 19 (𝑦𝐽𝑦 𝐽)
6564ad2antrl 728 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦𝐽𝑥𝑦)) → 𝑦 𝐽)
66 fibas 22999 . . . . . . . . . . . . . . . . . . . . . . 23 (fi‘𝐵) ∈ TopBases
67 tgtopon 22993 . . . . . . . . . . . . . . . . . . . . . . 23 ((fi‘𝐵) ∈ TopBases → (topGen‘(fi‘𝐵)) ∈ (TopOn‘ (fi‘𝐵)))
6866, 67ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 (topGen‘(fi‘𝐵)) ∈ (TopOn‘ (fi‘𝐵))
692, 68eqeltrdi 2846 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐽 ∈ (TopOn‘ (fi‘𝐵)))
70 fiuni 9465 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐵 ∈ V → 𝐵 = (fi‘𝐵))
7117, 70syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 𝐵 = (fi‘𝐵))
7213, 71eqtrd 2774 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑋 = (fi‘𝐵))
7372fveq2d 6910 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (TopOn‘𝑋) = (TopOn‘ (fi‘𝐵)))
7469, 73eleqtrrd 2841 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐽 ∈ (TopOn‘𝑋))
75 toponuni 22935 . . . . . . . . . . . . . . . . . . . 20 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
7674, 75syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑋 = 𝐽)
7776ad2antrr 726 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦𝐽𝑥𝑦)) → 𝑋 = 𝐽)
7865, 77sseqtrrd 4036 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦𝐽𝑥𝑦)) → 𝑦𝑋)
7978adantr 480 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦𝐽𝑥𝑦)) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥𝑧𝑧𝑦))) → 𝑦𝑋)
80 simprrr 782 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦𝐽𝑥𝑦)) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥𝑧𝑧𝑦))) → 𝑧𝑦)
81 filss 23876 . . . . . . . . . . . . . . . 16 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑧𝐹𝑦𝑋𝑧𝑦)) → 𝑦𝐹)
8212, 63, 79, 80, 81syl13anc 1371 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦𝐽𝑥𝑦)) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥𝑧𝑧𝑦))) → 𝑦𝐹)
838, 82rexlimddv 3158 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦𝐽𝑥𝑦)) → 𝑦𝐹)
8483expr 456 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ 𝑦𝐽) → (𝑥𝑦𝑦𝐹))
8584ralrimiva 3143 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) → ∀𝑦𝐽 (𝑥𝑦𝑦𝐹))
8685expr 456 . . . . . . . . . . 11 ((𝜑𝑥𝑋) → (¬ 𝑥 (𝐵𝐹) → ∀𝑦𝐽 (𝑥𝑦𝑦𝐹)))
8786imdistanda 571 . . . . . . . . . 10 (𝜑 → ((𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹)) → (𝑥𝑋 ∧ ∀𝑦𝐽 (𝑥𝑦𝑦𝐹))))
881, 87biimtrid 242 . . . . . . . . 9 (𝜑 → (𝑥 ∈ (𝑋 (𝐵𝐹)) → (𝑥𝑋 ∧ ∀𝑦𝐽 (𝑥𝑦𝑦𝐹))))
89 flimopn 23998 . . . . . . . . . 10 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) → (𝑥 ∈ (𝐽 fLim 𝐹) ↔ (𝑥𝑋 ∧ ∀𝑦𝐽 (𝑥𝑦𝑦𝐹))))
9074, 11, 89syl2anc 584 . . . . . . . . 9 (𝜑 → (𝑥 ∈ (𝐽 fLim 𝐹) ↔ (𝑥𝑋 ∧ ∀𝑦𝐽 (𝑥𝑦𝑦𝐹))))
9188, 90sylibrd 259 . . . . . . . 8 (𝜑 → (𝑥 ∈ (𝑋 (𝐵𝐹)) → 𝑥 ∈ (𝐽 fLim 𝐹)))
9291ssrdv 4000 . . . . . . 7 (𝜑 → (𝑋 (𝐵𝐹)) ⊆ (𝐽 fLim 𝐹))
93 alexsub.6 . . . . . . 7 (𝜑 → (𝐽 fLim 𝐹) = ∅)
94 sseq0 4408 . . . . . . 7 (((𝑋 (𝐵𝐹)) ⊆ (𝐽 fLim 𝐹) ∧ (𝐽 fLim 𝐹) = ∅) → (𝑋 (𝐵𝐹)) = ∅)
9592, 93, 94syl2anc 584 . . . . . 6 (𝜑 → (𝑋 (𝐵𝐹)) = ∅)
96 ssdif0 4371 . . . . . 6 (𝑋 (𝐵𝐹) ↔ (𝑋 (𝐵𝐹)) = ∅)
9795, 96sylibr 234 . . . . 5 (𝜑𝑋 (𝐵𝐹))
98 difss 4145 . . . . . . 7 (𝐵𝐹) ⊆ 𝐵
9998unissi 4920 . . . . . 6 (𝐵𝐹) ⊆ 𝐵
10099, 13sseqtrrid 4048 . . . . 5 (𝜑 (𝐵𝐹) ⊆ 𝑋)
10197, 100eqssd 4012 . . . 4 (𝜑𝑋 = (𝐵𝐹))
102101, 98jctil 519 . . 3 (𝜑 → ((𝐵𝐹) ⊆ 𝐵𝑋 = (𝐵𝐹)))
10317difexd 5336 . . . . 5 (𝜑 → (𝐵𝐹) ∈ V)
104103adantr 480 . . . 4 ((𝜑 ∧ ((𝐵𝐹) ⊆ 𝐵𝑋 = (𝐵𝐹))) → (𝐵𝐹) ∈ V)
105 sseq1 4020 . . . . . . . 8 (𝑥 = (𝐵𝐹) → (𝑥𝐵 ↔ (𝐵𝐹) ⊆ 𝐵))
106 unieq 4922 . . . . . . . . 9 (𝑥 = (𝐵𝐹) → 𝑥 = (𝐵𝐹))
107106eqeq2d 2745 . . . . . . . 8 (𝑥 = (𝐵𝐹) → (𝑋 = 𝑥𝑋 = (𝐵𝐹)))
108105, 107anbi12d 632 . . . . . . 7 (𝑥 = (𝐵𝐹) → ((𝑥𝐵𝑋 = 𝑥) ↔ ((𝐵𝐹) ⊆ 𝐵𝑋 = (𝐵𝐹))))
109108anbi2d 630 . . . . . 6 (𝑥 = (𝐵𝐹) → ((𝜑 ∧ (𝑥𝐵𝑋 = 𝑥)) ↔ (𝜑 ∧ ((𝐵𝐹) ⊆ 𝐵𝑋 = (𝐵𝐹)))))
110 pweq 4618 . . . . . . . 8 (𝑥 = (𝐵𝐹) → 𝒫 𝑥 = 𝒫 (𝐵𝐹))
111110ineq1d 4226 . . . . . . 7 (𝑥 = (𝐵𝐹) → (𝒫 𝑥 ∩ Fin) = (𝒫 (𝐵𝐹) ∩ Fin))
112111rexeqdv 3324 . . . . . 6 (𝑥 = (𝐵𝐹) → (∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = 𝑦 ↔ ∃𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)𝑋 = 𝑦))
113109, 112imbi12d 344 . . . . 5 (𝑥 = (𝐵𝐹) → (((𝜑 ∧ (𝑥𝐵𝑋 = 𝑥)) → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = 𝑦) ↔ ((𝜑 ∧ ((𝐵𝐹) ⊆ 𝐵𝑋 = (𝐵𝐹))) → ∃𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)𝑋 = 𝑦)))
114 alexsub.4 . . . . 5 ((𝜑 ∧ (𝑥𝐵𝑋 = 𝑥)) → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = 𝑦)
115113, 114vtoclg 3553 . . . 4 ((𝐵𝐹) ∈ V → ((𝜑 ∧ ((𝐵𝐹) ⊆ 𝐵𝑋 = (𝐵𝐹))) → ∃𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)𝑋 = 𝑦))
116104, 115mpcom 38 . . 3 ((𝜑 ∧ ((𝐵𝐹) ⊆ 𝐵𝑋 = (𝐵𝐹))) → ∃𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)𝑋 = 𝑦)
117102, 116mpdan 687 . 2 (𝜑 → ∃𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)𝑋 = 𝑦)
118 unieq 4922 . . . . . . 7 (𝑦 = ∅ → 𝑦 = ∅)
119 uni0 4939 . . . . . . 7 ∅ = ∅
120118, 119eqtrdi 2790 . . . . . 6 (𝑦 = ∅ → 𝑦 = ∅)
121120neeq2d 2998 . . . . 5 (𝑦 = ∅ → (𝑋 𝑦𝑋 ≠ ∅))
122 difssd 4146 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) → (𝑋𝑧) ⊆ 𝑋)
123122ralrimivw 3147 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) → ∀𝑧𝑦 (𝑋𝑧) ⊆ 𝑋)
124 riinn0 5087 . . . . . . . . . 10 ((∀𝑧𝑦 (𝑋𝑧) ⊆ 𝑋𝑦 ≠ ∅) → (𝑋 𝑧𝑦 (𝑋𝑧)) = 𝑧𝑦 (𝑋𝑧))
125123, 124sylan 580 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑋 𝑧𝑦 (𝑋𝑧)) = 𝑧𝑦 (𝑋𝑧))
12614ad2antrr 726 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑋 ∈ V)
127126difexd 5336 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑋𝑧) ∈ V)
128127ralrimivw 3147 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ∀𝑧𝑦 (𝑋𝑧) ∈ V)
129 dfiin2g 5036 . . . . . . . . . . 11 (∀𝑧𝑦 (𝑋𝑧) ∈ V → 𝑧𝑦 (𝑋𝑧) = {𝑥 ∣ ∃𝑧𝑦 𝑥 = (𝑋𝑧)})
130128, 129syl 17 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑧𝑦 (𝑋𝑧) = {𝑥 ∣ ∃𝑧𝑦 𝑥 = (𝑋𝑧)})
131 eqid 2734 . . . . . . . . . . . 12 (𝑧𝑦 ↦ (𝑋𝑧)) = (𝑧𝑦 ↦ (𝑋𝑧))
132131rnmpt 5970 . . . . . . . . . . 11 ran (𝑧𝑦 ↦ (𝑋𝑧)) = {𝑥 ∣ ∃𝑧𝑦 𝑥 = (𝑋𝑧)}
133132inteqi 4954 . . . . . . . . . 10 ran (𝑧𝑦 ↦ (𝑋𝑧)) = {𝑥 ∣ ∃𝑧𝑦 𝑥 = (𝑋𝑧)}
134130, 133eqtr4di 2792 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑧𝑦 (𝑋𝑧) = ran (𝑧𝑦 ↦ (𝑋𝑧)))
135125, 134eqtrd 2774 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑋 𝑧𝑦 (𝑋𝑧)) = ran (𝑧𝑦 ↦ (𝑋𝑧)))
13611ad2antrr 726 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝐹 ∈ (Fil‘𝑋))
137 elfpw 9391 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin) ↔ (𝑦 ⊆ (𝐵𝐹) ∧ 𝑦 ∈ Fin))
138137simplbi 497 . . . . . . . . . . . . . . 15 (𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin) → 𝑦 ⊆ (𝐵𝐹))
139138ad2antlr 727 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑦 ⊆ (𝐵𝐹))
140139sselda 3994 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧𝑦) → 𝑧 ∈ (𝐵𝐹))
141140eldifbd 3975 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧𝑦) → ¬ 𝑧𝐹)
1429ad3antrrr 730 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧𝑦) → 𝐹 ∈ (UFil‘𝑋))
143139difss2d 4148 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑦𝐵)
144143sselda 3994 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧𝑦) → 𝑧𝐵)
145 elssuni 4941 . . . . . . . . . . . . . . 15 (𝑧𝐵𝑧 𝐵)
146144, 145syl 17 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧𝑦) → 𝑧 𝐵)
14713ad3antrrr 730 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧𝑦) → 𝑋 = 𝐵)
148146, 147sseqtrrd 4036 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧𝑦) → 𝑧𝑋)
149 ufilb 23929 . . . . . . . . . . . . 13 ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑧𝑋) → (¬ 𝑧𝐹 ↔ (𝑋𝑧) ∈ 𝐹))
150142, 148, 149syl2anc 584 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧𝑦) → (¬ 𝑧𝐹 ↔ (𝑋𝑧) ∈ 𝐹))
151141, 150mpbid 232 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧𝑦) → (𝑋𝑧) ∈ 𝐹)
152151fmpttd 7134 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑧𝑦 ↦ (𝑋𝑧)):𝑦𝐹)
153152frnd 6744 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ran (𝑧𝑦 ↦ (𝑋𝑧)) ⊆ 𝐹)
154131, 151dmmptd 6713 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → dom (𝑧𝑦 ↦ (𝑋𝑧)) = 𝑦)
155 simpr 484 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑦 ≠ ∅)
156154, 155eqnetrd 3005 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → dom (𝑧𝑦 ↦ (𝑋𝑧)) ≠ ∅)
157 dm0rn0 5937 . . . . . . . . . . 11 (dom (𝑧𝑦 ↦ (𝑋𝑧)) = ∅ ↔ ran (𝑧𝑦 ↦ (𝑋𝑧)) = ∅)
158157necon3bii 2990 . . . . . . . . . 10 (dom (𝑧𝑦 ↦ (𝑋𝑧)) ≠ ∅ ↔ ran (𝑧𝑦 ↦ (𝑋𝑧)) ≠ ∅)
159156, 158sylib 218 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ran (𝑧𝑦 ↦ (𝑋𝑧)) ≠ ∅)
160 elinel2 4211 . . . . . . . . . . 11 (𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin) → 𝑦 ∈ Fin)
161160ad2antlr 727 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑦 ∈ Fin)
162 abrexfi 9389 . . . . . . . . . . 11 (𝑦 ∈ Fin → {𝑥 ∣ ∃𝑧𝑦 𝑥 = (𝑋𝑧)} ∈ Fin)
163132, 162eqeltrid 2842 . . . . . . . . . 10 (𝑦 ∈ Fin → ran (𝑧𝑦 ↦ (𝑋𝑧)) ∈ Fin)
164161, 163syl 17 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ran (𝑧𝑦 ↦ (𝑋𝑧)) ∈ Fin)
165 filintn0 23884 . . . . . . . . 9 ((𝐹 ∈ (Fil‘𝑋) ∧ (ran (𝑧𝑦 ↦ (𝑋𝑧)) ⊆ 𝐹 ∧ ran (𝑧𝑦 ↦ (𝑋𝑧)) ≠ ∅ ∧ ran (𝑧𝑦 ↦ (𝑋𝑧)) ∈ Fin)) → ran (𝑧𝑦 ↦ (𝑋𝑧)) ≠ ∅)
166136, 153, 159, 164, 165syl13anc 1371 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ran (𝑧𝑦 ↦ (𝑋𝑧)) ≠ ∅)
167135, 166eqnetrd 3005 . . . . . . 7 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑋 𝑧𝑦 (𝑋𝑧)) ≠ ∅)
168 disj3 4459 . . . . . . . 8 ((𝑋 𝑧𝑦 (𝑋𝑧)) = ∅ ↔ 𝑋 = (𝑋 𝑧𝑦 (𝑋𝑧)))
169168necon3bii 2990 . . . . . . 7 ((𝑋 𝑧𝑦 (𝑋𝑧)) ≠ ∅ ↔ 𝑋 ≠ (𝑋 𝑧𝑦 (𝑋𝑧)))
170167, 169sylib 218 . . . . . 6 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑋 ≠ (𝑋 𝑧𝑦 (𝑋𝑧)))
171 iundif2 5078 . . . . . . 7 𝑧𝑦 (𝑋 ∖ (𝑋𝑧)) = (𝑋 𝑧𝑦 (𝑋𝑧))
172 dfss4 4274 . . . . . . . . . 10 (𝑧𝑋 ↔ (𝑋 ∖ (𝑋𝑧)) = 𝑧)
173148, 172sylib 218 . . . . . . . . 9 ((((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧𝑦) → (𝑋 ∖ (𝑋𝑧)) = 𝑧)
174173iuneq2dv 5020 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑧𝑦 (𝑋 ∖ (𝑋𝑧)) = 𝑧𝑦 𝑧)
175 uniiun 5062 . . . . . . . 8 𝑦 = 𝑧𝑦 𝑧
176174, 175eqtr4di 2792 . . . . . . 7 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑧𝑦 (𝑋 ∖ (𝑋𝑧)) = 𝑦)
177171, 176eqtr3id 2788 . . . . . 6 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑋 𝑧𝑦 (𝑋𝑧)) = 𝑦)
178170, 177neeqtrd 3007 . . . . 5 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑋 𝑦)
17911adantr 480 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) → 𝐹 ∈ (Fil‘𝑋))
180 filtop 23878 . . . . . 6 (𝐹 ∈ (Fil‘𝑋) → 𝑋𝐹)
181 fileln0 23873 . . . . . 6 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑋𝐹) → 𝑋 ≠ ∅)
182179, 180, 181syl2anc2 585 . . . . 5 ((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) → 𝑋 ≠ ∅)
183121, 178, 182pm2.61ne 3024 . . . 4 ((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) → 𝑋 𝑦)
184183neneqd 2942 . . 3 ((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) → ¬ 𝑋 = 𝑦)
185184nrexdv 3146 . 2 (𝜑 → ¬ ∃𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)𝑋 = 𝑦)
186117, 185pm2.65i 194 1 ¬ 𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395   = wceq 1536  wcel 2105  {cab 2711  wne 2937  wral 3058  wrex 3067  Vcvv 3477  cdif 3959  cin 3961  wss 3962  c0 4338  𝒫 cpw 4604  {csn 4630   cuni 4911   cint 4950   ciun 4995   ciin 4996  cmpt 5230  dom cdm 5688  ran crn 5689  cfv 6562  (class class class)co 7430  Fincfn 8983  ficfi 9447  topGenctg 17483  TopOnctopon 22931  TopBasesctb 22967  Filcfil 23868  UFilcufil 23922  UFLcufl 23923   fLim cflim 23957
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-iin 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-1o 8504  df-2o 8505  df-en 8984  df-dom 8985  df-fin 8987  df-fi 9448  df-topgen 17489  df-fbas 21378  df-top 22915  df-topon 22932  df-bases 22968  df-ntr 23043  df-nei 23121  df-fil 23869  df-ufil 23924  df-flim 23962
This theorem is referenced by:  alexsub  24068
  Copyright terms: Public domain W3C validator