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 32964
Description: Lemma for filnet 32965. (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 32963 . . . 4 (𝐻 = 𝐷 ∧ (𝐹 ∈ (Fil‘𝑋) → (𝐻 ⊆ (𝐹 × 𝑋) ∧ 𝐷 ∈ DirRel)))
43simpri 481 . . 3 (𝐹 ∈ (Fil‘𝑋) → (𝐻 ⊆ (𝐹 × 𝑋) ∧ 𝐷 ∈ DirRel))
54simprd 491 . 2 (𝐹 ∈ (Fil‘𝑋) → 𝐷 ∈ DirRel)
6 f2ndres 7470 . . . . 5 (2nd ↾ (𝐹 × 𝑋)):(𝐹 × 𝑋)⟶𝑋
74simpld 490 . . . . 5 (𝐹 ∈ (Fil‘𝑋) → 𝐻 ⊆ (𝐹 × 𝑋))
8 fssres2 6322 . . . . 5 (((2nd ↾ (𝐹 × 𝑋)):(𝐹 × 𝑋)⟶𝑋𝐻 ⊆ (𝐹 × 𝑋)) → (2nd𝐻):𝐻𝑋)
96, 7, 8sylancr 581 . . . 4 (𝐹 ∈ (Fil‘𝑋) → (2nd𝐻):𝐻𝑋)
10 filtop 22067 . . . . . 6 (𝐹 ∈ (Fil‘𝑋) → 𝑋𝐹)
11 xpexg 7237 . . . . . 6 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑋𝐹) → (𝐹 × 𝑋) ∈ V)
1210, 11mpdan 677 . . . . 5 (𝐹 ∈ (Fil‘𝑋) → (𝐹 × 𝑋) ∈ V)
1312, 7ssexd 5042 . . . 4 (𝐹 ∈ (Fil‘𝑋) → 𝐻 ∈ V)
14 fex 6761 . . . 4 (((2nd𝐻):𝐻𝑋𝐻 ∈ V) → (2nd𝐻) ∈ V)
159, 13, 14syl2anc 579 . . 3 (𝐹 ∈ (Fil‘𝑋) → (2nd𝐻) ∈ V)
16 dirdm 17620 . . . . . . . 8 (𝐷 ∈ DirRel → dom 𝐷 = 𝐷)
175, 16syl 17 . . . . . . 7 (𝐹 ∈ (Fil‘𝑋) → dom 𝐷 = 𝐷)
183simpli 478 . . . . . . 7 𝐻 = 𝐷
1917, 18syl6reqr 2833 . . . . . 6 (𝐹 ∈ (Fil‘𝑋) → 𝐻 = dom 𝐷)
2019feq2d 6277 . . . . 5 (𝐹 ∈ (Fil‘𝑋) → ((2nd𝐻):𝐻𝑋 ↔ (2nd𝐻):dom 𝐷𝑋))
219, 20mpbid 224 . . . 4 (𝐹 ∈ (Fil‘𝑋) → (2nd𝐻):dom 𝐷𝑋)
22 eqid 2778 . . . . . . . . . . . . . 14 dom 𝐷 = dom 𝐷
2322tailf 32958 . . . . . . . . . . . . 13 (𝐷 ∈ DirRel → (tail‘𝐷):dom 𝐷⟶𝒫 dom 𝐷)
245, 23syl 17 . . . . . . . . . . . 12 (𝐹 ∈ (Fil‘𝑋) → (tail‘𝐷):dom 𝐷⟶𝒫 dom 𝐷)
2519feq2d 6277 . . . . . . . . . . . 12 (𝐹 ∈ (Fil‘𝑋) → ((tail‘𝐷):𝐻⟶𝒫 dom 𝐷 ↔ (tail‘𝐷):dom 𝐷⟶𝒫 dom 𝐷))
2624, 25mpbird 249 . . . . . . . . . . 11 (𝐹 ∈ (Fil‘𝑋) → (tail‘𝐷):𝐻⟶𝒫 dom 𝐷)
2726adantr 474 . . . . . . . . . 10 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) → (tail‘𝐷):𝐻⟶𝒫 dom 𝐷)
28 ffn 6291 . . . . . . . . . 10 ((tail‘𝐷):𝐻⟶𝒫 dom 𝐷 → (tail‘𝐷) Fn 𝐻)
29 imaeq2 5716 . . . . . . . . . . . 12 (𝑑 = ((tail‘𝐷)‘𝑓) → ((2nd𝐻) “ 𝑑) = ((2nd𝐻) “ ((tail‘𝐷)‘𝑓)))
3029sseq1d 3851 . . . . . . . . . . 11 (𝑑 = ((tail‘𝐷)‘𝑓) → (((2nd𝐻) “ 𝑑) ⊆ 𝑡 ↔ ((2nd𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡))
3130rexrn 6625 . . . . . . . . . 10 ((tail‘𝐷) Fn 𝐻 → (∃𝑑 ∈ ran (tail‘𝐷)((2nd𝐻) “ 𝑑) ⊆ 𝑡 ↔ ∃𝑓𝐻 ((2nd𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡))
3227, 28, 313syl 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)
3533, 34ax-mp 5 . . . . . . . . . . . . . 14 2nd Fn V
36 ssv 3844 . . . . . . . . . . . . . 14 𝐻 ⊆ V
37 fnssres 6250 . . . . . . . . . . . . . 14 ((2nd Fn V ∧ 𝐻 ⊆ V) → (2nd𝐻) Fn 𝐻)
3835, 36, 37mp2an 682 . . . . . . . . . . . . 13 (2nd𝐻) Fn 𝐻
39 fnfun 6233 . . . . . . . . . . . . 13 ((2nd𝐻) Fn 𝐻 → Fun (2nd𝐻))
4038, 39ax-mp 5 . . . . . . . . . . . 12 Fun (2nd𝐻)
4127ffvelrnda 6623 . . . . . . . . . . . . . . 15 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → ((tail‘𝐷)‘𝑓) ∈ 𝒫 dom 𝐷)
4241elpwid 4391 . . . . . . . . . . . . . 14 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → ((tail‘𝐷)‘𝑓) ⊆ dom 𝐷)
4319ad2antrr 716 . . . . . . . . . . . . . 14 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → 𝐻 = dom 𝐷)
4442, 43sseqtr4d 3861 . . . . . . . . . . . . 13 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → ((tail‘𝐷)‘𝑓) ⊆ 𝐻)
45 fndm 6235 . . . . . . . . . . . . . 14 ((2nd𝐻) Fn 𝐻 → dom (2nd𝐻) = 𝐻)
4638, 45ax-mp 5 . . . . . . . . . . . . 13 dom (2nd𝐻) = 𝐻
4744, 46syl6sseqr 3871 . . . . . . . . . . . 12 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → ((tail‘𝐷)‘𝑓) ⊆ dom (2nd𝐻))
48 funimass4 6507 . . . . . . . . . . . 12 ((Fun (2nd𝐻) ∧ ((tail‘𝐷)‘𝑓) ⊆ dom (2nd𝐻)) → (((2nd𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∀𝑑 ∈ ((tail‘𝐷)‘𝑓)((2nd𝐻)‘𝑑) ∈ 𝑡))
4940, 47, 48sylancr 581 . . . . . . . . . . 11 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → (((2nd𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∀𝑑 ∈ ((tail‘𝐷)‘𝑓)((2nd𝐻)‘𝑑) ∈ 𝑡))
505ad2antrr 716 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → 𝐷 ∈ DirRel)
51 simpr 479 . . . . . . . . . . . . . . . . 17 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → 𝑓𝐻)
5251, 43eleqtrd 2861 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → 𝑓 ∈ dom 𝐷)
53 vex 3401 . . . . . . . . . . . . . . . . 17 𝑑 ∈ V
5453a1i 11 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → 𝑑 ∈ V)
5522eltail 32957 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ DirRel ∧ 𝑓 ∈ dom 𝐷𝑑 ∈ V) → (𝑑 ∈ ((tail‘𝐷)‘𝑓) ↔ 𝑓𝐷𝑑))
5650, 52, 54, 55syl3anc 1439 . . . . . . . . . . . . . . 15 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → (𝑑 ∈ ((tail‘𝐷)‘𝑓) ↔ 𝑓𝐷𝑑))
5751biantrurd 528 . . . . . . . . . . . . . . . . 17 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → (𝑑𝐻 ↔ (𝑓𝐻𝑑𝐻)))
5857anbi1d 623 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → ((𝑑𝐻 ∧ (1st𝑑) ⊆ (1st𝑓)) ↔ ((𝑓𝐻𝑑𝐻) ∧ (1st𝑑) ⊆ (1st𝑓))))
59 vex 3401 . . . . . . . . . . . . . . . . 17 𝑓 ∈ V
601, 2, 59, 53filnetlem1 32961 . . . . . . . . . . . . . . . 16 (𝑓𝐷𝑑 ↔ ((𝑓𝐻𝑑𝐻) ∧ (1st𝑑) ⊆ (1st𝑓)))
6158, 60syl6bbr 281 . . . . . . . . . . . . . . 15 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → ((𝑑𝐻 ∧ (1st𝑑) ⊆ (1st𝑓)) ↔ 𝑓𝐷𝑑))
6256, 61bitr4d 274 . . . . . . . . . . . . . 14 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → (𝑑 ∈ ((tail‘𝐷)‘𝑓) ↔ (𝑑𝐻 ∧ (1st𝑑) ⊆ (1st𝑓))))
6362imbi1d 333 . . . . . . . . . . . . 13 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → ((𝑑 ∈ ((tail‘𝐷)‘𝑓) → ((2nd𝐻)‘𝑑) ∈ 𝑡) ↔ ((𝑑𝐻 ∧ (1st𝑑) ⊆ (1st𝑓)) → ((2nd𝐻)‘𝑑) ∈ 𝑡)))
64 fvres 6465 . . . . . . . . . . . . . . . . 17 (𝑑𝐻 → ((2nd𝐻)‘𝑑) = (2nd𝑑))
6564eleq1d 2844 . . . . . . . . . . . . . . . 16 (𝑑𝐻 → (((2nd𝐻)‘𝑑) ∈ 𝑡 ↔ (2nd𝑑) ∈ 𝑡))
6665adantr 474 . . . . . . . . . . . . . . 15 ((𝑑𝐻 ∧ (1st𝑑) ⊆ (1st𝑓)) → (((2nd𝐻)‘𝑑) ∈ 𝑡 ↔ (2nd𝑑) ∈ 𝑡))
6766pm5.74i 263 . . . . . . . . . . . . . 14 (((𝑑𝐻 ∧ (1st𝑑) ⊆ (1st𝑓)) → ((2nd𝐻)‘𝑑) ∈ 𝑡) ↔ ((𝑑𝐻 ∧ (1st𝑑) ⊆ (1st𝑓)) → (2nd𝑑) ∈ 𝑡))
68 impexp 443 . . . . . . . . . . . . . 14 (((𝑑𝐻 ∧ (1st𝑑) ⊆ (1st𝑓)) → (2nd𝑑) ∈ 𝑡) ↔ (𝑑𝐻 → ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡)))
6967, 68bitri 267 . . . . . . . . . . . . 13 (((𝑑𝐻 ∧ (1st𝑑) ⊆ (1st𝑓)) → ((2nd𝐻)‘𝑑) ∈ 𝑡) ↔ (𝑑𝐻 → ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡)))
7063, 69syl6bb 279 . . . . . . . . . . . 12 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → ((𝑑 ∈ ((tail‘𝐷)‘𝑓) → ((2nd𝐻)‘𝑑) ∈ 𝑡) ↔ (𝑑𝐻 → ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡))))
7170ralbidv2 3166 . . . . . . . . . . 11 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → (∀𝑑 ∈ ((tail‘𝐷)‘𝑓)((2nd𝐻)‘𝑑) ∈ 𝑡 ↔ ∀𝑑𝐻 ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡)))
7249, 71bitrd 271 . . . . . . . . . 10 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → (((2nd𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∀𝑑𝐻 ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡)))
7372rexbidva 3234 . . . . . . . . 9 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) → (∃𝑓𝐻 ((2nd𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∃𝑓𝐻𝑑𝐻 ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡)))
74 vex 3401 . . . . . . . . . . . . . . . . 17 𝑘 ∈ V
75 vex 3401 . . . . . . . . . . . . . . . . 17 𝑣 ∈ V
7674, 75op1std 7455 . . . . . . . . . . . . . . . 16 (𝑑 = ⟨𝑘, 𝑣⟩ → (1st𝑑) = 𝑘)
7776sseq1d 3851 . . . . . . . . . . . . . . 15 (𝑑 = ⟨𝑘, 𝑣⟩ → ((1st𝑑) ⊆ (1st𝑓) ↔ 𝑘 ⊆ (1st𝑓)))
7874, 75op2ndd 7456 . . . . . . . . . . . . . . . 16 (𝑑 = ⟨𝑘, 𝑣⟩ → (2nd𝑑) = 𝑣)
7978eleq1d 2844 . . . . . . . . . . . . . . 15 (𝑑 = ⟨𝑘, 𝑣⟩ → ((2nd𝑑) ∈ 𝑡𝑣𝑡))
8077, 79imbi12d 336 . . . . . . . . . . . . . 14 (𝑑 = ⟨𝑘, 𝑣⟩ → (((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡) ↔ (𝑘 ⊆ (1st𝑓) → 𝑣𝑡)))
8180raliunxp 5507 . . . . . . . . . . . . 13 (∀𝑑 𝑘𝐹 ({𝑘} × 𝑘)((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡) ↔ ∀𝑘𝐹𝑣𝑘 (𝑘 ⊆ (1st𝑓) → 𝑣𝑡))
82 sneq 4408 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑘 → {𝑛} = {𝑘})
83 id 22 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑘𝑛 = 𝑘)
8482, 83xpeq12d 5386 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑘 → ({𝑛} × 𝑛) = ({𝑘} × 𝑘))
8584cbviunv 4792 . . . . . . . . . . . . . . 15 𝑛𝐹 ({𝑛} × 𝑛) = 𝑘𝐹 ({𝑘} × 𝑘)
861, 85eqtri 2802 . . . . . . . . . . . . . 14 𝐻 = 𝑘𝐹 ({𝑘} × 𝑘)
8786raleqi 3338 . . . . . . . . . . . . 13 (∀𝑑𝐻 ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡) ↔ ∀𝑑 𝑘𝐹 ({𝑘} × 𝑘)((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡))
88 dfss3 3810 . . . . . . . . . . . . . . . 16 (𝑘𝑡 ↔ ∀𝑣𝑘 𝑣𝑡)
8988imbi2i 328 . . . . . . . . . . . . . . 15 ((𝑘 ⊆ (1st𝑓) → 𝑘𝑡) ↔ (𝑘 ⊆ (1st𝑓) → ∀𝑣𝑘 𝑣𝑡))
90 r19.21v 3142 . . . . . . . . . . . . . . 15 (∀𝑣𝑘 (𝑘 ⊆ (1st𝑓) → 𝑣𝑡) ↔ (𝑘 ⊆ (1st𝑓) → ∀𝑣𝑘 𝑣𝑡))
9189, 90bitr4i 270 . . . . . . . . . . . . . 14 ((𝑘 ⊆ (1st𝑓) → 𝑘𝑡) ↔ ∀𝑣𝑘 (𝑘 ⊆ (1st𝑓) → 𝑣𝑡))
9291ralbii 3162 . . . . . . . . . . . . 13 (∀𝑘𝐹 (𝑘 ⊆ (1st𝑓) → 𝑘𝑡) ↔ ∀𝑘𝐹𝑣𝑘 (𝑘 ⊆ (1st𝑓) → 𝑣𝑡))
9381, 87, 923bitr4i 295 . . . . . . . . . . . 12 (∀𝑑𝐻 ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡) ↔ ∀𝑘𝐹 (𝑘 ⊆ (1st𝑓) → 𝑘𝑡))
9493rexbii 3224 . . . . . . . . . . 11 (∃𝑓𝐻𝑑𝐻 ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡) ↔ ∃𝑓𝐻𝑘𝐹 (𝑘 ⊆ (1st𝑓) → 𝑘𝑡))
951rexeqi 3339 . . . . . . . . . . 11 (∃𝑓𝐻𝑘𝐹 (𝑘 ⊆ (1st𝑓) → 𝑘𝑡) ↔ ∃𝑓 𝑛𝐹 ({𝑛} × 𝑛)∀𝑘𝐹 (𝑘 ⊆ (1st𝑓) → 𝑘𝑡))
96 vex 3401 . . . . . . . . . . . . . . . 16 𝑛 ∈ V
97 vex 3401 . . . . . . . . . . . . . . . 16 𝑚 ∈ V
9896, 97op1std 7455 . . . . . . . . . . . . . . 15 (𝑓 = ⟨𝑛, 𝑚⟩ → (1st𝑓) = 𝑛)
9998sseq2d 3852 . . . . . . . . . . . . . 14 (𝑓 = ⟨𝑛, 𝑚⟩ → (𝑘 ⊆ (1st𝑓) ↔ 𝑘𝑛))
10099imbi1d 333 . . . . . . . . . . . . 13 (𝑓 = ⟨𝑛, 𝑚⟩ → ((𝑘 ⊆ (1st𝑓) → 𝑘𝑡) ↔ (𝑘𝑛𝑘𝑡)))
101100ralbidv 3168 . . . . . . . . . . . 12 (𝑓 = ⟨𝑛, 𝑚⟩ → (∀𝑘𝐹 (𝑘 ⊆ (1st𝑓) → 𝑘𝑡) ↔ ∀𝑘𝐹 (𝑘𝑛𝑘𝑡)))
102101rexiunxp 5508 . . . . . . . . . . 11 (∃𝑓 𝑛𝐹 ({𝑛} × 𝑛)∀𝑘𝐹 (𝑘 ⊆ (1st𝑓) → 𝑘𝑡) ↔ ∃𝑛𝐹𝑚𝑛𝑘𝐹 (𝑘𝑛𝑘𝑡))
10394, 95, 1023bitri 289 . . . . . . . . . 10 (∃𝑓𝐻𝑑𝐻 ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡) ↔ ∃𝑛𝐹𝑚𝑛𝑘𝐹 (𝑘𝑛𝑘𝑡))
104 fileln0 22062 . . . . . . . . . . . . . 14 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛𝐹) → 𝑛 ≠ ∅)
105104adantlr 705 . . . . . . . . . . . . 13 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑛𝐹) → 𝑛 ≠ ∅)
106 r19.9rzv 4288 . . . . . . . . . . . . 13 (𝑛 ≠ ∅ → (∀𝑘𝐹 (𝑘𝑛𝑘𝑡) ↔ ∃𝑚𝑛𝑘𝐹 (𝑘𝑛𝑘𝑡)))
107105, 106syl 17 . . . . . . . . . . . 12 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑛𝐹) → (∀𝑘𝐹 (𝑘𝑛𝑘𝑡) ↔ ∃𝑚𝑛𝑘𝐹 (𝑘𝑛𝑘𝑡)))
108 ssid 3842 . . . . . . . . . . . . . . 15 𝑛𝑛
109 sseq1 3845 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑛 → (𝑘𝑛𝑛𝑛))
110 sseq1 3845 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑛 → (𝑘𝑡𝑛𝑡))
111109, 110imbi12d 336 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑛 → ((𝑘𝑛𝑘𝑡) ↔ (𝑛𝑛𝑛𝑡)))
112111rspcv 3507 . . . . . . . . . . . . . . 15 (𝑛𝐹 → (∀𝑘𝐹 (𝑘𝑛𝑘𝑡) → (𝑛𝑛𝑛𝑡)))
113108, 112mpii 46 . . . . . . . . . . . . . 14 (𝑛𝐹 → (∀𝑘𝐹 (𝑘𝑛𝑘𝑡) → 𝑛𝑡))
114113adantl 475 . . . . . . . . . . . . 13 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑛𝐹) → (∀𝑘𝐹 (𝑘𝑛𝑘𝑡) → 𝑛𝑡))
115 sstr2 3828 . . . . . . . . . . . . . . 15 (𝑘𝑛 → (𝑛𝑡𝑘𝑡))
116115com12 32 . . . . . . . . . . . . . 14 (𝑛𝑡 → (𝑘𝑛𝑘𝑡))
117116ralrimivw 3149 . . . . . . . . . . . . 13 (𝑛𝑡 → ∀𝑘𝐹 (𝑘𝑛𝑘𝑡))
118114, 117impbid1 217 . . . . . . . . . . . 12 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑛𝐹) → (∀𝑘𝐹 (𝑘𝑛𝑘𝑡) ↔ 𝑛𝑡))
119107, 118bitr3d 273 . . . . . . . . . . 11 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑛𝐹) → (∃𝑚𝑛𝑘𝐹 (𝑘𝑛𝑘𝑡) ↔ 𝑛𝑡))
120119rexbidva 3234 . . . . . . . . . 10 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) → (∃𝑛𝐹𝑚𝑛𝑘𝐹 (𝑘𝑛𝑘𝑡) ↔ ∃𝑛𝐹 𝑛𝑡))
121103, 120syl5bb 275 . . . . . . . . 9 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) → (∃𝑓𝐻𝑑𝐻 ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡) ↔ ∃𝑛𝐹 𝑛𝑡))
12232, 73, 1213bitrd 297 . . . . . . . 8 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) → (∃𝑑 ∈ ran (tail‘𝐷)((2nd𝐻) “ 𝑑) ⊆ 𝑡 ↔ ∃𝑛𝐹 𝑛𝑡))
123122pm5.32da 574 . . . . . . 7 (𝐹 ∈ (Fil‘𝑋) → ((𝑡𝑋 ∧ ∃𝑑 ∈ ran (tail‘𝐷)((2nd𝐻) “ 𝑑) ⊆ 𝑡) ↔ (𝑡𝑋 ∧ ∃𝑛𝐹 𝑛𝑡)))
124 filn0 22074 . . . . . . . . . . . 12 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ≠ ∅)
12596snnz 4542 . . . . . . . . . . . . . . . 16 {𝑛} ≠ ∅
126104, 125jctil 515 . . . . . . . . . . . . . . 15 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛𝐹) → ({𝑛} ≠ ∅ ∧ 𝑛 ≠ ∅))
127 neanior 3062 . . . . . . . . . . . . . . 15 (({𝑛} ≠ ∅ ∧ 𝑛 ≠ ∅) ↔ ¬ ({𝑛} = ∅ ∨ 𝑛 = ∅))
128126, 127sylib 210 . . . . . . . . . . . . . 14 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛𝐹) → ¬ ({𝑛} = ∅ ∨ 𝑛 = ∅))
129 ss0b 4199 . . . . . . . . . . . . . . 15 (({𝑛} × 𝑛) ⊆ ∅ ↔ ({𝑛} × 𝑛) = ∅)
130 xpeq0 5808 . . . . . . . . . . . . . . 15 (({𝑛} × 𝑛) = ∅ ↔ ({𝑛} = ∅ ∨ 𝑛 = ∅))
131129, 130bitri 267 . . . . . . . . . . . . . 14 (({𝑛} × 𝑛) ⊆ ∅ ↔ ({𝑛} = ∅ ∨ 𝑛 = ∅))
132128, 131sylnibr 321 . . . . . . . . . . . . 13 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛𝐹) → ¬ ({𝑛} × 𝑛) ⊆ ∅)
133132ralrimiva 3148 . . . . . . . . . . . 12 (𝐹 ∈ (Fil‘𝑋) → ∀𝑛𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅)
134 r19.2z 4283 . . . . . . . . . . . 12 ((𝐹 ≠ ∅ ∧ ∀𝑛𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅) → ∃𝑛𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅)
135124, 133, 134syl2anc 579 . . . . . . . . . . 11 (𝐹 ∈ (Fil‘𝑋) → ∃𝑛𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅)
136 rexnal 3176 . . . . . . . . . . 11 (∃𝑛𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅ ↔ ¬ ∀𝑛𝐹 ({𝑛} × 𝑛) ⊆ ∅)
137135, 136sylib 210 . . . . . . . . . 10 (𝐹 ∈ (Fil‘𝑋) → ¬ ∀𝑛𝐹 ({𝑛} × 𝑛) ⊆ ∅)
1381sseq1i 3848 . . . . . . . . . . . 12 (𝐻 ⊆ ∅ ↔ 𝑛𝐹 ({𝑛} × 𝑛) ⊆ ∅)
139 ss0b 4199 . . . . . . . . . . . 12 (𝐻 ⊆ ∅ ↔ 𝐻 = ∅)
140 iunss 4794 . . . . . . . . . . . 12 ( 𝑛𝐹 ({𝑛} × 𝑛) ⊆ ∅ ↔ ∀𝑛𝐹 ({𝑛} × 𝑛) ⊆ ∅)
141138, 139, 1403bitr3i 293 . . . . . . . . . . 11 (𝐻 = ∅ ↔ ∀𝑛𝐹 ({𝑛} × 𝑛) ⊆ ∅)
142141necon3abii 3015 . . . . . . . . . 10 (𝐻 ≠ ∅ ↔ ¬ ∀𝑛𝐹 ({𝑛} × 𝑛) ⊆ ∅)
143137, 142sylibr 226 . . . . . . . . 9 (𝐹 ∈ (Fil‘𝑋) → 𝐻 ≠ ∅)
144 dmresi 5713 . . . . . . . . . . . 12 dom ( I ↾ 𝐻) = 𝐻
1451, 2filnetlem2 32962 . . . . . . . . . . . . . 14 (( I ↾ 𝐻) ⊆ 𝐷𝐷 ⊆ (𝐻 × 𝐻))
146145simpli 478 . . . . . . . . . . . . 13 ( I ↾ 𝐻) ⊆ 𝐷
147 dmss 5568 . . . . . . . . . . . . 13 (( I ↾ 𝐻) ⊆ 𝐷 → dom ( I ↾ 𝐻) ⊆ dom 𝐷)
148146, 147ax-mp 5 . . . . . . . . . . . 12 dom ( I ↾ 𝐻) ⊆ dom 𝐷
149144, 148eqsstr3i 3855 . . . . . . . . . . 11 𝐻 ⊆ dom 𝐷
150145simpri 481 . . . . . . . . . . . . 13 𝐷 ⊆ (𝐻 × 𝐻)
151 dmss 5568 . . . . . . . . . . . . 13 (𝐷 ⊆ (𝐻 × 𝐻) → dom 𝐷 ⊆ dom (𝐻 × 𝐻))
152150, 151ax-mp 5 . . . . . . . . . . . 12 dom 𝐷 ⊆ dom (𝐻 × 𝐻)
153 dmxpid 5590 . . . . . . . . . . . 12 dom (𝐻 × 𝐻) = 𝐻
154152, 153sseqtri 3856 . . . . . . . . . . 11 dom 𝐷𝐻
155149, 154eqssi 3837 . . . . . . . . . 10 𝐻 = dom 𝐷
156155tailfb 32960 . . . . . . . . 9 ((𝐷 ∈ DirRel ∧ 𝐻 ≠ ∅) → ran (tail‘𝐷) ∈ (fBas‘𝐻))
1575, 143, 156syl2anc 579 . . . . . . . 8 (𝐹 ∈ (Fil‘𝑋) → ran (tail‘𝐷) ∈ (fBas‘𝐻))
158 elfm 22159 . . . . . . . 8 ((𝑋𝐹 ∧ ran (tail‘𝐷) ∈ (fBas‘𝐻) ∧ (2nd𝐻):𝐻𝑋) → (𝑡 ∈ ((𝑋 FilMap (2nd𝐻))‘ran (tail‘𝐷)) ↔ (𝑡𝑋 ∧ ∃𝑑 ∈ ran (tail‘𝐷)((2nd𝐻) “ 𝑑) ⊆ 𝑡)))
15910, 157, 9, 158syl3anc 1439 . . . . . . 7 (𝐹 ∈ (Fil‘𝑋) → (𝑡 ∈ ((𝑋 FilMap (2nd𝐻))‘ran (tail‘𝐷)) ↔ (𝑡𝑋 ∧ ∃𝑑 ∈ ran (tail‘𝐷)((2nd𝐻) “ 𝑑) ⊆ 𝑡)))
160 filfbas 22060 . . . . . . . 8 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋))
161 elfg 22083 . . . . . . . 8 (𝐹 ∈ (fBas‘𝑋) → (𝑡 ∈ (𝑋filGen𝐹) ↔ (𝑡𝑋 ∧ ∃𝑛𝐹 𝑛𝑡)))
162160, 161syl 17 . . . . . . 7 (𝐹 ∈ (Fil‘𝑋) → (𝑡 ∈ (𝑋filGen𝐹) ↔ (𝑡𝑋 ∧ ∃𝑛𝐹 𝑛𝑡)))
163123, 159, 1623bitr4d 303 . . . . . 6 (𝐹 ∈ (Fil‘𝑋) → (𝑡 ∈ ((𝑋 FilMap (2nd𝐻))‘ran (tail‘𝐷)) ↔ 𝑡 ∈ (𝑋filGen𝐹)))
164163eqrdv 2776 . . . . 5 (𝐹 ∈ (Fil‘𝑋) → ((𝑋 FilMap (2nd𝐻))‘ran (tail‘𝐷)) = (𝑋filGen𝐹))
165 fgfil 22087 . . . . 5 (𝐹 ∈ (Fil‘𝑋) → (𝑋filGen𝐹) = 𝐹)
166164, 165eqtr2d 2815 . . . 4 (𝐹 ∈ (Fil‘𝑋) → 𝐹 = ((𝑋 FilMap (2nd𝐻))‘ran (tail‘𝐷)))
16721, 166jca 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𝐻)))
170169fveq1d 6448 . . . . . 6 (𝑓 = (2nd𝐻) → ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)) = ((𝑋 FilMap (2nd𝐻))‘ran (tail‘𝐷)))
171170eqeq2d 2788 . . . . 5 (𝑓 = (2nd𝐻) → (𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)) ↔ 𝐹 = ((𝑋 FilMap (2nd𝐻))‘ran (tail‘𝐷))))
172168, 171anbi12d 624 . . . 4 (𝑓 = (2nd𝐻) → ((𝑓:dom 𝐷𝑋𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷))) ↔ ((2nd𝐻):dom 𝐷𝑋𝐹 = ((𝑋 FilMap (2nd𝐻))‘ran (tail‘𝐷)))))
173172spcegv 3496 . . 3 ((2nd𝐻) ∈ V → (((2nd𝐻):dom 𝐷𝑋𝐹 = ((𝑋 FilMap (2nd𝐻))‘ran (tail‘𝐷))) → ∃𝑓(𝑓:dom 𝐷𝑋𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))))
17415, 167, 173sylc 65 . 2 (𝐹 ∈ (Fil‘𝑋) → ∃𝑓(𝑓:dom 𝐷𝑋𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷))))
175 dmeq 5569 . . . . . 6 (𝑑 = 𝐷 → dom 𝑑 = dom 𝐷)
176175feq2d 6277 . . . . 5 (𝑑 = 𝐷 → (𝑓:dom 𝑑𝑋𝑓:dom 𝐷𝑋))
177 fveq2 6446 . . . . . . . 8 (𝑑 = 𝐷 → (tail‘𝑑) = (tail‘𝐷))
178177rneqd 5598 . . . . . . 7 (𝑑 = 𝐷 → ran (tail‘𝑑) = ran (tail‘𝐷))
179178fveq2d 6450 . . . . . 6 (𝑑 = 𝐷 → ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑)) = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))
180179eqeq2d 2788 . . . . 5 (𝑑 = 𝐷 → (𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑)) ↔ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷))))
181176, 180anbi12d 624 . . . 4 (𝑑 = 𝐷 → ((𝑓:dom 𝑑𝑋𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))) ↔ (𝑓:dom 𝐷𝑋𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))))
182181exbidv 1964 . . 3 (𝑑 = 𝐷 → (∃𝑓(𝑓:dom 𝑑𝑋𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))) ↔ ∃𝑓(𝑓:dom 𝐷𝑋𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))))
183182rspcev 3511 . 2 ((𝐷 ∈ DirRel ∧ ∃𝑓(𝑓:dom 𝐷𝑋𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))) → ∃𝑑 ∈ DirRel ∃𝑓(𝑓:dom 𝑑𝑋𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))))
1845, 174, 183syl2anc 579 1 (𝐹 ∈ (Fil‘𝑋) → ∃𝑑 ∈ DirRel ∃𝑓(𝑓:dom 𝑑𝑋𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 386  wo 836   = wceq 1601  wex 1823  wcel 2107  wne 2969  wral 3090  wrex 3091  Vcvv 3398  wss 3792  c0 4141  𝒫 cpw 4379  {csn 4398  cop 4404   cuni 4671   ciun 4753   class class class wbr 4886  {copab 4948   I cid 5260   × cxp 5353  dom cdm 5355  ran crn 5356  cres 5357  cima 5358  Fun wfun 6129   Fn wfn 6130  wf 6131  ontowfo 6133  cfv 6135  (class class class)co 6922  1st c1st 7443  2nd c2nd 7444  DirRelcdir 17614  tailctail 17615  fBascfbas 20130  filGencfg 20131  Filcfil 22057   FilMap cfm 22145
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5006  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4672  df-iun 4755  df-br 4887  df-opab 4949  df-mpt 4966  df-id 5261  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-1st 7445  df-2nd 7446  df-dir 17616  df-tail 17617  df-fbas 20139  df-fg 20140  df-fil 22058  df-fm 22150
This theorem is referenced by:  filnet  32965
  Copyright terms: Public domain W3C validator