Step | Hyp | Ref
| Expression |
1 | | filnet.h |
. . . . 5
⊢ 𝐻 = ∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛) |
2 | | filnet.d |
. . . . 5
⊢ 𝐷 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) ∧ (1st ‘𝑦) ⊆ (1st
‘𝑥))} |
3 | 1, 2 | filnetlem3 32963 |
. . . 4
⊢ (𝐻 = ∪
∪ 𝐷 ∧ (𝐹 ∈ (Fil‘𝑋) → (𝐻 ⊆ (𝐹 × 𝑋) ∧ 𝐷 ∈ DirRel))) |
4 | 3 | simpri 481 |
. . 3
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐻 ⊆ (𝐹 × 𝑋) ∧ 𝐷 ∈ DirRel)) |
5 | 4 | simprd 491 |
. 2
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐷 ∈ DirRel) |
6 | | f2ndres 7470 |
. . . . 5
⊢
(2nd ↾ (𝐹 × 𝑋)):(𝐹 × 𝑋)⟶𝑋 |
7 | 4 | simpld 490 |
. . . . 5
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐻 ⊆ (𝐹 × 𝑋)) |
8 | | fssres2 6322 |
. . . . 5
⊢
(((2nd ↾ (𝐹 × 𝑋)):(𝐹 × 𝑋)⟶𝑋 ∧ 𝐻 ⊆ (𝐹 × 𝑋)) → (2nd ↾ 𝐻):𝐻⟶𝑋) |
9 | 6, 7, 8 | sylancr 581 |
. . . 4
⊢ (𝐹 ∈ (Fil‘𝑋) → (2nd ↾
𝐻):𝐻⟶𝑋) |
10 | | filtop 22067 |
. . . . . 6
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐹) |
11 | | xpexg 7237 |
. . . . . 6
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑋 ∈ 𝐹) → (𝐹 × 𝑋) ∈ V) |
12 | 10, 11 | mpdan 677 |
. . . . 5
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 × 𝑋) ∈ V) |
13 | 12, 7 | ssexd 5042 |
. . . 4
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐻 ∈ V) |
14 | | fex 6761 |
. . . 4
⊢
(((2nd ↾ 𝐻):𝐻⟶𝑋 ∧ 𝐻 ∈ V) → (2nd ↾
𝐻) ∈
V) |
15 | 9, 13, 14 | syl2anc 579 |
. . 3
⊢ (𝐹 ∈ (Fil‘𝑋) → (2nd ↾
𝐻) ∈
V) |
16 | | dirdm 17620 |
. . . . . . . 8
⊢ (𝐷 ∈ DirRel → dom 𝐷 = ∪
∪ 𝐷) |
17 | 5, 16 | syl 17 |
. . . . . . 7
⊢ (𝐹 ∈ (Fil‘𝑋) → dom 𝐷 = ∪ ∪ 𝐷) |
18 | 3 | simpli 478 |
. . . . . . 7
⊢ 𝐻 = ∪
∪ 𝐷 |
19 | 17, 18 | syl6reqr 2833 |
. . . . . 6
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐻 = dom 𝐷) |
20 | 19 | feq2d 6277 |
. . . . 5
⊢ (𝐹 ∈ (Fil‘𝑋) → ((2nd
↾ 𝐻):𝐻⟶𝑋 ↔ (2nd ↾ 𝐻):dom 𝐷⟶𝑋)) |
21 | 9, 20 | mpbid 224 |
. . . 4
⊢ (𝐹 ∈ (Fil‘𝑋) → (2nd ↾
𝐻):dom 𝐷⟶𝑋) |
22 | | eqid 2778 |
. . . . . . . . . . . . . 14
⊢ dom 𝐷 = dom 𝐷 |
23 | 22 | tailf 32958 |
. . . . . . . . . . . . 13
⊢ (𝐷 ∈ DirRel →
(tail‘𝐷):dom 𝐷⟶𝒫 dom 𝐷) |
24 | 5, 23 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (Fil‘𝑋) → (tail‘𝐷):dom 𝐷⟶𝒫 dom 𝐷) |
25 | 19 | feq2d 6277 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (Fil‘𝑋) → ((tail‘𝐷):𝐻⟶𝒫 dom 𝐷 ↔ (tail‘𝐷):dom 𝐷⟶𝒫 dom 𝐷)) |
26 | 24, 25 | mpbird 249 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (Fil‘𝑋) → (tail‘𝐷):𝐻⟶𝒫 dom 𝐷) |
27 | 26 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) → (tail‘𝐷):𝐻⟶𝒫 dom 𝐷) |
28 | | ffn 6291 |
. . . . . . . . . 10
⊢
((tail‘𝐷):𝐻⟶𝒫 dom 𝐷 → (tail‘𝐷) Fn 𝐻) |
29 | | imaeq2 5716 |
. . . . . . . . . . . 12
⊢ (𝑑 = ((tail‘𝐷)‘𝑓) → ((2nd ↾ 𝐻) “ 𝑑) = ((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓))) |
30 | 29 | sseq1d 3851 |
. . . . . . . . . . 11
⊢ (𝑑 = ((tail‘𝐷)‘𝑓) → (((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡 ↔ ((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡)) |
31 | 30 | rexrn 6625 |
. . . . . . . . . 10
⊢
((tail‘𝐷) Fn
𝐻 → (∃𝑑 ∈ ran (tail‘𝐷)((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡 ↔ ∃𝑓 ∈ 𝐻 ((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡)) |
32 | 27, 28, 31 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) → (∃𝑑 ∈ ran (tail‘𝐷)((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡 ↔ ∃𝑓 ∈ 𝐻 ((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡)) |
33 | | fo2nd 7466 |
. . . . . . . . . . . . . . 15
⊢
2nd :V–onto→V |
34 | | fofn 6368 |
. . . . . . . . . . . . . . 15
⊢
(2nd :V–onto→V → 2nd Fn V) |
35 | 33, 34 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
2nd Fn V |
36 | | ssv 3844 |
. . . . . . . . . . . . . 14
⊢ 𝐻 ⊆ V |
37 | | fnssres 6250 |
. . . . . . . . . . . . . 14
⊢
((2nd Fn V ∧ 𝐻 ⊆ V) → (2nd ↾
𝐻) Fn 𝐻) |
38 | 35, 36, 37 | mp2an 682 |
. . . . . . . . . . . . 13
⊢
(2nd ↾ 𝐻) Fn 𝐻 |
39 | | fnfun 6233 |
. . . . . . . . . . . . 13
⊢
((2nd ↾ 𝐻) Fn 𝐻 → Fun (2nd ↾ 𝐻)) |
40 | 38, 39 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ Fun
(2nd ↾ 𝐻) |
41 | 27 | ffvelrnda 6623 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((tail‘𝐷)‘𝑓) ∈ 𝒫 dom 𝐷) |
42 | 41 | elpwid 4391 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((tail‘𝐷)‘𝑓) ⊆ dom 𝐷) |
43 | 19 | ad2antrr 716 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → 𝐻 = dom 𝐷) |
44 | 42, 43 | sseqtr4d 3861 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((tail‘𝐷)‘𝑓) ⊆ 𝐻) |
45 | | fndm 6235 |
. . . . . . . . . . . . . 14
⊢
((2nd ↾ 𝐻) Fn 𝐻 → dom (2nd ↾ 𝐻) = 𝐻) |
46 | 38, 45 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ dom
(2nd ↾ 𝐻)
= 𝐻 |
47 | 44, 46 | syl6sseqr 3871 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((tail‘𝐷)‘𝑓) ⊆ dom (2nd ↾ 𝐻)) |
48 | | funimass4 6507 |
. . . . . . . . . . . 12
⊢ ((Fun
(2nd ↾ 𝐻)
∧ ((tail‘𝐷)‘𝑓) ⊆ dom (2nd ↾ 𝐻)) → (((2nd
↾ 𝐻) “
((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∀𝑑 ∈ ((tail‘𝐷)‘𝑓)((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡)) |
49 | 40, 47, 48 | sylancr 581 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → (((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∀𝑑 ∈ ((tail‘𝐷)‘𝑓)((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡)) |
50 | 5 | ad2antrr 716 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → 𝐷 ∈ DirRel) |
51 | | simpr 479 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → 𝑓 ∈ 𝐻) |
52 | 51, 43 | eleqtrd 2861 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → 𝑓 ∈ dom 𝐷) |
53 | | vex 3401 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑑 ∈ V |
54 | 53 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → 𝑑 ∈ V) |
55 | 22 | eltail 32957 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ DirRel ∧ 𝑓 ∈ dom 𝐷 ∧ 𝑑 ∈ V) → (𝑑 ∈ ((tail‘𝐷)‘𝑓) ↔ 𝑓𝐷𝑑)) |
56 | 50, 52, 54, 55 | syl3anc 1439 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → (𝑑 ∈ ((tail‘𝐷)‘𝑓) ↔ 𝑓𝐷𝑑)) |
57 | 51 | biantrurd 528 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → (𝑑 ∈ 𝐻 ↔ (𝑓 ∈ 𝐻 ∧ 𝑑 ∈ 𝐻))) |
58 | 57 | anbi1d 623 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st
‘𝑓)) ↔ ((𝑓 ∈ 𝐻 ∧ 𝑑 ∈ 𝐻) ∧ (1st ‘𝑑) ⊆ (1st
‘𝑓)))) |
59 | | vex 3401 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑓 ∈ V |
60 | 1, 2, 59, 53 | filnetlem1 32961 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓𝐷𝑑 ↔ ((𝑓 ∈ 𝐻 ∧ 𝑑 ∈ 𝐻) ∧ (1st ‘𝑑) ⊆ (1st
‘𝑓))) |
61 | 58, 60 | syl6bbr 281 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st
‘𝑓)) ↔ 𝑓𝐷𝑑)) |
62 | 56, 61 | bitr4d 274 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → (𝑑 ∈ ((tail‘𝐷)‘𝑓) ↔ (𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st
‘𝑓)))) |
63 | 62 | imbi1d 333 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((𝑑 ∈ ((tail‘𝐷)‘𝑓) → ((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡) ↔ ((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st
‘𝑓)) →
((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡))) |
64 | | fvres 6465 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑑 ∈ 𝐻 → ((2nd ↾ 𝐻)‘𝑑) = (2nd ‘𝑑)) |
65 | 64 | eleq1d 2844 |
. . . . . . . . . . . . . . . 16
⊢ (𝑑 ∈ 𝐻 → (((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡 ↔ (2nd ‘𝑑) ∈ 𝑡)) |
66 | 65 | adantr 474 |
. . . . . . . . . . . . . . 15
⊢ ((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st
‘𝑓)) →
(((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡 ↔ (2nd ‘𝑑) ∈ 𝑡)) |
67 | 66 | pm5.74i 263 |
. . . . . . . . . . . . . 14
⊢ (((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st
‘𝑓)) →
((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡) ↔ ((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st
‘𝑓)) →
(2nd ‘𝑑)
∈ 𝑡)) |
68 | | impexp 443 |
. . . . . . . . . . . . . 14
⊢ (((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st
‘𝑓)) →
(2nd ‘𝑑)
∈ 𝑡) ↔ (𝑑 ∈ 𝐻 → ((1st ‘𝑑) ⊆ (1st
‘𝑓) →
(2nd ‘𝑑)
∈ 𝑡))) |
69 | 67, 68 | bitri 267 |
. . . . . . . . . . . . 13
⊢ (((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st
‘𝑓)) →
((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡) ↔ (𝑑 ∈ 𝐻 → ((1st ‘𝑑) ⊆ (1st
‘𝑓) →
(2nd ‘𝑑)
∈ 𝑡))) |
70 | 63, 69 | syl6bb 279 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((𝑑 ∈ ((tail‘𝐷)‘𝑓) → ((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡) ↔ (𝑑 ∈ 𝐻 → ((1st ‘𝑑) ⊆ (1st
‘𝑓) →
(2nd ‘𝑑)
∈ 𝑡)))) |
71 | 70 | ralbidv2 3166 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → (∀𝑑 ∈ ((tail‘𝐷)‘𝑓)((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡 ↔ ∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd
‘𝑑) ∈ 𝑡))) |
72 | 49, 71 | bitrd 271 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → (((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd
‘𝑑) ∈ 𝑡))) |
73 | 72 | rexbidva 3234 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) → (∃𝑓 ∈ 𝐻 ((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∃𝑓 ∈ 𝐻 ∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd
‘𝑑) ∈ 𝑡))) |
74 | | vex 3401 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑘 ∈ V |
75 | | vex 3401 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑣 ∈ V |
76 | 74, 75 | op1std 7455 |
. . . . . . . . . . . . . . . 16
⊢ (𝑑 = 〈𝑘, 𝑣〉 → (1st ‘𝑑) = 𝑘) |
77 | 76 | sseq1d 3851 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 = 〈𝑘, 𝑣〉 → ((1st ‘𝑑) ⊆ (1st
‘𝑓) ↔ 𝑘 ⊆ (1st
‘𝑓))) |
78 | 74, 75 | op2ndd 7456 |
. . . . . . . . . . . . . . . 16
⊢ (𝑑 = 〈𝑘, 𝑣〉 → (2nd ‘𝑑) = 𝑣) |
79 | 78 | eleq1d 2844 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 = 〈𝑘, 𝑣〉 → ((2nd ‘𝑑) ∈ 𝑡 ↔ 𝑣 ∈ 𝑡)) |
80 | 77, 79 | imbi12d 336 |
. . . . . . . . . . . . . 14
⊢ (𝑑 = 〈𝑘, 𝑣〉 → (((1st ‘𝑑) ⊆ (1st
‘𝑓) →
(2nd ‘𝑑)
∈ 𝑡) ↔ (𝑘 ⊆ (1st
‘𝑓) → 𝑣 ∈ 𝑡))) |
81 | 80 | raliunxp 5507 |
. . . . . . . . . . . . 13
⊢
(∀𝑑 ∈
∪ 𝑘 ∈ 𝐹 ({𝑘} × 𝑘)((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd
‘𝑑) ∈ 𝑡) ↔ ∀𝑘 ∈ 𝐹 ∀𝑣 ∈ 𝑘 (𝑘 ⊆ (1st ‘𝑓) → 𝑣 ∈ 𝑡)) |
82 | | sneq 4408 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑘 → {𝑛} = {𝑘}) |
83 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑘 → 𝑛 = 𝑘) |
84 | 82, 83 | xpeq12d 5386 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑘 → ({𝑛} × 𝑛) = ({𝑘} × 𝑘)) |
85 | 84 | cbviunv 4792 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛) = ∪ 𝑘 ∈ 𝐹 ({𝑘} × 𝑘) |
86 | 1, 85 | eqtri 2802 |
. . . . . . . . . . . . . 14
⊢ 𝐻 = ∪ 𝑘 ∈ 𝐹 ({𝑘} × 𝑘) |
87 | 86 | raleqi 3338 |
. . . . . . . . . . . . 13
⊢
(∀𝑑 ∈
𝐻 ((1st
‘𝑑) ⊆
(1st ‘𝑓)
→ (2nd ‘𝑑) ∈ 𝑡) ↔ ∀𝑑 ∈ ∪
𝑘 ∈ 𝐹 ({𝑘} × 𝑘)((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd
‘𝑑) ∈ 𝑡)) |
88 | | dfss3 3810 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ⊆ 𝑡 ↔ ∀𝑣 ∈ 𝑘 𝑣 ∈ 𝑡) |
89 | 88 | imbi2i 328 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ⊆ (1st
‘𝑓) → 𝑘 ⊆ 𝑡) ↔ (𝑘 ⊆ (1st ‘𝑓) → ∀𝑣 ∈ 𝑘 𝑣 ∈ 𝑡)) |
90 | | r19.21v 3142 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑣 ∈
𝑘 (𝑘 ⊆ (1st ‘𝑓) → 𝑣 ∈ 𝑡) ↔ (𝑘 ⊆ (1st ‘𝑓) → ∀𝑣 ∈ 𝑘 𝑣 ∈ 𝑡)) |
91 | 89, 90 | bitr4i 270 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ⊆ (1st
‘𝑓) → 𝑘 ⊆ 𝑡) ↔ ∀𝑣 ∈ 𝑘 (𝑘 ⊆ (1st ‘𝑓) → 𝑣 ∈ 𝑡)) |
92 | 91 | ralbii 3162 |
. . . . . . . . . . . . 13
⊢
(∀𝑘 ∈
𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ ∀𝑘 ∈ 𝐹 ∀𝑣 ∈ 𝑘 (𝑘 ⊆ (1st ‘𝑓) → 𝑣 ∈ 𝑡)) |
93 | 81, 87, 92 | 3bitr4i 295 |
. . . . . . . . . . . 12
⊢
(∀𝑑 ∈
𝐻 ((1st
‘𝑑) ⊆
(1st ‘𝑓)
→ (2nd ‘𝑑) ∈ 𝑡) ↔ ∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡)) |
94 | 93 | rexbii 3224 |
. . . . . . . . . . 11
⊢
(∃𝑓 ∈
𝐻 ∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd
‘𝑑) ∈ 𝑡) ↔ ∃𝑓 ∈ 𝐻 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡)) |
95 | 1 | rexeqi 3339 |
. . . . . . . . . . 11
⊢
(∃𝑓 ∈
𝐻 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ ∃𝑓 ∈ ∪
𝑛 ∈ 𝐹 ({𝑛} × 𝑛)∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡)) |
96 | | vex 3401 |
. . . . . . . . . . . . . . . 16
⊢ 𝑛 ∈ V |
97 | | vex 3401 |
. . . . . . . . . . . . . . . 16
⊢ 𝑚 ∈ V |
98 | 96, 97 | op1std 7455 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = 〈𝑛, 𝑚〉 → (1st ‘𝑓) = 𝑛) |
99 | 98 | sseq2d 3852 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = 〈𝑛, 𝑚〉 → (𝑘 ⊆ (1st ‘𝑓) ↔ 𝑘 ⊆ 𝑛)) |
100 | 99 | imbi1d 333 |
. . . . . . . . . . . . 13
⊢ (𝑓 = 〈𝑛, 𝑚〉 → ((𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡))) |
101 | 100 | ralbidv 3168 |
. . . . . . . . . . . 12
⊢ (𝑓 = 〈𝑛, 𝑚〉 → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡))) |
102 | 101 | rexiunxp 5508 |
. . . . . . . . . . 11
⊢
(∃𝑓 ∈
∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛)∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ ∃𝑛 ∈ 𝐹 ∃𝑚 ∈ 𝑛 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡)) |
103 | 94, 95, 102 | 3bitri 289 |
. . . . . . . . . 10
⊢
(∃𝑓 ∈
𝐻 ∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd
‘𝑑) ∈ 𝑡) ↔ ∃𝑛 ∈ 𝐹 ∃𝑚 ∈ 𝑛 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡)) |
104 | | fileln0 22062 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛 ∈ 𝐹) → 𝑛 ≠ ∅) |
105 | 104 | adantlr 705 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑛 ∈ 𝐹) → 𝑛 ≠ ∅) |
106 | | r19.9rzv 4288 |
. . . . . . . . . . . . 13
⊢ (𝑛 ≠ ∅ →
(∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) ↔ ∃𝑚 ∈ 𝑛 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡))) |
107 | 105, 106 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑛 ∈ 𝐹) → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) ↔ ∃𝑚 ∈ 𝑛 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡))) |
108 | | ssid 3842 |
. . . . . . . . . . . . . . 15
⊢ 𝑛 ⊆ 𝑛 |
109 | | sseq1 3845 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑛 → (𝑘 ⊆ 𝑛 ↔ 𝑛 ⊆ 𝑛)) |
110 | | sseq1 3845 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑛 → (𝑘 ⊆ 𝑡 ↔ 𝑛 ⊆ 𝑡)) |
111 | 109, 110 | imbi12d 336 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑛 → ((𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) ↔ (𝑛 ⊆ 𝑛 → 𝑛 ⊆ 𝑡))) |
112 | 111 | rspcv 3507 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ 𝐹 → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) → (𝑛 ⊆ 𝑛 → 𝑛 ⊆ 𝑡))) |
113 | 108, 112 | mpii 46 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ 𝐹 → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) → 𝑛 ⊆ 𝑡)) |
114 | 113 | adantl 475 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑛 ∈ 𝐹) → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) → 𝑛 ⊆ 𝑡)) |
115 | | sstr2 3828 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ⊆ 𝑛 → (𝑛 ⊆ 𝑡 → 𝑘 ⊆ 𝑡)) |
116 | 115 | com12 32 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ⊆ 𝑡 → (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡)) |
117 | 116 | ralrimivw 3149 |
. . . . . . . . . . . . 13
⊢ (𝑛 ⊆ 𝑡 → ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡)) |
118 | 114, 117 | impbid1 217 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑛 ∈ 𝐹) → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) ↔ 𝑛 ⊆ 𝑡)) |
119 | 107, 118 | bitr3d 273 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑛 ∈ 𝐹) → (∃𝑚 ∈ 𝑛 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) ↔ 𝑛 ⊆ 𝑡)) |
120 | 119 | rexbidva 3234 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) → (∃𝑛 ∈ 𝐹 ∃𝑚 ∈ 𝑛 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) ↔ ∃𝑛 ∈ 𝐹 𝑛 ⊆ 𝑡)) |
121 | 103, 120 | syl5bb 275 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) → (∃𝑓 ∈ 𝐻 ∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd
‘𝑑) ∈ 𝑡) ↔ ∃𝑛 ∈ 𝐹 𝑛 ⊆ 𝑡)) |
122 | 32, 73, 121 | 3bitrd 297 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) → (∃𝑑 ∈ ran (tail‘𝐷)((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡 ↔ ∃𝑛 ∈ 𝐹 𝑛 ⊆ 𝑡)) |
123 | 122 | pm5.32da 574 |
. . . . . . 7
⊢ (𝐹 ∈ (Fil‘𝑋) → ((𝑡 ⊆ 𝑋 ∧ ∃𝑑 ∈ ran (tail‘𝐷)((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡) ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑛 ∈ 𝐹 𝑛 ⊆ 𝑡))) |
124 | | filn0 22074 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ≠ ∅) |
125 | 96 | snnz 4542 |
. . . . . . . . . . . . . . . 16
⊢ {𝑛} ≠ ∅ |
126 | 104, 125 | jctil 515 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛 ∈ 𝐹) → ({𝑛} ≠ ∅ ∧ 𝑛 ≠ ∅)) |
127 | | neanior 3062 |
. . . . . . . . . . . . . . 15
⊢ (({𝑛} ≠ ∅ ∧ 𝑛 ≠ ∅) ↔ ¬
({𝑛} = ∅ ∨ 𝑛 = ∅)) |
128 | 126, 127 | sylib 210 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛 ∈ 𝐹) → ¬ ({𝑛} = ∅ ∨ 𝑛 = ∅)) |
129 | | ss0b 4199 |
. . . . . . . . . . . . . . 15
⊢ (({𝑛} × 𝑛) ⊆ ∅ ↔ ({𝑛} × 𝑛) = ∅) |
130 | | xpeq0 5808 |
. . . . . . . . . . . . . . 15
⊢ (({𝑛} × 𝑛) = ∅ ↔ ({𝑛} = ∅ ∨ 𝑛 = ∅)) |
131 | 129, 130 | bitri 267 |
. . . . . . . . . . . . . 14
⊢ (({𝑛} × 𝑛) ⊆ ∅ ↔ ({𝑛} = ∅ ∨ 𝑛 = ∅)) |
132 | 128, 131 | sylnibr 321 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛 ∈ 𝐹) → ¬ ({𝑛} × 𝑛) ⊆ ∅) |
133 | 132 | ralrimiva 3148 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (Fil‘𝑋) → ∀𝑛 ∈ 𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅) |
134 | | r19.2z 4283 |
. . . . . . . . . . . 12
⊢ ((𝐹 ≠ ∅ ∧
∀𝑛 ∈ 𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅) → ∃𝑛 ∈ 𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅) |
135 | 124, 133,
134 | syl2anc 579 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (Fil‘𝑋) → ∃𝑛 ∈ 𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅) |
136 | | rexnal 3176 |
. . . . . . . . . . 11
⊢
(∃𝑛 ∈
𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅ ↔ ¬ ∀𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅) |
137 | 135, 136 | sylib 210 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (Fil‘𝑋) → ¬ ∀𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅) |
138 | 1 | sseq1i 3848 |
. . . . . . . . . . . 12
⊢ (𝐻 ⊆ ∅ ↔ ∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅) |
139 | | ss0b 4199 |
. . . . . . . . . . . 12
⊢ (𝐻 ⊆ ∅ ↔ 𝐻 = ∅) |
140 | | iunss 4794 |
. . . . . . . . . . . 12
⊢ (∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅ ↔ ∀𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅) |
141 | 138, 139,
140 | 3bitr3i 293 |
. . . . . . . . . . 11
⊢ (𝐻 = ∅ ↔ ∀𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅) |
142 | 141 | necon3abii 3015 |
. . . . . . . . . 10
⊢ (𝐻 ≠ ∅ ↔ ¬
∀𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅) |
143 | 137, 142 | sylibr 226 |
. . . . . . . . 9
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐻 ≠ ∅) |
144 | | dmresi 5713 |
. . . . . . . . . . . 12
⊢ dom ( I
↾ 𝐻) = 𝐻 |
145 | 1, 2 | filnetlem2 32962 |
. . . . . . . . . . . . . 14
⊢ (( I
↾ 𝐻) ⊆ 𝐷 ∧ 𝐷 ⊆ (𝐻 × 𝐻)) |
146 | 145 | simpli 478 |
. . . . . . . . . . . . 13
⊢ ( I
↾ 𝐻) ⊆ 𝐷 |
147 | | dmss 5568 |
. . . . . . . . . . . . 13
⊢ (( I
↾ 𝐻) ⊆ 𝐷 → dom ( I ↾ 𝐻) ⊆ dom 𝐷) |
148 | 146, 147 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ dom ( I
↾ 𝐻) ⊆ dom
𝐷 |
149 | 144, 148 | eqsstr3i 3855 |
. . . . . . . . . . 11
⊢ 𝐻 ⊆ dom 𝐷 |
150 | 145 | simpri 481 |
. . . . . . . . . . . . 13
⊢ 𝐷 ⊆ (𝐻 × 𝐻) |
151 | | dmss 5568 |
. . . . . . . . . . . . 13
⊢ (𝐷 ⊆ (𝐻 × 𝐻) → dom 𝐷 ⊆ dom (𝐻 × 𝐻)) |
152 | 150, 151 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ dom 𝐷 ⊆ dom (𝐻 × 𝐻) |
153 | | dmxpid 5590 |
. . . . . . . . . . . 12
⊢ dom
(𝐻 × 𝐻) = 𝐻 |
154 | 152, 153 | sseqtri 3856 |
. . . . . . . . . . 11
⊢ dom 𝐷 ⊆ 𝐻 |
155 | 149, 154 | eqssi 3837 |
. . . . . . . . . 10
⊢ 𝐻 = dom 𝐷 |
156 | 155 | tailfb 32960 |
. . . . . . . . 9
⊢ ((𝐷 ∈ DirRel ∧ 𝐻 ≠ ∅) → ran
(tail‘𝐷) ∈
(fBas‘𝐻)) |
157 | 5, 143, 156 | syl2anc 579 |
. . . . . . . 8
⊢ (𝐹 ∈ (Fil‘𝑋) → ran (tail‘𝐷) ∈ (fBas‘𝐻)) |
158 | | elfm 22159 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝐹 ∧ ran (tail‘𝐷) ∈ (fBas‘𝐻) ∧ (2nd ↾ 𝐻):𝐻⟶𝑋) → (𝑡 ∈ ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)) ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑑 ∈ ran (tail‘𝐷)((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡))) |
159 | 10, 157, 9, 158 | syl3anc 1439 |
. . . . . . 7
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑡 ∈ ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)) ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑑 ∈ ran (tail‘𝐷)((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡))) |
160 | | filfbas 22060 |
. . . . . . . 8
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋)) |
161 | | elfg 22083 |
. . . . . . . 8
⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑡 ∈ (𝑋filGen𝐹) ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑛 ∈ 𝐹 𝑛 ⊆ 𝑡))) |
162 | 160, 161 | syl 17 |
. . . . . . 7
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑡 ∈ (𝑋filGen𝐹) ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑛 ∈ 𝐹 𝑛 ⊆ 𝑡))) |
163 | 123, 159,
162 | 3bitr4d 303 |
. . . . . 6
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑡 ∈ ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)) ↔ 𝑡 ∈ (𝑋filGen𝐹))) |
164 | 163 | eqrdv 2776 |
. . . . 5
⊢ (𝐹 ∈ (Fil‘𝑋) → ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)) = (𝑋filGen𝐹)) |
165 | | fgfil 22087 |
. . . . 5
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑋filGen𝐹) = 𝐹) |
166 | 164, 165 | eqtr2d 2815 |
. . . 4
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 = ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷))) |
167 | 21, 166 | jca 507 |
. . 3
⊢ (𝐹 ∈ (Fil‘𝑋) → ((2nd
↾ 𝐻):dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)))) |
168 | | feq1 6272 |
. . . . 5
⊢ (𝑓 = (2nd ↾ 𝐻) → (𝑓:dom 𝐷⟶𝑋 ↔ (2nd ↾ 𝐻):dom 𝐷⟶𝑋)) |
169 | | oveq2 6930 |
. . . . . . 7
⊢ (𝑓 = (2nd ↾ 𝐻) → (𝑋 FilMap 𝑓) = (𝑋 FilMap (2nd ↾ 𝐻))) |
170 | 169 | fveq1d 6448 |
. . . . . 6
⊢ (𝑓 = (2nd ↾ 𝐻) → ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)) = ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷))) |
171 | 170 | eqeq2d 2788 |
. . . . 5
⊢ (𝑓 = (2nd ↾ 𝐻) → (𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)) ↔ 𝐹 = ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)))) |
172 | 168, 171 | anbi12d 624 |
. . . 4
⊢ (𝑓 = (2nd ↾ 𝐻) → ((𝑓:dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷))) ↔ ((2nd ↾ 𝐻):dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷))))) |
173 | 172 | spcegv 3496 |
. . 3
⊢
((2nd ↾ 𝐻) ∈ V → (((2nd ↾
𝐻):dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷))) → ∃𝑓(𝑓:dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷))))) |
174 | 15, 167, 173 | sylc 65 |
. 2
⊢ (𝐹 ∈ (Fil‘𝑋) → ∃𝑓(𝑓:dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))) |
175 | | dmeq 5569 |
. . . . . 6
⊢ (𝑑 = 𝐷 → dom 𝑑 = dom 𝐷) |
176 | 175 | feq2d 6277 |
. . . . 5
⊢ (𝑑 = 𝐷 → (𝑓:dom 𝑑⟶𝑋 ↔ 𝑓:dom 𝐷⟶𝑋)) |
177 | | fveq2 6446 |
. . . . . . . 8
⊢ (𝑑 = 𝐷 → (tail‘𝑑) = (tail‘𝐷)) |
178 | 177 | rneqd 5598 |
. . . . . . 7
⊢ (𝑑 = 𝐷 → ran (tail‘𝑑) = ran (tail‘𝐷)) |
179 | 178 | fveq2d 6450 |
. . . . . 6
⊢ (𝑑 = 𝐷 → ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑)) = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷))) |
180 | 179 | eqeq2d 2788 |
. . . . 5
⊢ (𝑑 = 𝐷 → (𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑)) ↔ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))) |
181 | 176, 180 | anbi12d 624 |
. . . 4
⊢ (𝑑 = 𝐷 → ((𝑓:dom 𝑑⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))) ↔ (𝑓:dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷))))) |
182 | 181 | exbidv 1964 |
. . 3
⊢ (𝑑 = 𝐷 → (∃𝑓(𝑓:dom 𝑑⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))) ↔ ∃𝑓(𝑓:dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷))))) |
183 | 182 | rspcev 3511 |
. 2
⊢ ((𝐷 ∈ DirRel ∧
∃𝑓(𝑓:dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))) → ∃𝑑 ∈ DirRel ∃𝑓(𝑓:dom 𝑑⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑)))) |
184 | 5, 174, 183 | syl2anc 579 |
1
⊢ (𝐹 ∈ (Fil‘𝑋) → ∃𝑑 ∈ DirRel ∃𝑓(𝑓:dom 𝑑⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑)))) |