Step | Hyp | Ref
| Expression |
1 | | filnet.h |
. . . . 5
⊢ 𝐻 = ∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛) |
2 | | filnet.d |
. . . . 5
⊢ 𝐷 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) ∧ (1st ‘𝑦) ⊆ (1st
‘𝑥))} |
3 | 1, 2 | filnetlem3 33841 |
. . . 4
⊢ (𝐻 = ∪
∪ 𝐷 ∧ (𝐹 ∈ (Fil‘𝑋) → (𝐻 ⊆ (𝐹 × 𝑋) ∧ 𝐷 ∈ DirRel))) |
4 | 3 | simpri 489 |
. . 3
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐻 ⊆ (𝐹 × 𝑋) ∧ 𝐷 ∈ DirRel)) |
5 | 4 | simprd 499 |
. 2
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐷 ∈ DirRel) |
6 | | f2ndres 7696 |
. . . . 5
⊢
(2nd ↾ (𝐹 × 𝑋)):(𝐹 × 𝑋)⟶𝑋 |
7 | 4 | simpld 498 |
. . . . 5
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐻 ⊆ (𝐹 × 𝑋)) |
8 | | fssres2 6520 |
. . . . 5
⊢
(((2nd ↾ (𝐹 × 𝑋)):(𝐹 × 𝑋)⟶𝑋 ∧ 𝐻 ⊆ (𝐹 × 𝑋)) → (2nd ↾ 𝐻):𝐻⟶𝑋) |
9 | 6, 7, 8 | sylancr 590 |
. . . 4
⊢ (𝐹 ∈ (Fil‘𝑋) → (2nd ↾
𝐻):𝐻⟶𝑋) |
10 | | filtop 22460 |
. . . . . 6
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐹) |
11 | | xpexg 7453 |
. . . . . 6
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑋 ∈ 𝐹) → (𝐹 × 𝑋) ∈ V) |
12 | 10, 11 | mpdan 686 |
. . . . 5
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 × 𝑋) ∈ V) |
13 | 12, 7 | ssexd 5192 |
. . . 4
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐻 ∈ V) |
14 | | fex 6966 |
. . . 4
⊢
(((2nd ↾ 𝐻):𝐻⟶𝑋 ∧ 𝐻 ∈ V) → (2nd ↾
𝐻) ∈
V) |
15 | 9, 13, 14 | syl2anc 587 |
. . 3
⊢ (𝐹 ∈ (Fil‘𝑋) → (2nd ↾
𝐻) ∈
V) |
16 | 3 | simpli 487 |
. . . . . . 7
⊢ 𝐻 = ∪
∪ 𝐷 |
17 | | dirdm 17836 |
. . . . . . . 8
⊢ (𝐷 ∈ DirRel → dom 𝐷 = ∪
∪ 𝐷) |
18 | 5, 17 | syl 17 |
. . . . . . 7
⊢ (𝐹 ∈ (Fil‘𝑋) → dom 𝐷 = ∪ ∪ 𝐷) |
19 | 16, 18 | eqtr4id 2852 |
. . . . . 6
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐻 = dom 𝐷) |
20 | 19 | feq2d 6473 |
. . . . 5
⊢ (𝐹 ∈ (Fil‘𝑋) → ((2nd
↾ 𝐻):𝐻⟶𝑋 ↔ (2nd ↾ 𝐻):dom 𝐷⟶𝑋)) |
21 | 9, 20 | mpbid 235 |
. . . 4
⊢ (𝐹 ∈ (Fil‘𝑋) → (2nd ↾
𝐻):dom 𝐷⟶𝑋) |
22 | | eqid 2798 |
. . . . . . . . . . . . . 14
⊢ dom 𝐷 = dom 𝐷 |
23 | 22 | tailf 33836 |
. . . . . . . . . . . . 13
⊢ (𝐷 ∈ DirRel →
(tail‘𝐷):dom 𝐷⟶𝒫 dom 𝐷) |
24 | 5, 23 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (Fil‘𝑋) → (tail‘𝐷):dom 𝐷⟶𝒫 dom 𝐷) |
25 | 19 | feq2d 6473 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (Fil‘𝑋) → ((tail‘𝐷):𝐻⟶𝒫 dom 𝐷 ↔ (tail‘𝐷):dom 𝐷⟶𝒫 dom 𝐷)) |
26 | 24, 25 | mpbird 260 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (Fil‘𝑋) → (tail‘𝐷):𝐻⟶𝒫 dom 𝐷) |
27 | 26 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) → (tail‘𝐷):𝐻⟶𝒫 dom 𝐷) |
28 | | ffn 6487 |
. . . . . . . . . 10
⊢
((tail‘𝐷):𝐻⟶𝒫 dom 𝐷 → (tail‘𝐷) Fn 𝐻) |
29 | | imaeq2 5892 |
. . . . . . . . . . . 12
⊢ (𝑑 = ((tail‘𝐷)‘𝑓) → ((2nd ↾ 𝐻) “ 𝑑) = ((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓))) |
30 | 29 | sseq1d 3946 |
. . . . . . . . . . 11
⊢ (𝑑 = ((tail‘𝐷)‘𝑓) → (((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡 ↔ ((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡)) |
31 | 30 | rexrn 6830 |
. . . . . . . . . 10
⊢
((tail‘𝐷) Fn
𝐻 → (∃𝑑 ∈ ran (tail‘𝐷)((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡 ↔ ∃𝑓 ∈ 𝐻 ((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡)) |
32 | 27, 28, 31 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) → (∃𝑑 ∈ ran (tail‘𝐷)((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡 ↔ ∃𝑓 ∈ 𝐻 ((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡)) |
33 | | fo2nd 7692 |
. . . . . . . . . . . . . . 15
⊢
2nd :V–onto→V |
34 | | fofn 6567 |
. . . . . . . . . . . . . . 15
⊢
(2nd :V–onto→V → 2nd Fn V) |
35 | 33, 34 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
2nd Fn V |
36 | | ssv 3939 |
. . . . . . . . . . . . . 14
⊢ 𝐻 ⊆ V |
37 | | fnssres 6442 |
. . . . . . . . . . . . . 14
⊢
((2nd Fn V ∧ 𝐻 ⊆ V) → (2nd ↾
𝐻) Fn 𝐻) |
38 | 35, 36, 37 | mp2an 691 |
. . . . . . . . . . . . 13
⊢
(2nd ↾ 𝐻) Fn 𝐻 |
39 | | fnfun 6423 |
. . . . . . . . . . . . 13
⊢
((2nd ↾ 𝐻) Fn 𝐻 → Fun (2nd ↾ 𝐻)) |
40 | 38, 39 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ Fun
(2nd ↾ 𝐻) |
41 | 27 | ffvelrnda 6828 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((tail‘𝐷)‘𝑓) ∈ 𝒫 dom 𝐷) |
42 | 41 | elpwid 4508 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((tail‘𝐷)‘𝑓) ⊆ dom 𝐷) |
43 | 19 | ad2antrr 725 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → 𝐻 = dom 𝐷) |
44 | 42, 43 | sseqtrrd 3956 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((tail‘𝐷)‘𝑓) ⊆ 𝐻) |
45 | 38 | fndmi 6426 |
. . . . . . . . . . . . 13
⊢ dom
(2nd ↾ 𝐻)
= 𝐻 |
46 | 44, 45 | sseqtrrdi 3966 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((tail‘𝐷)‘𝑓) ⊆ dom (2nd ↾ 𝐻)) |
47 | | funimass4 6705 |
. . . . . . . . . . . 12
⊢ ((Fun
(2nd ↾ 𝐻)
∧ ((tail‘𝐷)‘𝑓) ⊆ dom (2nd ↾ 𝐻)) → (((2nd
↾ 𝐻) “
((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∀𝑑 ∈ ((tail‘𝐷)‘𝑓)((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡)) |
48 | 40, 46, 47 | sylancr 590 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → (((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∀𝑑 ∈ ((tail‘𝐷)‘𝑓)((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡)) |
49 | 5 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → 𝐷 ∈ DirRel) |
50 | | simpr 488 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → 𝑓 ∈ 𝐻) |
51 | 50, 43 | eleqtrd 2892 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → 𝑓 ∈ dom 𝐷) |
52 | | vex 3444 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑑 ∈ V |
53 | 52 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → 𝑑 ∈ V) |
54 | 22 | eltail 33835 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ DirRel ∧ 𝑓 ∈ dom 𝐷 ∧ 𝑑 ∈ V) → (𝑑 ∈ ((tail‘𝐷)‘𝑓) ↔ 𝑓𝐷𝑑)) |
55 | 49, 51, 53, 54 | syl3anc 1368 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → (𝑑 ∈ ((tail‘𝐷)‘𝑓) ↔ 𝑓𝐷𝑑)) |
56 | 50 | biantrurd 536 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → (𝑑 ∈ 𝐻 ↔ (𝑓 ∈ 𝐻 ∧ 𝑑 ∈ 𝐻))) |
57 | 56 | anbi1d 632 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st
‘𝑓)) ↔ ((𝑓 ∈ 𝐻 ∧ 𝑑 ∈ 𝐻) ∧ (1st ‘𝑑) ⊆ (1st
‘𝑓)))) |
58 | | vex 3444 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑓 ∈ V |
59 | 1, 2, 58, 52 | filnetlem1 33839 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓𝐷𝑑 ↔ ((𝑓 ∈ 𝐻 ∧ 𝑑 ∈ 𝐻) ∧ (1st ‘𝑑) ⊆ (1st
‘𝑓))) |
60 | 57, 59 | syl6bbr 292 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st
‘𝑓)) ↔ 𝑓𝐷𝑑)) |
61 | 55, 60 | bitr4d 285 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → (𝑑 ∈ ((tail‘𝐷)‘𝑓) ↔ (𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st
‘𝑓)))) |
62 | 61 | imbi1d 345 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((𝑑 ∈ ((tail‘𝐷)‘𝑓) → ((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡) ↔ ((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st
‘𝑓)) →
((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡))) |
63 | | fvres 6664 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑑 ∈ 𝐻 → ((2nd ↾ 𝐻)‘𝑑) = (2nd ‘𝑑)) |
64 | 63 | eleq1d 2874 |
. . . . . . . . . . . . . . . 16
⊢ (𝑑 ∈ 𝐻 → (((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡 ↔ (2nd ‘𝑑) ∈ 𝑡)) |
65 | 64 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st
‘𝑓)) →
(((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡 ↔ (2nd ‘𝑑) ∈ 𝑡)) |
66 | 65 | pm5.74i 274 |
. . . . . . . . . . . . . 14
⊢ (((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st
‘𝑓)) →
((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡) ↔ ((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st
‘𝑓)) →
(2nd ‘𝑑)
∈ 𝑡)) |
67 | | impexp 454 |
. . . . . . . . . . . . . 14
⊢ (((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st
‘𝑓)) →
(2nd ‘𝑑)
∈ 𝑡) ↔ (𝑑 ∈ 𝐻 → ((1st ‘𝑑) ⊆ (1st
‘𝑓) →
(2nd ‘𝑑)
∈ 𝑡))) |
68 | 66, 67 | bitri 278 |
. . . . . . . . . . . . 13
⊢ (((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st
‘𝑓)) →
((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡) ↔ (𝑑 ∈ 𝐻 → ((1st ‘𝑑) ⊆ (1st
‘𝑓) →
(2nd ‘𝑑)
∈ 𝑡))) |
69 | 62, 68 | syl6bb 290 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((𝑑 ∈ ((tail‘𝐷)‘𝑓) → ((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡) ↔ (𝑑 ∈ 𝐻 → ((1st ‘𝑑) ⊆ (1st
‘𝑓) →
(2nd ‘𝑑)
∈ 𝑡)))) |
70 | 69 | ralbidv2 3160 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → (∀𝑑 ∈ ((tail‘𝐷)‘𝑓)((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡 ↔ ∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd
‘𝑑) ∈ 𝑡))) |
71 | 48, 70 | bitrd 282 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → (((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd
‘𝑑) ∈ 𝑡))) |
72 | 71 | rexbidva 3255 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) → (∃𝑓 ∈ 𝐻 ((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∃𝑓 ∈ 𝐻 ∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd
‘𝑑) ∈ 𝑡))) |
73 | | vex 3444 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑘 ∈ V |
74 | | vex 3444 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑣 ∈ V |
75 | 73, 74 | op1std 7681 |
. . . . . . . . . . . . . . . 16
⊢ (𝑑 = 〈𝑘, 𝑣〉 → (1st ‘𝑑) = 𝑘) |
76 | 75 | sseq1d 3946 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 = 〈𝑘, 𝑣〉 → ((1st ‘𝑑) ⊆ (1st
‘𝑓) ↔ 𝑘 ⊆ (1st
‘𝑓))) |
77 | 73, 74 | op2ndd 7682 |
. . . . . . . . . . . . . . . 16
⊢ (𝑑 = 〈𝑘, 𝑣〉 → (2nd ‘𝑑) = 𝑣) |
78 | 77 | eleq1d 2874 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 = 〈𝑘, 𝑣〉 → ((2nd ‘𝑑) ∈ 𝑡 ↔ 𝑣 ∈ 𝑡)) |
79 | 76, 78 | imbi12d 348 |
. . . . . . . . . . . . . 14
⊢ (𝑑 = 〈𝑘, 𝑣〉 → (((1st ‘𝑑) ⊆ (1st
‘𝑓) →
(2nd ‘𝑑)
∈ 𝑡) ↔ (𝑘 ⊆ (1st
‘𝑓) → 𝑣 ∈ 𝑡))) |
80 | 79 | raliunxp 5674 |
. . . . . . . . . . . . 13
⊢
(∀𝑑 ∈
∪ 𝑘 ∈ 𝐹 ({𝑘} × 𝑘)((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd
‘𝑑) ∈ 𝑡) ↔ ∀𝑘 ∈ 𝐹 ∀𝑣 ∈ 𝑘 (𝑘 ⊆ (1st ‘𝑓) → 𝑣 ∈ 𝑡)) |
81 | | sneq 4535 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑘 → {𝑛} = {𝑘}) |
82 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑘 → 𝑛 = 𝑘) |
83 | 81, 82 | xpeq12d 5550 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑘 → ({𝑛} × 𝑛) = ({𝑘} × 𝑘)) |
84 | 83 | cbviunv 4927 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛) = ∪ 𝑘 ∈ 𝐹 ({𝑘} × 𝑘) |
85 | 1, 84 | eqtri 2821 |
. . . . . . . . . . . . . 14
⊢ 𝐻 = ∪ 𝑘 ∈ 𝐹 ({𝑘} × 𝑘) |
86 | 85 | raleqi 3362 |
. . . . . . . . . . . . 13
⊢
(∀𝑑 ∈
𝐻 ((1st
‘𝑑) ⊆
(1st ‘𝑓)
→ (2nd ‘𝑑) ∈ 𝑡) ↔ ∀𝑑 ∈ ∪
𝑘 ∈ 𝐹 ({𝑘} × 𝑘)((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd
‘𝑑) ∈ 𝑡)) |
87 | | dfss3 3903 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ⊆ 𝑡 ↔ ∀𝑣 ∈ 𝑘 𝑣 ∈ 𝑡) |
88 | 87 | imbi2i 339 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ⊆ (1st
‘𝑓) → 𝑘 ⊆ 𝑡) ↔ (𝑘 ⊆ (1st ‘𝑓) → ∀𝑣 ∈ 𝑘 𝑣 ∈ 𝑡)) |
89 | | r19.21v 3142 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑣 ∈
𝑘 (𝑘 ⊆ (1st ‘𝑓) → 𝑣 ∈ 𝑡) ↔ (𝑘 ⊆ (1st ‘𝑓) → ∀𝑣 ∈ 𝑘 𝑣 ∈ 𝑡)) |
90 | 88, 89 | bitr4i 281 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ⊆ (1st
‘𝑓) → 𝑘 ⊆ 𝑡) ↔ ∀𝑣 ∈ 𝑘 (𝑘 ⊆ (1st ‘𝑓) → 𝑣 ∈ 𝑡)) |
91 | 90 | ralbii 3133 |
. . . . . . . . . . . . 13
⊢
(∀𝑘 ∈
𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ ∀𝑘 ∈ 𝐹 ∀𝑣 ∈ 𝑘 (𝑘 ⊆ (1st ‘𝑓) → 𝑣 ∈ 𝑡)) |
92 | 80, 86, 91 | 3bitr4i 306 |
. . . . . . . . . . . 12
⊢
(∀𝑑 ∈
𝐻 ((1st
‘𝑑) ⊆
(1st ‘𝑓)
→ (2nd ‘𝑑) ∈ 𝑡) ↔ ∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡)) |
93 | 92 | rexbii 3210 |
. . . . . . . . . . 11
⊢
(∃𝑓 ∈
𝐻 ∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd
‘𝑑) ∈ 𝑡) ↔ ∃𝑓 ∈ 𝐻 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡)) |
94 | 1 | rexeqi 3363 |
. . . . . . . . . . 11
⊢
(∃𝑓 ∈
𝐻 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ ∃𝑓 ∈ ∪
𝑛 ∈ 𝐹 ({𝑛} × 𝑛)∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡)) |
95 | | vex 3444 |
. . . . . . . . . . . . . . . 16
⊢ 𝑛 ∈ V |
96 | | vex 3444 |
. . . . . . . . . . . . . . . 16
⊢ 𝑚 ∈ V |
97 | 95, 96 | op1std 7681 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = 〈𝑛, 𝑚〉 → (1st ‘𝑓) = 𝑛) |
98 | 97 | sseq2d 3947 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = 〈𝑛, 𝑚〉 → (𝑘 ⊆ (1st ‘𝑓) ↔ 𝑘 ⊆ 𝑛)) |
99 | 98 | imbi1d 345 |
. . . . . . . . . . . . 13
⊢ (𝑓 = 〈𝑛, 𝑚〉 → ((𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡))) |
100 | 99 | ralbidv 3162 |
. . . . . . . . . . . 12
⊢ (𝑓 = 〈𝑛, 𝑚〉 → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡))) |
101 | 100 | rexiunxp 5675 |
. . . . . . . . . . 11
⊢
(∃𝑓 ∈
∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛)∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ ∃𝑛 ∈ 𝐹 ∃𝑚 ∈ 𝑛 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡)) |
102 | 93, 94, 101 | 3bitri 300 |
. . . . . . . . . 10
⊢
(∃𝑓 ∈
𝐻 ∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd
‘𝑑) ∈ 𝑡) ↔ ∃𝑛 ∈ 𝐹 ∃𝑚 ∈ 𝑛 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡)) |
103 | | fileln0 22455 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛 ∈ 𝐹) → 𝑛 ≠ ∅) |
104 | 103 | adantlr 714 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑛 ∈ 𝐹) → 𝑛 ≠ ∅) |
105 | | r19.9rzv 4403 |
. . . . . . . . . . . . 13
⊢ (𝑛 ≠ ∅ →
(∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) ↔ ∃𝑚 ∈ 𝑛 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡))) |
106 | 104, 105 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑛 ∈ 𝐹) → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) ↔ ∃𝑚 ∈ 𝑛 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡))) |
107 | | ssid 3937 |
. . . . . . . . . . . . . . 15
⊢ 𝑛 ⊆ 𝑛 |
108 | | sseq1 3940 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑛 → (𝑘 ⊆ 𝑛 ↔ 𝑛 ⊆ 𝑛)) |
109 | | sseq1 3940 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑛 → (𝑘 ⊆ 𝑡 ↔ 𝑛 ⊆ 𝑡)) |
110 | 108, 109 | imbi12d 348 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑛 → ((𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) ↔ (𝑛 ⊆ 𝑛 → 𝑛 ⊆ 𝑡))) |
111 | 110 | rspcv 3566 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ 𝐹 → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) → (𝑛 ⊆ 𝑛 → 𝑛 ⊆ 𝑡))) |
112 | 107, 111 | mpii 46 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ 𝐹 → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) → 𝑛 ⊆ 𝑡)) |
113 | 112 | adantl 485 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑛 ∈ 𝐹) → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) → 𝑛 ⊆ 𝑡)) |
114 | | sstr2 3922 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ⊆ 𝑛 → (𝑛 ⊆ 𝑡 → 𝑘 ⊆ 𝑡)) |
115 | 114 | com12 32 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ⊆ 𝑡 → (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡)) |
116 | 115 | ralrimivw 3150 |
. . . . . . . . . . . . 13
⊢ (𝑛 ⊆ 𝑡 → ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡)) |
117 | 113, 116 | impbid1 228 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑛 ∈ 𝐹) → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) ↔ 𝑛 ⊆ 𝑡)) |
118 | 106, 117 | bitr3d 284 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑛 ∈ 𝐹) → (∃𝑚 ∈ 𝑛 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) ↔ 𝑛 ⊆ 𝑡)) |
119 | 118 | rexbidva 3255 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) → (∃𝑛 ∈ 𝐹 ∃𝑚 ∈ 𝑛 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) ↔ ∃𝑛 ∈ 𝐹 𝑛 ⊆ 𝑡)) |
120 | 102, 119 | syl5bb 286 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) → (∃𝑓 ∈ 𝐻 ∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd
‘𝑑) ∈ 𝑡) ↔ ∃𝑛 ∈ 𝐹 𝑛 ⊆ 𝑡)) |
121 | 32, 72, 120 | 3bitrd 308 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) → (∃𝑑 ∈ ran (tail‘𝐷)((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡 ↔ ∃𝑛 ∈ 𝐹 𝑛 ⊆ 𝑡)) |
122 | 121 | pm5.32da 582 |
. . . . . . 7
⊢ (𝐹 ∈ (Fil‘𝑋) → ((𝑡 ⊆ 𝑋 ∧ ∃𝑑 ∈ ran (tail‘𝐷)((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡) ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑛 ∈ 𝐹 𝑛 ⊆ 𝑡))) |
123 | | filn0 22467 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ≠ ∅) |
124 | 95 | snnz 4672 |
. . . . . . . . . . . . . . . 16
⊢ {𝑛} ≠ ∅ |
125 | 103, 124 | jctil 523 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛 ∈ 𝐹) → ({𝑛} ≠ ∅ ∧ 𝑛 ≠ ∅)) |
126 | | neanior 3079 |
. . . . . . . . . . . . . . 15
⊢ (({𝑛} ≠ ∅ ∧ 𝑛 ≠ ∅) ↔ ¬
({𝑛} = ∅ ∨ 𝑛 = ∅)) |
127 | 125, 126 | sylib 221 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛 ∈ 𝐹) → ¬ ({𝑛} = ∅ ∨ 𝑛 = ∅)) |
128 | | ss0b 4305 |
. . . . . . . . . . . . . . 15
⊢ (({𝑛} × 𝑛) ⊆ ∅ ↔ ({𝑛} × 𝑛) = ∅) |
129 | | xpeq0 5984 |
. . . . . . . . . . . . . . 15
⊢ (({𝑛} × 𝑛) = ∅ ↔ ({𝑛} = ∅ ∨ 𝑛 = ∅)) |
130 | 128, 129 | bitri 278 |
. . . . . . . . . . . . . 14
⊢ (({𝑛} × 𝑛) ⊆ ∅ ↔ ({𝑛} = ∅ ∨ 𝑛 = ∅)) |
131 | 127, 130 | sylnibr 332 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛 ∈ 𝐹) → ¬ ({𝑛} × 𝑛) ⊆ ∅) |
132 | 131 | ralrimiva 3149 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (Fil‘𝑋) → ∀𝑛 ∈ 𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅) |
133 | | r19.2z 4398 |
. . . . . . . . . . . 12
⊢ ((𝐹 ≠ ∅ ∧
∀𝑛 ∈ 𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅) → ∃𝑛 ∈ 𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅) |
134 | 123, 132,
133 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (Fil‘𝑋) → ∃𝑛 ∈ 𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅) |
135 | | rexnal 3201 |
. . . . . . . . . . 11
⊢
(∃𝑛 ∈
𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅ ↔ ¬ ∀𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅) |
136 | 134, 135 | sylib 221 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (Fil‘𝑋) → ¬ ∀𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅) |
137 | 1 | sseq1i 3943 |
. . . . . . . . . . . 12
⊢ (𝐻 ⊆ ∅ ↔ ∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅) |
138 | | ss0b 4305 |
. . . . . . . . . . . 12
⊢ (𝐻 ⊆ ∅ ↔ 𝐻 = ∅) |
139 | | iunss 4932 |
. . . . . . . . . . . 12
⊢ (∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅ ↔ ∀𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅) |
140 | 137, 138,
139 | 3bitr3i 304 |
. . . . . . . . . . 11
⊢ (𝐻 = ∅ ↔ ∀𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅) |
141 | 140 | necon3abii 3033 |
. . . . . . . . . 10
⊢ (𝐻 ≠ ∅ ↔ ¬
∀𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅) |
142 | 136, 141 | sylibr 237 |
. . . . . . . . 9
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐻 ≠ ∅) |
143 | | dmresi 5888 |
. . . . . . . . . . . 12
⊢ dom ( I
↾ 𝐻) = 𝐻 |
144 | 1, 2 | filnetlem2 33840 |
. . . . . . . . . . . . . 14
⊢ (( I
↾ 𝐻) ⊆ 𝐷 ∧ 𝐷 ⊆ (𝐻 × 𝐻)) |
145 | 144 | simpli 487 |
. . . . . . . . . . . . 13
⊢ ( I
↾ 𝐻) ⊆ 𝐷 |
146 | | dmss 5735 |
. . . . . . . . . . . . 13
⊢ (( I
↾ 𝐻) ⊆ 𝐷 → dom ( I ↾ 𝐻) ⊆ dom 𝐷) |
147 | 145, 146 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ dom ( I
↾ 𝐻) ⊆ dom
𝐷 |
148 | 143, 147 | eqsstrri 3950 |
. . . . . . . . . . 11
⊢ 𝐻 ⊆ dom 𝐷 |
149 | 144 | simpri 489 |
. . . . . . . . . . . . 13
⊢ 𝐷 ⊆ (𝐻 × 𝐻) |
150 | | dmss 5735 |
. . . . . . . . . . . . 13
⊢ (𝐷 ⊆ (𝐻 × 𝐻) → dom 𝐷 ⊆ dom (𝐻 × 𝐻)) |
151 | 149, 150 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ dom 𝐷 ⊆ dom (𝐻 × 𝐻) |
152 | | dmxpid 5764 |
. . . . . . . . . . . 12
⊢ dom
(𝐻 × 𝐻) = 𝐻 |
153 | 151, 152 | sseqtri 3951 |
. . . . . . . . . . 11
⊢ dom 𝐷 ⊆ 𝐻 |
154 | 148, 153 | eqssi 3931 |
. . . . . . . . . 10
⊢ 𝐻 = dom 𝐷 |
155 | 154 | tailfb 33838 |
. . . . . . . . 9
⊢ ((𝐷 ∈ DirRel ∧ 𝐻 ≠ ∅) → ran
(tail‘𝐷) ∈
(fBas‘𝐻)) |
156 | 5, 142, 155 | syl2anc 587 |
. . . . . . . 8
⊢ (𝐹 ∈ (Fil‘𝑋) → ran (tail‘𝐷) ∈ (fBas‘𝐻)) |
157 | | elfm 22552 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝐹 ∧ ran (tail‘𝐷) ∈ (fBas‘𝐻) ∧ (2nd ↾ 𝐻):𝐻⟶𝑋) → (𝑡 ∈ ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)) ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑑 ∈ ran (tail‘𝐷)((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡))) |
158 | 10, 156, 9, 157 | syl3anc 1368 |
. . . . . . 7
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑡 ∈ ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)) ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑑 ∈ ran (tail‘𝐷)((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡))) |
159 | | filfbas 22453 |
. . . . . . . 8
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋)) |
160 | | elfg 22476 |
. . . . . . . 8
⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑡 ∈ (𝑋filGen𝐹) ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑛 ∈ 𝐹 𝑛 ⊆ 𝑡))) |
161 | 159, 160 | syl 17 |
. . . . . . 7
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑡 ∈ (𝑋filGen𝐹) ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑛 ∈ 𝐹 𝑛 ⊆ 𝑡))) |
162 | 122, 158,
161 | 3bitr4d 314 |
. . . . . 6
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑡 ∈ ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)) ↔ 𝑡 ∈ (𝑋filGen𝐹))) |
163 | 162 | eqrdv 2796 |
. . . . 5
⊢ (𝐹 ∈ (Fil‘𝑋) → ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)) = (𝑋filGen𝐹)) |
164 | | fgfil 22480 |
. . . . 5
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑋filGen𝐹) = 𝐹) |
165 | 163, 164 | eqtr2d 2834 |
. . . 4
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 = ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷))) |
166 | 21, 165 | jca 515 |
. . 3
⊢ (𝐹 ∈ (Fil‘𝑋) → ((2nd
↾ 𝐻):dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)))) |
167 | | feq1 6468 |
. . . . 5
⊢ (𝑓 = (2nd ↾ 𝐻) → (𝑓:dom 𝐷⟶𝑋 ↔ (2nd ↾ 𝐻):dom 𝐷⟶𝑋)) |
168 | | oveq2 7143 |
. . . . . . 7
⊢ (𝑓 = (2nd ↾ 𝐻) → (𝑋 FilMap 𝑓) = (𝑋 FilMap (2nd ↾ 𝐻))) |
169 | 168 | fveq1d 6647 |
. . . . . 6
⊢ (𝑓 = (2nd ↾ 𝐻) → ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)) = ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷))) |
170 | 169 | eqeq2d 2809 |
. . . . 5
⊢ (𝑓 = (2nd ↾ 𝐻) → (𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)) ↔ 𝐹 = ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)))) |
171 | 167, 170 | anbi12d 633 |
. . . 4
⊢ (𝑓 = (2nd ↾ 𝐻) → ((𝑓:dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷))) ↔ ((2nd ↾ 𝐻):dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷))))) |
172 | 171 | spcegv 3545 |
. . 3
⊢
((2nd ↾ 𝐻) ∈ V → (((2nd ↾
𝐻):dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷))) → ∃𝑓(𝑓:dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷))))) |
173 | 15, 166, 172 | sylc 65 |
. 2
⊢ (𝐹 ∈ (Fil‘𝑋) → ∃𝑓(𝑓:dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))) |
174 | | dmeq 5736 |
. . . . . 6
⊢ (𝑑 = 𝐷 → dom 𝑑 = dom 𝐷) |
175 | 174 | feq2d 6473 |
. . . . 5
⊢ (𝑑 = 𝐷 → (𝑓:dom 𝑑⟶𝑋 ↔ 𝑓:dom 𝐷⟶𝑋)) |
176 | | fveq2 6645 |
. . . . . . . 8
⊢ (𝑑 = 𝐷 → (tail‘𝑑) = (tail‘𝐷)) |
177 | 176 | rneqd 5772 |
. . . . . . 7
⊢ (𝑑 = 𝐷 → ran (tail‘𝑑) = ran (tail‘𝐷)) |
178 | 177 | fveq2d 6649 |
. . . . . 6
⊢ (𝑑 = 𝐷 → ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑)) = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷))) |
179 | 178 | eqeq2d 2809 |
. . . . 5
⊢ (𝑑 = 𝐷 → (𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑)) ↔ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))) |
180 | 175, 179 | anbi12d 633 |
. . . 4
⊢ (𝑑 = 𝐷 → ((𝑓:dom 𝑑⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))) ↔ (𝑓:dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷))))) |
181 | 180 | exbidv 1922 |
. . 3
⊢ (𝑑 = 𝐷 → (∃𝑓(𝑓:dom 𝑑⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))) ↔ ∃𝑓(𝑓:dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷))))) |
182 | 181 | rspcev 3571 |
. 2
⊢ ((𝐷 ∈ DirRel ∧
∃𝑓(𝑓:dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))) → ∃𝑑 ∈ DirRel ∃𝑓(𝑓:dom 𝑑⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑)))) |
183 | 5, 173, 182 | syl2anc 587 |
1
⊢ (𝐹 ∈ (Fil‘𝑋) → ∃𝑑 ∈ DirRel ∃𝑓(𝑓:dom 𝑑⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑)))) |