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 32713
Description: Lemma for filnet 32714. (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 32712 . . . 4 (𝐻 = 𝐷 ∧ (𝐹 ∈ (Fil‘𝑋) → (𝐻 ⊆ (𝐹 × 𝑋) ∧ 𝐷 ∈ DirRel)))
43simpri 473 . . 3 (𝐹 ∈ (Fil‘𝑋) → (𝐻 ⊆ (𝐹 × 𝑋) ∧ 𝐷 ∈ DirRel))
54simprd 483 . 2 (𝐹 ∈ (Fil‘𝑋) → 𝐷 ∈ DirRel)
6 f2ndres 7340 . . . . 5 (2nd ↾ (𝐹 × 𝑋)):(𝐹 × 𝑋)⟶𝑋
74simpld 482 . . . . 5 (𝐹 ∈ (Fil‘𝑋) → 𝐻 ⊆ (𝐹 × 𝑋))
8 fssres2 6212 . . . . 5 (((2nd ↾ (𝐹 × 𝑋)):(𝐹 × 𝑋)⟶𝑋𝐻 ⊆ (𝐹 × 𝑋)) → (2nd𝐻):𝐻𝑋)
96, 7, 8sylancr 575 . . . 4 (𝐹 ∈ (Fil‘𝑋) → (2nd𝐻):𝐻𝑋)
10 filtop 21879 . . . . . 6 (𝐹 ∈ (Fil‘𝑋) → 𝑋𝐹)
11 xpexg 7107 . . . . . 6 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑋𝐹) → (𝐹 × 𝑋) ∈ V)
1210, 11mpdan 667 . . . . 5 (𝐹 ∈ (Fil‘𝑋) → (𝐹 × 𝑋) ∈ V)
1312, 7ssexd 4939 . . . 4 (𝐹 ∈ (Fil‘𝑋) → 𝐻 ∈ V)
14 fex 6633 . . . 4 (((2nd𝐻):𝐻𝑋𝐻 ∈ V) → (2nd𝐻) ∈ V)
159, 13, 14syl2anc 573 . . 3 (𝐹 ∈ (Fil‘𝑋) → (2nd𝐻) ∈ V)
16 dirdm 17442 . . . . . . . 8 (𝐷 ∈ DirRel → dom 𝐷 = 𝐷)
175, 16syl 17 . . . . . . 7 (𝐹 ∈ (Fil‘𝑋) → dom 𝐷 = 𝐷)
183simpli 470 . . . . . . 7 𝐻 = 𝐷
1917, 18syl6reqr 2824 . . . . . 6 (𝐹 ∈ (Fil‘𝑋) → 𝐻 = dom 𝐷)
2019feq2d 6171 . . . . 5 (𝐹 ∈ (Fil‘𝑋) → ((2nd𝐻):𝐻𝑋 ↔ (2nd𝐻):dom 𝐷𝑋))
219, 20mpbid 222 . . . 4 (𝐹 ∈ (Fil‘𝑋) → (2nd𝐻):dom 𝐷𝑋)
22 eqid 2771 . . . . . . . . . . . . . 14 dom 𝐷 = dom 𝐷
2322tailf 32707 . . . . . . . . . . . . 13 (𝐷 ∈ DirRel → (tail‘𝐷):dom 𝐷⟶𝒫 dom 𝐷)
245, 23syl 17 . . . . . . . . . . . 12 (𝐹 ∈ (Fil‘𝑋) → (tail‘𝐷):dom 𝐷⟶𝒫 dom 𝐷)
2519feq2d 6171 . . . . . . . . . . . 12 (𝐹 ∈ (Fil‘𝑋) → ((tail‘𝐷):𝐻⟶𝒫 dom 𝐷 ↔ (tail‘𝐷):dom 𝐷⟶𝒫 dom 𝐷))
2624, 25mpbird 247 . . . . . . . . . . 11 (𝐹 ∈ (Fil‘𝑋) → (tail‘𝐷):𝐻⟶𝒫 dom 𝐷)
2726adantr 466 . . . . . . . . . 10 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) → (tail‘𝐷):𝐻⟶𝒫 dom 𝐷)
28 ffn 6185 . . . . . . . . . 10 ((tail‘𝐷):𝐻⟶𝒫 dom 𝐷 → (tail‘𝐷) Fn 𝐻)
29 imaeq2 5603 . . . . . . . . . . . 12 (𝑑 = ((tail‘𝐷)‘𝑓) → ((2nd𝐻) “ 𝑑) = ((2nd𝐻) “ ((tail‘𝐷)‘𝑓)))
3029sseq1d 3781 . . . . . . . . . . 11 (𝑑 = ((tail‘𝐷)‘𝑓) → (((2nd𝐻) “ 𝑑) ⊆ 𝑡 ↔ ((2nd𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡))
3130rexrn 6504 . . . . . . . . . 10 ((tail‘𝐷) Fn 𝐻 → (∃𝑑 ∈ ran (tail‘𝐷)((2nd𝐻) “ 𝑑) ⊆ 𝑡 ↔ ∃𝑓𝐻 ((2nd𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡))
3227, 28, 313syl 18 . . . . . . . . 9 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) → (∃𝑑 ∈ ran (tail‘𝐷)((2nd𝐻) “ 𝑑) ⊆ 𝑡 ↔ ∃𝑓𝐻 ((2nd𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡))
33 fo2nd 7336 . . . . . . . . . . . . . . 15 2nd :V–onto→V
34 fofn 6258 . . . . . . . . . . . . . . 15 (2nd :V–onto→V → 2nd Fn V)
3533, 34ax-mp 5 . . . . . . . . . . . . . 14 2nd Fn V
36 ssv 3774 . . . . . . . . . . . . . 14 𝐻 ⊆ V
37 fnssres 6144 . . . . . . . . . . . . . 14 ((2nd Fn V ∧ 𝐻 ⊆ V) → (2nd𝐻) Fn 𝐻)
3835, 36, 37mp2an 672 . . . . . . . . . . . . 13 (2nd𝐻) Fn 𝐻
39 fnfun 6128 . . . . . . . . . . . . 13 ((2nd𝐻) Fn 𝐻 → Fun (2nd𝐻))
4038, 39ax-mp 5 . . . . . . . . . . . 12 Fun (2nd𝐻)
4127ffvelrnda 6502 . . . . . . . . . . . . . . 15 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → ((tail‘𝐷)‘𝑓) ∈ 𝒫 dom 𝐷)
4241elpwid 4309 . . . . . . . . . . . . . 14 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → ((tail‘𝐷)‘𝑓) ⊆ dom 𝐷)
4319ad2antrr 705 . . . . . . . . . . . . . 14 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → 𝐻 = dom 𝐷)
4442, 43sseqtr4d 3791 . . . . . . . . . . . . 13 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → ((tail‘𝐷)‘𝑓) ⊆ 𝐻)
45 fndm 6130 . . . . . . . . . . . . . 14 ((2nd𝐻) Fn 𝐻 → dom (2nd𝐻) = 𝐻)
4638, 45ax-mp 5 . . . . . . . . . . . . 13 dom (2nd𝐻) = 𝐻
4744, 46syl6sseqr 3801 . . . . . . . . . . . 12 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → ((tail‘𝐷)‘𝑓) ⊆ dom (2nd𝐻))
48 funimass4 6389 . . . . . . . . . . . 12 ((Fun (2nd𝐻) ∧ ((tail‘𝐷)‘𝑓) ⊆ dom (2nd𝐻)) → (((2nd𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∀𝑑 ∈ ((tail‘𝐷)‘𝑓)((2nd𝐻)‘𝑑) ∈ 𝑡))
4940, 47, 48sylancr 575 . . . . . . . . . . 11 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → (((2nd𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∀𝑑 ∈ ((tail‘𝐷)‘𝑓)((2nd𝐻)‘𝑑) ∈ 𝑡))
505ad2antrr 705 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → 𝐷 ∈ DirRel)
51 simpr 471 . . . . . . . . . . . . . . . . 17 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → 𝑓𝐻)
5251, 43eleqtrd 2852 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → 𝑓 ∈ dom 𝐷)
53 vex 3354 . . . . . . . . . . . . . . . . 17 𝑑 ∈ V
5453a1i 11 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → 𝑑 ∈ V)
5522eltail 32706 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ DirRel ∧ 𝑓 ∈ dom 𝐷𝑑 ∈ V) → (𝑑 ∈ ((tail‘𝐷)‘𝑓) ↔ 𝑓𝐷𝑑))
5650, 52, 54, 55syl3anc 1476 . . . . . . . . . . . . . . 15 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → (𝑑 ∈ ((tail‘𝐷)‘𝑓) ↔ 𝑓𝐷𝑑))
5751biantrurd 522 . . . . . . . . . . . . . . . . 17 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → (𝑑𝐻 ↔ (𝑓𝐻𝑑𝐻)))
5857anbi1d 615 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → ((𝑑𝐻 ∧ (1st𝑑) ⊆ (1st𝑓)) ↔ ((𝑓𝐻𝑑𝐻) ∧ (1st𝑑) ⊆ (1st𝑓))))
59 vex 3354 . . . . . . . . . . . . . . . . 17 𝑓 ∈ V
601, 2, 59, 53filnetlem1 32710 . . . . . . . . . . . . . . . 16 (𝑓𝐷𝑑 ↔ ((𝑓𝐻𝑑𝐻) ∧ (1st𝑑) ⊆ (1st𝑓)))
6158, 60syl6bbr 278 . . . . . . . . . . . . . . 15 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → ((𝑑𝐻 ∧ (1st𝑑) ⊆ (1st𝑓)) ↔ 𝑓𝐷𝑑))
6256, 61bitr4d 271 . . . . . . . . . . . . . 14 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → (𝑑 ∈ ((tail‘𝐷)‘𝑓) ↔ (𝑑𝐻 ∧ (1st𝑑) ⊆ (1st𝑓))))
6362imbi1d 330 . . . . . . . . . . . . 13 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → ((𝑑 ∈ ((tail‘𝐷)‘𝑓) → ((2nd𝐻)‘𝑑) ∈ 𝑡) ↔ ((𝑑𝐻 ∧ (1st𝑑) ⊆ (1st𝑓)) → ((2nd𝐻)‘𝑑) ∈ 𝑡)))
64 fvres 6348 . . . . . . . . . . . . . . . . 17 (𝑑𝐻 → ((2nd𝐻)‘𝑑) = (2nd𝑑))
6564eleq1d 2835 . . . . . . . . . . . . . . . 16 (𝑑𝐻 → (((2nd𝐻)‘𝑑) ∈ 𝑡 ↔ (2nd𝑑) ∈ 𝑡))
6665adantr 466 . . . . . . . . . . . . . . 15 ((𝑑𝐻 ∧ (1st𝑑) ⊆ (1st𝑓)) → (((2nd𝐻)‘𝑑) ∈ 𝑡 ↔ (2nd𝑑) ∈ 𝑡))
6766pm5.74i 260 . . . . . . . . . . . . . 14 (((𝑑𝐻 ∧ (1st𝑑) ⊆ (1st𝑓)) → ((2nd𝐻)‘𝑑) ∈ 𝑡) ↔ ((𝑑𝐻 ∧ (1st𝑑) ⊆ (1st𝑓)) → (2nd𝑑) ∈ 𝑡))
68 impexp 437 . . . . . . . . . . . . . 14 (((𝑑𝐻 ∧ (1st𝑑) ⊆ (1st𝑓)) → (2nd𝑑) ∈ 𝑡) ↔ (𝑑𝐻 → ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡)))
6967, 68bitri 264 . . . . . . . . . . . . 13 (((𝑑𝐻 ∧ (1st𝑑) ⊆ (1st𝑓)) → ((2nd𝐻)‘𝑑) ∈ 𝑡) ↔ (𝑑𝐻 → ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡)))
7063, 69syl6bb 276 . . . . . . . . . . . 12 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → ((𝑑 ∈ ((tail‘𝐷)‘𝑓) → ((2nd𝐻)‘𝑑) ∈ 𝑡) ↔ (𝑑𝐻 → ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡))))
7170ralbidv2 3133 . . . . . . . . . . 11 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → (∀𝑑 ∈ ((tail‘𝐷)‘𝑓)((2nd𝐻)‘𝑑) ∈ 𝑡 ↔ ∀𝑑𝐻 ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡)))
7249, 71bitrd 268 . . . . . . . . . 10 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → (((2nd𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∀𝑑𝐻 ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡)))
7372rexbidva 3197 . . . . . . . . 9 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) → (∃𝑓𝐻 ((2nd𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∃𝑓𝐻𝑑𝐻 ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡)))
74 vex 3354 . . . . . . . . . . . . . . . . 17 𝑘 ∈ V
75 vex 3354 . . . . . . . . . . . . . . . . 17 𝑣 ∈ V
7674, 75op1std 7325 . . . . . . . . . . . . . . . 16 (𝑑 = ⟨𝑘, 𝑣⟩ → (1st𝑑) = 𝑘)
7776sseq1d 3781 . . . . . . . . . . . . . . 15 (𝑑 = ⟨𝑘, 𝑣⟩ → ((1st𝑑) ⊆ (1st𝑓) ↔ 𝑘 ⊆ (1st𝑓)))
7874, 75op2ndd 7326 . . . . . . . . . . . . . . . 16 (𝑑 = ⟨𝑘, 𝑣⟩ → (2nd𝑑) = 𝑣)
7978eleq1d 2835 . . . . . . . . . . . . . . 15 (𝑑 = ⟨𝑘, 𝑣⟩ → ((2nd𝑑) ∈ 𝑡𝑣𝑡))
8077, 79imbi12d 333 . . . . . . . . . . . . . 14 (𝑑 = ⟨𝑘, 𝑣⟩ → (((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡) ↔ (𝑘 ⊆ (1st𝑓) → 𝑣𝑡)))
8180raliunxp 5400 . . . . . . . . . . . . 13 (∀𝑑 𝑘𝐹 ({𝑘} × 𝑘)((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡) ↔ ∀𝑘𝐹𝑣𝑘 (𝑘 ⊆ (1st𝑓) → 𝑣𝑡))
82 sneq 4326 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑘 → {𝑛} = {𝑘})
83 id 22 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑘𝑛 = 𝑘)
8482, 83xpeq12d 5280 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑘 → ({𝑛} × 𝑛) = ({𝑘} × 𝑘))
8584cbviunv 4693 . . . . . . . . . . . . . . 15 𝑛𝐹 ({𝑛} × 𝑛) = 𝑘𝐹 ({𝑘} × 𝑘)
861, 85eqtri 2793 . . . . . . . . . . . . . 14 𝐻 = 𝑘𝐹 ({𝑘} × 𝑘)
8786raleqi 3291 . . . . . . . . . . . . 13 (∀𝑑𝐻 ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡) ↔ ∀𝑑 𝑘𝐹 ({𝑘} × 𝑘)((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡))
88 dfss3 3741 . . . . . . . . . . . . . . . 16 (𝑘𝑡 ↔ ∀𝑣𝑘 𝑣𝑡)
8988imbi2i 325 . . . . . . . . . . . . . . 15 ((𝑘 ⊆ (1st𝑓) → 𝑘𝑡) ↔ (𝑘 ⊆ (1st𝑓) → ∀𝑣𝑘 𝑣𝑡))
90 r19.21v 3109 . . . . . . . . . . . . . . 15 (∀𝑣𝑘 (𝑘 ⊆ (1st𝑓) → 𝑣𝑡) ↔ (𝑘 ⊆ (1st𝑓) → ∀𝑣𝑘 𝑣𝑡))
9189, 90bitr4i 267 . . . . . . . . . . . . . 14 ((𝑘 ⊆ (1st𝑓) → 𝑘𝑡) ↔ ∀𝑣𝑘 (𝑘 ⊆ (1st𝑓) → 𝑣𝑡))
9291ralbii 3129 . . . . . . . . . . . . 13 (∀𝑘𝐹 (𝑘 ⊆ (1st𝑓) → 𝑘𝑡) ↔ ∀𝑘𝐹𝑣𝑘 (𝑘 ⊆ (1st𝑓) → 𝑣𝑡))
9381, 87, 923bitr4i 292 . . . . . . . . . . . 12 (∀𝑑𝐻 ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡) ↔ ∀𝑘𝐹 (𝑘 ⊆ (1st𝑓) → 𝑘𝑡))
9493rexbii 3189 . . . . . . . . . . 11 (∃𝑓𝐻𝑑𝐻 ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡) ↔ ∃𝑓𝐻𝑘𝐹 (𝑘 ⊆ (1st𝑓) → 𝑘𝑡))
951rexeqi 3292 . . . . . . . . . . 11 (∃𝑓𝐻𝑘𝐹 (𝑘 ⊆ (1st𝑓) → 𝑘𝑡) ↔ ∃𝑓 𝑛𝐹 ({𝑛} × 𝑛)∀𝑘𝐹 (𝑘 ⊆ (1st𝑓) → 𝑘𝑡))
96 vex 3354 . . . . . . . . . . . . . . . 16 𝑛 ∈ V
97 vex 3354 . . . . . . . . . . . . . . . 16 𝑚 ∈ V
9896, 97op1std 7325 . . . . . . . . . . . . . . 15 (𝑓 = ⟨𝑛, 𝑚⟩ → (1st𝑓) = 𝑛)
9998sseq2d 3782 . . . . . . . . . . . . . 14 (𝑓 = ⟨𝑛, 𝑚⟩ → (𝑘 ⊆ (1st𝑓) ↔ 𝑘𝑛))
10099imbi1d 330 . . . . . . . . . . . . 13 (𝑓 = ⟨𝑛, 𝑚⟩ → ((𝑘 ⊆ (1st𝑓) → 𝑘𝑡) ↔ (𝑘𝑛𝑘𝑡)))
101100ralbidv 3135 . . . . . . . . . . . 12 (𝑓 = ⟨𝑛, 𝑚⟩ → (∀𝑘𝐹 (𝑘 ⊆ (1st𝑓) → 𝑘𝑡) ↔ ∀𝑘𝐹 (𝑘𝑛𝑘𝑡)))
102101rexiunxp 5401 . . . . . . . . . . 11 (∃𝑓 𝑛𝐹 ({𝑛} × 𝑛)∀𝑘𝐹 (𝑘 ⊆ (1st𝑓) → 𝑘𝑡) ↔ ∃𝑛𝐹𝑚𝑛𝑘𝐹 (𝑘𝑛𝑘𝑡))
10394, 95, 1023bitri 286 . . . . . . . . . 10 (∃𝑓𝐻𝑑𝐻 ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡) ↔ ∃𝑛𝐹𝑚𝑛𝑘𝐹 (𝑘𝑛𝑘𝑡))
104 fileln0 21874 . . . . . . . . . . . . . 14 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛𝐹) → 𝑛 ≠ ∅)
105104adantlr 694 . . . . . . . . . . . . 13 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑛𝐹) → 𝑛 ≠ ∅)
106 r19.9rzv 4206 . . . . . . . . . . . . 13 (𝑛 ≠ ∅ → (∀𝑘𝐹 (𝑘𝑛𝑘𝑡) ↔ ∃𝑚𝑛𝑘𝐹 (𝑘𝑛𝑘𝑡)))
107105, 106syl 17 . . . . . . . . . . . 12 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑛𝐹) → (∀𝑘𝐹 (𝑘𝑛𝑘𝑡) ↔ ∃𝑚𝑛𝑘𝐹 (𝑘𝑛𝑘𝑡)))
108 ssid 3773 . . . . . . . . . . . . . . 15 𝑛𝑛
109 sseq1 3775 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑛 → (𝑘𝑛𝑛𝑛))
110 sseq1 3775 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑛 → (𝑘𝑡𝑛𝑡))
111109, 110imbi12d 333 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑛 → ((𝑘𝑛𝑘𝑡) ↔ (𝑛𝑛𝑛𝑡)))
112111rspcv 3456 . . . . . . . . . . . . . . 15 (𝑛𝐹 → (∀𝑘𝐹 (𝑘𝑛𝑘𝑡) → (𝑛𝑛𝑛𝑡)))
113108, 112mpii 46 . . . . . . . . . . . . . 14 (𝑛𝐹 → (∀𝑘𝐹 (𝑘𝑛𝑘𝑡) → 𝑛𝑡))
114113adantl 467 . . . . . . . . . . . . 13 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑛𝐹) → (∀𝑘𝐹 (𝑘𝑛𝑘𝑡) → 𝑛𝑡))
115 sstr2 3759 . . . . . . . . . . . . . . 15 (𝑘𝑛 → (𝑛𝑡𝑘𝑡))
116115com12 32 . . . . . . . . . . . . . 14 (𝑛𝑡 → (𝑘𝑛𝑘𝑡))
117116ralrimivw 3116 . . . . . . . . . . . . 13 (𝑛𝑡 → ∀𝑘𝐹 (𝑘𝑛𝑘𝑡))
118114, 117impbid1 215 . . . . . . . . . . . 12 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑛𝐹) → (∀𝑘𝐹 (𝑘𝑛𝑘𝑡) ↔ 𝑛𝑡))
119107, 118bitr3d 270 . . . . . . . . . . 11 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑛𝐹) → (∃𝑚𝑛𝑘𝐹 (𝑘𝑛𝑘𝑡) ↔ 𝑛𝑡))
120119rexbidva 3197 . . . . . . . . . 10 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) → (∃𝑛𝐹𝑚𝑛𝑘𝐹 (𝑘𝑛𝑘𝑡) ↔ ∃𝑛𝐹 𝑛𝑡))
121103, 120syl5bb 272 . . . . . . . . 9 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) → (∃𝑓𝐻𝑑𝐻 ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡) ↔ ∃𝑛𝐹 𝑛𝑡))
12232, 73, 1213bitrd 294 . . . . . . . 8 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) → (∃𝑑 ∈ ran (tail‘𝐷)((2nd𝐻) “ 𝑑) ⊆ 𝑡 ↔ ∃𝑛𝐹 𝑛𝑡))
123122pm5.32da 568 . . . . . . 7 (𝐹 ∈ (Fil‘𝑋) → ((𝑡𝑋 ∧ ∃𝑑 ∈ ran (tail‘𝐷)((2nd𝐻) “ 𝑑) ⊆ 𝑡) ↔ (𝑡𝑋 ∧ ∃𝑛𝐹 𝑛𝑡)))
124 filn0 21886 . . . . . . . . . . . 12 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ≠ ∅)
12596snnz 4444 . . . . . . . . . . . . . . . 16 {𝑛} ≠ ∅
126104, 125jctil 509 . . . . . . . . . . . . . . 15 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛𝐹) → ({𝑛} ≠ ∅ ∧ 𝑛 ≠ ∅))
127 neanior 3035 . . . . . . . . . . . . . . 15 (({𝑛} ≠ ∅ ∧ 𝑛 ≠ ∅) ↔ ¬ ({𝑛} = ∅ ∨ 𝑛 = ∅))
128126, 127sylib 208 . . . . . . . . . . . . . 14 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛𝐹) → ¬ ({𝑛} = ∅ ∨ 𝑛 = ∅))
129 ss0b 4117 . . . . . . . . . . . . . . 15 (({𝑛} × 𝑛) ⊆ ∅ ↔ ({𝑛} × 𝑛) = ∅)
130 xpeq0 5695 . . . . . . . . . . . . . . 15 (({𝑛} × 𝑛) = ∅ ↔ ({𝑛} = ∅ ∨ 𝑛 = ∅))
131129, 130bitri 264 . . . . . . . . . . . . . 14 (({𝑛} × 𝑛) ⊆ ∅ ↔ ({𝑛} = ∅ ∨ 𝑛 = ∅))
132128, 131sylnibr 318 . . . . . . . . . . . . 13 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛𝐹) → ¬ ({𝑛} × 𝑛) ⊆ ∅)
133132ralrimiva 3115 . . . . . . . . . . . 12 (𝐹 ∈ (Fil‘𝑋) → ∀𝑛𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅)
134 r19.2z 4201 . . . . . . . . . . . 12 ((𝐹 ≠ ∅ ∧ ∀𝑛𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅) → ∃𝑛𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅)
135124, 133, 134syl2anc 573 . . . . . . . . . . 11 (𝐹 ∈ (Fil‘𝑋) → ∃𝑛𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅)
136 rexnal 3143 . . . . . . . . . . 11 (∃𝑛𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅ ↔ ¬ ∀𝑛𝐹 ({𝑛} × 𝑛) ⊆ ∅)
137135, 136sylib 208 . . . . . . . . . 10 (𝐹 ∈ (Fil‘𝑋) → ¬ ∀𝑛𝐹 ({𝑛} × 𝑛) ⊆ ∅)
1381sseq1i 3778 . . . . . . . . . . . 12 (𝐻 ⊆ ∅ ↔ 𝑛𝐹 ({𝑛} × 𝑛) ⊆ ∅)
139 ss0b 4117 . . . . . . . . . . . 12 (𝐻 ⊆ ∅ ↔ 𝐻 = ∅)
140 iunss 4695 . . . . . . . . . . . 12 ( 𝑛𝐹 ({𝑛} × 𝑛) ⊆ ∅ ↔ ∀𝑛𝐹 ({𝑛} × 𝑛) ⊆ ∅)
141138, 139, 1403bitr3i 290 . . . . . . . . . . 11 (𝐻 = ∅ ↔ ∀𝑛𝐹 ({𝑛} × 𝑛) ⊆ ∅)
142141necon3abii 2989 . . . . . . . . . 10 (𝐻 ≠ ∅ ↔ ¬ ∀𝑛𝐹 ({𝑛} × 𝑛) ⊆ ∅)
143137, 142sylibr 224 . . . . . . . . 9 (𝐹 ∈ (Fil‘𝑋) → 𝐻 ≠ ∅)
144 dmresi 5598 . . . . . . . . . . . 12 dom ( I ↾ 𝐻) = 𝐻
1451, 2filnetlem2 32711 . . . . . . . . . . . . . 14 (( I ↾ 𝐻) ⊆ 𝐷𝐷 ⊆ (𝐻 × 𝐻))
146145simpli 470 . . . . . . . . . . . . 13 ( I ↾ 𝐻) ⊆ 𝐷
147 dmss 5461 . . . . . . . . . . . . 13 (( I ↾ 𝐻) ⊆ 𝐷 → dom ( I ↾ 𝐻) ⊆ dom 𝐷)
148146, 147ax-mp 5 . . . . . . . . . . . 12 dom ( I ↾ 𝐻) ⊆ dom 𝐷
149144, 148eqsstr3i 3785 . . . . . . . . . . 11 𝐻 ⊆ dom 𝐷
150145simpri 473 . . . . . . . . . . . . 13 𝐷 ⊆ (𝐻 × 𝐻)
151 dmss 5461 . . . . . . . . . . . . 13 (𝐷 ⊆ (𝐻 × 𝐻) → dom 𝐷 ⊆ dom (𝐻 × 𝐻))
152150, 151ax-mp 5 . . . . . . . . . . . 12 dom 𝐷 ⊆ dom (𝐻 × 𝐻)
153 dmxpid 5483 . . . . . . . . . . . 12 dom (𝐻 × 𝐻) = 𝐻
154152, 153sseqtri 3786 . . . . . . . . . . 11 dom 𝐷𝐻
155149, 154eqssi 3768 . . . . . . . . . 10 𝐻 = dom 𝐷
156155tailfb 32709 . . . . . . . . 9 ((𝐷 ∈ DirRel ∧ 𝐻 ≠ ∅) → ran (tail‘𝐷) ∈ (fBas‘𝐻))
1575, 143, 156syl2anc 573 . . . . . . . 8 (𝐹 ∈ (Fil‘𝑋) → ran (tail‘𝐷) ∈ (fBas‘𝐻))
158 elfm 21971 . . . . . . . 8 ((𝑋𝐹 ∧ ran (tail‘𝐷) ∈ (fBas‘𝐻) ∧ (2nd𝐻):𝐻𝑋) → (𝑡 ∈ ((𝑋 FilMap (2nd𝐻))‘ran (tail‘𝐷)) ↔ (𝑡𝑋 ∧ ∃𝑑 ∈ ran (tail‘𝐷)((2nd𝐻) “ 𝑑) ⊆ 𝑡)))
15910, 157, 9, 158syl3anc 1476 . . . . . . 7 (𝐹 ∈ (Fil‘𝑋) → (𝑡 ∈ ((𝑋 FilMap (2nd𝐻))‘ran (tail‘𝐷)) ↔ (𝑡𝑋 ∧ ∃𝑑 ∈ ran (tail‘𝐷)((2nd𝐻) “ 𝑑) ⊆ 𝑡)))
160 filfbas 21872 . . . . . . . 8 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋))
161 elfg 21895 . . . . . . . 8 (𝐹 ∈ (fBas‘𝑋) → (𝑡 ∈ (𝑋filGen𝐹) ↔ (𝑡𝑋 ∧ ∃𝑛𝐹 𝑛𝑡)))
162160, 161syl 17 . . . . . . 7 (𝐹 ∈ (Fil‘𝑋) → (𝑡 ∈ (𝑋filGen𝐹) ↔ (𝑡𝑋 ∧ ∃𝑛𝐹 𝑛𝑡)))
163123, 159, 1623bitr4d 300 . . . . . 6 (𝐹 ∈ (Fil‘𝑋) → (𝑡 ∈ ((𝑋 FilMap (2nd𝐻))‘ran (tail‘𝐷)) ↔ 𝑡 ∈ (𝑋filGen𝐹)))
164163eqrdv 2769 . . . . 5 (𝐹 ∈ (Fil‘𝑋) → ((𝑋 FilMap (2nd𝐻))‘ran (tail‘𝐷)) = (𝑋filGen𝐹))
165 fgfil 21899 . . . . 5 (𝐹 ∈ (Fil‘𝑋) → (𝑋filGen𝐹) = 𝐹)
166164, 165eqtr2d 2806 . . . 4 (𝐹 ∈ (Fil‘𝑋) → 𝐹 = ((𝑋 FilMap (2nd𝐻))‘ran (tail‘𝐷)))
16721, 166jca 501 . . 3 (𝐹 ∈ (Fil‘𝑋) → ((2nd𝐻):dom 𝐷𝑋𝐹 = ((𝑋 FilMap (2nd𝐻))‘ran (tail‘𝐷))))
168 feq1 6166 . . . . 5 (𝑓 = (2nd𝐻) → (𝑓:dom 𝐷𝑋 ↔ (2nd𝐻):dom 𝐷𝑋))
169 oveq2 6801 . . . . . . 7 (𝑓 = (2nd𝐻) → (𝑋 FilMap 𝑓) = (𝑋 FilMap (2nd𝐻)))
170169fveq1d 6334 . . . . . 6 (𝑓 = (2nd𝐻) → ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)) = ((𝑋 FilMap (2nd𝐻))‘ran (tail‘𝐷)))
171170eqeq2d 2781 . . . . 5 (𝑓 = (2nd𝐻) → (𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)) ↔ 𝐹 = ((𝑋 FilMap (2nd𝐻))‘ran (tail‘𝐷))))
172168, 171anbi12d 616 . . . 4 (𝑓 = (2nd𝐻) → ((𝑓:dom 𝐷𝑋𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷))) ↔ ((2nd𝐻):dom 𝐷𝑋𝐹 = ((𝑋 FilMap (2nd𝐻))‘ran (tail‘𝐷)))))
173172spcegv 3445 . . 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 5462 . . . . . 6 (𝑑 = 𝐷 → dom 𝑑 = dom 𝐷)
176175feq2d 6171 . . . . 5 (𝑑 = 𝐷 → (𝑓:dom 𝑑𝑋𝑓:dom 𝐷𝑋))
177 fveq2 6332 . . . . . . . 8 (𝑑 = 𝐷 → (tail‘𝑑) = (tail‘𝐷))
178177rneqd 5491 . . . . . . 7 (𝑑 = 𝐷 → ran (tail‘𝑑) = ran (tail‘𝐷))
179178fveq2d 6336 . . . . . 6 (𝑑 = 𝐷 → ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑)) = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))
180179eqeq2d 2781 . . . . 5 (𝑑 = 𝐷 → (𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑)) ↔ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷))))
181176, 180anbi12d 616 . . . 4 (𝑑 = 𝐷 → ((𝑓:dom 𝑑𝑋𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))) ↔ (𝑓:dom 𝐷𝑋𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))))
182181exbidv 2002 . . 3 (𝑑 = 𝐷 → (∃𝑓(𝑓:dom 𝑑𝑋𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))) ↔ ∃𝑓(𝑓:dom 𝐷𝑋𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))))
183182rspcev 3460 . 2 ((𝐷 ∈ DirRel ∧ ∃𝑓(𝑓:dom 𝐷𝑋𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))) → ∃𝑑 ∈ DirRel ∃𝑓(𝑓:dom 𝑑𝑋𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))))
1845, 174, 183syl2anc 573 1 (𝐹 ∈ (Fil‘𝑋) → ∃𝑑 ∈ DirRel ∃𝑓(𝑓:dom 𝑑𝑋𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382  wo 836   = wceq 1631  wex 1852  wcel 2145  wne 2943  wral 3061  wrex 3062  Vcvv 3351  wss 3723  c0 4063  𝒫 cpw 4297  {csn 4316  cop 4322   cuni 4574   ciun 4654   class class class wbr 4786  {copab 4846   I cid 5156   × cxp 5247  dom cdm 5249  ran crn 5250  cres 5251  cima 5252  Fun wfun 6025   Fn wfn 6026  wf 6027  ontowfo 6029  cfv 6031  (class class class)co 6793  1st c1st 7313  2nd c2nd 7314  DirRelcdir 17436  tailctail 17437  fBascfbas 19949  filGencfg 19950  Filcfil 21869   FilMap cfm 21957
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-1st 7315  df-2nd 7316  df-dir 17438  df-tail 17439  df-fbas 19958  df-fg 19959  df-fil 21870  df-fm 21962
This theorem is referenced by:  filnet  32714
  Copyright terms: Public domain W3C validator