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 35993
Description: Lemma for filnet 35994. (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 35992 . . . 4 (𝐻 = 𝐷 ∧ (𝐹 ∈ (Fil‘𝑋) → (𝐻 ⊆ (𝐹 × 𝑋) ∧ 𝐷 ∈ DirRel)))
43simpri 484 . . 3 (𝐹 ∈ (Fil‘𝑋) → (𝐻 ⊆ (𝐹 × 𝑋) ∧ 𝐷 ∈ DirRel))
54simprd 494 . 2 (𝐹 ∈ (Fil‘𝑋) → 𝐷 ∈ DirRel)
6 f2ndres 8019 . . . . 5 (2nd ↾ (𝐹 × 𝑋)):(𝐹 × 𝑋)⟶𝑋
74simpld 493 . . . . 5 (𝐹 ∈ (Fil‘𝑋) → 𝐻 ⊆ (𝐹 × 𝑋))
8 fssres2 6765 . . . . 5 (((2nd ↾ (𝐹 × 𝑋)):(𝐹 × 𝑋)⟶𝑋𝐻 ⊆ (𝐹 × 𝑋)) → (2nd𝐻):𝐻𝑋)
96, 7, 8sylancr 585 . . . 4 (𝐹 ∈ (Fil‘𝑋) → (2nd𝐻):𝐻𝑋)
10 filtop 23803 . . . . . 6 (𝐹 ∈ (Fil‘𝑋) → 𝑋𝐹)
11 xpexg 7753 . . . . . 6 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑋𝐹) → (𝐹 × 𝑋) ∈ V)
1210, 11mpdan 685 . . . . 5 (𝐹 ∈ (Fil‘𝑋) → (𝐹 × 𝑋) ∈ V)
1312, 7ssexd 5325 . . . 4 (𝐹 ∈ (Fil‘𝑋) → 𝐻 ∈ V)
149, 13fexd 7239 . . 3 (𝐹 ∈ (Fil‘𝑋) → (2nd𝐻) ∈ V)
153simpli 482 . . . . . . 7 𝐻 = 𝐷
16 dirdm 18595 . . . . . . . 8 (𝐷 ∈ DirRel → dom 𝐷 = 𝐷)
175, 16syl 17 . . . . . . 7 (𝐹 ∈ (Fil‘𝑋) → dom 𝐷 = 𝐷)
1815, 17eqtr4id 2784 . . . . . 6 (𝐹 ∈ (Fil‘𝑋) → 𝐻 = dom 𝐷)
1918feq2d 6709 . . . . 5 (𝐹 ∈ (Fil‘𝑋) → ((2nd𝐻):𝐻𝑋 ↔ (2nd𝐻):dom 𝐷𝑋))
209, 19mpbid 231 . . . 4 (𝐹 ∈ (Fil‘𝑋) → (2nd𝐻):dom 𝐷𝑋)
21 eqid 2725 . . . . . . . . . . . . . 14 dom 𝐷 = dom 𝐷
2221tailf 35987 . . . . . . . . . . . . 13 (𝐷 ∈ DirRel → (tail‘𝐷):dom 𝐷⟶𝒫 dom 𝐷)
235, 22syl 17 . . . . . . . . . . . 12 (𝐹 ∈ (Fil‘𝑋) → (tail‘𝐷):dom 𝐷⟶𝒫 dom 𝐷)
2418feq2d 6709 . . . . . . . . . . . 12 (𝐹 ∈ (Fil‘𝑋) → ((tail‘𝐷):𝐻⟶𝒫 dom 𝐷 ↔ (tail‘𝐷):dom 𝐷⟶𝒫 dom 𝐷))
2523, 24mpbird 256 . . . . . . . . . . 11 (𝐹 ∈ (Fil‘𝑋) → (tail‘𝐷):𝐻⟶𝒫 dom 𝐷)
2625adantr 479 . . . . . . . . . 10 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) → (tail‘𝐷):𝐻⟶𝒫 dom 𝐷)
27 ffn 6723 . . . . . . . . . 10 ((tail‘𝐷):𝐻⟶𝒫 dom 𝐷 → (tail‘𝐷) Fn 𝐻)
28 imaeq2 6060 . . . . . . . . . . . 12 (𝑑 = ((tail‘𝐷)‘𝑓) → ((2nd𝐻) “ 𝑑) = ((2nd𝐻) “ ((tail‘𝐷)‘𝑓)))
2928sseq1d 4008 . . . . . . . . . . 11 (𝑑 = ((tail‘𝐷)‘𝑓) → (((2nd𝐻) “ 𝑑) ⊆ 𝑡 ↔ ((2nd𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡))
3029rexrn 7096 . . . . . . . . . 10 ((tail‘𝐷) Fn 𝐻 → (∃𝑑 ∈ ran (tail‘𝐷)((2nd𝐻) “ 𝑑) ⊆ 𝑡 ↔ ∃𝑓𝐻 ((2nd𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡))
3126, 27, 303syl 18 . . . . . . . . 9 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) → (∃𝑑 ∈ ran (tail‘𝐷)((2nd𝐻) “ 𝑑) ⊆ 𝑡 ↔ ∃𝑓𝐻 ((2nd𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡))
32 fo2nd 8015 . . . . . . . . . . . . . . 15 2nd :V–onto→V
33 fofn 6812 . . . . . . . . . . . . . . 15 (2nd :V–onto→V → 2nd Fn V)
3432, 33ax-mp 5 . . . . . . . . . . . . . 14 2nd Fn V
35 ssv 4001 . . . . . . . . . . . . . 14 𝐻 ⊆ V
36 fnssres 6679 . . . . . . . . . . . . . 14 ((2nd Fn V ∧ 𝐻 ⊆ V) → (2nd𝐻) Fn 𝐻)
3734, 35, 36mp2an 690 . . . . . . . . . . . . 13 (2nd𝐻) Fn 𝐻
38 fnfun 6655 . . . . . . . . . . . . 13 ((2nd𝐻) Fn 𝐻 → Fun (2nd𝐻))
3937, 38ax-mp 5 . . . . . . . . . . . 12 Fun (2nd𝐻)
4026ffvelcdmda 7093 . . . . . . . . . . . . . . 15 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → ((tail‘𝐷)‘𝑓) ∈ 𝒫 dom 𝐷)
4140elpwid 4613 . . . . . . . . . . . . . 14 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → ((tail‘𝐷)‘𝑓) ⊆ dom 𝐷)
4218ad2antrr 724 . . . . . . . . . . . . . 14 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → 𝐻 = dom 𝐷)
4341, 42sseqtrrd 4018 . . . . . . . . . . . . 13 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → ((tail‘𝐷)‘𝑓) ⊆ 𝐻)
4437fndmi 6659 . . . . . . . . . . . . 13 dom (2nd𝐻) = 𝐻
4543, 44sseqtrrdi 4028 . . . . . . . . . . . 12 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → ((tail‘𝐷)‘𝑓) ⊆ dom (2nd𝐻))
46 funimass4 6962 . . . . . . . . . . . 12 ((Fun (2nd𝐻) ∧ ((tail‘𝐷)‘𝑓) ⊆ dom (2nd𝐻)) → (((2nd𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∀𝑑 ∈ ((tail‘𝐷)‘𝑓)((2nd𝐻)‘𝑑) ∈ 𝑡))
4739, 45, 46sylancr 585 . . . . . . . . . . 11 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → (((2nd𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∀𝑑 ∈ ((tail‘𝐷)‘𝑓)((2nd𝐻)‘𝑑) ∈ 𝑡))
485ad2antrr 724 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → 𝐷 ∈ DirRel)
49 simpr 483 . . . . . . . . . . . . . . . . 17 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → 𝑓𝐻)
5049, 42eleqtrd 2827 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → 𝑓 ∈ dom 𝐷)
51 vex 3465 . . . . . . . . . . . . . . . . 17 𝑑 ∈ V
5251a1i 11 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → 𝑑 ∈ V)
5321eltail 35986 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ DirRel ∧ 𝑓 ∈ dom 𝐷𝑑 ∈ V) → (𝑑 ∈ ((tail‘𝐷)‘𝑓) ↔ 𝑓𝐷𝑑))
5448, 50, 52, 53syl3anc 1368 . . . . . . . . . . . . . . 15 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → (𝑑 ∈ ((tail‘𝐷)‘𝑓) ↔ 𝑓𝐷𝑑))
5549biantrurd 531 . . . . . . . . . . . . . . . . 17 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → (𝑑𝐻 ↔ (𝑓𝐻𝑑𝐻)))
5655anbi1d 629 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → ((𝑑𝐻 ∧ (1st𝑑) ⊆ (1st𝑓)) ↔ ((𝑓𝐻𝑑𝐻) ∧ (1st𝑑) ⊆ (1st𝑓))))
57 vex 3465 . . . . . . . . . . . . . . . . 17 𝑓 ∈ V
581, 2, 57, 51filnetlem1 35990 . . . . . . . . . . . . . . . 16 (𝑓𝐷𝑑 ↔ ((𝑓𝐻𝑑𝐻) ∧ (1st𝑑) ⊆ (1st𝑓)))
5956, 58bitr4di 288 . . . . . . . . . . . . . . 15 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → ((𝑑𝐻 ∧ (1st𝑑) ⊆ (1st𝑓)) ↔ 𝑓𝐷𝑑))
6054, 59bitr4d 281 . . . . . . . . . . . . . 14 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → (𝑑 ∈ ((tail‘𝐷)‘𝑓) ↔ (𝑑𝐻 ∧ (1st𝑑) ⊆ (1st𝑓))))
6160imbi1d 340 . . . . . . . . . . . . 13 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → ((𝑑 ∈ ((tail‘𝐷)‘𝑓) → ((2nd𝐻)‘𝑑) ∈ 𝑡) ↔ ((𝑑𝐻 ∧ (1st𝑑) ⊆ (1st𝑓)) → ((2nd𝐻)‘𝑑) ∈ 𝑡)))
62 fvres 6915 . . . . . . . . . . . . . . . . 17 (𝑑𝐻 → ((2nd𝐻)‘𝑑) = (2nd𝑑))
6362eleq1d 2810 . . . . . . . . . . . . . . . 16 (𝑑𝐻 → (((2nd𝐻)‘𝑑) ∈ 𝑡 ↔ (2nd𝑑) ∈ 𝑡))
6463adantr 479 . . . . . . . . . . . . . . 15 ((𝑑𝐻 ∧ (1st𝑑) ⊆ (1st𝑓)) → (((2nd𝐻)‘𝑑) ∈ 𝑡 ↔ (2nd𝑑) ∈ 𝑡))
6564pm5.74i 270 . . . . . . . . . . . . . 14 (((𝑑𝐻 ∧ (1st𝑑) ⊆ (1st𝑓)) → ((2nd𝐻)‘𝑑) ∈ 𝑡) ↔ ((𝑑𝐻 ∧ (1st𝑑) ⊆ (1st𝑓)) → (2nd𝑑) ∈ 𝑡))
66 impexp 449 . . . . . . . . . . . . . 14 (((𝑑𝐻 ∧ (1st𝑑) ⊆ (1st𝑓)) → (2nd𝑑) ∈ 𝑡) ↔ (𝑑𝐻 → ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡)))
6765, 66bitri 274 . . . . . . . . . . . . 13 (((𝑑𝐻 ∧ (1st𝑑) ⊆ (1st𝑓)) → ((2nd𝐻)‘𝑑) ∈ 𝑡) ↔ (𝑑𝐻 → ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡)))
6861, 67bitrdi 286 . . . . . . . . . . . 12 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → ((𝑑 ∈ ((tail‘𝐷)‘𝑓) → ((2nd𝐻)‘𝑑) ∈ 𝑡) ↔ (𝑑𝐻 → ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡))))
6968ralbidv2 3163 . . . . . . . . . . 11 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → (∀𝑑 ∈ ((tail‘𝐷)‘𝑓)((2nd𝐻)‘𝑑) ∈ 𝑡 ↔ ∀𝑑𝐻 ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡)))
7047, 69bitrd 278 . . . . . . . . . 10 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → (((2nd𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∀𝑑𝐻 ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡)))
7170rexbidva 3166 . . . . . . . . 9 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) → (∃𝑓𝐻 ((2nd𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∃𝑓𝐻𝑑𝐻 ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡)))
72 vex 3465 . . . . . . . . . . . . . . . . 17 𝑘 ∈ V
73 vex 3465 . . . . . . . . . . . . . . . . 17 𝑣 ∈ V
7472, 73op1std 8004 . . . . . . . . . . . . . . . 16 (𝑑 = ⟨𝑘, 𝑣⟩ → (1st𝑑) = 𝑘)
7574sseq1d 4008 . . . . . . . . . . . . . . 15 (𝑑 = ⟨𝑘, 𝑣⟩ → ((1st𝑑) ⊆ (1st𝑓) ↔ 𝑘 ⊆ (1st𝑓)))
7672, 73op2ndd 8005 . . . . . . . . . . . . . . . 16 (𝑑 = ⟨𝑘, 𝑣⟩ → (2nd𝑑) = 𝑣)
7776eleq1d 2810 . . . . . . . . . . . . . . 15 (𝑑 = ⟨𝑘, 𝑣⟩ → ((2nd𝑑) ∈ 𝑡𝑣𝑡))
7875, 77imbi12d 343 . . . . . . . . . . . . . 14 (𝑑 = ⟨𝑘, 𝑣⟩ → (((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡) ↔ (𝑘 ⊆ (1st𝑓) → 𝑣𝑡)))
7978raliunxp 5842 . . . . . . . . . . . . 13 (∀𝑑 𝑘𝐹 ({𝑘} × 𝑘)((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡) ↔ ∀𝑘𝐹𝑣𝑘 (𝑘 ⊆ (1st𝑓) → 𝑣𝑡))
80 sneq 4640 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑘 → {𝑛} = {𝑘})
81 id 22 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑘𝑛 = 𝑘)
8280, 81xpeq12d 5709 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑘 → ({𝑛} × 𝑛) = ({𝑘} × 𝑘))
8382cbviunv 5044 . . . . . . . . . . . . . . 15 𝑛𝐹 ({𝑛} × 𝑛) = 𝑘𝐹 ({𝑘} × 𝑘)
841, 83eqtri 2753 . . . . . . . . . . . . . 14 𝐻 = 𝑘𝐹 ({𝑘} × 𝑘)
8584raleqi 3312 . . . . . . . . . . . . 13 (∀𝑑𝐻 ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡) ↔ ∀𝑑 𝑘𝐹 ({𝑘} × 𝑘)((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡))
86 dfss3 3965 . . . . . . . . . . . . . . . 16 (𝑘𝑡 ↔ ∀𝑣𝑘 𝑣𝑡)
8786imbi2i 335 . . . . . . . . . . . . . . 15 ((𝑘 ⊆ (1st𝑓) → 𝑘𝑡) ↔ (𝑘 ⊆ (1st𝑓) → ∀𝑣𝑘 𝑣𝑡))
88 r19.21v 3169 . . . . . . . . . . . . . . 15 (∀𝑣𝑘 (𝑘 ⊆ (1st𝑓) → 𝑣𝑡) ↔ (𝑘 ⊆ (1st𝑓) → ∀𝑣𝑘 𝑣𝑡))
8987, 88bitr4i 277 . . . . . . . . . . . . . 14 ((𝑘 ⊆ (1st𝑓) → 𝑘𝑡) ↔ ∀𝑣𝑘 (𝑘 ⊆ (1st𝑓) → 𝑣𝑡))
9089ralbii 3082 . . . . . . . . . . . . 13 (∀𝑘𝐹 (𝑘 ⊆ (1st𝑓) → 𝑘𝑡) ↔ ∀𝑘𝐹𝑣𝑘 (𝑘 ⊆ (1st𝑓) → 𝑣𝑡))
9179, 85, 903bitr4i 302 . . . . . . . . . . . 12 (∀𝑑𝐻 ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡) ↔ ∀𝑘𝐹 (𝑘 ⊆ (1st𝑓) → 𝑘𝑡))
9291rexbii 3083 . . . . . . . . . . 11 (∃𝑓𝐻𝑑𝐻 ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡) ↔ ∃𝑓𝐻𝑘𝐹 (𝑘 ⊆ (1st𝑓) → 𝑘𝑡))
931rexeqi 3313 . . . . . . . . . . 11 (∃𝑓𝐻𝑘𝐹 (𝑘 ⊆ (1st𝑓) → 𝑘𝑡) ↔ ∃𝑓 𝑛𝐹 ({𝑛} × 𝑛)∀𝑘𝐹 (𝑘 ⊆ (1st𝑓) → 𝑘𝑡))
94 vex 3465 . . . . . . . . . . . . . . . 16 𝑛 ∈ V
95 vex 3465 . . . . . . . . . . . . . . . 16 𝑚 ∈ V
9694, 95op1std 8004 . . . . . . . . . . . . . . 15 (𝑓 = ⟨𝑛, 𝑚⟩ → (1st𝑓) = 𝑛)
9796sseq2d 4009 . . . . . . . . . . . . . 14 (𝑓 = ⟨𝑛, 𝑚⟩ → (𝑘 ⊆ (1st𝑓) ↔ 𝑘𝑛))
9897imbi1d 340 . . . . . . . . . . . . 13 (𝑓 = ⟨𝑛, 𝑚⟩ → ((𝑘 ⊆ (1st𝑓) → 𝑘𝑡) ↔ (𝑘𝑛𝑘𝑡)))
9998ralbidv 3167 . . . . . . . . . . . 12 (𝑓 = ⟨𝑛, 𝑚⟩ → (∀𝑘𝐹 (𝑘 ⊆ (1st𝑓) → 𝑘𝑡) ↔ ∀𝑘𝐹 (𝑘𝑛𝑘𝑡)))
10099rexiunxp 5843 . . . . . . . . . . 11 (∃𝑓 𝑛𝐹 ({𝑛} × 𝑛)∀𝑘𝐹 (𝑘 ⊆ (1st𝑓) → 𝑘𝑡) ↔ ∃𝑛𝐹𝑚𝑛𝑘𝐹 (𝑘𝑛𝑘𝑡))
10192, 93, 1003bitri 296 . . . . . . . . . 10 (∃𝑓𝐻𝑑𝐻 ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡) ↔ ∃𝑛𝐹𝑚𝑛𝑘𝐹 (𝑘𝑛𝑘𝑡))
102 fileln0 23798 . . . . . . . . . . . . . 14 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛𝐹) → 𝑛 ≠ ∅)
103102adantlr 713 . . . . . . . . . . . . 13 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑛𝐹) → 𝑛 ≠ ∅)
104 r19.9rzv 4501 . . . . . . . . . . . . 13 (𝑛 ≠ ∅ → (∀𝑘𝐹 (𝑘𝑛𝑘𝑡) ↔ ∃𝑚𝑛𝑘𝐹 (𝑘𝑛𝑘𝑡)))
105103, 104syl 17 . . . . . . . . . . . 12 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑛𝐹) → (∀𝑘𝐹 (𝑘𝑛𝑘𝑡) ↔ ∃𝑚𝑛𝑘𝐹 (𝑘𝑛𝑘𝑡)))
106 ssid 3999 . . . . . . . . . . . . . . 15 𝑛𝑛
107 sseq1 4002 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑛 → (𝑘𝑛𝑛𝑛))
108 sseq1 4002 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑛 → (𝑘𝑡𝑛𝑡))
109107, 108imbi12d 343 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑛 → ((𝑘𝑛𝑘𝑡) ↔ (𝑛𝑛𝑛𝑡)))
110109rspcv 3602 . . . . . . . . . . . . . . 15 (𝑛𝐹 → (∀𝑘𝐹 (𝑘𝑛𝑘𝑡) → (𝑛𝑛𝑛𝑡)))
111106, 110mpii 46 . . . . . . . . . . . . . 14 (𝑛𝐹 → (∀𝑘𝐹 (𝑘𝑛𝑘𝑡) → 𝑛𝑡))
112111adantl 480 . . . . . . . . . . . . 13 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑛𝐹) → (∀𝑘𝐹 (𝑘𝑛𝑘𝑡) → 𝑛𝑡))
113 sstr2 3983 . . . . . . . . . . . . . . 15 (𝑘𝑛 → (𝑛𝑡𝑘𝑡))
114113com12 32 . . . . . . . . . . . . . 14 (𝑛𝑡 → (𝑘𝑛𝑘𝑡))
115114ralrimivw 3139 . . . . . . . . . . . . 13 (𝑛𝑡 → ∀𝑘𝐹 (𝑘𝑛𝑘𝑡))
116112, 115impbid1 224 . . . . . . . . . . . 12 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑛𝐹) → (∀𝑘𝐹 (𝑘𝑛𝑘𝑡) ↔ 𝑛𝑡))
117105, 116bitr3d 280 . . . . . . . . . . 11 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑛𝐹) → (∃𝑚𝑛𝑘𝐹 (𝑘𝑛𝑘𝑡) ↔ 𝑛𝑡))
118117rexbidva 3166 . . . . . . . . . 10 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) → (∃𝑛𝐹𝑚𝑛𝑘𝐹 (𝑘𝑛𝑘𝑡) ↔ ∃𝑛𝐹 𝑛𝑡))
119101, 118bitrid 282 . . . . . . . . 9 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) → (∃𝑓𝐻𝑑𝐻 ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡) ↔ ∃𝑛𝐹 𝑛𝑡))
12031, 71, 1193bitrd 304 . . . . . . . 8 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) → (∃𝑑 ∈ ran (tail‘𝐷)((2nd𝐻) “ 𝑑) ⊆ 𝑡 ↔ ∃𝑛𝐹 𝑛𝑡))
121120pm5.32da 577 . . . . . . 7 (𝐹 ∈ (Fil‘𝑋) → ((𝑡𝑋 ∧ ∃𝑑 ∈ ran (tail‘𝐷)((2nd𝐻) “ 𝑑) ⊆ 𝑡) ↔ (𝑡𝑋 ∧ ∃𝑛𝐹 𝑛𝑡)))
122 filn0 23810 . . . . . . . . . . . 12 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ≠ ∅)
12394snnz 4782 . . . . . . . . . . . . . . . 16 {𝑛} ≠ ∅
124102, 123jctil 518 . . . . . . . . . . . . . . 15 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛𝐹) → ({𝑛} ≠ ∅ ∧ 𝑛 ≠ ∅))
125 neanior 3024 . . . . . . . . . . . . . . 15 (({𝑛} ≠ ∅ ∧ 𝑛 ≠ ∅) ↔ ¬ ({𝑛} = ∅ ∨ 𝑛 = ∅))
126124, 125sylib 217 . . . . . . . . . . . . . 14 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛𝐹) → ¬ ({𝑛} = ∅ ∨ 𝑛 = ∅))
127 ss0b 4399 . . . . . . . . . . . . . . 15 (({𝑛} × 𝑛) ⊆ ∅ ↔ ({𝑛} × 𝑛) = ∅)
128 xpeq0 6166 . . . . . . . . . . . . . . 15 (({𝑛} × 𝑛) = ∅ ↔ ({𝑛} = ∅ ∨ 𝑛 = ∅))
129127, 128bitri 274 . . . . . . . . . . . . . 14 (({𝑛} × 𝑛) ⊆ ∅ ↔ ({𝑛} = ∅ ∨ 𝑛 = ∅))
130126, 129sylnibr 328 . . . . . . . . . . . . 13 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛𝐹) → ¬ ({𝑛} × 𝑛) ⊆ ∅)
131130ralrimiva 3135 . . . . . . . . . . . 12 (𝐹 ∈ (Fil‘𝑋) → ∀𝑛𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅)
132 r19.2z 4496 . . . . . . . . . . . 12 ((𝐹 ≠ ∅ ∧ ∀𝑛𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅) → ∃𝑛𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅)
133122, 131, 132syl2anc 582 . . . . . . . . . . 11 (𝐹 ∈ (Fil‘𝑋) → ∃𝑛𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅)
134 rexnal 3089 . . . . . . . . . . 11 (∃𝑛𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅ ↔ ¬ ∀𝑛𝐹 ({𝑛} × 𝑛) ⊆ ∅)
135133, 134sylib 217 . . . . . . . . . 10 (𝐹 ∈ (Fil‘𝑋) → ¬ ∀𝑛𝐹 ({𝑛} × 𝑛) ⊆ ∅)
1361sseq1i 4005 . . . . . . . . . . . 12 (𝐻 ⊆ ∅ ↔ 𝑛𝐹 ({𝑛} × 𝑛) ⊆ ∅)
137 ss0b 4399 . . . . . . . . . . . 12 (𝐻 ⊆ ∅ ↔ 𝐻 = ∅)
138 iunss 5049 . . . . . . . . . . . 12 ( 𝑛𝐹 ({𝑛} × 𝑛) ⊆ ∅ ↔ ∀𝑛𝐹 ({𝑛} × 𝑛) ⊆ ∅)
139136, 137, 1383bitr3i 300 . . . . . . . . . . 11 (𝐻 = ∅ ↔ ∀𝑛𝐹 ({𝑛} × 𝑛) ⊆ ∅)
140139necon3abii 2976 . . . . . . . . . 10 (𝐻 ≠ ∅ ↔ ¬ ∀𝑛𝐹 ({𝑛} × 𝑛) ⊆ ∅)
141135, 140sylibr 233 . . . . . . . . 9 (𝐹 ∈ (Fil‘𝑋) → 𝐻 ≠ ∅)
142 dmresi 6056 . . . . . . . . . . . 12 dom ( I ↾ 𝐻) = 𝐻
1431, 2filnetlem2 35991 . . . . . . . . . . . . . 14 (( I ↾ 𝐻) ⊆ 𝐷𝐷 ⊆ (𝐻 × 𝐻))
144143simpli 482 . . . . . . . . . . . . 13 ( I ↾ 𝐻) ⊆ 𝐷
145 dmss 5905 . . . . . . . . . . . . 13 (( I ↾ 𝐻) ⊆ 𝐷 → dom ( I ↾ 𝐻) ⊆ dom 𝐷)
146144, 145ax-mp 5 . . . . . . . . . . . 12 dom ( I ↾ 𝐻) ⊆ dom 𝐷
147142, 146eqsstrri 4012 . . . . . . . . . . 11 𝐻 ⊆ dom 𝐷
148143simpri 484 . . . . . . . . . . . . 13 𝐷 ⊆ (𝐻 × 𝐻)
149 dmss 5905 . . . . . . . . . . . . 13 (𝐷 ⊆ (𝐻 × 𝐻) → dom 𝐷 ⊆ dom (𝐻 × 𝐻))
150148, 149ax-mp 5 . . . . . . . . . . . 12 dom 𝐷 ⊆ dom (𝐻 × 𝐻)
151 dmxpid 5932 . . . . . . . . . . . 12 dom (𝐻 × 𝐻) = 𝐻
152150, 151sseqtri 4013 . . . . . . . . . . 11 dom 𝐷𝐻
153147, 152eqssi 3993 . . . . . . . . . 10 𝐻 = dom 𝐷
154153tailfb 35989 . . . . . . . . 9 ((𝐷 ∈ DirRel ∧ 𝐻 ≠ ∅) → ran (tail‘𝐷) ∈ (fBas‘𝐻))
1555, 141, 154syl2anc 582 . . . . . . . 8 (𝐹 ∈ (Fil‘𝑋) → ran (tail‘𝐷) ∈ (fBas‘𝐻))
156 elfm 23895 . . . . . . . 8 ((𝑋𝐹 ∧ ran (tail‘𝐷) ∈ (fBas‘𝐻) ∧ (2nd𝐻):𝐻𝑋) → (𝑡 ∈ ((𝑋 FilMap (2nd𝐻))‘ran (tail‘𝐷)) ↔ (𝑡𝑋 ∧ ∃𝑑 ∈ ran (tail‘𝐷)((2nd𝐻) “ 𝑑) ⊆ 𝑡)))
15710, 155, 9, 156syl3anc 1368 . . . . . . 7 (𝐹 ∈ (Fil‘𝑋) → (𝑡 ∈ ((𝑋 FilMap (2nd𝐻))‘ran (tail‘𝐷)) ↔ (𝑡𝑋 ∧ ∃𝑑 ∈ ran (tail‘𝐷)((2nd𝐻) “ 𝑑) ⊆ 𝑡)))
158 filfbas 23796 . . . . . . . 8 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋))
159 elfg 23819 . . . . . . . 8 (𝐹 ∈ (fBas‘𝑋) → (𝑡 ∈ (𝑋filGen𝐹) ↔ (𝑡𝑋 ∧ ∃𝑛𝐹 𝑛𝑡)))
160158, 159syl 17 . . . . . . 7 (𝐹 ∈ (Fil‘𝑋) → (𝑡 ∈ (𝑋filGen𝐹) ↔ (𝑡𝑋 ∧ ∃𝑛𝐹 𝑛𝑡)))
161121, 157, 1603bitr4d 310 . . . . . 6 (𝐹 ∈ (Fil‘𝑋) → (𝑡 ∈ ((𝑋 FilMap (2nd𝐻))‘ran (tail‘𝐷)) ↔ 𝑡 ∈ (𝑋filGen𝐹)))
162161eqrdv 2723 . . . . 5 (𝐹 ∈ (Fil‘𝑋) → ((𝑋 FilMap (2nd𝐻))‘ran (tail‘𝐷)) = (𝑋filGen𝐹))
163 fgfil 23823 . . . . 5 (𝐹 ∈ (Fil‘𝑋) → (𝑋filGen𝐹) = 𝐹)
164162, 163eqtr2d 2766 . . . 4 (𝐹 ∈ (Fil‘𝑋) → 𝐹 = ((𝑋 FilMap (2nd𝐻))‘ran (tail‘𝐷)))
16520, 164jca 510 . . 3 (𝐹 ∈ (Fil‘𝑋) → ((2nd𝐻):dom 𝐷𝑋𝐹 = ((𝑋 FilMap (2nd𝐻))‘ran (tail‘𝐷))))
166 feq1 6704 . . . . 5 (𝑓 = (2nd𝐻) → (𝑓:dom 𝐷𝑋 ↔ (2nd𝐻):dom 𝐷𝑋))
167 oveq2 7427 . . . . . . 7 (𝑓 = (2nd𝐻) → (𝑋 FilMap 𝑓) = (𝑋 FilMap (2nd𝐻)))
168167fveq1d 6898 . . . . . 6 (𝑓 = (2nd𝐻) → ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)) = ((𝑋 FilMap (2nd𝐻))‘ran (tail‘𝐷)))
169168eqeq2d 2736 . . . . 5 (𝑓 = (2nd𝐻) → (𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)) ↔ 𝐹 = ((𝑋 FilMap (2nd𝐻))‘ran (tail‘𝐷))))
170166, 169anbi12d 630 . . . 4 (𝑓 = (2nd𝐻) → ((𝑓:dom 𝐷𝑋𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷))) ↔ ((2nd𝐻):dom 𝐷𝑋𝐹 = ((𝑋 FilMap (2nd𝐻))‘ran (tail‘𝐷)))))
171170spcegv 3581 . . 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 5906 . . . . . 6 (𝑑 = 𝐷 → dom 𝑑 = dom 𝐷)
174173feq2d 6709 . . . . 5 (𝑑 = 𝐷 → (𝑓:dom 𝑑𝑋𝑓:dom 𝐷𝑋))
175 fveq2 6896 . . . . . . . 8 (𝑑 = 𝐷 → (tail‘𝑑) = (tail‘𝐷))
176175rneqd 5940 . . . . . . 7 (𝑑 = 𝐷 → ran (tail‘𝑑) = ran (tail‘𝐷))
177176fveq2d 6900 . . . . . 6 (𝑑 = 𝐷 → ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑)) = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))
178177eqeq2d 2736 . . . . 5 (𝑑 = 𝐷 → (𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑)) ↔ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷))))
179174, 178anbi12d 630 . . . 4 (𝑑 = 𝐷 → ((𝑓:dom 𝑑𝑋𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))) ↔ (𝑓:dom 𝐷𝑋𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))))
180179exbidv 1916 . . 3 (𝑑 = 𝐷 → (∃𝑓(𝑓:dom 𝑑𝑋𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))) ↔ ∃𝑓(𝑓:dom 𝐷𝑋𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))))
181180rspcev 3606 . 2 ((𝐷 ∈ DirRel ∧ ∃𝑓(𝑓:dom 𝐷𝑋𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))) → ∃𝑑 ∈ DirRel ∃𝑓(𝑓:dom 𝑑𝑋𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))))
1825, 172, 181syl2anc 582 1 (𝐹 ∈ (Fil‘𝑋) → ∃𝑑 ∈ DirRel ∃𝑓(𝑓:dom 𝑑𝑋𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394  wo 845   = wceq 1533  wex 1773  wcel 2098  wne 2929  wral 3050  wrex 3059  Vcvv 3461  wss 3944  c0 4322  𝒫 cpw 4604  {csn 4630  cop 4636   cuni 4909   ciun 4997   class class class wbr 5149  {copab 5211   I cid 5575   × cxp 5676  dom cdm 5678  ran crn 5679  cres 5680  cima 5681  Fun wfun 6543   Fn wfn 6544  wf 6545  ontowfo 6547  cfv 6549  (class class class)co 7419  1st c1st 7992  2nd c2nd 7993  DirRelcdir 18589  tailctail 18590  fBascfbas 21284  filGencfg 21285  Filcfil 23793   FilMap cfm 23881
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-iun 4999  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5576  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-ov 7422  df-oprab 7423  df-mpo 7424  df-1st 7994  df-2nd 7995  df-dir 18591  df-tail 18592  df-fbas 21293  df-fg 21294  df-fil 23794  df-fm 23886
This theorem is referenced by:  filnet  35994
  Copyright terms: Public domain W3C validator