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

Theorem alexsublem 22653
Description: Lemma for alexsub 22654. (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 3894 . . . . . . . . . 10 (𝑥 ∈ (𝑋 (𝐵𝐹)) ↔ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹)))
2 alexsub.3 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐽 = (topGen‘(fi‘𝐵)))
32eleq2d 2878 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑦𝐽𝑦 ∈ (topGen‘(fi‘𝐵))))
43anbi1d 632 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑦𝐽𝑥𝑦) ↔ (𝑦 ∈ (topGen‘(fi‘𝐵)) ∧ 𝑥𝑦)))
54biimpa 480 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑦𝐽𝑥𝑦)) → (𝑦 ∈ (topGen‘(fi‘𝐵)) ∧ 𝑥𝑦))
65adantlr 714 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦𝐽𝑥𝑦)) → (𝑦 ∈ (topGen‘(fi‘𝐵)) ∧ 𝑥𝑦))
7 tg2 21574 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ (topGen‘(fi‘𝐵)) ∧ 𝑥𝑦) → ∃𝑧 ∈ (fi‘𝐵)(𝑥𝑧𝑧𝑦))
86, 7syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦𝐽𝑥𝑦)) → ∃𝑧 ∈ (fi‘𝐵)(𝑥𝑧𝑧𝑦))
9 alexsub.5 . . . . . . . . . . . . . . . . . 18 (𝜑𝐹 ∈ (UFil‘𝑋))
10 ufilfil 22513 . . . . . . . . . . . . . . . . . 18 (𝐹 ∈ (UFil‘𝑋) → 𝐹 ∈ (Fil‘𝑋))
119, 10syl 17 . . . . . . . . . . . . . . . . 17 (𝜑𝐹 ∈ (Fil‘𝑋))
1211ad3antrrr 729 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦𝐽𝑥𝑦)) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥𝑧𝑧𝑦))) → 𝐹 ∈ (Fil‘𝑋))
13 alexsub.2 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑋 = 𝐵)
149elfvexd 6683 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑋 ∈ V)
1513, 14eqeltrrd 2894 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 𝐵 ∈ V)
16 uniexb 7470 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐵 ∈ V ↔ 𝐵 ∈ V)
1715, 16sylibr 237 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐵 ∈ V)
18 elfi2 8866 . . . . . . . . . . . . . . . . . . . . . 22 (𝐵 ∈ V → (𝑧 ∈ (fi‘𝐵) ↔ ∃𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})𝑧 = 𝑦))
1917, 18syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑧 ∈ (fi‘𝐵) ↔ ∃𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})𝑧 = 𝑦))
2019adantr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) → (𝑧 ∈ (fi‘𝐵) ↔ ∃𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})𝑧 = 𝑦))
2111ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦)) → 𝐹 ∈ (Fil‘𝑋))
22 simplrr 777 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦) ∧ 𝑧𝑦)) → ¬ 𝑥 (𝐵𝐹))
23 intss1 4856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑧𝑦 𝑦𝑧)
2423adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦) ∧ 𝑧𝑦) → 𝑦𝑧)
25 simplr 768 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦) ∧ 𝑧𝑦) → 𝑥 𝑦)
2624, 25sseldd 3919 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦) ∧ 𝑧𝑦) → 𝑥𝑧)
2726ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦) ∧ 𝑧𝑦)) ∧ ¬ 𝑧𝐹) → 𝑥𝑧)
28 eldifsn 4683 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ↔ (𝑦 ∈ (𝒫 𝐵 ∩ Fin) ∧ 𝑦 ≠ ∅))
2928simplbi 501 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) → 𝑦 ∈ (𝒫 𝐵 ∩ Fin))
3029ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦)) → 𝑦 ∈ (𝒫 𝐵 ∩ Fin))
31 elfpw 8814 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝑦𝐵𝑦 ∈ Fin))
3231simplbi 501 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 ∈ (𝒫 𝐵 ∩ Fin) → 𝑦𝐵)
3330, 32syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦)) → 𝑦𝐵)
3433sselda 3918 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦)) ∧ 𝑧𝑦) → 𝑧𝐵)
3534anasss 470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦) ∧ 𝑧𝑦)) → 𝑧𝐵)
3635anim1i 617 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦) ∧ 𝑧𝑦)) ∧ ¬ 𝑧𝐹) → (𝑧𝐵 ∧ ¬ 𝑧𝐹))
37 eldif 3894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑧 ∈ (𝐵𝐹) ↔ (𝑧𝐵 ∧ ¬ 𝑧𝐹))
3836, 37sylibr 237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦) ∧ 𝑧𝑦)) ∧ ¬ 𝑧𝐹) → 𝑧 ∈ (𝐵𝐹))
39 elunii 4808 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑥𝑧𝑧 ∈ (𝐵𝐹)) → 𝑥 (𝐵𝐹))
4027, 38, 39syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦) ∧ 𝑧𝑦)) ∧ ¬ 𝑧𝐹) → 𝑥 (𝐵𝐹))
4140ex 416 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦) ∧ 𝑧𝑦)) → (¬ 𝑧𝐹𝑥 (𝐵𝐹)))
4222, 41mt3d 150 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦) ∧ 𝑧𝑦)) → 𝑧𝐹)
4342expr 460 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦)) → (𝑧𝑦𝑧𝐹))
4443ssrdv 3924 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦)) → 𝑦𝐹)
45 eldifsni 4686 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) → 𝑦 ≠ ∅)
4645ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦)) → 𝑦 ≠ ∅)
47 elinel2 4126 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ (𝒫 𝐵 ∩ Fin) → 𝑦 ∈ Fin)
4830, 47syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦)) → 𝑦 ∈ Fin)
49 elfir 8867 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑦𝐹𝑦 ≠ ∅ ∧ 𝑦 ∈ Fin)) → 𝑦 ∈ (fi‘𝐹))
5021, 44, 46, 48, 49syl13anc 1369 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦)) → 𝑦 ∈ (fi‘𝐹))
51 filfi 22468 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐹 ∈ (Fil‘𝑋) → (fi‘𝐹) = 𝐹)
5221, 51syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦)) → (fi‘𝐹) = 𝐹)
5350, 52eleqtrd 2895 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 𝑦)) → 𝑦𝐹)
5453expr 460 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ 𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})) → (𝑥 𝑦 𝑦𝐹))
55 eleq2 2881 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = 𝑦 → (𝑥𝑧𝑥 𝑦))
56 eleq1 2880 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = 𝑦 → (𝑧𝐹 𝑦𝐹))
5755, 56imbi12d 348 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = 𝑦 → ((𝑥𝑧𝑧𝐹) ↔ (𝑥 𝑦 𝑦𝐹)))
5854, 57syl5ibrcom 250 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ 𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})) → (𝑧 = 𝑦 → (𝑥𝑧𝑧𝐹)))
5958rexlimdva 3246 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) → (∃𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})𝑧 = 𝑦 → (𝑥𝑧𝑧𝐹)))
6020, 59sylbid 243 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) → (𝑧 ∈ (fi‘𝐵) → (𝑥𝑧𝑧𝐹)))
6160imp32 422 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑧 ∈ (fi‘𝐵) ∧ 𝑥𝑧)) → 𝑧𝐹)
6261adantrrr 724 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥𝑧𝑧𝑦))) → 𝑧𝐹)
6362adantlr 714 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦𝐽𝑥𝑦)) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥𝑧𝑧𝑦))) → 𝑧𝐹)
64 elssuni 4833 . . . . . . . . . . . . . . . . . . 19 (𝑦𝐽𝑦 𝐽)
6564ad2antrl 727 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦𝐽𝑥𝑦)) → 𝑦 𝐽)
66 fibas 21586 . . . . . . . . . . . . . . . . . . . . . . 23 (fi‘𝐵) ∈ TopBases
67 tgtopon 21580 . . . . . . . . . . . . . . . . . . . . . . 23 ((fi‘𝐵) ∈ TopBases → (topGen‘(fi‘𝐵)) ∈ (TopOn‘ (fi‘𝐵)))
6866, 67ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 (topGen‘(fi‘𝐵)) ∈ (TopOn‘ (fi‘𝐵))
692, 68eqeltrdi 2901 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐽 ∈ (TopOn‘ (fi‘𝐵)))
70 fiuni 8880 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐵 ∈ V → 𝐵 = (fi‘𝐵))
7117, 70syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 𝐵 = (fi‘𝐵))
7213, 71eqtrd 2836 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑋 = (fi‘𝐵))
7372fveq2d 6653 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (TopOn‘𝑋) = (TopOn‘ (fi‘𝐵)))
7469, 73eleqtrrd 2896 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐽 ∈ (TopOn‘𝑋))
75 toponuni 21523 . . . . . . . . . . . . . . . . . . . 20 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
7674, 75syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑋 = 𝐽)
7776ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦𝐽𝑥𝑦)) → 𝑋 = 𝐽)
7865, 77sseqtrrd 3959 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦𝐽𝑥𝑦)) → 𝑦𝑋)
7978adantr 484 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦𝐽𝑥𝑦)) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥𝑧𝑧𝑦))) → 𝑦𝑋)
80 simprrr 781 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦𝐽𝑥𝑦)) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥𝑧𝑧𝑦))) → 𝑧𝑦)
81 filss 22462 . . . . . . . . . . . . . . . 16 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑧𝐹𝑦𝑋𝑧𝑦)) → 𝑦𝐹)
8212, 63, 79, 80, 81syl13anc 1369 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦𝐽𝑥𝑦)) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥𝑧𝑧𝑦))) → 𝑦𝐹)
838, 82rexlimddv 3253 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ (𝑦𝐽𝑥𝑦)) → 𝑦𝐹)
8483expr 460 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) ∧ 𝑦𝐽) → (𝑥𝑦𝑦𝐹))
8584ralrimiva 3152 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹))) → ∀𝑦𝐽 (𝑥𝑦𝑦𝐹))
8685expr 460 . . . . . . . . . . 11 ((𝜑𝑥𝑋) → (¬ 𝑥 (𝐵𝐹) → ∀𝑦𝐽 (𝑥𝑦𝑦𝐹)))
8786imdistanda 575 . . . . . . . . . 10 (𝜑 → ((𝑥𝑋 ∧ ¬ 𝑥 (𝐵𝐹)) → (𝑥𝑋 ∧ ∀𝑦𝐽 (𝑥𝑦𝑦𝐹))))
881, 87syl5bi 245 . . . . . . . . 9 (𝜑 → (𝑥 ∈ (𝑋 (𝐵𝐹)) → (𝑥𝑋 ∧ ∀𝑦𝐽 (𝑥𝑦𝑦𝐹))))
89 flimopn 22584 . . . . . . . . . 10 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) → (𝑥 ∈ (𝐽 fLim 𝐹) ↔ (𝑥𝑋 ∧ ∀𝑦𝐽 (𝑥𝑦𝑦𝐹))))
9074, 11, 89syl2anc 587 . . . . . . . . 9 (𝜑 → (𝑥 ∈ (𝐽 fLim 𝐹) ↔ (𝑥𝑋 ∧ ∀𝑦𝐽 (𝑥𝑦𝑦𝐹))))
9188, 90sylibrd 262 . . . . . . . 8 (𝜑 → (𝑥 ∈ (𝑋 (𝐵𝐹)) → 𝑥 ∈ (𝐽 fLim 𝐹)))
9291ssrdv 3924 . . . . . . 7 (𝜑 → (𝑋 (𝐵𝐹)) ⊆ (𝐽 fLim 𝐹))
93 alexsub.6 . . . . . . 7 (𝜑 → (𝐽 fLim 𝐹) = ∅)
94 sseq0 4310 . . . . . . 7 (((𝑋 (𝐵𝐹)) ⊆ (𝐽 fLim 𝐹) ∧ (𝐽 fLim 𝐹) = ∅) → (𝑋 (𝐵𝐹)) = ∅)
9592, 93, 94syl2anc 587 . . . . . 6 (𝜑 → (𝑋 (𝐵𝐹)) = ∅)
96 ssdif0 4280 . . . . . 6 (𝑋 (𝐵𝐹) ↔ (𝑋 (𝐵𝐹)) = ∅)
9795, 96sylibr 237 . . . . 5 (𝜑𝑋 (𝐵𝐹))
98 difss 4062 . . . . . . 7 (𝐵𝐹) ⊆ 𝐵
9998unissi 4812 . . . . . 6 (𝐵𝐹) ⊆ 𝐵
10099, 13sseqtrrid 3971 . . . . 5 (𝜑 (𝐵𝐹) ⊆ 𝑋)
10197, 100eqssd 3935 . . . 4 (𝜑𝑋 = (𝐵𝐹))
102101, 98jctil 523 . . 3 (𝜑 → ((𝐵𝐹) ⊆ 𝐵𝑋 = (𝐵𝐹)))
103 difexg 5198 . . . . . 6 (𝐵 ∈ V → (𝐵𝐹) ∈ V)
10417, 103syl 17 . . . . 5 (𝜑 → (𝐵𝐹) ∈ V)
105104adantr 484 . . . 4 ((𝜑 ∧ ((𝐵𝐹) ⊆ 𝐵𝑋 = (𝐵𝐹))) → (𝐵𝐹) ∈ V)
106 sseq1 3943 . . . . . . . 8 (𝑥 = (𝐵𝐹) → (𝑥𝐵 ↔ (𝐵𝐹) ⊆ 𝐵))
107 unieq 4814 . . . . . . . . 9 (𝑥 = (𝐵𝐹) → 𝑥 = (𝐵𝐹))
108107eqeq2d 2812 . . . . . . . 8 (𝑥 = (𝐵𝐹) → (𝑋 = 𝑥𝑋 = (𝐵𝐹)))
109106, 108anbi12d 633 . . . . . . 7 (𝑥 = (𝐵𝐹) → ((𝑥𝐵𝑋 = 𝑥) ↔ ((𝐵𝐹) ⊆ 𝐵𝑋 = (𝐵𝐹))))
110109anbi2d 631 . . . . . 6 (𝑥 = (𝐵𝐹) → ((𝜑 ∧ (𝑥𝐵𝑋 = 𝑥)) ↔ (𝜑 ∧ ((𝐵𝐹) ⊆ 𝐵𝑋 = (𝐵𝐹)))))
111 pweq 4516 . . . . . . . 8 (𝑥 = (𝐵𝐹) → 𝒫 𝑥 = 𝒫 (𝐵𝐹))
112111ineq1d 4141 . . . . . . 7 (𝑥 = (𝐵𝐹) → (𝒫 𝑥 ∩ Fin) = (𝒫 (𝐵𝐹) ∩ Fin))
113112rexeqdv 3368 . . . . . 6 (𝑥 = (𝐵𝐹) → (∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = 𝑦 ↔ ∃𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)𝑋 = 𝑦))
114110, 113imbi12d 348 . . . . 5 (𝑥 = (𝐵𝐹) → (((𝜑 ∧ (𝑥𝐵𝑋 = 𝑥)) → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = 𝑦) ↔ ((𝜑 ∧ ((𝐵𝐹) ⊆ 𝐵𝑋 = (𝐵𝐹))) → ∃𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)𝑋 = 𝑦)))
115 alexsub.4 . . . . 5 ((𝜑 ∧ (𝑥𝐵𝑋 = 𝑥)) → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = 𝑦)
116114, 115vtoclg 3518 . . . 4 ((𝐵𝐹) ∈ V → ((𝜑 ∧ ((𝐵𝐹) ⊆ 𝐵𝑋 = (𝐵𝐹))) → ∃𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)𝑋 = 𝑦))
117105, 116mpcom 38 . . 3 ((𝜑 ∧ ((𝐵𝐹) ⊆ 𝐵𝑋 = (𝐵𝐹))) → ∃𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)𝑋 = 𝑦)
118102, 117mpdan 686 . 2 (𝜑 → ∃𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)𝑋 = 𝑦)
119 unieq 4814 . . . . . . 7 (𝑦 = ∅ → 𝑦 = ∅)
120 uni0 4831 . . . . . . 7 ∅ = ∅
121119, 120eqtrdi 2852 . . . . . 6 (𝑦 = ∅ → 𝑦 = ∅)
122121neeq2d 3050 . . . . 5 (𝑦 = ∅ → (𝑋 𝑦𝑋 ≠ ∅))
123 difssd 4063 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) → (𝑋𝑧) ⊆ 𝑋)
124123ralrimivw 3153 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) → ∀𝑧𝑦 (𝑋𝑧) ⊆ 𝑋)
125 riinn0 4971 . . . . . . . . . 10 ((∀𝑧𝑦 (𝑋𝑧) ⊆ 𝑋𝑦 ≠ ∅) → (𝑋 𝑧𝑦 (𝑋𝑧)) = 𝑧𝑦 (𝑋𝑧))
126124, 125sylan 583 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑋 𝑧𝑦 (𝑋𝑧)) = 𝑧𝑦 (𝑋𝑧))
12714ad2antrr 725 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑋 ∈ V)
128 difexg 5198 . . . . . . . . . . . . 13 (𝑋 ∈ V → (𝑋𝑧) ∈ V)
129127, 128syl 17 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑋𝑧) ∈ V)
130129ralrimivw 3153 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ∀𝑧𝑦 (𝑋𝑧) ∈ V)
131 dfiin2g 4922 . . . . . . . . . . 11 (∀𝑧𝑦 (𝑋𝑧) ∈ V → 𝑧𝑦 (𝑋𝑧) = {𝑥 ∣ ∃𝑧𝑦 𝑥 = (𝑋𝑧)})
132130, 131syl 17 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑧𝑦 (𝑋𝑧) = {𝑥 ∣ ∃𝑧𝑦 𝑥 = (𝑋𝑧)})
133 eqid 2801 . . . . . . . . . . . 12 (𝑧𝑦 ↦ (𝑋𝑧)) = (𝑧𝑦 ↦ (𝑋𝑧))
134133rnmpt 5795 . . . . . . . . . . 11 ran (𝑧𝑦 ↦ (𝑋𝑧)) = {𝑥 ∣ ∃𝑧𝑦 𝑥 = (𝑋𝑧)}
135134inteqi 4845 . . . . . . . . . 10 ran (𝑧𝑦 ↦ (𝑋𝑧)) = {𝑥 ∣ ∃𝑧𝑦 𝑥 = (𝑋𝑧)}
136132, 135eqtr4di 2854 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑧𝑦 (𝑋𝑧) = ran (𝑧𝑦 ↦ (𝑋𝑧)))
137126, 136eqtrd 2836 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑋 𝑧𝑦 (𝑋𝑧)) = ran (𝑧𝑦 ↦ (𝑋𝑧)))
13811ad2antrr 725 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝐹 ∈ (Fil‘𝑋))
139 elfpw 8814 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin) ↔ (𝑦 ⊆ (𝐵𝐹) ∧ 𝑦 ∈ Fin))
140139simplbi 501 . . . . . . . . . . . . . . 15 (𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin) → 𝑦 ⊆ (𝐵𝐹))
141140ad2antlr 726 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑦 ⊆ (𝐵𝐹))
142141sselda 3918 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧𝑦) → 𝑧 ∈ (𝐵𝐹))
143142eldifbd 3897 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧𝑦) → ¬ 𝑧𝐹)
1449ad3antrrr 729 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧𝑦) → 𝐹 ∈ (UFil‘𝑋))
145141difss2d 4065 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑦𝐵)
146145sselda 3918 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧𝑦) → 𝑧𝐵)
147 elssuni 4833 . . . . . . . . . . . . . . 15 (𝑧𝐵𝑧 𝐵)
148146, 147syl 17 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧𝑦) → 𝑧 𝐵)
14913ad3antrrr 729 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧𝑦) → 𝑋 = 𝐵)
150148, 149sseqtrrd 3959 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧𝑦) → 𝑧𝑋)
151 ufilb 22515 . . . . . . . . . . . . 13 ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑧𝑋) → (¬ 𝑧𝐹 ↔ (𝑋𝑧) ∈ 𝐹))
152144, 150, 151syl2anc 587 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧𝑦) → (¬ 𝑧𝐹 ↔ (𝑋𝑧) ∈ 𝐹))
153143, 152mpbid 235 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧𝑦) → (𝑋𝑧) ∈ 𝐹)
154153fmpttd 6860 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑧𝑦 ↦ (𝑋𝑧)):𝑦𝐹)
155154frnd 6498 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ran (𝑧𝑦 ↦ (𝑋𝑧)) ⊆ 𝐹)
156133, 153dmmptd 6469 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → dom (𝑧𝑦 ↦ (𝑋𝑧)) = 𝑦)
157 simpr 488 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑦 ≠ ∅)
158156, 157eqnetrd 3057 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → dom (𝑧𝑦 ↦ (𝑋𝑧)) ≠ ∅)
159 dm0rn0 5763 . . . . . . . . . . 11 (dom (𝑧𝑦 ↦ (𝑋𝑧)) = ∅ ↔ ran (𝑧𝑦 ↦ (𝑋𝑧)) = ∅)
160159necon3bii 3042 . . . . . . . . . 10 (dom (𝑧𝑦 ↦ (𝑋𝑧)) ≠ ∅ ↔ ran (𝑧𝑦 ↦ (𝑋𝑧)) ≠ ∅)
161158, 160sylib 221 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ran (𝑧𝑦 ↦ (𝑋𝑧)) ≠ ∅)
162 elinel2 4126 . . . . . . . . . . 11 (𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin) → 𝑦 ∈ Fin)
163162ad2antlr 726 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑦 ∈ Fin)
164 abrexfi 8812 . . . . . . . . . . 11 (𝑦 ∈ Fin → {𝑥 ∣ ∃𝑧𝑦 𝑥 = (𝑋𝑧)} ∈ Fin)
165134, 164eqeltrid 2897 . . . . . . . . . 10 (𝑦 ∈ Fin → ran (𝑧𝑦 ↦ (𝑋𝑧)) ∈ Fin)
166163, 165syl 17 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ran (𝑧𝑦 ↦ (𝑋𝑧)) ∈ Fin)
167 filintn0 22470 . . . . . . . . 9 ((𝐹 ∈ (Fil‘𝑋) ∧ (ran (𝑧𝑦 ↦ (𝑋𝑧)) ⊆ 𝐹 ∧ ran (𝑧𝑦 ↦ (𝑋𝑧)) ≠ ∅ ∧ ran (𝑧𝑦 ↦ (𝑋𝑧)) ∈ Fin)) → ran (𝑧𝑦 ↦ (𝑋𝑧)) ≠ ∅)
168138, 155, 161, 166, 167syl13anc 1369 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ran (𝑧𝑦 ↦ (𝑋𝑧)) ≠ ∅)
169137, 168eqnetrd 3057 . . . . . . 7 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑋 𝑧𝑦 (𝑋𝑧)) ≠ ∅)
170 disj3 4364 . . . . . . . 8 ((𝑋 𝑧𝑦 (𝑋𝑧)) = ∅ ↔ 𝑋 = (𝑋 𝑧𝑦 (𝑋𝑧)))
171170necon3bii 3042 . . . . . . 7 ((𝑋 𝑧𝑦 (𝑋𝑧)) ≠ ∅ ↔ 𝑋 ≠ (𝑋 𝑧𝑦 (𝑋𝑧)))
172169, 171sylib 221 . . . . . 6 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑋 ≠ (𝑋 𝑧𝑦 (𝑋𝑧)))
173 iundif2 4962 . . . . . . 7 𝑧𝑦 (𝑋 ∖ (𝑋𝑧)) = (𝑋 𝑧𝑦 (𝑋𝑧))
174 dfss4 4188 . . . . . . . . . 10 (𝑧𝑋 ↔ (𝑋 ∖ (𝑋𝑧)) = 𝑧)
175150, 174sylib 221 . . . . . . . . 9 ((((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧𝑦) → (𝑋 ∖ (𝑋𝑧)) = 𝑧)
176175iuneq2dv 4908 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑧𝑦 (𝑋 ∖ (𝑋𝑧)) = 𝑧𝑦 𝑧)
177 uniiun 4948 . . . . . . . 8 𝑦 = 𝑧𝑦 𝑧
178176, 177eqtr4di 2854 . . . . . . 7 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑧𝑦 (𝑋 ∖ (𝑋𝑧)) = 𝑦)
179173, 178syl5eqr 2850 . . . . . 6 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑋 𝑧𝑦 (𝑋𝑧)) = 𝑦)
180172, 179neeqtrd 3059 . . . . 5 (((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑋 𝑦)
18111adantr 484 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) → 𝐹 ∈ (Fil‘𝑋))
182 filtop 22464 . . . . . 6 (𝐹 ∈ (Fil‘𝑋) → 𝑋𝐹)
183 fileln0 22459 . . . . . 6 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑋𝐹) → 𝑋 ≠ ∅)
184181, 182, 183syl2anc2 588 . . . . 5 ((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) → 𝑋 ≠ ∅)
185122, 180, 184pm2.61ne 3075 . . . 4 ((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) → 𝑋 𝑦)
186185neneqd 2995 . . 3 ((𝜑𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)) → ¬ 𝑋 = 𝑦)
187186nrexdv 3232 . 2 (𝜑 → ¬ ∃𝑦 ∈ (𝒫 (𝐵𝐹) ∩ Fin)𝑋 = 𝑦)
188118, 187pm2.65i 197 1 ¬ 𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399   = wceq 1538  wcel 2112  {cab 2779  wne 2990  wral 3109  wrex 3110  Vcvv 3444  cdif 3881  cin 3883  wss 3884  c0 4246  𝒫 cpw 4500  {csn 4528   cuni 4803   cint 4841   ciun 4884   ciin 4885  cmpt 5113  dom cdm 5523  ran crn 5524  cfv 6328  (class class class)co 7139  Fincfn 8496  ficfi 8862  topGenctg 16707  TopOnctopon 21519  TopBasesctb 21554  Filcfil 22454  UFilcufil 22508  UFLcufl 22509   fLim cflim 22543
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-reu 3116  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-int 4842  df-iun 4886  df-iin 4887  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-ov 7142  df-oprab 7143  df-mpo 7144  df-om 7565  df-1st 7675  df-2nd 7676  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-oadd 8093  df-er 8276  df-en 8497  df-dom 8498  df-fin 8500  df-fi 8863  df-topgen 16713  df-fbas 20092  df-top 21503  df-topon 21520  df-bases 21555  df-ntr 21629  df-nei 21707  df-fil 22455  df-ufil 22510  df-flim 22548
This theorem is referenced by:  alexsub  22654
  Copyright terms: Public domain W3C validator