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 32501
Description: Lemma for filnet 32502. (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 32500 . . . 4 (𝐻 = 𝐷 ∧ (𝐹 ∈ (Fil‘𝑋) → (𝐻 ⊆ (𝐹 × 𝑋) ∧ 𝐷 ∈ DirRel)))
43simpri 477 . . 3 (𝐹 ∈ (Fil‘𝑋) → (𝐻 ⊆ (𝐹 × 𝑋) ∧ 𝐷 ∈ DirRel))
54simprd 478 . 2 (𝐹 ∈ (Fil‘𝑋) → 𝐷 ∈ DirRel)
6 f2ndres 7235 . . . . 5 (2nd ↾ (𝐹 × 𝑋)):(𝐹 × 𝑋)⟶𝑋
74simpld 474 . . . . 5 (𝐹 ∈ (Fil‘𝑋) → 𝐻 ⊆ (𝐹 × 𝑋))
8 fssres2 6110 . . . . 5 (((2nd ↾ (𝐹 × 𝑋)):(𝐹 × 𝑋)⟶𝑋𝐻 ⊆ (𝐹 × 𝑋)) → (2nd𝐻):𝐻𝑋)
96, 7, 8sylancr 696 . . . 4 (𝐹 ∈ (Fil‘𝑋) → (2nd𝐻):𝐻𝑋)
10 filtop 21706 . . . . . 6 (𝐹 ∈ (Fil‘𝑋) → 𝑋𝐹)
11 xpexg 7002 . . . . . 6 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑋𝐹) → (𝐹 × 𝑋) ∈ V)
1210, 11mpdan 703 . . . . 5 (𝐹 ∈ (Fil‘𝑋) → (𝐹 × 𝑋) ∈ V)
1312, 7ssexd 4838 . . . 4 (𝐹 ∈ (Fil‘𝑋) → 𝐻 ∈ V)
14 fex 6530 . . . 4 (((2nd𝐻):𝐻𝑋𝐻 ∈ V) → (2nd𝐻) ∈ V)
159, 13, 14syl2anc 694 . . 3 (𝐹 ∈ (Fil‘𝑋) → (2nd𝐻) ∈ V)
16 dirdm 17281 . . . . . . . 8 (𝐷 ∈ DirRel → dom 𝐷 = 𝐷)
175, 16syl 17 . . . . . . 7 (𝐹 ∈ (Fil‘𝑋) → dom 𝐷 = 𝐷)
183simpli 473 . . . . . . 7 𝐻 = 𝐷
1917, 18syl6reqr 2704 . . . . . 6 (𝐹 ∈ (Fil‘𝑋) → 𝐻 = dom 𝐷)
2019feq2d 6069 . . . . 5 (𝐹 ∈ (Fil‘𝑋) → ((2nd𝐻):𝐻𝑋 ↔ (2nd𝐻):dom 𝐷𝑋))
219, 20mpbid 222 . . . 4 (𝐹 ∈ (Fil‘𝑋) → (2nd𝐻):dom 𝐷𝑋)
22 eqid 2651 . . . . . . . . . . . . . 14 dom 𝐷 = dom 𝐷
2322tailf 32495 . . . . . . . . . . . . 13 (𝐷 ∈ DirRel → (tail‘𝐷):dom 𝐷⟶𝒫 dom 𝐷)
245, 23syl 17 . . . . . . . . . . . 12 (𝐹 ∈ (Fil‘𝑋) → (tail‘𝐷):dom 𝐷⟶𝒫 dom 𝐷)
2519feq2d 6069 . . . . . . . . . . . 12 (𝐹 ∈ (Fil‘𝑋) → ((tail‘𝐷):𝐻⟶𝒫 dom 𝐷 ↔ (tail‘𝐷):dom 𝐷⟶𝒫 dom 𝐷))
2624, 25mpbird 247 . . . . . . . . . . 11 (𝐹 ∈ (Fil‘𝑋) → (tail‘𝐷):𝐻⟶𝒫 dom 𝐷)
2726adantr 480 . . . . . . . . . 10 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) → (tail‘𝐷):𝐻⟶𝒫 dom 𝐷)
28 ffn 6083 . . . . . . . . . 10 ((tail‘𝐷):𝐻⟶𝒫 dom 𝐷 → (tail‘𝐷) Fn 𝐻)
29 imaeq2 5497 . . . . . . . . . . . 12 (𝑑 = ((tail‘𝐷)‘𝑓) → ((2nd𝐻) “ 𝑑) = ((2nd𝐻) “ ((tail‘𝐷)‘𝑓)))
3029sseq1d 3665 . . . . . . . . . . 11 (𝑑 = ((tail‘𝐷)‘𝑓) → (((2nd𝐻) “ 𝑑) ⊆ 𝑡 ↔ ((2nd𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡))
3130rexrn 6401 . . . . . . . . . 10 ((tail‘𝐷) Fn 𝐻 → (∃𝑑 ∈ ran (tail‘𝐷)((2nd𝐻) “ 𝑑) ⊆ 𝑡 ↔ ∃𝑓𝐻 ((2nd𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡))
3227, 28, 313syl 18 . . . . . . . . 9 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) → (∃𝑑 ∈ ran (tail‘𝐷)((2nd𝐻) “ 𝑑) ⊆ 𝑡 ↔ ∃𝑓𝐻 ((2nd𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡))
33 fo2nd 7231 . . . . . . . . . . . . . . 15 2nd :V–onto→V
34 fofn 6155 . . . . . . . . . . . . . . 15 (2nd :V–onto→V → 2nd Fn V)
3533, 34ax-mp 5 . . . . . . . . . . . . . 14 2nd Fn V
36 ssv 3658 . . . . . . . . . . . . . 14 𝐻 ⊆ V
37 fnssres 6042 . . . . . . . . . . . . . 14 ((2nd Fn V ∧ 𝐻 ⊆ V) → (2nd𝐻) Fn 𝐻)
3835, 36, 37mp2an 708 . . . . . . . . . . . . 13 (2nd𝐻) Fn 𝐻
39 fnfun 6026 . . . . . . . . . . . . 13 ((2nd𝐻) Fn 𝐻 → Fun (2nd𝐻))
4038, 39ax-mp 5 . . . . . . . . . . . 12 Fun (2nd𝐻)
4127ffvelrnda 6399 . . . . . . . . . . . . . . 15 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → ((tail‘𝐷)‘𝑓) ∈ 𝒫 dom 𝐷)
4241elpwid 4203 . . . . . . . . . . . . . 14 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → ((tail‘𝐷)‘𝑓) ⊆ dom 𝐷)
4319ad2antrr 762 . . . . . . . . . . . . . 14 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → 𝐻 = dom 𝐷)
4442, 43sseqtr4d 3675 . . . . . . . . . . . . 13 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → ((tail‘𝐷)‘𝑓) ⊆ 𝐻)
45 fndm 6028 . . . . . . . . . . . . . 14 ((2nd𝐻) Fn 𝐻 → dom (2nd𝐻) = 𝐻)
4638, 45ax-mp 5 . . . . . . . . . . . . 13 dom (2nd𝐻) = 𝐻
4744, 46syl6sseqr 3685 . . . . . . . . . . . 12 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → ((tail‘𝐷)‘𝑓) ⊆ dom (2nd𝐻))
48 funimass4 6286 . . . . . . . . . . . 12 ((Fun (2nd𝐻) ∧ ((tail‘𝐷)‘𝑓) ⊆ dom (2nd𝐻)) → (((2nd𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∀𝑑 ∈ ((tail‘𝐷)‘𝑓)((2nd𝐻)‘𝑑) ∈ 𝑡))
4940, 47, 48sylancr 696 . . . . . . . . . . 11 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → (((2nd𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∀𝑑 ∈ ((tail‘𝐷)‘𝑓)((2nd𝐻)‘𝑑) ∈ 𝑡))
505ad2antrr 762 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → 𝐷 ∈ DirRel)
51 simpr 476 . . . . . . . . . . . . . . . . 17 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → 𝑓𝐻)
5251, 43eleqtrd 2732 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → 𝑓 ∈ dom 𝐷)
53 vex 3234 . . . . . . . . . . . . . . . . 17 𝑑 ∈ V
5453a1i 11 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → 𝑑 ∈ V)
5522eltail 32494 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ DirRel ∧ 𝑓 ∈ dom 𝐷𝑑 ∈ V) → (𝑑 ∈ ((tail‘𝐷)‘𝑓) ↔ 𝑓𝐷𝑑))
5650, 52, 54, 55syl3anc 1366 . . . . . . . . . . . . . . 15 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → (𝑑 ∈ ((tail‘𝐷)‘𝑓) ↔ 𝑓𝐷𝑑))
5751biantrurd 528 . . . . . . . . . . . . . . . . 17 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → (𝑑𝐻 ↔ (𝑓𝐻𝑑𝐻)))
5857anbi1d 741 . . . . . . . . . . . . . . . 16 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → ((𝑑𝐻 ∧ (1st𝑑) ⊆ (1st𝑓)) ↔ ((𝑓𝐻𝑑𝐻) ∧ (1st𝑑) ⊆ (1st𝑓))))
59 vex 3234 . . . . . . . . . . . . . . . . 17 𝑓 ∈ V
601, 2, 59, 53filnetlem1 32498 . . . . . . . . . . . . . . . 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 6245 . . . . . . . . . . . . . . . . 17 (𝑑𝐻 → ((2nd𝐻)‘𝑑) = (2nd𝑑))
6564eleq1d 2715 . . . . . . . . . . . . . . . 16 (𝑑𝐻 → (((2nd𝐻)‘𝑑) ∈ 𝑡 ↔ (2nd𝑑) ∈ 𝑡))
6665adantr 480 . . . . . . . . . . . . . . 15 ((𝑑𝐻 ∧ (1st𝑑) ⊆ (1st𝑓)) → (((2nd𝐻)‘𝑑) ∈ 𝑡 ↔ (2nd𝑑) ∈ 𝑡))
6766pm5.74i 260 . . . . . . . . . . . . . 14 (((𝑑𝐻 ∧ (1st𝑑) ⊆ (1st𝑓)) → ((2nd𝐻)‘𝑑) ∈ 𝑡) ↔ ((𝑑𝐻 ∧ (1st𝑑) ⊆ (1st𝑓)) → (2nd𝑑) ∈ 𝑡))
68 impexp 461 . . . . . . . . . . . . . 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 3013 . . . . . . . . . . 11 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → (∀𝑑 ∈ ((tail‘𝐷)‘𝑓)((2nd𝐻)‘𝑑) ∈ 𝑡 ↔ ∀𝑑𝐻 ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡)))
7249, 71bitrd 268 . . . . . . . . . 10 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑓𝐻) → (((2nd𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∀𝑑𝐻 ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡)))
7372rexbidva 3078 . . . . . . . . 9 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) → (∃𝑓𝐻 ((2nd𝐻) “ ((tail‘𝐷)‘𝑓)) ⊆ 𝑡 ↔ ∃𝑓𝐻𝑑𝐻 ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡)))
74 vex 3234 . . . . . . . . . . . . . . . . 17 𝑘 ∈ V
75 vex 3234 . . . . . . . . . . . . . . . . 17 𝑣 ∈ V
7674, 75op1std 7220 . . . . . . . . . . . . . . . 16 (𝑑 = ⟨𝑘, 𝑣⟩ → (1st𝑑) = 𝑘)
7776sseq1d 3665 . . . . . . . . . . . . . . 15 (𝑑 = ⟨𝑘, 𝑣⟩ → ((1st𝑑) ⊆ (1st𝑓) ↔ 𝑘 ⊆ (1st𝑓)))
7874, 75op2ndd 7221 . . . . . . . . . . . . . . . 16 (𝑑 = ⟨𝑘, 𝑣⟩ → (2nd𝑑) = 𝑣)
7978eleq1d 2715 . . . . . . . . . . . . . . 15 (𝑑 = ⟨𝑘, 𝑣⟩ → ((2nd𝑑) ∈ 𝑡𝑣𝑡))
8077, 79imbi12d 333 . . . . . . . . . . . . . 14 (𝑑 = ⟨𝑘, 𝑣⟩ → (((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡) ↔ (𝑘 ⊆ (1st𝑓) → 𝑣𝑡)))
8180raliunxp 5294 . . . . . . . . . . . . 13 (∀𝑑 𝑘𝐹 ({𝑘} × 𝑘)((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡) ↔ ∀𝑘𝐹𝑣𝑘 (𝑘 ⊆ (1st𝑓) → 𝑣𝑡))
82 sneq 4220 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑘 → {𝑛} = {𝑘})
83 id 22 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑘𝑛 = 𝑘)
8482, 83xpeq12d 5174 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑘 → ({𝑛} × 𝑛) = ({𝑘} × 𝑘))
8584cbviunv 4591 . . . . . . . . . . . . . . 15 𝑛𝐹 ({𝑛} × 𝑛) = 𝑘𝐹 ({𝑘} × 𝑘)
861, 85eqtri 2673 . . . . . . . . . . . . . 14 𝐻 = 𝑘𝐹 ({𝑘} × 𝑘)
8786raleqi 3172 . . . . . . . . . . . . 13 (∀𝑑𝐻 ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡) ↔ ∀𝑑 𝑘𝐹 ({𝑘} × 𝑘)((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡))
88 dfss3 3625 . . . . . . . . . . . . . . . 16 (𝑘𝑡 ↔ ∀𝑣𝑘 𝑣𝑡)
8988imbi2i 325 . . . . . . . . . . . . . . 15 ((𝑘 ⊆ (1st𝑓) → 𝑘𝑡) ↔ (𝑘 ⊆ (1st𝑓) → ∀𝑣𝑘 𝑣𝑡))
90 r19.21v 2989 . . . . . . . . . . . . . . 15 (∀𝑣𝑘 (𝑘 ⊆ (1st𝑓) → 𝑣𝑡) ↔ (𝑘 ⊆ (1st𝑓) → ∀𝑣𝑘 𝑣𝑡))
9189, 90bitr4i 267 . . . . . . . . . . . . . 14 ((𝑘 ⊆ (1st𝑓) → 𝑘𝑡) ↔ ∀𝑣𝑘 (𝑘 ⊆ (1st𝑓) → 𝑣𝑡))
9291ralbii 3009 . . . . . . . . . . . . 13 (∀𝑘𝐹 (𝑘 ⊆ (1st𝑓) → 𝑘𝑡) ↔ ∀𝑘𝐹𝑣𝑘 (𝑘 ⊆ (1st𝑓) → 𝑣𝑡))
9381, 87, 923bitr4i 292 . . . . . . . . . . . 12 (∀𝑑𝐻 ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡) ↔ ∀𝑘𝐹 (𝑘 ⊆ (1st𝑓) → 𝑘𝑡))
9493rexbii 3070 . . . . . . . . . . 11 (∃𝑓𝐻𝑑𝐻 ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡) ↔ ∃𝑓𝐻𝑘𝐹 (𝑘 ⊆ (1st𝑓) → 𝑘𝑡))
951rexeqi 3173 . . . . . . . . . . 11 (∃𝑓𝐻𝑘𝐹 (𝑘 ⊆ (1st𝑓) → 𝑘𝑡) ↔ ∃𝑓 𝑛𝐹 ({𝑛} × 𝑛)∀𝑘𝐹 (𝑘 ⊆ (1st𝑓) → 𝑘𝑡))
96 vex 3234 . . . . . . . . . . . . . . . 16 𝑛 ∈ V
97 vex 3234 . . . . . . . . . . . . . . . 16 𝑚 ∈ V
9896, 97op1std 7220 . . . . . . . . . . . . . . 15 (𝑓 = ⟨𝑛, 𝑚⟩ → (1st𝑓) = 𝑛)
9998sseq2d 3666 . . . . . . . . . . . . . 14 (𝑓 = ⟨𝑛, 𝑚⟩ → (𝑘 ⊆ (1st𝑓) ↔ 𝑘𝑛))
10099imbi1d 330 . . . . . . . . . . . . 13 (𝑓 = ⟨𝑛, 𝑚⟩ → ((𝑘 ⊆ (1st𝑓) → 𝑘𝑡) ↔ (𝑘𝑛𝑘𝑡)))
101100ralbidv 3015 . . . . . . . . . . . 12 (𝑓 = ⟨𝑛, 𝑚⟩ → (∀𝑘𝐹 (𝑘 ⊆ (1st𝑓) → 𝑘𝑡) ↔ ∀𝑘𝐹 (𝑘𝑛𝑘𝑡)))
102101rexiunxp 5295 . . . . . . . . . . 11 (∃𝑓 𝑛𝐹 ({𝑛} × 𝑛)∀𝑘𝐹 (𝑘 ⊆ (1st𝑓) → 𝑘𝑡) ↔ ∃𝑛𝐹𝑚𝑛𝑘𝐹 (𝑘𝑛𝑘𝑡))
10394, 95, 1023bitri 286 . . . . . . . . . 10 (∃𝑓𝐻𝑑𝐻 ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡) ↔ ∃𝑛𝐹𝑚𝑛𝑘𝐹 (𝑘𝑛𝑘𝑡))
104 fileln0 21701 . . . . . . . . . . . . . 14 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛𝐹) → 𝑛 ≠ ∅)
105104adantlr 751 . . . . . . . . . . . . 13 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑛𝐹) → 𝑛 ≠ ∅)
106 r19.9rzv 4098 . . . . . . . . . . . . 13 (𝑛 ≠ ∅ → (∀𝑘𝐹 (𝑘𝑛𝑘𝑡) ↔ ∃𝑚𝑛𝑘𝐹 (𝑘𝑛𝑘𝑡)))
107105, 106syl 17 . . . . . . . . . . . 12 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑛𝐹) → (∀𝑘𝐹 (𝑘𝑛𝑘𝑡) ↔ ∃𝑚𝑛𝑘𝐹 (𝑘𝑛𝑘𝑡)))
108 ssid 3657 . . . . . . . . . . . . . . 15 𝑛𝑛
109 sseq1 3659 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑛 → (𝑘𝑛𝑛𝑛))
110 sseq1 3659 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑛 → (𝑘𝑡𝑛𝑡))
111109, 110imbi12d 333 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑛 → ((𝑘𝑛𝑘𝑡) ↔ (𝑛𝑛𝑛𝑡)))
112111rspcv 3336 . . . . . . . . . . . . . . 15 (𝑛𝐹 → (∀𝑘𝐹 (𝑘𝑛𝑘𝑡) → (𝑛𝑛𝑛𝑡)))
113108, 112mpii 46 . . . . . . . . . . . . . 14 (𝑛𝐹 → (∀𝑘𝐹 (𝑘𝑛𝑘𝑡) → 𝑛𝑡))
114113adantl 481 . . . . . . . . . . . . 13 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑛𝐹) → (∀𝑘𝐹 (𝑘𝑛𝑘𝑡) → 𝑛𝑡))
115 sstr2 3643 . . . . . . . . . . . . . . 15 (𝑘𝑛 → (𝑛𝑡𝑘𝑡))
116115com12 32 . . . . . . . . . . . . . 14 (𝑛𝑡 → (𝑘𝑛𝑘𝑡))
117116ralrimivw 2996 . . . . . . . . . . . . 13 (𝑛𝑡 → ∀𝑘𝐹 (𝑘𝑛𝑘𝑡))
118114, 117impbid1 215 . . . . . . . . . . . 12 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑛𝐹) → (∀𝑘𝐹 (𝑘𝑛𝑘𝑡) ↔ 𝑛𝑡))
119107, 118bitr3d 270 . . . . . . . . . . 11 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) ∧ 𝑛𝐹) → (∃𝑚𝑛𝑘𝐹 (𝑘𝑛𝑘𝑡) ↔ 𝑛𝑡))
120119rexbidva 3078 . . . . . . . . . 10 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) → (∃𝑛𝐹𝑚𝑛𝑘𝐹 (𝑘𝑛𝑘𝑡) ↔ ∃𝑛𝐹 𝑛𝑡))
121103, 120syl5bb 272 . . . . . . . . 9 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) → (∃𝑓𝐻𝑑𝐻 ((1st𝑑) ⊆ (1st𝑓) → (2nd𝑑) ∈ 𝑡) ↔ ∃𝑛𝐹 𝑛𝑡))
12232, 73, 1213bitrd 294 . . . . . . . 8 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑡𝑋) → (∃𝑑 ∈ ran (tail‘𝐷)((2nd𝐻) “ 𝑑) ⊆ 𝑡 ↔ ∃𝑛𝐹 𝑛𝑡))
123122pm5.32da 674 . . . . . . 7 (𝐹 ∈ (Fil‘𝑋) → ((𝑡𝑋 ∧ ∃𝑑 ∈ ran (tail‘𝐷)((2nd𝐻) “ 𝑑) ⊆ 𝑡) ↔ (𝑡𝑋 ∧ ∃𝑛𝐹 𝑛𝑡)))
124 filn0 21713 . . . . . . . . . . . 12 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ≠ ∅)
12596snnz 4340 . . . . . . . . . . . . . . . 16 {𝑛} ≠ ∅
126104, 125jctil 559 . . . . . . . . . . . . . . 15 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛𝐹) → ({𝑛} ≠ ∅ ∧ 𝑛 ≠ ∅))
127 neanior 2915 . . . . . . . . . . . . . . 15 (({𝑛} ≠ ∅ ∧ 𝑛 ≠ ∅) ↔ ¬ ({𝑛} = ∅ ∨ 𝑛 = ∅))
128126, 127sylib 208 . . . . . . . . . . . . . 14 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛𝐹) → ¬ ({𝑛} = ∅ ∨ 𝑛 = ∅))
129 ss0b 4006 . . . . . . . . . . . . . . 15 (({𝑛} × 𝑛) ⊆ ∅ ↔ ({𝑛} × 𝑛) = ∅)
130 xpeq0 5589 . . . . . . . . . . . . . . 15 (({𝑛} × 𝑛) = ∅ ↔ ({𝑛} = ∅ ∨ 𝑛 = ∅))
131129, 130bitri 264 . . . . . . . . . . . . . 14 (({𝑛} × 𝑛) ⊆ ∅ ↔ ({𝑛} = ∅ ∨ 𝑛 = ∅))
132128, 131sylnibr 318 . . . . . . . . . . . . 13 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛𝐹) → ¬ ({𝑛} × 𝑛) ⊆ ∅)
133132ralrimiva 2995 . . . . . . . . . . . 12 (𝐹 ∈ (Fil‘𝑋) → ∀𝑛𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅)
134 r19.2z 4093 . . . . . . . . . . . 12 ((𝐹 ≠ ∅ ∧ ∀𝑛𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅) → ∃𝑛𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅)
135124, 133, 134syl2anc 694 . . . . . . . . . . 11 (𝐹 ∈ (Fil‘𝑋) → ∃𝑛𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅)
136 rexnal 3024 . . . . . . . . . . 11 (∃𝑛𝐹 ¬ ({𝑛} × 𝑛) ⊆ ∅ ↔ ¬ ∀𝑛𝐹 ({𝑛} × 𝑛) ⊆ ∅)
137135, 136sylib 208 . . . . . . . . . 10 (𝐹 ∈ (Fil‘𝑋) → ¬ ∀𝑛𝐹 ({𝑛} × 𝑛) ⊆ ∅)
1381sseq1i 3662 . . . . . . . . . . . 12 (𝐻 ⊆ ∅ ↔ 𝑛𝐹 ({𝑛} × 𝑛) ⊆ ∅)
139 ss0b 4006 . . . . . . . . . . . 12 (𝐻 ⊆ ∅ ↔ 𝐻 = ∅)
140 iunss 4593 . . . . . . . . . . . 12 ( 𝑛𝐹 ({𝑛} × 𝑛) ⊆ ∅ ↔ ∀𝑛𝐹 ({𝑛} × 𝑛) ⊆ ∅)
141138, 139, 1403bitr3i 290 . . . . . . . . . . 11 (𝐻 = ∅ ↔ ∀𝑛𝐹 ({𝑛} × 𝑛) ⊆ ∅)
142141necon3abii 2869 . . . . . . . . . 10 (𝐻 ≠ ∅ ↔ ¬ ∀𝑛𝐹 ({𝑛} × 𝑛) ⊆ ∅)
143137, 142sylibr 224 . . . . . . . . 9 (𝐹 ∈ (Fil‘𝑋) → 𝐻 ≠ ∅)
144 dmresi 5492 . . . . . . . . . . . 12 dom ( I ↾ 𝐻) = 𝐻
1451, 2filnetlem2 32499 . . . . . . . . . . . . . 14 (( I ↾ 𝐻) ⊆ 𝐷𝐷 ⊆ (𝐻 × 𝐻))
146145simpli 473 . . . . . . . . . . . . 13 ( I ↾ 𝐻) ⊆ 𝐷
147 dmss 5355 . . . . . . . . . . . . 13 (( I ↾ 𝐻) ⊆ 𝐷 → dom ( I ↾ 𝐻) ⊆ dom 𝐷)
148146, 147ax-mp 5 . . . . . . . . . . . 12 dom ( I ↾ 𝐻) ⊆ dom 𝐷
149144, 148eqsstr3i 3669 . . . . . . . . . . 11 𝐻 ⊆ dom 𝐷
150145simpri 477 . . . . . . . . . . . . 13 𝐷 ⊆ (𝐻 × 𝐻)
151 dmss 5355 . . . . . . . . . . . . 13 (𝐷 ⊆ (𝐻 × 𝐻) → dom 𝐷 ⊆ dom (𝐻 × 𝐻))
152150, 151ax-mp 5 . . . . . . . . . . . 12 dom 𝐷 ⊆ dom (𝐻 × 𝐻)
153 dmxpid 5377 . . . . . . . . . . . 12 dom (𝐻 × 𝐻) = 𝐻
154152, 153sseqtri 3670 . . . . . . . . . . 11 dom 𝐷𝐻
155149, 154eqssi 3652 . . . . . . . . . 10 𝐻 = dom 𝐷
156155tailfb 32497 . . . . . . . . 9 ((𝐷 ∈ DirRel ∧ 𝐻 ≠ ∅) → ran (tail‘𝐷) ∈ (fBas‘𝐻))
1575, 143, 156syl2anc 694 . . . . . . . 8 (𝐹 ∈ (Fil‘𝑋) → ran (tail‘𝐷) ∈ (fBas‘𝐻))
158 elfm 21798 . . . . . . . 8 ((𝑋𝐹 ∧ ran (tail‘𝐷) ∈ (fBas‘𝐻) ∧ (2nd𝐻):𝐻𝑋) → (𝑡 ∈ ((𝑋 FilMap (2nd𝐻))‘ran (tail‘𝐷)) ↔ (𝑡𝑋 ∧ ∃𝑑 ∈ ran (tail‘𝐷)((2nd𝐻) “ 𝑑) ⊆ 𝑡)))
15910, 157, 9, 158syl3anc 1366 . . . . . . 7 (𝐹 ∈ (Fil‘𝑋) → (𝑡 ∈ ((𝑋 FilMap (2nd𝐻))‘ran (tail‘𝐷)) ↔ (𝑡𝑋 ∧ ∃𝑑 ∈ ran (tail‘𝐷)((2nd𝐻) “ 𝑑) ⊆ 𝑡)))
160 filfbas 21699 . . . . . . . 8 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋))
161 elfg 21722 . . . . . . . 8 (𝐹 ∈ (fBas‘𝑋) → (𝑡 ∈ (𝑋filGen𝐹) ↔ (𝑡𝑋 ∧ ∃𝑛𝐹 𝑛𝑡)))
162160, 161syl 17 . . . . . . 7 (𝐹 ∈ (Fil‘𝑋) → (𝑡 ∈ (𝑋filGen𝐹) ↔ (𝑡𝑋 ∧ ∃𝑛𝐹 𝑛𝑡)))
163123, 159, 1623bitr4d 300 . . . . . 6 (𝐹 ∈ (Fil‘𝑋) → (𝑡 ∈ ((𝑋 FilMap (2nd𝐻))‘ran (tail‘𝐷)) ↔ 𝑡 ∈ (𝑋filGen𝐹)))
164163eqrdv 2649 . . . . 5 (𝐹 ∈ (Fil‘𝑋) → ((𝑋 FilMap (2nd𝐻))‘ran (tail‘𝐷)) = (𝑋filGen𝐹))
165 fgfil 21726 . . . . 5 (𝐹 ∈ (Fil‘𝑋) → (𝑋filGen𝐹) = 𝐹)
166164, 165eqtr2d 2686 . . . 4 (𝐹 ∈ (Fil‘𝑋) → 𝐹 = ((𝑋 FilMap (2nd𝐻))‘ran (tail‘𝐷)))
16721, 166jca 553 . . 3 (𝐹 ∈ (Fil‘𝑋) → ((2nd𝐻):dom 𝐷𝑋𝐹 = ((𝑋 FilMap (2nd𝐻))‘ran (tail‘𝐷))))
168 feq1 6064 . . . . 5 (𝑓 = (2nd𝐻) → (𝑓:dom 𝐷𝑋 ↔ (2nd𝐻):dom 𝐷𝑋))
169 oveq2 6698 . . . . . . 7 (𝑓 = (2nd𝐻) → (𝑋 FilMap 𝑓) = (𝑋 FilMap (2nd𝐻)))
170169fveq1d 6231 . . . . . 6 (𝑓 = (2nd𝐻) → ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)) = ((𝑋 FilMap (2nd𝐻))‘ran (tail‘𝐷)))
171170eqeq2d 2661 . . . . 5 (𝑓 = (2nd𝐻) → (𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)) ↔ 𝐹 = ((𝑋 FilMap (2nd𝐻))‘ran (tail‘𝐷))))
172168, 171anbi12d 747 . . . 4 (𝑓 = (2nd𝐻) → ((𝑓:dom 𝐷𝑋𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷))) ↔ ((2nd𝐻):dom 𝐷𝑋𝐹 = ((𝑋 FilMap (2nd𝐻))‘ran (tail‘𝐷)))))
173172spcegv 3325 . . 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 5356 . . . . . 6 (𝑑 = 𝐷 → dom 𝑑 = dom 𝐷)
176175feq2d 6069 . . . . 5 (𝑑 = 𝐷 → (𝑓:dom 𝑑𝑋𝑓:dom 𝐷𝑋))
177 fveq2 6229 . . . . . . . 8 (𝑑 = 𝐷 → (tail‘𝑑) = (tail‘𝐷))
178177rneqd 5385 . . . . . . 7 (𝑑 = 𝐷 → ran (tail‘𝑑) = ran (tail‘𝐷))
179178fveq2d 6233 . . . . . 6 (𝑑 = 𝐷 → ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑)) = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))
180179eqeq2d 2661 . . . . 5 (𝑑 = 𝐷 → (𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑)) ↔ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷))))
181176, 180anbi12d 747 . . . 4 (𝑑 = 𝐷 → ((𝑓:dom 𝑑𝑋𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))) ↔ (𝑓:dom 𝐷𝑋𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))))
182181exbidv 1890 . . 3 (𝑑 = 𝐷 → (∃𝑓(𝑓:dom 𝑑𝑋𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))) ↔ ∃𝑓(𝑓:dom 𝐷𝑋𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))))
183182rspcev 3340 . 2 ((𝐷 ∈ DirRel ∧ ∃𝑓(𝑓:dom 𝐷𝑋𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝐷)))) → ∃𝑑 ∈ DirRel ∃𝑓(𝑓:dom 𝑑𝑋𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))))
1845, 174, 183syl2anc 694 1 (𝐹 ∈ (Fil‘𝑋) → ∃𝑑 ∈ DirRel ∃𝑓(𝑓:dom 𝑑𝑋𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383   = wceq 1523  wex 1744  wcel 2030  wne 2823  wral 2941  wrex 2942  Vcvv 3231  wss 3607  c0 3948  𝒫 cpw 4191  {csn 4210  cop 4216   cuni 4468   ciun 4552   class class class wbr 4685  {copab 4745   I cid 5052   × cxp 5141  dom cdm 5143  ran crn 5144  cres 5145  cima 5146  Fun wfun 5920   Fn wfn 5921  wf 5922  ontowfo 5924  cfv 5926  (class class class)co 6690  1st c1st 7208  2nd c2nd 7209  DirRelcdir 17275  tailctail 17276  fBascfbas 19782  filGencfg 19783  Filcfil 21696   FilMap cfm 21784
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-1st 7210  df-2nd 7211  df-dir 17277  df-tail 17278  df-fbas 19791  df-fg 19792  df-fil 21697  df-fm 21789
This theorem is referenced by:  filnet  32502
  Copyright terms: Public domain W3C validator