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

Theorem alexsublem 22068
Description: Lemma for alexsub 22069. (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 3733 . . . . . . . . . 10 (𝑥 ∈ (𝑋 (𝐵𝐹)) ↔ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹)))
2 alexsub.3 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐽 = (topGen‘(fi‘𝐵)))
32eleq2d 2836 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑦𝐽𝑦 ∈ (topGen‘(fi‘𝐵))))
43anbi1d 615 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑦𝐽𝑥𝑦) ↔ (𝑦 ∈ (topGen‘(fi‘𝐵)) ∧ 𝑥𝑦)))
54biimpa 462 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑦𝐽𝑥𝑦)) → (𝑦 ∈ (topGen‘(fi‘𝐵)) ∧ 𝑥𝑦))
65adantlr 694 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦𝐽𝑥𝑦)) → (𝑦 ∈ (topGen‘(fi‘𝐵)) ∧ 𝑥𝑦))
7 tg2 20990 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ (topGen‘(fi‘𝐵)) ∧ 𝑥𝑦) → ∃𝑧 ∈ (fi‘𝐵)(𝑥𝑧𝑧𝑦))
86, 7syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦𝐽𝑥𝑦)) → ∃𝑧 ∈ (fi‘𝐵)(𝑥𝑧𝑧𝑦))
9 alexsub.5 . . . . . . . . . . . . . . . . . 18 (𝜑𝐹 ∈ (UFil‘𝑋))
10 ufilfil 21928 . . . . . . . . . . . . . . . . . 18 (𝐹 ∈ (UFil‘𝑋) → 𝐹 ∈ (Fil‘𝑋))
119, 10syl 17 . . . . . . . . . . . . . . . . 17 (𝜑𝐹 ∈ (Fil‘𝑋))
1211ad3antrrr 709 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦𝐽𝑥𝑦)) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥𝑧𝑧𝑦))) → 𝐹 ∈ (Fil‘𝑋))
13 alexsub.2 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑋 = 𝐵)
149elfvexd 6363 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑋 ∈ V)
1513, 14eqeltrrd 2851 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 𝐵 ∈ V)
16 uniexb 7120 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐵 ∈ V ↔ 𝐵 ∈ V)
1715, 16sylibr 224 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐵 ∈ V)
18 elfi2 8476 . . . . . . . . . . . . . . . . . . . . . 22 (𝐵 ∈ V → (𝑧 ∈ (fi‘𝐵) ↔ ∃𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})𝑧 = 𝑦))
1917, 18syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑧 ∈ (fi‘𝐵) ↔ ∃𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})𝑧 = 𝑦))
2019adantr 466 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) → (𝑧 ∈ (fi‘𝐵) ↔ ∃𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})𝑧 = 𝑦))
2111ad2antrr 705 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦)) → 𝐹 ∈ (Fil‘𝑋))
22 simplrr 763 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦) ∧ 𝑧𝑦)) → ¬ 𝑥 (𝐵𝐹))
23 intss1 4626 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧𝑦 𝑦𝑧)
2423adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦) ∧ 𝑧𝑦) → 𝑦𝑧)
25 simplr 752 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦) ∧ 𝑧𝑦) → 𝑥 𝑦)
2624, 25sseldd 3753 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦) ∧ 𝑧𝑦) → 𝑥𝑧)
2726ad2antlr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦) ∧ 𝑧𝑦)) ∧ ¬ 𝑧𝐹) → 𝑥𝑧)
28 eldifsn 4453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ↔ (𝑦 ∈ (𝒫 𝐵 ∩ Fin) ∧ 𝑦 ≠ ∅))
2928simplbi 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) → 𝑦 ∈ (𝒫 𝐵 ∩ Fin))
3029ad2antrl 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦)) → 𝑦 ∈ (𝒫 𝐵 ∩ Fin))
31 elfpw 8424 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝑦𝐵𝑦 ∈ Fin))
3231simplbi 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 ∈ (𝒫 𝐵 ∩ Fin) → 𝑦𝐵)
3330, 32syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦)) → 𝑦𝐵)
3433sselda 3752 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦)) ∧ 𝑧𝑦) → 𝑧𝐵)
3534anasss 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦) ∧ 𝑧𝑦)) → 𝑧𝐵)
3635anim1i 602 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦) ∧ 𝑧𝑦)) ∧ ¬ 𝑧𝐹) → (𝑧𝐵 ∧ ¬ 𝑧𝐹))
37 eldif 3733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑧 ∈ (𝐵𝐹) ↔ (𝑧𝐵 ∧ ¬ 𝑧𝐹))
3836, 37sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦) ∧ 𝑧𝑦)) ∧ ¬ 𝑧𝐹) → 𝑧 ∈ (𝐵𝐹))
39 elunii 4579 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑥𝑧𝑧 ∈ (𝐵𝐹)) → 𝑥 (𝐵𝐹))
4027, 38, 39syl2anc 573 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦) ∧ 𝑧𝑦)) ∧ ¬ 𝑧𝐹) → 𝑥 (𝐵𝐹))
4140ex 397 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦) ∧ 𝑧𝑦)) → (¬ 𝑧𝐹𝑥 (𝐵𝐹)))
4222, 41mt3d 142 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦) ∧ 𝑧𝑦)) → 𝑧𝐹)
4342expr 444 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦)) → (𝑧𝑦𝑧𝐹))
4443ssrdv 3758 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦)) → 𝑦𝐹)
4528simprbi 484 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) → 𝑦 ≠ ∅)
4645ad2antrl 707 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦)) → 𝑦 ≠ ∅)
4731simprbi 484 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ (𝒫 𝐵 ∩ Fin) → 𝑦 ∈ Fin)
4830, 47syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦)) → 𝑦 ∈ Fin)
49 elfir 8477 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑦𝐹𝑦 ≠ ∅ ∧ 𝑦 ∈ Fin)) → 𝑦 ∈ (fi‘𝐹))
5021, 44, 46, 48, 49syl13anc 1478 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦)) → 𝑦 ∈ (fi‘𝐹))
51 filfi 21883 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐹 ∈ (Fil‘𝑋) → (fi‘𝐹) = 𝐹)
5221, 51syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦)) → (fi‘𝐹) = 𝐹)
5350, 52eleqtrd 2852 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦)) → 𝑦𝐹)
5453expr 444 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ 𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})) → (𝑥 𝑦 𝑦𝐹))
55 eleq2 2839 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = 𝑦 → (𝑥𝑧𝑥 𝑦))
56 eleq1 2838 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = 𝑦 → (𝑧𝐹 𝑦𝐹))
5755, 56imbi12d 333 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = 𝑦 → ((𝑥𝑧𝑧𝐹) ↔ (𝑥 𝑦 𝑦𝐹)))
5854, 57syl5ibrcom 237 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ 𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})) → (𝑧 = 𝑦 → (𝑥𝑧𝑧𝐹)))
5958rexlimdva 3179 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) → (∃𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})𝑧 = 𝑦 → (𝑥𝑧𝑧𝐹)))
6020, 59sylbid 230 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) → (𝑧 ∈ (fi‘𝐵) → (𝑥𝑧𝑧𝐹)))
6160imp32 405 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑧 ∈ (fi‘𝐵) ∧ 𝑥𝑧)) → 𝑧𝐹)
6261adantrrr 704 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥𝑧𝑧𝑦))) → 𝑧𝐹)
6362adantlr 694 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦𝐽𝑥𝑦)) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥𝑧𝑧𝑦))) → 𝑧𝐹)
64 elssuni 4603 . . . . . . . . . . . . . . . . . . 19 (𝑦𝐽𝑦 𝐽)
6564ad2antrl 707 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦𝐽𝑥𝑦)) → 𝑦 𝐽)
66 fibas 21002 . . . . . . . . . . . . . . . . . . . . . . 23 (fi‘𝐵) ∈ TopBases
67 tgtopon 20996 . . . . . . . . . . . . . . . . . . . . . . 23 ((fi‘𝐵) ∈ TopBases → (topGen‘(fi‘𝐵)) ∈ (TopOn‘ (fi‘𝐵)))
6866, 67ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 (topGen‘(fi‘𝐵)) ∈ (TopOn‘ (fi‘𝐵))
692, 68syl6eqel 2858 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐽 ∈ (TopOn‘ (fi‘𝐵)))
70 fiuni 8490 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐵 ∈ V → 𝐵 = (fi‘𝐵))
7117, 70syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 𝐵 = (fi‘𝐵))
7213, 71eqtrd 2805 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑋 = (fi‘𝐵))
7372fveq2d 6336 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (TopOn‘𝑋) = (TopOn‘ (fi‘𝐵)))
7469, 73eleqtrrd 2853 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐽 ∈ (TopOn‘𝑋))
75 toponuni 20939 . . . . . . . . . . . . . . . . . . . 20 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
7674, 75syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑋 = 𝐽)
7776ad2antrr 705 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦𝐽𝑥𝑦)) → 𝑋 = 𝐽)
7865, 77sseqtr4d 3791 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦𝐽𝑥𝑦)) → 𝑦𝑋)
7978adantr 466 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦𝐽𝑥𝑦)) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥𝑧𝑧𝑦))) → 𝑦𝑋)
80 simprrr 767 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦𝐽𝑥𝑦)) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥𝑧𝑧𝑦))) → 𝑧𝑦)
81 filss 21877 . . . . . . . . . . . . . . . 16 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑧𝐹𝑦𝑋𝑧𝑦)) → 𝑦𝐹)
8212, 63, 79, 80, 81syl13anc 1478 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦𝐽𝑥𝑦)) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥𝑧𝑧𝑦))) → 𝑦𝐹)
838, 82rexlimddv 3183 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦𝐽𝑥𝑦)) → 𝑦𝐹)
8483expr 444 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ 𝑦𝐽) → (𝑥𝑦𝑦𝐹))
8584ralrimiva 3115 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) → ∀𝑦𝐽 (𝑥𝑦𝑦𝐹))
8685expr 444 . . . . . . . . . . 11 ((𝜑𝑥𝑋) → (¬ 𝑥 (𝐵𝐹) → ∀𝑦𝐽 (𝑥𝑦𝑦𝐹)))
8786imdistanda 561 . . . . . . . . . 10 (𝜑 → ((𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹)) → (𝑥𝑋 ∧ ∀𝑦𝐽 (𝑥𝑦𝑦𝐹))))
881, 87syl5bi 232 . . . . . . . . 9 (𝜑 → (𝑥 ∈ (𝑋 (𝐵𝐹)) → (𝑥𝑋 ∧ ∀𝑦𝐽 (𝑥𝑦𝑦𝐹))))
89 flimopn 21999 . . . . . . . . . 10 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) → (𝑥 ∈ (𝐽 fLim 𝐹) ↔ (𝑥𝑋 ∧ ∀𝑦𝐽 (𝑥𝑦𝑦𝐹))))
9074, 11, 89syl2anc 573 . . . . . . . . 9 (𝜑 → (𝑥 ∈ (𝐽 fLim 𝐹) ↔ (𝑥𝑋 ∧ ∀𝑦𝐽 (𝑥𝑦𝑦𝐹))))
9188, 90sylibrd 249 . . . . . . . 8 (𝜑 → (𝑥 ∈ (𝑋 (𝐵𝐹)) → 𝑥 ∈ (𝐽 fLim 𝐹)))
9291ssrdv 3758 . . . . . . 7 (𝜑 → (𝑋 (𝐵𝐹)) ⊆ (𝐽 fLim 𝐹))
93 alexsub.6 . . . . . . 7 (𝜑 → (𝐽 fLim 𝐹) = ∅)
94 sseq0 4119 . . . . . . 7 (((𝑋 (𝐵𝐹)) ⊆ (𝐽 fLim 𝐹) ∧ (𝐽 fLim 𝐹) = ∅) → (𝑋 (𝐵𝐹)) = ∅)
9592, 93, 94syl2anc 573 . . . . . 6 (𝜑 → (𝑋 (𝐵𝐹)) = ∅)
96 ssdif0 4089 . . . . . 6 (𝑋 (𝐵𝐹) ↔ (𝑋 (𝐵𝐹)) = ∅)
9795, 96sylibr 224 . . . . 5 (𝜑𝑋 (𝐵𝐹))
98 difss 3888 . . . . . . 7 (𝐵𝐹) ⊆ 𝐵
9998unissi 4597 . . . . . 6 (𝐵𝐹) ⊆ 𝐵
10099, 13syl5sseqr 3803 . . . . 5 (𝜑 (𝐵𝐹) ⊆ 𝑋)
10197, 100eqssd 3769 . . . 4 (𝜑𝑋 = (𝐵𝐹))
102101, 98jctil 509 . . 3 (𝜑 → ((𝐵𝐹) ⊆ 𝐵𝑋 = (𝐵𝐹)))
103 difexg 4942 . . . . . 6 (𝐵 ∈ V → (𝐵𝐹) ∈ V)
10417, 103syl 17 . . . . 5 (𝜑 → (𝐵𝐹) ∈ V)
105104adantr 466 . . . 4 ((𝜑 ∧ ((𝐵𝐹) ⊆ 𝐵𝑋 = (𝐵𝐹))) → (𝐵𝐹) ∈ V)
106 sseq1 3775 . . . . . . . 8 (𝑥 = (𝐵𝐹) → (𝑥𝐵 ↔ (𝐵𝐹) ⊆ 𝐵))
107 unieq 4582 . . . . . . . . 9 (𝑥 = (𝐵𝐹) → 𝑥 = (𝐵𝐹))
108107eqeq2d 2781 . . . . . . . 8 (𝑥 = (𝐵𝐹) → (𝑋 = 𝑥𝑋 = (𝐵𝐹)))
109106, 108anbi12d 616 . . . . . . 7 (𝑥 = (𝐵𝐹) → ((𝑥𝐵𝑋 = 𝑥) ↔ ((𝐵𝐹) ⊆ 𝐵𝑋 = (𝐵𝐹))))
110109anbi2d 614 . . . . . 6 (𝑥 = (𝐵𝐹) → ((𝜑 ∧ (𝑥𝐵𝑋 = 𝑥)) ↔ (𝜑 ∧ ((𝐵𝐹) ⊆ 𝐵𝑋 = (𝐵𝐹)))))
111 pweq 4300 . . . . . . . 8 (𝑥 = (𝐵𝐹) → 𝒫 𝑥 = 𝒫 (𝐵𝐹))
112111ineq1d 3964 . . . . . . 7 (𝑥 = (𝐵𝐹) → (𝒫 𝑥 ∩ Fin) = (𝒫 (𝐵𝐹) ∩ Fin))
113112rexeqdv 3294 . . . . . 6 (𝑥 = (𝐵𝐹) → (∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = 𝑦 ↔ ∃𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)𝑋 = 𝑦))
114110, 113imbi12d 333 . . . . 5 (𝑥 = (𝐵𝐹) → (((𝜑 ∧ (𝑥𝐵𝑋 = 𝑥)) → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = 𝑦) ↔ ((𝜑 ∧ ((𝐵𝐹) ⊆ 𝐵𝑋 = (𝐵𝐹))) → ∃𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)𝑋 = 𝑦)))
115 alexsub.4 . . . . 5 ((𝜑 ∧ (𝑥𝐵𝑋 = 𝑥)) → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = 𝑦)
116114, 115vtoclg 3417 . . . 4 ((𝐵𝐹) ∈ V → ((𝜑 ∧ ((𝐵𝐹) ⊆ 𝐵𝑋 = (𝐵𝐹))) → ∃𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)𝑋 = 𝑦))
117105, 116mpcom 38 . . 3 ((𝜑 ∧ ((𝐵𝐹) ⊆ 𝐵𝑋 = (𝐵𝐹))) → ∃𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)𝑋 = 𝑦)
118102, 117mpdan 667 . 2 (𝜑 → ∃𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)𝑋 = 𝑦)
119 unieq 4582 . . . . . . 7 (𝑦 = ∅ → 𝑦 = ∅)
120 uni0 4601 . . . . . . 7 ∅ = ∅
121119, 120syl6eq 2821 . . . . . 6 (𝑦 = ∅ → 𝑦 = ∅)
122121neeq2d 3003 . . . . 5 (𝑦 = ∅ → (𝑋 𝑦𝑋 ≠ ∅))
123 difssd 3889 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) → (𝑋𝑧) ⊆ 𝑋)
124123ralrimivw 3116 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) → ∀𝑧𝑦 (𝑋𝑧) ⊆ 𝑋)
125 riinn0 4729 . . . . . . . . . 10 ((∀𝑧𝑦 (𝑋𝑧) ⊆ 𝑋𝑦 ≠ ∅) → (𝑋 𝑧𝑦 (𝑋𝑧)) = 𝑧𝑦 (𝑋𝑧))
126124, 125sylan 569 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑋 𝑧𝑦 (𝑋𝑧)) = 𝑧𝑦 (𝑋𝑧))
12714ad2antrr 705 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑋 ∈ V)
128 difexg 4942 . . . . . . . . . . . . 13 (𝑋 ∈ V → (𝑋𝑧) ∈ V)
129127, 128syl 17 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑋𝑧) ∈ V)
130129ralrimivw 3116 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ∀𝑧𝑦 (𝑋𝑧) ∈ V)
131 dfiin2g 4687 . . . . . . . . . . 11 (∀𝑧𝑦 (𝑋𝑧) ∈ V → 𝑧𝑦 (𝑋𝑧) = {𝑥 ∣ ∃𝑧𝑦 𝑥 = (𝑋𝑧)})
132130, 131syl 17 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑧𝑦 (𝑋𝑧) = {𝑥 ∣ ∃𝑧𝑦 𝑥 = (𝑋𝑧)})
133 eqid 2771 . . . . . . . . . . . 12 (𝑧𝑦 ↦ (𝑋𝑧)) = (𝑧𝑦 ↦ (𝑋𝑧))
134133rnmpt 5509 . . . . . . . . . . 11 ran (𝑧𝑦 ↦ (𝑋𝑧)) = {𝑥 ∣ ∃𝑧𝑦 𝑥 = (𝑋𝑧)}
135134inteqi 4615 . . . . . . . . . 10 ran (𝑧𝑦 ↦ (𝑋𝑧)) = {𝑥 ∣ ∃𝑧𝑦 𝑥 = (𝑋𝑧)}
136132, 135syl6eqr 2823 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑧𝑦 (𝑋𝑧) = ran (𝑧𝑦 ↦ (𝑋𝑧)))
137126, 136eqtrd 2805 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑋 𝑧𝑦 (𝑋𝑧)) = ran (𝑧𝑦 ↦ (𝑋𝑧)))
13811ad2antrr 705 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝐹 ∈ (Fil‘𝑋))
139 elfpw 8424 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin) ↔ (𝑦 ⊆ (𝐵𝐹) ∧ 𝑦 ∈ Fin))
140139simplbi 485 . . . . . . . . . . . . . . 15 (𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin) → 𝑦 ⊆ (𝐵𝐹))
141140ad2antlr 706 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑦 ⊆ (𝐵𝐹))
142141sselda 3752 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧𝑦) → 𝑧 ∈ (𝐵𝐹))
143142eldifbd 3736 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧𝑦) → ¬ 𝑧𝐹)
1449ad3antrrr 709 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧𝑦) → 𝐹 ∈ (UFil‘𝑋))
145141difss2d 3891 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑦𝐵)
146145sselda 3752 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧𝑦) → 𝑧𝐵)
147 elssuni 4603 . . . . . . . . . . . . . . 15 (𝑧𝐵𝑧 𝐵)
148146, 147syl 17 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧𝑦) → 𝑧 𝐵)
14913ad3antrrr 709 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧𝑦) → 𝑋 = 𝐵)
150148, 149sseqtr4d 3791 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧𝑦) → 𝑧𝑋)
151 ufilb 21930 . . . . . . . . . . . . 13 ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑧𝑋) → (¬ 𝑧𝐹 ↔ (𝑋𝑧) ∈ 𝐹))
152144, 150, 151syl2anc 573 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧𝑦) → (¬ 𝑧𝐹 ↔ (𝑋𝑧) ∈ 𝐹))
153143, 152mpbid 222 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧𝑦) → (𝑋𝑧) ∈ 𝐹)
154153, 133fmptd 6527 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑧𝑦 ↦ (𝑋𝑧)):𝑦𝐹)
155 frn 6193 . . . . . . . . . 10 ((𝑧𝑦 ↦ (𝑋𝑧)):𝑦𝐹 → ran (𝑧𝑦 ↦ (𝑋𝑧)) ⊆ 𝐹)
156154, 155syl 17 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ran (𝑧𝑦 ↦ (𝑋𝑧)) ⊆ 𝐹)
157133, 153dmmptd 6164 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → dom (𝑧𝑦 ↦ (𝑋𝑧)) = 𝑦)
158 simpr 471 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑦 ≠ ∅)
159157, 158eqnetrd 3010 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → dom (𝑧𝑦 ↦ (𝑋𝑧)) ≠ ∅)
160 dm0rn0 5480 . . . . . . . . . . 11 (dom (𝑧𝑦 ↦ (𝑋𝑧)) = ∅ ↔ ran (𝑧𝑦 ↦ (𝑋𝑧)) = ∅)
161160necon3bii 2995 . . . . . . . . . 10 (dom (𝑧𝑦 ↦ (𝑋𝑧)) ≠ ∅ ↔ ran (𝑧𝑦 ↦ (𝑋𝑧)) ≠ ∅)
162159, 161sylib 208 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ran (𝑧𝑦 ↦ (𝑋𝑧)) ≠ ∅)
163139simprbi 484 . . . . . . . . . . 11 (𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin) → 𝑦 ∈ Fin)
164163ad2antlr 706 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑦 ∈ Fin)
165 abrexfi 8422 . . . . . . . . . . 11 (𝑦 ∈ Fin → {𝑥 ∣ ∃𝑧𝑦 𝑥 = (𝑋𝑧)} ∈ Fin)
166134, 165syl5eqel 2854 . . . . . . . . . 10 (𝑦 ∈ Fin → ran (𝑧𝑦 ↦ (𝑋𝑧)) ∈ Fin)
167164, 166syl 17 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ran (𝑧𝑦 ↦ (𝑋𝑧)) ∈ Fin)
168 filintn0 21885 . . . . . . . . 9 ((𝐹 ∈ (Fil‘𝑋) ∧ (ran (𝑧𝑦 ↦ (𝑋𝑧)) ⊆ 𝐹 ∧ ran (𝑧𝑦 ↦ (𝑋𝑧)) ≠ ∅ ∧ ran (𝑧𝑦 ↦ (𝑋𝑧)) ∈ Fin)) → ran (𝑧𝑦 ↦ (𝑋𝑧)) ≠ ∅)
169138, 156, 162, 167, 168syl13anc 1478 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ran (𝑧𝑦 ↦ (𝑋𝑧)) ≠ ∅)
170137, 169eqnetrd 3010 . . . . . . 7 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑋 𝑧𝑦 (𝑋𝑧)) ≠ ∅)
171 disj3 4164 . . . . . . . 8 ((𝑋 𝑧𝑦 (𝑋𝑧)) = ∅ ↔ 𝑋 = (𝑋 𝑧𝑦 (𝑋𝑧)))
172171necon3bii 2995 . . . . . . 7 ((𝑋 𝑧𝑦 (𝑋𝑧)) ≠ ∅ ↔ 𝑋 ≠ (𝑋 𝑧𝑦 (𝑋𝑧)))
173170, 172sylib 208 . . . . . 6 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑋 ≠ (𝑋 𝑧𝑦 (𝑋𝑧)))
174 iundif2 4721 . . . . . . 7 𝑧𝑦 (𝑋 ∖ (𝑋𝑧)) = (𝑋 𝑧𝑦 (𝑋𝑧))
175 dfss4 4007 . . . . . . . . . 10 (𝑧𝑋 ↔ (𝑋 ∖ (𝑋𝑧)) = 𝑧)
176150, 175sylib 208 . . . . . . . . 9 ((((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧𝑦) → (𝑋 ∖ (𝑋𝑧)) = 𝑧)
177176iuneq2dv 4676 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑧𝑦 (𝑋 ∖ (𝑋𝑧)) = 𝑧𝑦 𝑧)
178 uniiun 4707 . . . . . . . 8 𝑦 = 𝑧𝑦 𝑧
179177, 178syl6eqr 2823 . . . . . . 7 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑧𝑦 (𝑋 ∖ (𝑋𝑧)) = 𝑦)
180174, 179syl5eqr 2819 . . . . . 6 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑋 𝑧𝑦 (𝑋𝑧)) = 𝑦)
181173, 180neeqtrd 3012 . . . . 5 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑋 𝑦)
18211adantr 466 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) → 𝐹 ∈ (Fil‘𝑋))
183 filtop 21879 . . . . . . 7 (𝐹 ∈ (Fil‘𝑋) → 𝑋𝐹)
184 fileln0 21874 . . . . . . 7 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑋𝐹) → 𝑋 ≠ ∅)
185183, 184mpdan 667 . . . . . 6 (𝐹 ∈ (Fil‘𝑋) → 𝑋 ≠ ∅)
186182, 185syl 17 . . . . 5 ((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) → 𝑋 ≠ ∅)
187122, 181, 186pm2.61ne 3028 . . . 4 ((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) → 𝑋 𝑦)
188187neneqd 2948 . . 3 ((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) → ¬ 𝑋 = 𝑦)
189188nrexdv 3149 . 2 (𝜑 → ¬ ∃𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)𝑋 = 𝑦)
190118, 189pm2.65i 185 1 ¬ 𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382   = wceq 1631  wcel 2145  {cab 2757  wne 2943  wral 3061  wrex 3062  Vcvv 3351  cdif 3720  cin 3722  wss 3723  c0 4063  𝒫 cpw 4297  {csn 4316   cuni 4574   cint 4611   ciun 4654   ciin 4655  cmpt 4863  dom cdm 5249  ran crn 5250  wf 6027  cfv 6031  (class class class)co 6793  Fincfn 8109  ficfi 8472  topGenctg 16306  TopOnctopon 20935  TopBasesctb 20970  Filcfil 21869  UFilcufil 21923  UFLcufl 21924   fLim cflim 21958
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-iin 4657  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-om 7213  df-1st 7315  df-2nd 7316  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-1o 7713  df-oadd 7717  df-er 7896  df-en 8110  df-dom 8111  df-fin 8113  df-fi 8473  df-topgen 16312  df-fbas 19958  df-top 20919  df-topon 20936  df-bases 20971  df-ntr 21045  df-nei 21123  df-fil 21870  df-ufil 21925  df-flim 21963
This theorem is referenced by:  alexsub  22069
  Copyright terms: Public domain W3C validator