Step | Hyp | Ref
| Expression |
1 | | filnet.h |
. . . . 5
⊢ 𝐻 = ∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛) |
2 | | filnet.d |
. . . . 5
⊢ 𝐷 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) ∧ (1st ‘𝑦) ⊆ (1st
‘𝑥))} |
3 | 1, 2 | filnetlem3 31545 |
. . . 4
⊢ (𝐻 = ∪
∪ 𝐷 ∧ (𝐹 ∈ (Fil‘𝑋) → (𝐻 ⊆ (𝐹 × 𝑋) ∧ 𝐷 ∈ DirRel))) |
4 | 3 | simpri 477 |
. . 3
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐻 ⊆ (𝐹 × 𝑋) ∧ 𝐷 ∈ DirRel)) |
5 | 4 | simprd 478 |
. 2
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐷 ∈ DirRel) |
6 | | f2ndres 7082 |
. . . . 5
⊢
(2nd ↾ (𝐹 × 𝑋)):(𝐹 × 𝑋)⟶𝑋 |
7 | 4 | simpld 474 |
. . . . 5
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐻 ⊆ (𝐹 × 𝑋)) |
8 | | fssres2 5985 |
. . . . 5
⊢
(((2nd ↾ (𝐹 × 𝑋)):(𝐹 × 𝑋)⟶𝑋 ∧ 𝐻 ⊆ (𝐹 × 𝑋)) → (2nd ↾ 𝐻):𝐻⟶𝑋) |
9 | 6, 7, 8 | sylancr 694 |
. . . 4
⊢ (𝐹 ∈ (Fil‘𝑋) → (2nd ↾
𝐻):𝐻⟶𝑋) |
10 | | filtop 21469 |
. . . . . 6
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐹) |
11 | | xpexg 6858 |
. . . . . 6
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑋 ∈ 𝐹) → (𝐹 × 𝑋) ∈ V) |
12 | 10, 11 | mpdan 699 |
. . . . 5
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 × 𝑋) ∈ V) |
13 | 12, 7 | ssexd 4733 |
. . . 4
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐻 ∈ V) |
14 | | fex 6394 |
. . . 4
⊢
(((2nd ↾ 𝐻):𝐻⟶𝑋 ∧ 𝐻 ∈ V) → (2nd ↾
𝐻) ∈
V) |
15 | 9, 13, 14 | syl2anc 691 |
. . 3
⊢ (𝐹 ∈ (Fil‘𝑋) → (2nd ↾
𝐻) ∈
V) |
16 | | dirdm 17057 |
. . . . . . . 8
⊢ (𝐷 ∈ DirRel → dom 𝐷 = ∪
∪ 𝐷) |
17 | 5, 16 | syl 17 |
. . . . . . 7
⊢ (𝐹 ∈ (Fil‘𝑋) → dom 𝐷 = ∪ ∪ 𝐷) |
18 | 3 | simpli 473 |
. . . . . . 7
⊢ 𝐻 = ∪
∪ 𝐷 |
19 | 17, 18 | syl6reqr 2663 |
. . . . . 6
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐻 = dom 𝐷) |
20 | 19 | feq2d 5944 |
. . . . 5
⊢ (𝐹 ∈ (Fil‘𝑋) → ((2nd
↾ 𝐻):𝐻⟶𝑋 ↔ (2nd ↾ 𝐻):dom 𝐷⟶𝑋)) |
21 | 9, 20 | mpbid 221 |
. . . 4
⊢ (𝐹 ∈ (Fil‘𝑋) → (2nd ↾
𝐻):dom 𝐷⟶𝑋) |
22 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢ dom 𝐷 = dom 𝐷 |
23 | 22 | tailf 31540 |
. . . . . . . . . . . . 13
⊢ (𝐷 ∈ DirRel →
(tail‘𝐷):dom 𝐷⟶𝒫 dom 𝐷) |
24 | 5, 23 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (Fil‘𝑋) → (tail‘𝐷):dom 𝐷⟶𝒫 dom 𝐷) |
25 | 19 | feq2d 5944 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (Fil‘𝑋) → ((tail‘𝐷):𝐻⟶𝒫 dom 𝐷 ↔ (tail‘𝐷):dom 𝐷⟶𝒫 dom 𝐷)) |
26 | 24, 25 | mpbird 246 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (Fil‘𝑋) → (tail‘𝐷):𝐻⟶𝒫 dom 𝐷) |
27 | 26 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) → (tail‘𝐷):𝐻⟶𝒫 dom 𝐷) |
28 | | ffn 5958 |
. . . . . . . . . 10
⊢
((tail‘𝐷):𝐻⟶𝒫 dom 𝐷 → (tail‘𝐷) Fn 𝐻) |
29 | | imaeq2 5381 |
. . . . . . . . . . . 12
⊢ (𝑑 = ((tail‘𝐷)‘𝑓) → ((2nd ↾ 𝐻) “ 𝑑) = ((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓))) |
30 | 29 | sseq1d 3595 |
. . . . . . . . . . 11
⊢ (𝑑 = ((tail‘𝐷)‘𝑓) → (((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡 ↔ ((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡)) |
31 | 30 | rexrn 6269 |
. . . . . . . . . 10
⊢
((tail‘𝐷) Fn
𝐻 → (∃𝑑 ∈ ran (tail‘𝐷)((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡 ↔ ∃𝑓 ∈ 𝐻 ((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡)) |
32 | 27, 28, 31 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) → (∃𝑑 ∈ ran (tail‘𝐷)((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡 ↔ ∃𝑓 ∈ 𝐻 ((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡)) |
33 | | fo2nd 7080 |
. . . . . . . . . . . . . . 15
⊢
2nd :V–onto→V |
34 | | fofn 6030 |
. . . . . . . . . . . . . . 15
⊢
(2nd :V–onto→V → 2nd Fn V) |
35 | 33, 34 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
2nd Fn V |
36 | | ssv 3588 |
. . . . . . . . . . . . . 14
⊢ 𝐻 ⊆ V |
37 | | fnssres 5918 |
. . . . . . . . . . . . . 14
⊢
((2nd Fn V ∧ 𝐻 ⊆ V) → (2nd ↾
𝐻) Fn 𝐻) |
38 | 35, 36, 37 | mp2an 704 |
. . . . . . . . . . . . 13
⊢
(2nd ↾ 𝐻) Fn 𝐻 |
39 | | fnfun 5902 |
. . . . . . . . . . . . 13
⊢
((2nd ↾ 𝐻) Fn 𝐻 → Fun (2nd ↾ 𝐻)) |
40 | 38, 39 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ Fun
(2nd ↾ 𝐻) |
41 | 27 | ffvelrnda 6267 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((tail‘𝐷)‘𝑓) ∈ 𝒫 dom 𝐷) |
42 | 41 | elpwid 4118 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((tail‘𝐷)‘𝑓) ⊆ dom 𝐷) |
43 | 19 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → 𝐻 = dom 𝐷) |
44 | 42, 43 | sseqtr4d 3605 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((tail‘𝐷)‘𝑓) ⊆ 𝐻) |
45 | | fndm 5904 |
. . . . . . . . . . . . . 14
⊢
((2nd ↾ 𝐻) Fn 𝐻 → dom (2nd ↾ 𝐻) = 𝐻) |
46 | 38, 45 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ dom
(2nd ↾ 𝐻)
= 𝐻 |
47 | 44, 46 | syl6sseqr 3615 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((tail‘𝐷)‘𝑓) ⊆ dom (2nd ↾ 𝐻)) |
48 | | funimass4 6157 |
. . . . . . . . . . . 12
⊢ ((Fun
(2nd ↾ 𝐻)
∧ ((tail‘𝐷)‘𝑓) ⊆ dom (2nd ↾ 𝐻)) → (((2nd
↾ 𝐻) “
((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∀𝑑 ∈ ((tail‘𝐷)‘𝑓)((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡)) |
49 | 40, 47, 48 | sylancr 694 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → (((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∀𝑑 ∈ ((tail‘𝐷)‘𝑓)((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡)) |
50 | 5 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → 𝐷 ∈ DirRel) |
51 | | simpr 476 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → 𝑓 ∈ 𝐻) |
52 | 51, 43 | eleqtrd 2690 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → 𝑓 ∈ dom 𝐷) |
53 | | vex 3176 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑑 ∈ V |
54 | 53 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → 𝑑 ∈ V) |
55 | 22 | eltail 31539 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ DirRel ∧ 𝑓 ∈ dom 𝐷 ∧ 𝑑 ∈ V) → (𝑑 ∈ ((tail‘𝐷)‘𝑓) ↔ 𝑓𝐷𝑑)) |
56 | 50, 52, 54, 55 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → (𝑑 ∈ ((tail‘𝐷)‘𝑓) ↔ 𝑓𝐷𝑑)) |
57 | 51 | biantrurd 528 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → (𝑑 ∈ 𝐻 ↔ (𝑓 ∈ 𝐻 ∧ 𝑑 ∈ 𝐻))) |
58 | 57 | anbi1d 737 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st
‘𝑓)) ↔ ((𝑓 ∈ 𝐻 ∧ 𝑑 ∈ 𝐻) ∧ (1st ‘𝑑) ⊆ (1st
‘𝑓)))) |
59 | | vex 3176 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑓 ∈ V |
60 | 1, 2, 59, 53 | filnetlem1 31543 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓𝐷𝑑 ↔ ((𝑓 ∈ 𝐻 ∧ 𝑑 ∈ 𝐻) ∧ (1st ‘𝑑) ⊆ (1st
‘𝑓))) |
61 | 58, 60 | syl6bbr 277 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st
‘𝑓)) ↔ 𝑓𝐷𝑑)) |
62 | 56, 61 | bitr4d 270 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → (𝑑 ∈ ((tail‘𝐷)‘𝑓) ↔ (𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st
‘𝑓)))) |
63 | 62 | imbi1d 330 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((𝑑 ∈ ((tail‘𝐷)‘𝑓) → ((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡) ↔ ((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st
‘𝑓)) →
((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡))) |
64 | | fvres 6117 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑑 ∈ 𝐻 → ((2nd ↾ 𝐻)‘𝑑) = (2nd ‘𝑑)) |
65 | 64 | eleq1d 2672 |
. . . . . . . . . . . . . . . 16
⊢ (𝑑 ∈ 𝐻 → (((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡 ↔ (2nd ‘𝑑) ∈ 𝑡)) |
66 | 65 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st
‘𝑓)) →
(((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡 ↔ (2nd ‘𝑑) ∈ 𝑡)) |
67 | 66 | pm5.74i 259 |
. . . . . . . . . . . . . 14
⊢ (((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st
‘𝑓)) →
((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡) ↔ ((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st
‘𝑓)) →
(2nd ‘𝑑)
∈ 𝑡)) |
68 | | impexp 461 |
. . . . . . . . . . . . . 14
⊢ (((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st
‘𝑓)) →
(2nd ‘𝑑)
∈ 𝑡) ↔ (𝑑 ∈ 𝐻 → ((1st ‘𝑑) ⊆ (1st
‘𝑓) →
(2nd ‘𝑑)
∈ 𝑡))) |
69 | 67, 68 | bitri 263 |
. . . . . . . . . . . . 13
⊢ (((𝑑 ∈ 𝐻 ∧ (1st ‘𝑑) ⊆ (1st
‘𝑓)) →
((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡) ↔ (𝑑 ∈ 𝐻 → ((1st ‘𝑑) ⊆ (1st
‘𝑓) →
(2nd ‘𝑑)
∈ 𝑡))) |
70 | 63, 69 | syl6bb 275 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → ((𝑑 ∈ ((tail‘𝐷)‘𝑓) → ((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡) ↔ (𝑑 ∈ 𝐻 → ((1st ‘𝑑) ⊆ (1st
‘𝑓) →
(2nd ‘𝑑)
∈ 𝑡)))) |
71 | 70 | ralbidv2 2967 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → (∀𝑑 ∈ ((tail‘𝐷)‘𝑓)((2nd ↾ 𝐻)‘𝑑) ∈ 𝑡 ↔ ∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd
‘𝑑) ∈ 𝑡))) |
72 | 49, 71 | bitrd 267 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑓 ∈ 𝐻) → (((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd
‘𝑑) ∈ 𝑡))) |
73 | 72 | rexbidva 3031 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) → (∃𝑓 ∈ 𝐻 ((2nd ↾ 𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∃𝑓 ∈ 𝐻 ∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd
‘𝑑) ∈ 𝑡))) |
74 | | vex 3176 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑘 ∈ V |
75 | | vex 3176 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑣 ∈ V |
76 | 74, 75 | op1std 7069 |
. . . . . . . . . . . . . . . 16
⊢ (𝑑 = 〈𝑘, 𝑣〉 → (1st ‘𝑑) = 𝑘) |
77 | 76 | sseq1d 3595 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 = 〈𝑘, 𝑣〉 → ((1st ‘𝑑) ⊆ (1st
‘𝑓) ↔ 𝑘 ⊆ (1st
‘𝑓))) |
78 | 74, 75 | op2ndd 7070 |
. . . . . . . . . . . . . . . 16
⊢ (𝑑 = 〈𝑘, 𝑣〉 → (2nd ‘𝑑) = 𝑣) |
79 | 78 | eleq1d 2672 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 = 〈𝑘, 𝑣〉 → ((2nd ‘𝑑) ∈ 𝑡 ↔ 𝑣 ∈ 𝑡)) |
80 | 77, 79 | imbi12d 333 |
. . . . . . . . . . . . . 14
⊢ (𝑑 = 〈𝑘, 𝑣〉 → (((1st ‘𝑑) ⊆ (1st
‘𝑓) →
(2nd ‘𝑑)
∈ 𝑡) ↔ (𝑘 ⊆ (1st
‘𝑓) → 𝑣 ∈ 𝑡))) |
81 | 80 | raliunxp 5183 |
. . . . . . . . . . . . 13
⊢
(∀𝑑 ∈
∪ 𝑘 ∈ 𝐹 ({𝑘} × 𝑘)((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd
‘𝑑) ∈ 𝑡) ↔ ∀𝑘 ∈ 𝐹 ∀𝑣 ∈ 𝑘 (𝑘 ⊆ (1st ‘𝑓) → 𝑣 ∈ 𝑡)) |
82 | | sneq 4135 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑘 → {𝑛} = {𝑘}) |
83 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑘 → 𝑛 = 𝑘) |
84 | 82, 83 | xpeq12d 5064 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑘 → ({𝑛} × 𝑛) = ({𝑘} × 𝑘)) |
85 | 84 | cbviunv 4495 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛) = ∪ 𝑘 ∈ 𝐹 ({𝑘} × 𝑘) |
86 | 1, 85 | eqtri 2632 |
. . . . . . . . . . . . . 14
⊢ 𝐻 = ∪ 𝑘 ∈ 𝐹 ({𝑘} × 𝑘) |
87 | 86 | raleqi 3119 |
. . . . . . . . . . . . 13
⊢
(∀𝑑 ∈
𝐻 ((1st
‘𝑑) ⊆
(1st ‘𝑓)
→ (2nd ‘𝑑) ∈ 𝑡) ↔ ∀𝑑 ∈ ∪
𝑘 ∈ 𝐹 ({𝑘} × 𝑘)((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd
‘𝑑) ∈ 𝑡)) |
88 | | dfss3 3558 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ⊆ 𝑡 ↔ ∀𝑣 ∈ 𝑘 𝑣 ∈ 𝑡) |
89 | 88 | imbi2i 325 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ⊆ (1st
‘𝑓) → 𝑘 ⊆ 𝑡) ↔ (𝑘 ⊆ (1st ‘𝑓) → ∀𝑣 ∈ 𝑘 𝑣 ∈ 𝑡)) |
90 | | r19.21v 2943 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑣 ∈
𝑘 (𝑘 ⊆ (1st ‘𝑓) → 𝑣 ∈ 𝑡) ↔ (𝑘 ⊆ (1st ‘𝑓) → ∀𝑣 ∈ 𝑘 𝑣 ∈ 𝑡)) |
91 | 89, 90 | bitr4i 266 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ⊆ (1st
‘𝑓) → 𝑘 ⊆ 𝑡) ↔ ∀𝑣 ∈ 𝑘 (𝑘 ⊆ (1st ‘𝑓) → 𝑣 ∈ 𝑡)) |
92 | 91 | ralbii 2963 |
. . . . . . . . . . . . 13
⊢
(∀𝑘 ∈
𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ ∀𝑘 ∈ 𝐹 ∀𝑣 ∈ 𝑘 (𝑘 ⊆ (1st ‘𝑓) → 𝑣 ∈ 𝑡)) |
93 | 81, 87, 92 | 3bitr4i 291 |
. . . . . . . . . . . 12
⊢
(∀𝑑 ∈
𝐻 ((1st
‘𝑑) ⊆
(1st ‘𝑓)
→ (2nd ‘𝑑) ∈ 𝑡) ↔ ∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡)) |
94 | 93 | rexbii 3023 |
. . . . . . . . . . 11
⊢
(∃𝑓 ∈
𝐻 ∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd
‘𝑑) ∈ 𝑡) ↔ ∃𝑓 ∈ 𝐻 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡)) |
95 | 1 | rexeqi 3120 |
. . . . . . . . . . 11
⊢
(∃𝑓 ∈
𝐻 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ ∃𝑓 ∈ ∪
𝑛 ∈ 𝐹 ({𝑛} × 𝑛)∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡)) |
96 | | vex 3176 |
. . . . . . . . . . . . . . . 16
⊢ 𝑛 ∈ V |
97 | | vex 3176 |
. . . . . . . . . . . . . . . 16
⊢ 𝑚 ∈ V |
98 | 96, 97 | op1std 7069 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = 〈𝑛, 𝑚〉 → (1st ‘𝑓) = 𝑛) |
99 | 98 | sseq2d 3596 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = 〈𝑛, 𝑚〉 → (𝑘 ⊆ (1st ‘𝑓) ↔ 𝑘 ⊆ 𝑛)) |
100 | 99 | imbi1d 330 |
. . . . . . . . . . . . 13
⊢ (𝑓 = 〈𝑛, 𝑚〉 → ((𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡))) |
101 | 100 | ralbidv 2969 |
. . . . . . . . . . . 12
⊢ (𝑓 = 〈𝑛, 𝑚〉 → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡))) |
102 | 101 | rexiunxp 5184 |
. . . . . . . . . . 11
⊢
(∃𝑓 ∈
∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛)∀𝑘 ∈ 𝐹 (𝑘 ⊆ (1st ‘𝑓) → 𝑘 ⊆ 𝑡) ↔ ∃𝑛 ∈ 𝐹 ∃𝑚 ∈ 𝑛 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡)) |
103 | 94, 95, 102 | 3bitri 285 |
. . . . . . . . . 10
⊢
(∃𝑓 ∈
𝐻 ∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd
‘𝑑) ∈ 𝑡) ↔ ∃𝑛 ∈ 𝐹 ∃𝑚 ∈ 𝑛 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡)) |
104 | | fileln0 21464 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛 ∈ 𝐹) → 𝑛 ≠ ∅) |
105 | 104 | adantlr 747 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑛 ∈ 𝐹) → 𝑛 ≠ ∅) |
106 | | r19.9rzv 4017 |
. . . . . . . . . . . . 13
⊢ (𝑛 ≠ ∅ →
(∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) ↔ ∃𝑚 ∈ 𝑛 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡))) |
107 | 105, 106 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑛 ∈ 𝐹) → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) ↔ ∃𝑚 ∈ 𝑛 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡))) |
108 | | ssid 3587 |
. . . . . . . . . . . . . . 15
⊢ 𝑛 ⊆ 𝑛 |
109 | | sseq1 3589 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑛 → (𝑘 ⊆ 𝑛 ↔ 𝑛 ⊆ 𝑛)) |
110 | | sseq1 3589 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑛 → (𝑘 ⊆ 𝑡 ↔ 𝑛 ⊆ 𝑡)) |
111 | 109, 110 | imbi12d 333 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑛 → ((𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) ↔ (𝑛 ⊆ 𝑛 → 𝑛 ⊆ 𝑡))) |
112 | 111 | rspcv 3278 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ 𝐹 → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) → (𝑛 ⊆ 𝑛 → 𝑛 ⊆ 𝑡))) |
113 | 108, 112 | mpii 45 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ 𝐹 → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) → 𝑛 ⊆ 𝑡)) |
114 | 113 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑛 ∈ 𝐹) → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) → 𝑛 ⊆ 𝑡)) |
115 | | sstr2 3575 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ⊆ 𝑛 → (𝑛 ⊆ 𝑡 → 𝑘 ⊆ 𝑡)) |
116 | 115 | com12 32 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ⊆ 𝑡 → (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡)) |
117 | 116 | ralrimivw 2950 |
. . . . . . . . . . . . 13
⊢ (𝑛 ⊆ 𝑡 → ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡)) |
118 | 114, 117 | impbid1 214 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑛 ∈ 𝐹) → (∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) ↔ 𝑛 ⊆ 𝑡)) |
119 | 107, 118 | bitr3d 269 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) ∧ 𝑛 ∈ 𝐹) → (∃𝑚 ∈ 𝑛 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) ↔ 𝑛 ⊆ 𝑡)) |
120 | 119 | rexbidva 3031 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) → (∃𝑛 ∈ 𝐹 ∃𝑚 ∈ 𝑛 ∀𝑘 ∈ 𝐹 (𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡) ↔ ∃𝑛 ∈ 𝐹 𝑛 ⊆ 𝑡)) |
121 | 103, 120 | syl5bb 271 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) → (∃𝑓 ∈ 𝐻 ∀𝑑 ∈ 𝐻 ((1st ‘𝑑) ⊆ (1st ‘𝑓) → (2nd
‘𝑑) ∈ 𝑡) ↔ ∃𝑛 ∈ 𝐹 𝑛 ⊆ 𝑡)) |
122 | 32, 73, 121 | 3bitrd 293 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡 ⊆ 𝑋) → (∃𝑑 ∈ ran (tail‘𝐷)((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡 ↔ ∃𝑛 ∈ 𝐹 𝑛 ⊆ 𝑡)) |
123 | 122 | pm5.32da 671 |
. . . . . . 7
⊢ (𝐹 ∈ (Fil‘𝑋) → ((𝑡 ⊆ 𝑋 ∧ ∃𝑑 ∈ ran (tail‘𝐷)((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡) ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑛 ∈ 𝐹 𝑛 ⊆ 𝑡))) |
124 | | filn0 21476 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ≠ ∅) |
125 | 96 | snnz 4252 |
. . . . . . . . . . . . . . . 16
⊢ {𝑛} ≠ ∅ |
126 | 104, 125 | jctil 558 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛 ∈ 𝐹) → ({𝑛} ≠ ∅ ∧ 𝑛 ≠ ∅)) |
127 | | neanior 2874 |
. . . . . . . . . . . . . . 15
⊢ (({𝑛} ≠ ∅ ∧ 𝑛 ≠ ∅) ↔ ¬
({𝑛} = ∅ ∨ 𝑛 = ∅)) |
128 | 126, 127 | sylib 207 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛 ∈ 𝐹) → ¬ ({𝑛} = ∅ ∨ 𝑛 = ∅)) |
129 | | ss0b 3925 |
. . . . . . . . . . . . . . 15
⊢ (({𝑛} × 𝑛) ⊆ ∅ ↔ ({𝑛} × 𝑛) = ∅) |
130 | | xpeq0 5473 |
. . . . . . . . . . . . . . 15
⊢ (({𝑛} × 𝑛) = ∅ ↔ ({𝑛} = ∅ ∨ 𝑛 = ∅)) |
131 | 129, 130 | bitri 263 |
. . . . . . . . . . . . . 14
⊢ (({𝑛} × 𝑛) ⊆ ∅ ↔ ({𝑛} = ∅ ∨ 𝑛 = ∅)) |
132 | 128, 131 | sylnibr 318 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛 ∈ 𝐹) → ¬ ({𝑛} × 𝑛) ⊆ ∅) |
133 | 132 | ralrimiva 2949 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (Fil‘𝑋) → ∀𝑛 ∈ 𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅) |
134 | | r19.2z 4012 |
. . . . . . . . . . . 12
⊢ ((𝐹 ≠ ∅ ∧
∀𝑛 ∈ 𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅) → ∃𝑛 ∈ 𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅) |
135 | 124, 133,
134 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (Fil‘𝑋) → ∃𝑛 ∈ 𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅) |
136 | | rexnal 2978 |
. . . . . . . . . . 11
⊢
(∃𝑛 ∈
𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅ ↔ ¬ ∀𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅) |
137 | 135, 136 | sylib 207 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (Fil‘𝑋) → ¬ ∀𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅) |
138 | 1 | sseq1i 3592 |
. . . . . . . . . . . 12
⊢ (𝐻 ⊆ ∅ ↔ ∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅) |
139 | | ss0b 3925 |
. . . . . . . . . . . 12
⊢ (𝐻 ⊆ ∅ ↔ 𝐻 = ∅) |
140 | | iunss 4497 |
. . . . . . . . . . . 12
⊢ (∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅ ↔ ∀𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅) |
141 | 138, 139,
140 | 3bitr3i 289 |
. . . . . . . . . . 11
⊢ (𝐻 = ∅ ↔ ∀𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅) |
142 | 141 | necon3abii 2828 |
. . . . . . . . . 10
⊢ (𝐻 ≠ ∅ ↔ ¬
∀𝑛 ∈ 𝐹 ({𝑛} × 𝑛) ⊆ ∅) |
143 | 137, 142 | sylibr 223 |
. . . . . . . . 9
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐻 ≠ ∅) |
144 | | dmresi 5376 |
. . . . . . . . . . . 12
⊢ dom ( I
↾ 𝐻) = 𝐻 |
145 | 1, 2 | filnetlem2 31544 |
. . . . . . . . . . . . . 14
⊢ (( I
↾ 𝐻) ⊆ 𝐷 ∧ 𝐷 ⊆ (𝐻 × 𝐻)) |
146 | 145 | simpli 473 |
. . . . . . . . . . . . 13
⊢ ( I
↾ 𝐻) ⊆ 𝐷 |
147 | | dmss 5245 |
. . . . . . . . . . . . 13
⊢ (( I
↾ 𝐻) ⊆ 𝐷 → dom ( I ↾ 𝐻) ⊆ dom 𝐷) |
148 | 146, 147 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ dom ( I
↾ 𝐻) ⊆ dom
𝐷 |
149 | 144, 148 | eqsstr3i 3599 |
. . . . . . . . . . 11
⊢ 𝐻 ⊆ dom 𝐷 |
150 | 145 | simpri 477 |
. . . . . . . . . . . . 13
⊢ 𝐷 ⊆ (𝐻 × 𝐻) |
151 | | dmss 5245 |
. . . . . . . . . . . . 13
⊢ (𝐷 ⊆ (𝐻 × 𝐻) → dom 𝐷 ⊆ dom (𝐻 × 𝐻)) |
152 | 150, 151 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ dom 𝐷 ⊆ dom (𝐻 × 𝐻) |
153 | | dmxpid 5266 |
. . . . . . . . . . . 12
⊢ dom
(𝐻 × 𝐻) = 𝐻 |
154 | 152, 153 | sseqtri 3600 |
. . . . . . . . . . 11
⊢ dom 𝐷 ⊆ 𝐻 |
155 | 149, 154 | eqssi 3584 |
. . . . . . . . . 10
⊢ 𝐻 = dom 𝐷 |
156 | 155 | tailfb 31542 |
. . . . . . . . 9
⊢ ((𝐷 ∈ DirRel ∧ 𝐻 ≠ ∅) → ran
(tail‘𝐷) ∈
(fBas‘𝐻)) |
157 | 5, 143, 156 | syl2anc 691 |
. . . . . . . 8
⊢ (𝐹 ∈ (Fil‘𝑋) → ran (tail‘𝐷) ∈ (fBas‘𝐻)) |
158 | | elfm 21561 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝐹 ∧ ran (tail‘𝐷) ∈ (fBas‘𝐻) ∧ (2nd ↾ 𝐻):𝐻⟶𝑋) → (𝑡 ∈ ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)) ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑑 ∈ ran (tail‘𝐷)((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡))) |
159 | 10, 157, 9, 158 | syl3anc 1318 |
. . . . . . 7
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑡 ∈ ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)) ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑑 ∈ ran (tail‘𝐷)((2nd ↾ 𝐻) “ 𝑑) ⊆ 𝑡))) |
160 | | filfbas 21462 |
. . . . . . . 8
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋)) |
161 | | elfg 21485 |
. . . . . . . 8
⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑡 ∈ (𝑋filGen𝐹) ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑛 ∈ 𝐹 𝑛 ⊆ 𝑡))) |
162 | 160, 161 | syl 17 |
. . . . . . 7
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑡 ∈ (𝑋filGen𝐹) ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑛 ∈ 𝐹 𝑛 ⊆ 𝑡))) |
163 | 123, 159,
162 | 3bitr4d 299 |
. . . . . 6
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑡 ∈ ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)) ↔ 𝑡 ∈ (𝑋filGen𝐹))) |
164 | 163 | eqrdv 2608 |
. . . . 5
⊢ (𝐹 ∈ (Fil‘𝑋) → ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)) = (𝑋filGen𝐹)) |
165 | | fgfil 21489 |
. . . . 5
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑋filGen𝐹) = 𝐹) |
166 | 164, 165 | eqtr2d 2645 |
. . . 4
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 = ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷))) |
167 | 21, 166 | jca 553 |
. . 3
⊢ (𝐹 ∈ (Fil‘𝑋) → ((2nd
↾ 𝐻):dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)))) |
168 | | feq1 5939 |
. . . . 5
⊢ (𝑓 = (2nd ↾ 𝐻) → (𝑓:dom 𝐷⟶𝑋 ↔ (2nd ↾ 𝐻):dom 𝐷⟶𝑋)) |
169 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑓 = (2nd ↾ 𝐻) → (𝑋 FilMap 𝑓) = (𝑋 FilMap (2nd ↾ 𝐻))) |
170 | 169 | fveq1d 6105 |
. . . . . 6
⊢ (𝑓 = (2nd ↾ 𝐻) → ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)) = ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷))) |
171 | 170 | eqeq2d 2620 |
. . . . 5
⊢ (𝑓 = (2nd ↾ 𝐻) → (𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)) ↔ 𝐹 = ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷)))) |
172 | 168, 171 | anbi12d 743 |
. . . 4
⊢ (𝑓 = (2nd ↾ 𝐻) → ((𝑓:dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷))) ↔ ((2nd ↾ 𝐻):dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷))))) |
173 | 172 | spcegv 3267 |
. . 3
⊢
((2nd ↾ 𝐻) ∈ V → (((2nd ↾
𝐻):dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap (2nd ↾ 𝐻))‘ran (tail‘𝐷))) → ∃𝑓(𝑓:dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷))))) |
174 | 15, 167, 173 | sylc 63 |
. 2
⊢ (𝐹 ∈ (Fil‘𝑋) → ∃𝑓(𝑓:dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))) |
175 | | dmeq 5246 |
. . . . . 6
⊢ (𝑑 = 𝐷 → dom 𝑑 = dom 𝐷) |
176 | 175 | feq2d 5944 |
. . . . 5
⊢ (𝑑 = 𝐷 → (𝑓:dom 𝑑⟶𝑋 ↔ 𝑓:dom 𝐷⟶𝑋)) |
177 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑑 = 𝐷 → (tail‘𝑑) = (tail‘𝐷)) |
178 | 177 | rneqd 5274 |
. . . . . . 7
⊢ (𝑑 = 𝐷 → ran (tail‘𝑑) = ran (tail‘𝐷)) |
179 | 178 | fveq2d 6107 |
. . . . . 6
⊢ (𝑑 = 𝐷 → ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑)) = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷))) |
180 | 179 | eqeq2d 2620 |
. . . . 5
⊢ (𝑑 = 𝐷 → (𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑)) ↔ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))) |
181 | 176, 180 | anbi12d 743 |
. . . 4
⊢ (𝑑 = 𝐷 → ((𝑓:dom 𝑑⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))) ↔ (𝑓:dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷))))) |
182 | 181 | exbidv 1837 |
. . 3
⊢ (𝑑 = 𝐷 → (∃𝑓(𝑓:dom 𝑑⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))) ↔ ∃𝑓(𝑓:dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷))))) |
183 | 182 | rspcev 3282 |
. 2
⊢ ((𝐷 ∈ DirRel ∧
∃𝑓(𝑓:dom 𝐷⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))) → ∃𝑑 ∈ DirRel ∃𝑓(𝑓:dom 𝑑⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑)))) |
184 | 5, 174, 183 | syl2anc 691 |
1
⊢ (𝐹 ∈ (Fil‘𝑋) → ∃𝑑 ∈ DirRel ∃𝑓(𝑓:dom 𝑑⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑)))) |