Users' Mathboxes Mathbox for Jeff Hankins < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  filnetlem4 Structured version   Visualization version   GIF version

Theorem filnetlem4 36383
Description: Lemma for filnet 36384. (Contributed by Jeff Hankins, 15-Dec-2009.) (Revised by Mario Carneiro, 8-Aug-2015.)
Hypotheses
Ref Expression
filnet.h 𝐻 = 𝑛𝐹 ({𝑛} × 𝑛)
filnet.d 𝐷 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐻𝑦𝐻) ∧ (1st𝑦) ⊆ (1st𝑥))}
Assertion
Ref Expression
filnetlem4 (𝐹 ∈ (Fil‘𝑋) → ∃𝑑 ∈ DirRel ∃𝑓(𝑓:dom 𝑑𝑋𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))))
Distinct variable groups:   𝑥,𝑦   𝑓,𝑑,𝑛,𝑥,𝑦,𝐹   𝐻,𝑑,𝑓,𝑥,𝑦   𝐷,𝑑,𝑓   𝑋,𝑑,𝑓,𝑛
Allowed substitution hints:   𝐷(𝑥,𝑦,𝑛)   𝐻(𝑛)   𝑋(𝑥,𝑦)

Proof of Theorem filnetlem4
Dummy variables 𝑘 𝑚 𝑡 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 filnet.h . . . . 5 𝐻 = 𝑛𝐹 ({𝑛} × 𝑛)
2 filnet.d . . . . 5 𝐷 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐻𝑦𝐻) ∧ (1st𝑦) ⊆ (1st𝑥))}
31, 2filnetlem3 36382 . . . 4 (𝐻 = 𝐷 ∧ (𝐹 ∈ (Fil‘𝑋) → (𝐻 ⊆ (𝐹 × 𝑋) ∧ 𝐷 ∈ DirRel)))
43simpri 485 . . 3 (𝐹 ∈ (Fil‘𝑋) → (𝐻 ⊆ (𝐹 × 𝑋) ∧ 𝐷 ∈ DirRel))
54simprd 495 . 2 (𝐹 ∈ (Fil‘𝑋) → 𝐷 ∈ DirRel)
6 f2ndres 8040 . . . . 5 (2nd ↾ (𝐹 × 𝑋)):(𝐹 × 𝑋)⟶𝑋
74simpld 494 . . . . 5 (𝐹 ∈ (Fil‘𝑋) → 𝐻 ⊆ (𝐹 × 𝑋))
8 fssres2 6775 . . . . 5 (((2nd ↾ (𝐹 × 𝑋)):(𝐹 × 𝑋)⟶𝑋𝐻 ⊆ (𝐹 × 𝑋)) → (2nd𝐻):𝐻𝑋)
96, 7, 8sylancr 587 . . . 4 (𝐹 ∈ (Fil‘𝑋) → (2nd𝐻):𝐻𝑋)
10 filtop 23864 . . . . . 6 (𝐹 ∈ (Fil‘𝑋) → 𝑋𝐹)
11 xpexg 7771 . . . . . 6 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑋𝐹) → (𝐹 × 𝑋) ∈ V)
1210, 11mpdan 687 . . . . 5 (𝐹 ∈ (Fil‘𝑋) → (𝐹 × 𝑋) ∈ V)
1312, 7ssexd 5323 . . . 4 (𝐹 ∈ (Fil‘𝑋) → 𝐻 ∈ V)
149, 13fexd 7248 . . 3 (𝐹 ∈ (Fil‘𝑋) → (2nd𝐻) ∈ V)
153simpli 483 . . . . . . 7 𝐻 = 𝐷
16 dirdm 18646 . . . . . . . 8 (𝐷 ∈ DirRel → dom 𝐷 = 𝐷)
175, 16syl 17 . . . . . . 7 (𝐹 ∈ (Fil‘𝑋) → dom 𝐷 = 𝐷)
1815, 17eqtr4id 2795 . . . . . 6 (𝐹 ∈ (Fil‘𝑋) → 𝐻 = dom 𝐷)
1918feq2d 6721 . . . . 5 (𝐹 ∈ (Fil‘𝑋) → ((2nd𝐻):𝐻𝑋 ↔ (2nd𝐻):dom 𝐷𝑋))
209, 19mpbid 232 . . . 4 (𝐹 ∈ (Fil‘𝑋) → (2nd𝐻):dom 𝐷𝑋)
21 eqid 2736 . . . . . . . . . . . . . 14 dom 𝐷 = dom 𝐷
2221tailf 36377 . . . . . . . . . . . . 13 (𝐷 ∈ DirRel → (tail‘𝐷):dom 𝐷⟶𝒫 dom 𝐷)
235, 22syl 17 . . . . . . . . . . . 12 (𝐹 ∈ (Fil‘𝑋) → (tail‘𝐷):dom 𝐷⟶𝒫 dom 𝐷)
2418feq2d 6721 . . . . . . . . . . . 12 (𝐹 ∈ (Fil‘𝑋) → ((tail‘𝐷):𝐻⟶𝒫 dom 𝐷 ↔ (tail‘𝐷):dom 𝐷⟶𝒫 dom 𝐷))
2523, 24mpbird 257 . . . . . . . . . . 11 (𝐹 ∈ (Fil‘𝑋) → (tail‘𝐷):𝐻⟶𝒫 dom 𝐷)
2625adantr 480 . . . . . . . . . 10 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) → (tail‘𝐷):𝐻⟶𝒫 dom 𝐷)
27 ffn 6735 . . . . . . . . . 10 ((tail‘𝐷):𝐻⟶𝒫 dom 𝐷 → (tail‘𝐷) Fn 𝐻)
28 imaeq2 6073 . . . . . . . . . . . 12 (𝑑 = ((tail‘𝐷)‘𝑓) → ((2nd𝐻) “ 𝑑) = ((2nd𝐻) “ ((tail‘𝐷)‘𝑓)))
2928sseq1d 4014 . . . . . . . . . . 11 (𝑑 = ((tail‘𝐷)‘𝑓) → (((2nd𝐻) “ 𝑑) ⊆ 𝑡 ↔ ((2nd𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡))
3029rexrn 7106 . . . . . . . . . 10 ((tail‘𝐷) Fn 𝐻 → (∃𝑑 ∈ ran (tail‘𝐷)((2nd𝐻) “ 𝑑) ⊆ 𝑡 ↔ ∃𝑓𝐻 ((2nd𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡))
3126, 27, 303syl 18 . . . . . . . . 9 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) → (∃𝑑 ∈ ran (tail‘𝐷)((2nd𝐻) “ 𝑑) ⊆ 𝑡 ↔ ∃𝑓𝐻 ((2nd𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡))
32 fo2nd 8036 . . . . . . . . . . . . . . 15 2nd :V–onto→V
33 fofn 6821 . . . . . . . . . . . . . . 15 (2nd :V–onto→V → 2nd Fn V)
3432, 33ax-mp 5 . . . . . . . . . . . . . 14 2nd Fn V
35 ssv 4007 . . . . . . . . . . . . . 14 𝐻 ⊆ V
36 fnssres 6690 . . . . . . . . . . . . . 14 ((2nd Fn V ∧ 𝐻 ⊆ V) → (2nd𝐻) Fn 𝐻)
3734, 35, 36mp2an 692 . . . . . . . . . . . . 13 (2nd𝐻) Fn 𝐻
38 fnfun 6667 . . . . . . . . . . . . 13 ((2nd𝐻) Fn 𝐻 → Fun (2nd𝐻))
3937, 38ax-mp 5 . . . . . . . . . . . 12 Fun (2nd𝐻)
4026ffvelcdmda 7103 . . . . . . . . . . . . . . 15 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → ((tail‘𝐷)‘𝑓) ∈ 𝒫 dom 𝐷)
4140elpwid 4608 . . . . . . . . . . . . . 14 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → ((tail‘𝐷)‘𝑓) ⊆ dom 𝐷)
4218ad2antrr 726 . . . . . . . . . . . . . 14 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → 𝐻 = dom 𝐷)
4341, 42sseqtrrd 4020 . . . . . . . . . . . . 13 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → ((tail‘𝐷)‘𝑓) ⊆ 𝐻)
4437fndmi 6671 . . . . . . . . . . . . 13 dom (2nd𝐻) = 𝐻
4543, 44sseqtrrdi 4024 . . . . . . . . . . . 12 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → ((tail‘𝐷)‘𝑓) ⊆ dom (2nd𝐻))
46 funimass4 6972 . . . . . . . . . . . 12 ((Fun (2nd𝐻) ∧ ((tail‘𝐷)‘𝑓) ⊆ dom (2nd𝐻)) → (((2nd𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∀𝑑 ∈ ((tail‘𝐷)‘𝑓)((2nd𝐻)‘𝑑) ∈ 𝑡))
4739, 45, 46sylancr 587 . . . . . . . . . . 11 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → (((2nd𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∀𝑑 ∈ ((tail‘𝐷)‘𝑓)((2nd𝐻)‘𝑑) ∈ 𝑡))
485ad2antrr 726 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → 𝐷 ∈ DirRel)
49 simpr 484 . . . . . . . . . . . . . . . . 17 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → 𝑓𝐻)
5049, 42eleqtrd 2842 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → 𝑓 ∈ dom 𝐷)
51 vex 3483 . . . . . . . . . . . . . . . . 17 𝑑 ∈ V
5251a1i 11 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → 𝑑 ∈ V)
5321eltail 36376 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ DirRel ∧ 𝑓 ∈ dom 𝐷𝑑 ∈ V) → (𝑑 ∈ ((tail‘𝐷)‘𝑓) ↔ 𝑓𝐷𝑑))
5448, 50, 52, 53syl3anc 1372 . . . . . . . . . . . . . . 15 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → (𝑑 ∈ ((tail‘𝐷)‘𝑓) ↔ 𝑓𝐷𝑑))
5549biantrurd 532 . . . . . . . . . . . . . . . . 17 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → (𝑑𝐻 ↔ (𝑓𝐻𝑑𝐻)))
5655anbi1d 631 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → ((𝑑𝐻 ∧ (1st𝑑) ⊆ (1st𝑓)) ↔ ((𝑓𝐻𝑑𝐻) ∧ (1st𝑑) ⊆ (1st𝑓))))
57 vex 3483 . . . . . . . . . . . . . . . . 17 𝑓 ∈ V
581, 2, 57, 51filnetlem1 36380 . . . . . . . . . . . . . . . 16 (𝑓𝐷𝑑 ↔ ((𝑓𝐻𝑑𝐻) ∧ (1st𝑑) ⊆ (1st𝑓)))
5956, 58bitr4di 289 . . . . . . . . . . . . . . 15 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → ((𝑑𝐻 ∧ (1st𝑑) ⊆ (1st𝑓)) ↔ 𝑓𝐷𝑑))
6054, 59bitr4d 282 . . . . . . . . . . . . . 14 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → (𝑑 ∈ ((tail‘𝐷)‘𝑓) ↔ (𝑑𝐻 ∧ (1st𝑑) ⊆ (1st𝑓))))
6160imbi1d 341 . . . . . . . . . . . . 13 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → ((𝑑 ∈ ((tail‘𝐷)‘𝑓) → ((2nd𝐻)‘𝑑) ∈ 𝑡) ↔ ((𝑑𝐻 ∧ (1st𝑑) ⊆ (1st𝑓)) → ((2nd𝐻)‘𝑑) ∈ 𝑡)))
62 fvres 6924 . . . . . . . . . . . . . . . . 17 (𝑑𝐻 → ((2nd𝐻)‘𝑑) = (2nd𝑑))
6362eleq1d 2825 . . . . . . . . . . . . . . . 16 (𝑑𝐻 → (((2nd𝐻)‘𝑑) ∈ 𝑡 ↔ (2nd𝑑) ∈ 𝑡))
6463adantr 480 . . . . . . . . . . . . . . 15 ((𝑑𝐻 ∧ (1st𝑑) ⊆ (1st𝑓)) → (((2nd𝐻)‘𝑑) ∈ 𝑡 ↔ (2nd𝑑) ∈ 𝑡))
6564pm5.74i 271 . . . . . . . . . . . . . 14 (((𝑑𝐻 ∧ (1st𝑑) ⊆ (1st𝑓)) → ((2nd𝐻)‘𝑑) ∈ 𝑡) ↔ ((𝑑𝐻 ∧ (1st𝑑) ⊆ (1st𝑓)) → (2nd𝑑) ∈ 𝑡))
66 impexp 450 . . . . . . . . . . . . . 14 (((𝑑𝐻 ∧ (1st𝑑) ⊆ (1st𝑓)) → (2nd𝑑) ∈ 𝑡) ↔ (𝑑𝐻 → ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡)))
6765, 66bitri 275 . . . . . . . . . . . . 13 (((𝑑𝐻 ∧ (1st𝑑) ⊆ (1st𝑓)) → ((2nd𝐻)‘𝑑) ∈ 𝑡) ↔ (𝑑𝐻 → ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡)))
6861, 67bitrdi 287 . . . . . . . . . . . 12 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → ((𝑑 ∈ ((tail‘𝐷)‘𝑓) → ((2nd𝐻)‘𝑑) ∈ 𝑡) ↔ (𝑑𝐻 → ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡))))
6968ralbidv2 3173 . . . . . . . . . . 11 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → (∀𝑑 ∈ ((tail‘𝐷)‘𝑓)((2nd𝐻)‘𝑑) ∈ 𝑡 ↔ ∀𝑑𝐻 ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡)))
7047, 69bitrd 279 . . . . . . . . . 10 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → (((2nd𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∀𝑑𝐻 ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡)))
7170rexbidva 3176 . . . . . . . . 9 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) → (∃𝑓𝐻 ((2nd𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∃𝑓𝐻𝑑𝐻 ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡)))
72 vex 3483 . . . . . . . . . . . . . . . . 17 𝑘 ∈ V
73 vex 3483 . . . . . . . . . . . . . . . . 17 𝑣 ∈ V
7472, 73op1std 8025 . . . . . . . . . . . . . . . 16 (𝑑 = ⟨𝑘, 𝑣⟩ → (1st𝑑) = 𝑘)
7574sseq1d 4014 . . . . . . . . . . . . . . 15 (𝑑 = ⟨𝑘, 𝑣⟩ → ((1st𝑑) ⊆ (1st𝑓) ↔ 𝑘 ⊆ (1st𝑓)))
7672, 73op2ndd 8026 . . . . . . . . . . . . . . . 16 (𝑑 = ⟨𝑘, 𝑣⟩ → (2nd𝑑) = 𝑣)
7776eleq1d 2825 . . . . . . . . . . . . . . 15 (𝑑 = ⟨𝑘, 𝑣⟩ → ((2nd𝑑) ∈ 𝑡𝑣𝑡))
7875, 77imbi12d 344 . . . . . . . . . . . . . 14 (𝑑 = ⟨𝑘, 𝑣⟩ → (((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡) ↔ (𝑘 ⊆ (1st𝑓) → 𝑣𝑡)))
7978raliunxp 5849 . . . . . . . . . . . . 13 (∀𝑑 𝑘𝐹 ({𝑘} × 𝑘)((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡) ↔ ∀𝑘𝐹𝑣𝑘 (𝑘 ⊆ (1st𝑓) → 𝑣𝑡))
80 sneq 4635 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑘 → {𝑛} = {𝑘})
81 id 22 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑘𝑛 = 𝑘)
8280, 81xpeq12d 5715 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑘 → ({𝑛} × 𝑛) = ({𝑘} × 𝑘))
8382cbviunv 5039 . . . . . . . . . . . . . . 15 𝑛𝐹 ({𝑛} × 𝑛) = 𝑘𝐹 ({𝑘} × 𝑘)
841, 83eqtri 2764 . . . . . . . . . . . . . 14 𝐻 = 𝑘𝐹 ({𝑘} × 𝑘)
8584raleqi 3323 . . . . . . . . . . . . 13 (∀𝑑𝐻 ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡) ↔ ∀𝑑 𝑘𝐹 ({𝑘} × 𝑘)((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡))
86 dfss3 3971 . . . . . . . . . . . . . . . 16 (𝑘𝑡 ↔ ∀𝑣𝑘 𝑣𝑡)
8786imbi2i 336 . . . . . . . . . . . . . . 15 ((𝑘 ⊆ (1st𝑓) → 𝑘𝑡) ↔ (𝑘 ⊆ (1st𝑓) → ∀𝑣𝑘 𝑣𝑡))
88 r19.21v 3179 . . . . . . . . . . . . . . 15 (∀𝑣𝑘 (𝑘 ⊆ (1st𝑓) → 𝑣𝑡) ↔ (𝑘 ⊆ (1st𝑓) → ∀𝑣𝑘 𝑣𝑡))
8987, 88bitr4i 278 . . . . . . . . . . . . . 14 ((𝑘 ⊆ (1st𝑓) → 𝑘𝑡) ↔ ∀𝑣𝑘 (𝑘 ⊆ (1st𝑓) → 𝑣𝑡))
9089ralbii 3092 . . . . . . . . . . . . 13 (∀𝑘𝐹 (𝑘 ⊆ (1st𝑓) → 𝑘𝑡) ↔ ∀𝑘𝐹𝑣𝑘 (𝑘 ⊆ (1st𝑓) → 𝑣𝑡))
9179, 85, 903bitr4i 303 . . . . . . . . . . . 12 (∀𝑑𝐻 ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡) ↔ ∀𝑘𝐹 (𝑘 ⊆ (1st𝑓) → 𝑘𝑡))
9291rexbii 3093 . . . . . . . . . . 11 (∃𝑓𝐻𝑑𝐻 ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡) ↔ ∃𝑓𝐻𝑘𝐹 (𝑘 ⊆ (1st𝑓) → 𝑘𝑡))
931rexeqi 3324 . . . . . . . . . . 11 (∃𝑓𝐻𝑘𝐹 (𝑘 ⊆ (1st𝑓) → 𝑘𝑡) ↔ ∃𝑓 𝑛𝐹 ({𝑛} × 𝑛)∀𝑘𝐹 (𝑘 ⊆ (1st𝑓) → 𝑘𝑡))
94 vex 3483 . . . . . . . . . . . . . . . 16 𝑛 ∈ V
95 vex 3483 . . . . . . . . . . . . . . . 16 𝑚 ∈ V
9694, 95op1std 8025 . . . . . . . . . . . . . . 15 (𝑓 = ⟨𝑛, 𝑚⟩ → (1st𝑓) = 𝑛)
9796sseq2d 4015 . . . . . . . . . . . . . 14 (𝑓 = ⟨𝑛, 𝑚⟩ → (𝑘 ⊆ (1st𝑓) ↔ 𝑘𝑛))
9897imbi1d 341 . . . . . . . . . . . . 13 (𝑓 = ⟨𝑛, 𝑚⟩ → ((𝑘 ⊆ (1st𝑓) → 𝑘𝑡) ↔ (𝑘𝑛𝑘𝑡)))
9998ralbidv 3177 . . . . . . . . . . . 12 (𝑓 = ⟨𝑛, 𝑚⟩ → (∀𝑘𝐹 (𝑘 ⊆ (1st𝑓) → 𝑘𝑡) ↔ ∀𝑘𝐹 (𝑘𝑛𝑘𝑡)))
10099rexiunxp 5850 . . . . . . . . . . 11 (∃𝑓 𝑛𝐹 ({𝑛} × 𝑛)∀𝑘𝐹 (𝑘 ⊆ (1st𝑓) → 𝑘𝑡) ↔ ∃𝑛𝐹𝑚𝑛𝑘𝐹 (𝑘𝑛𝑘𝑡))
10192, 93, 1003bitri 297 . . . . . . . . . 10 (∃𝑓𝐻𝑑𝐻 ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡) ↔ ∃𝑛𝐹𝑚𝑛𝑘𝐹 (𝑘𝑛𝑘𝑡))
102 fileln0 23859 . . . . . . . . . . . . . 14 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛𝐹) → 𝑛 ≠ ∅)
103102adantlr 715 . . . . . . . . . . . . 13 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑛𝐹) → 𝑛 ≠ ∅)
104 r19.9rzv 4499 . . . . . . . . . . . . 13 (𝑛 ≠ ∅ → (∀𝑘𝐹 (𝑘𝑛𝑘𝑡) ↔ ∃𝑚𝑛𝑘𝐹 (𝑘𝑛𝑘𝑡)))
105103, 104syl 17 . . . . . . . . . . . 12 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑛𝐹) → (∀𝑘𝐹 (𝑘𝑛𝑘𝑡) ↔ ∃𝑚𝑛𝑘𝐹 (𝑘𝑛𝑘𝑡)))
106 ssid 4005 . . . . . . . . . . . . . . 15 𝑛𝑛
107 sseq1 4008 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑛 → (𝑘𝑛𝑛𝑛))
108 sseq1 4008 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑛 → (𝑘𝑡𝑛𝑡))
109107, 108imbi12d 344 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑛 → ((𝑘𝑛𝑘𝑡) ↔ (𝑛𝑛𝑛𝑡)))
110109rspcv 3617 . . . . . . . . . . . . . . 15 (𝑛𝐹 → (∀𝑘𝐹 (𝑘𝑛𝑘𝑡) → (𝑛𝑛𝑛𝑡)))
111106, 110mpii 46 . . . . . . . . . . . . . 14 (𝑛𝐹 → (∀𝑘𝐹 (𝑘𝑛𝑘𝑡) → 𝑛𝑡))
112111adantl 481 . . . . . . . . . . . . 13 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑛𝐹) → (∀𝑘𝐹 (𝑘𝑛𝑘𝑡) → 𝑛𝑡))
113 sstr2 3989 . . . . . . . . . . . . . . 15 (𝑘𝑛 → (𝑛𝑡𝑘𝑡))
114113com12 32 . . . . . . . . . . . . . 14 (𝑛𝑡 → (𝑘𝑛𝑘𝑡))
115114ralrimivw 3149 . . . . . . . . . . . . 13 (𝑛𝑡 → ∀𝑘𝐹 (𝑘𝑛𝑘𝑡))
116112, 115impbid1 225 . . . . . . . . . . . 12 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑛𝐹) → (∀𝑘𝐹 (𝑘𝑛𝑘𝑡) ↔ 𝑛𝑡))
117105, 116bitr3d 281 . . . . . . . . . . 11 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑛𝐹) → (∃𝑚𝑛𝑘𝐹 (𝑘𝑛𝑘𝑡) ↔ 𝑛𝑡))
118117rexbidva 3176 . . . . . . . . . 10 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) → (∃𝑛𝐹𝑚𝑛𝑘𝐹 (𝑘𝑛𝑘𝑡) ↔ ∃𝑛𝐹 𝑛𝑡))
119101, 118bitrid 283 . . . . . . . . 9 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) → (∃𝑓𝐻𝑑𝐻 ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡) ↔ ∃𝑛𝐹 𝑛𝑡))
12031, 71, 1193bitrd 305 . . . . . . . 8 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) → (∃𝑑 ∈ ran (tail‘𝐷)((2nd𝐻) “ 𝑑) ⊆ 𝑡 ↔ ∃𝑛𝐹 𝑛𝑡))
121120pm5.32da 579 . . . . . . 7 (𝐹 ∈ (Fil‘𝑋) → ((𝑡𝑋 ∧ ∃𝑑 ∈ ran (tail‘𝐷)((2nd𝐻) “ 𝑑) ⊆ 𝑡) ↔ (𝑡𝑋 ∧ ∃𝑛𝐹 𝑛𝑡)))
122 filn0 23871 . . . . . . . . . . . 12 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ≠ ∅)
12394snnz 4775 . . . . . . . . . . . . . . . 16 {𝑛} ≠ ∅
124102, 123jctil 519 . . . . . . . . . . . . . . 15 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛𝐹) → ({𝑛} ≠ ∅ ∧ 𝑛 ≠ ∅))
125 neanior 3034 . . . . . . . . . . . . . . 15 (({𝑛} ≠ ∅ ∧ 𝑛 ≠ ∅) ↔ ¬ ({𝑛} = ∅ ∨ 𝑛 = ∅))
126124, 125sylib 218 . . . . . . . . . . . . . 14 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛𝐹) → ¬ ({𝑛} = ∅ ∨ 𝑛 = ∅))
127 ss0b 4400 . . . . . . . . . . . . . . 15 (({𝑛} × 𝑛) ⊆ ∅ ↔ ({𝑛} × 𝑛) = ∅)
128 xpeq0 6179 . . . . . . . . . . . . . . 15 (({𝑛} × 𝑛) = ∅ ↔ ({𝑛} = ∅ ∨ 𝑛 = ∅))
129127, 128bitri 275 . . . . . . . . . . . . . 14 (({𝑛} × 𝑛) ⊆ ∅ ↔ ({𝑛} = ∅ ∨ 𝑛 = ∅))
130126, 129sylnibr 329 . . . . . . . . . . . . 13 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛𝐹) → ¬ ({𝑛} × 𝑛) ⊆ ∅)
131130ralrimiva 3145 . . . . . . . . . . . 12 (𝐹 ∈ (Fil‘𝑋) → ∀𝑛𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅)
132 r19.2z 4494 . . . . . . . . . . . 12 ((𝐹 ≠ ∅ ∧ ∀𝑛𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅) → ∃𝑛𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅)
133122, 131, 132syl2anc 584 . . . . . . . . . . 11 (𝐹 ∈ (Fil‘𝑋) → ∃𝑛𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅)
134 rexnal 3099 . . . . . . . . . . 11 (∃𝑛𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅ ↔ ¬ ∀𝑛𝐹 ({𝑛} × 𝑛) ⊆ ∅)
135133, 134sylib 218 . . . . . . . . . 10 (𝐹 ∈ (Fil‘𝑋) → ¬ ∀𝑛𝐹 ({𝑛} × 𝑛) ⊆ ∅)
1361sseq1i 4011 . . . . . . . . . . . 12 (𝐻 ⊆ ∅ ↔ 𝑛𝐹 ({𝑛} × 𝑛) ⊆ ∅)
137 ss0b 4400 . . . . . . . . . . . 12 (𝐻 ⊆ ∅ ↔ 𝐻 = ∅)
138 iunss 5044 . . . . . . . . . . . 12 ( 𝑛𝐹 ({𝑛} × 𝑛) ⊆ ∅ ↔ ∀𝑛𝐹 ({𝑛} × 𝑛) ⊆ ∅)
139136, 137, 1383bitr3i 301 . . . . . . . . . . 11 (𝐻 = ∅ ↔ ∀𝑛𝐹 ({𝑛} × 𝑛) ⊆ ∅)
140139necon3abii 2986 . . . . . . . . . 10 (𝐻 ≠ ∅ ↔ ¬ ∀𝑛𝐹 ({𝑛} × 𝑛) ⊆ ∅)
141135, 140sylibr 234 . . . . . . . . 9 (𝐹 ∈ (Fil‘𝑋) → 𝐻 ≠ ∅)
142 dmresi 6069 . . . . . . . . . . . 12 dom ( I ↾ 𝐻) = 𝐻
1431, 2filnetlem2 36381 . . . . . . . . . . . . . 14 (( I ↾ 𝐻) ⊆ 𝐷𝐷 ⊆ (𝐻 × 𝐻))
144143simpli 483 . . . . . . . . . . . . 13 ( I ↾ 𝐻) ⊆ 𝐷
145 dmss 5912 . . . . . . . . . . . . 13 (( I ↾ 𝐻) ⊆ 𝐷 → dom ( I ↾ 𝐻) ⊆ dom 𝐷)
146144, 145ax-mp 5 . . . . . . . . . . . 12 dom ( I ↾ 𝐻) ⊆ dom 𝐷
147142, 146eqsstrri 4030 . . . . . . . . . . 11 𝐻 ⊆ dom 𝐷
148143simpri 485 . . . . . . . . . . . . 13 𝐷 ⊆ (𝐻 × 𝐻)
149 dmss 5912 . . . . . . . . . . . . 13 (𝐷 ⊆ (𝐻 × 𝐻) → dom 𝐷 ⊆ dom (𝐻 × 𝐻))
150148, 149ax-mp 5 . . . . . . . . . . . 12 dom 𝐷 ⊆ dom (𝐻 × 𝐻)
151 dmxpid 5940 . . . . . . . . . . . 12 dom (𝐻 × 𝐻) = 𝐻
152150, 151sseqtri 4031 . . . . . . . . . . 11 dom 𝐷𝐻
153147, 152eqssi 3999 . . . . . . . . . 10 𝐻 = dom 𝐷
154153tailfb 36379 . . . . . . . . 9 ((𝐷 ∈ DirRel ∧ 𝐻 ≠ ∅) → ran (tail‘𝐷) ∈ (fBas‘𝐻))
1555, 141, 154syl2anc 584 . . . . . . . 8 (𝐹 ∈ (Fil‘𝑋) → ran (tail‘𝐷) ∈ (fBas‘𝐻))
156 elfm 23956 . . . . . . . 8 ((𝑋𝐹 ∧ ran (tail‘𝐷) ∈ (fBas‘𝐻) ∧ (2nd𝐻):𝐻𝑋) → (𝑡 ∈ ((𝑋 FilMap (2nd𝐻))‘ran (tail‘𝐷)) ↔ (𝑡𝑋 ∧ ∃𝑑 ∈ ran (tail‘𝐷)((2nd𝐻) “ 𝑑) ⊆ 𝑡)))
15710, 155, 9, 156syl3anc 1372 . . . . . . 7 (𝐹 ∈ (Fil‘𝑋) → (𝑡 ∈ ((𝑋 FilMap (2nd𝐻))‘ran (tail‘𝐷)) ↔ (𝑡𝑋 ∧ ∃𝑑 ∈ ran (tail‘𝐷)((2nd𝐻) “ 𝑑) ⊆ 𝑡)))
158 filfbas 23857 . . . . . . . 8 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋))
159 elfg 23880 . . . . . . . 8 (𝐹 ∈ (fBas‘𝑋) → (𝑡 ∈ (𝑋filGen𝐹) ↔ (𝑡𝑋 ∧ ∃𝑛𝐹 𝑛𝑡)))
160158, 159syl 17 . . . . . . 7 (𝐹 ∈ (Fil‘𝑋) → (𝑡 ∈ (𝑋filGen𝐹) ↔ (𝑡𝑋 ∧ ∃𝑛𝐹 𝑛𝑡)))
161121, 157, 1603bitr4d 311 . . . . . 6 (𝐹 ∈ (Fil‘𝑋) → (𝑡 ∈ ((𝑋 FilMap (2nd𝐻))‘ran (tail‘𝐷)) ↔ 𝑡 ∈ (𝑋filGen𝐹)))
162161eqrdv 2734 . . . . 5 (𝐹 ∈ (Fil‘𝑋) → ((𝑋 FilMap (2nd𝐻))‘ran (tail‘𝐷)) = (𝑋filGen𝐹))
163 fgfil 23884 . . . . 5 (𝐹 ∈ (Fil‘𝑋) → (𝑋filGen𝐹) = 𝐹)
164162, 163eqtr2d 2777 . . . 4 (𝐹 ∈ (Fil‘𝑋) → 𝐹 = ((𝑋 FilMap (2nd𝐻))‘ran (tail‘𝐷)))
16520, 164jca 511 . . 3 (𝐹 ∈ (Fil‘𝑋) → ((2nd𝐻):dom 𝐷𝑋𝐹 = ((𝑋 FilMap (2nd𝐻))‘ran (tail‘𝐷))))
166 feq1 6715 . . . . 5 (𝑓 = (2nd𝐻) → (𝑓:dom 𝐷𝑋 ↔ (2nd𝐻):dom 𝐷𝑋))
167 oveq2 7440 . . . . . . 7 (𝑓 = (2nd𝐻) → (𝑋 FilMap 𝑓) = (𝑋 FilMap (2nd𝐻)))
168167fveq1d 6907 . . . . . 6 (𝑓 = (2nd𝐻) → ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)) = ((𝑋 FilMap (2nd𝐻))‘ran (tail‘𝐷)))
169168eqeq2d 2747 . . . . 5 (𝑓 = (2nd𝐻) → (𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)) ↔ 𝐹 = ((𝑋 FilMap (2nd𝐻))‘ran (tail‘𝐷))))
170166, 169anbi12d 632 . . . 4 (𝑓 = (2nd𝐻) → ((𝑓:dom 𝐷𝑋𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷))) ↔ ((2nd𝐻):dom 𝐷𝑋𝐹 = ((𝑋 FilMap (2nd𝐻))‘ran (tail‘𝐷)))))
171170spcegv 3596 . . 3 ((2nd𝐻) ∈ V → (((2nd𝐻):dom 𝐷𝑋𝐹 = ((𝑋 FilMap (2nd𝐻))‘ran (tail‘𝐷))) → ∃𝑓(𝑓:dom 𝐷𝑋𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))))
17214, 165, 171sylc 65 . 2 (𝐹 ∈ (Fil‘𝑋) → ∃𝑓(𝑓:dom 𝐷𝑋𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷))))
173 dmeq 5913 . . . . . 6 (𝑑 = 𝐷 → dom 𝑑 = dom 𝐷)
174173feq2d 6721 . . . . 5 (𝑑 = 𝐷 → (𝑓:dom 𝑑𝑋𝑓:dom 𝐷𝑋))
175 fveq2 6905 . . . . . . . 8 (𝑑 = 𝐷 → (tail‘𝑑) = (tail‘𝐷))
176175rneqd 5948 . . . . . . 7 (𝑑 = 𝐷 → ran (tail‘𝑑) = ran (tail‘𝐷))
177176fveq2d 6909 . . . . . 6 (𝑑 = 𝐷 → ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑)) = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))
178177eqeq2d 2747 . . . . 5 (𝑑 = 𝐷 → (𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑)) ↔ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷))))
179174, 178anbi12d 632 . . . 4 (𝑑 = 𝐷 → ((𝑓:dom 𝑑𝑋𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))) ↔ (𝑓:dom 𝐷𝑋𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))))
180179exbidv 1920 . . 3 (𝑑 = 𝐷 → (∃𝑓(𝑓:dom 𝑑𝑋𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))) ↔ ∃𝑓(𝑓:dom 𝐷𝑋𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))))
181180rspcev 3621 . 2 ((𝐷 ∈ DirRel ∧ ∃𝑓(𝑓:dom 𝐷𝑋𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))) → ∃𝑑 ∈ DirRel ∃𝑓(𝑓:dom 𝑑𝑋𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))))
1825, 172, 181syl2anc 584 1 (𝐹 ∈ (Fil‘𝑋) → ∃𝑑 ∈ DirRel ∃𝑓(𝑓:dom 𝑑𝑋𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 847   = wceq 1539  wex 1778  wcel 2107  wne 2939  wral 3060  wrex 3069  Vcvv 3479  wss 3950  c0 4332  𝒫 cpw 4599  {csn 4625  cop 4631   cuni 4906   ciun 4990   class class class wbr 5142  {copab 5204   I cid 5576   × cxp 5682  dom cdm 5684  ran crn 5685  cres 5686  cima 5687  Fun wfun 6554   Fn wfn 6555  wf 6556  ontowfo 6558  cfv 6560  (class class class)co 7432  1st c1st 8013  2nd c2nd 8014  DirRelcdir 18640  tailctail 18641  fBascfbas 21353  filGencfg 21354  Filcfil 23854   FilMap cfm 23942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-rep 5278  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-iun 4992  df-br 5143  df-opab 5205  df-mpt 5225  df-id 5577  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-ov 7435  df-oprab 7436  df-mpo 7437  df-1st 8015  df-2nd 8016  df-dir 18642  df-tail 18643  df-fbas 21362  df-fg 21363  df-fil 23855  df-fm 23947
This theorem is referenced by:  filnet  36384
  Copyright terms: Public domain W3C validator