Metamath Proof Explorer

Theorem filnetlem4

Description: Lemma for filnet . (Contributed by Jeff Hankins, 15-Dec-2009) (Revised by Mario Carneiro, 8-Aug-2015)

Ref Expression
Hypotheses filnet.h ⊢ 𝐻 = ∪ 𝑛 ∈ 𝐹 ( { 𝑛 } × 𝑛 )
filnet.d ⊢ 𝐷 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) ∧ ( 1st ‘ 𝑦 ) ⊆ ( 1st ‘ 𝑥 ) ) }
Assertion filnetlem4 ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ∃ 𝑑 ∈ DirRel ∃ 𝑓 ( 𝑓 : dom 𝑑 ⟶ 𝑋 ∧ 𝐹 = ( ( 𝑋 FilMap 𝑓 ) ‘ ran ( tail ‘ 𝑑 ) ) ) )

Proof

Step Hyp Ref Expression
1 filnet.h ⊢ 𝐻 = ∪ 𝑛 ∈ 𝐹 ( { 𝑛 } × 𝑛 )
2 filnet.d ⊢ 𝐷 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) ∧ ( 1st ‘ 𝑦 ) ⊆ ( 1st ‘ 𝑥 ) ) }
3 1 2 filnetlem3 ⊢ ( 𝐻 = ∪ ∪ 𝐷 ∧ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝐻 ⊆ ( 𝐹 × 𝑋 ) ∧ 𝐷 ∈ DirRel ) ) )
4 3 simpri ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝐻 ⊆ ( 𝐹 × 𝑋 ) ∧ 𝐷 ∈ DirRel ) )
5 4 simprd ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐷 ∈ DirRel )
6 f2ndres ⊢ ( 2nd ↾ ( 𝐹 × 𝑋 ) ) : ( 𝐹 × 𝑋 ) ⟶ 𝑋
7 4 simpld ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐻 ⊆ ( 𝐹 × 𝑋 ) )
8 fssres2 ⊢ ( ( ( 2nd ↾ ( 𝐹 × 𝑋 ) ) : ( 𝐹 × 𝑋 ) ⟶ 𝑋 ∧ 𝐻 ⊆ ( 𝐹 × 𝑋 ) ) → ( 2nd ↾ 𝐻 ) : 𝐻 ⟶ 𝑋 )
9 6 7 8 sylancr ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 2nd ↾ 𝐻 ) : 𝐻 ⟶ 𝑋 )
10 filtop ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝑋 ∈ 𝐹 )
11 xpexg ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑋 ∈ 𝐹 ) → ( 𝐹 × 𝑋 ) ∈ V )
12 10 11 mpdan ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝐹 × 𝑋 ) ∈ V )
13 12 7 ssexd ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐻 ∈ V )
14 9 13 fexd ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 2nd ↾ 𝐻 ) ∈ V )
15 3 simpli ⊢ 𝐻 = ∪ ∪ 𝐷
16 dirdm ⊢ ( 𝐷 ∈ DirRel → dom 𝐷 = ∪ ∪ 𝐷 )
17 5 16 syl ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → dom 𝐷 = ∪ ∪ 𝐷 )
18 15 17 eqtr4id ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐻 = dom 𝐷 )
19 18 feq2d ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( ( 2nd ↾ 𝐻 ) : 𝐻 ⟶ 𝑋 ↔ ( 2nd ↾ 𝐻 ) : dom 𝐷 ⟶ 𝑋 ) )
20 9 19 mpbid ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 2nd ↾ 𝐻 ) : dom 𝐷 ⟶ 𝑋 )
21 eqid ⊢ dom 𝐷 = dom 𝐷
22 21 tailf ⊢ ( 𝐷 ∈ DirRel → ( tail ‘ 𝐷 ) : dom 𝐷 ⟶ 𝒫 dom 𝐷 )
23 5 22 syl ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( tail ‘ 𝐷 ) : dom 𝐷 ⟶ 𝒫 dom 𝐷 )
24 18 feq2d ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( ( tail ‘ 𝐷 ) : 𝐻 ⟶ 𝒫 dom 𝐷 ↔ ( tail ‘ 𝐷 ) : dom 𝐷 ⟶ 𝒫 dom 𝐷 ) )
25 23 24 mpbird ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( tail ‘ 𝐷 ) : 𝐻 ⟶ 𝒫 dom 𝐷 )
26 25 adantr ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑡 ⊆ 𝑋 ) → ( tail ‘ 𝐷 ) : 𝐻 ⟶ 𝒫 dom 𝐷 )
27 ffn ⊢ ( ( tail ‘ 𝐷 ) : 𝐻 ⟶ 𝒫 dom 𝐷 → ( tail ‘ 𝐷 ) Fn 𝐻 )
28 imaeq2 ⊢ ( 𝑑 = ( ( tail ‘ 𝐷 ) ‘ 𝑓 ) → ( ( 2nd ↾ 𝐻 ) “ 𝑑 ) = ( ( 2nd ↾ 𝐻 ) “ ( ( tail ‘ 𝐷 ) ‘ 𝑓 ) ) )
29 28 sseq1d ⊢ ( 𝑑 = ( ( tail ‘ 𝐷 ) ‘ 𝑓 ) → ( ( ( 2nd ↾ 𝐻 ) “ 𝑑 ) ⊆ 𝑡 ↔ ( ( 2nd ↾ 𝐻 ) “ ( ( tail ‘ 𝐷 ) ‘ 𝑓 ) ) ⊆ 𝑡 ) )
30 29 rexrn ⊢ ( ( tail ‘ 𝐷 ) Fn 𝐻 → ( ∃ 𝑑 ∈ ran ( tail ‘ 𝐷 ) ( ( 2nd ↾ 𝐻 ) “ 𝑑 ) ⊆ 𝑡 ↔ ∃ 𝑓 ∈ 𝐻 ( ( 2nd ↾ 𝐻 ) “ ( ( tail ‘ 𝐷 ) ‘ 𝑓 ) ) ⊆ 𝑡 ) )
31 26 27 30 3syl ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑡 ⊆ 𝑋 ) → ( ∃ 𝑑 ∈ ran ( tail ‘ 𝐷 ) ( ( 2nd ↾ 𝐻 ) “ 𝑑 ) ⊆ 𝑡 ↔ ∃ 𝑓 ∈ 𝐻 ( ( 2nd ↾ 𝐻 ) “ ( ( tail ‘ 𝐷 ) ‘ 𝑓 ) ) ⊆ 𝑡 ) )
32 fo2nd ⊢ 2nd : V –onto→ V
33 fofn ⊢ ( 2nd : V –onto→ V → 2nd Fn V )
34 32 33 ax-mp ⊢ 2nd Fn V
35 ssv ⊢ 𝐻 ⊆ V
36 fnssres ⊢ ( ( 2nd Fn V ∧ 𝐻 ⊆ V ) → ( 2nd ↾ 𝐻 ) Fn 𝐻 )
37 34 35 36 mp2an ⊢ ( 2nd ↾ 𝐻 ) Fn 𝐻
38 fnfun ⊢ ( ( 2nd ↾ 𝐻 ) Fn 𝐻 → Fun ( 2nd ↾ 𝐻 ) )
39 37 38 ax-mp ⊢ Fun ( 2nd ↾ 𝐻 )
40 26 ffvelcdmda ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑡 ⊆ 𝑋 ) ∧ 𝑓 ∈ 𝐻 ) → ( ( tail ‘ 𝐷 ) ‘ 𝑓 ) ∈ 𝒫 dom 𝐷 )
41 40 elpwid ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑡 ⊆ 𝑋 ) ∧ 𝑓 ∈ 𝐻 ) → ( ( tail ‘ 𝐷 ) ‘ 𝑓 ) ⊆ dom 𝐷 )
42 18 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑡 ⊆ 𝑋 ) ∧ 𝑓 ∈ 𝐻 ) → 𝐻 = dom 𝐷 )
43 41 42 sseqtrrd ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑡 ⊆ 𝑋 ) ∧ 𝑓 ∈ 𝐻 ) → ( ( tail ‘ 𝐷 ) ‘ 𝑓 ) ⊆ 𝐻 )
44 37 fndmi ⊢ dom ( 2nd ↾ 𝐻 ) = 𝐻
45 43 44 sseqtrrdi ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑡 ⊆ 𝑋 ) ∧ 𝑓 ∈ 𝐻 ) → ( ( tail ‘ 𝐷 ) ‘ 𝑓 ) ⊆ dom ( 2nd ↾ 𝐻 ) )
46 funimass4 ⊢ ( ( Fun ( 2nd ↾ 𝐻 ) ∧ ( ( tail ‘ 𝐷 ) ‘ 𝑓 ) ⊆ dom ( 2nd ↾ 𝐻 ) ) → ( ( ( 2nd ↾ 𝐻 ) “ ( ( tail ‘ 𝐷 ) ‘ 𝑓 ) ) ⊆ 𝑡 ↔ ∀ 𝑑 ∈ ( ( tail ‘ 𝐷 ) ‘ 𝑓 ) ( ( 2nd ↾ 𝐻 ) ‘ 𝑑 ) ∈ 𝑡 ) )
47 39 45 46 sylancr ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑡 ⊆ 𝑋 ) ∧ 𝑓 ∈ 𝐻 ) → ( ( ( 2nd ↾ 𝐻 ) “ ( ( tail ‘ 𝐷 ) ‘ 𝑓 ) ) ⊆ 𝑡 ↔ ∀ 𝑑 ∈ ( ( tail ‘ 𝐷 ) ‘ 𝑓 ) ( ( 2nd ↾ 𝐻 ) ‘ 𝑑 ) ∈ 𝑡 ) )
48 5 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑡 ⊆ 𝑋 ) ∧ 𝑓 ∈ 𝐻 ) → 𝐷 ∈ DirRel )
49 simpr ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑡 ⊆ 𝑋 ) ∧ 𝑓 ∈ 𝐻 ) → 𝑓 ∈ 𝐻 )
50 49 42 eleqtrd ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑡 ⊆ 𝑋 ) ∧ 𝑓 ∈ 𝐻 ) → 𝑓 ∈ dom 𝐷 )
51 vex ⊢ 𝑑 ∈ V
52 51 a1i ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑡 ⊆ 𝑋 ) ∧ 𝑓 ∈ 𝐻 ) → 𝑑 ∈ V )
53 21 eltail ⊢ ( ( 𝐷 ∈ DirRel ∧ 𝑓 ∈ dom 𝐷 ∧ 𝑑 ∈ V ) → ( 𝑑 ∈ ( ( tail ‘ 𝐷 ) ‘ 𝑓 ) ↔ 𝑓 𝐷 𝑑 ) )
54 48 50 52 53 syl3anc ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑡 ⊆ 𝑋 ) ∧ 𝑓 ∈ 𝐻 ) → ( 𝑑 ∈ ( ( tail ‘ 𝐷 ) ‘ 𝑓 ) ↔ 𝑓 𝐷 𝑑 ) )
55 49 biantrurd ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑡 ⊆ 𝑋 ) ∧ 𝑓 ∈ 𝐻 ) → ( 𝑑 ∈ 𝐻 ↔ ( 𝑓 ∈ 𝐻 ∧ 𝑑 ∈ 𝐻 ) ) )
56 55 anbi1d ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑡 ⊆ 𝑋 ) ∧ 𝑓 ∈ 𝐻 ) → ( ( 𝑑 ∈ 𝐻 ∧ ( 1st ‘ 𝑑 ) ⊆ ( 1st ‘ 𝑓 ) ) ↔ ( ( 𝑓 ∈ 𝐻 ∧ 𝑑 ∈ 𝐻 ) ∧ ( 1st ‘ 𝑑 ) ⊆ ( 1st ‘ 𝑓 ) ) ) )
57 vex ⊢ 𝑓 ∈ V
58 1 2 57 51 filnetlem1 ⊢ ( 𝑓 𝐷 𝑑 ↔ ( ( 𝑓 ∈ 𝐻 ∧ 𝑑 ∈ 𝐻 ) ∧ ( 1st ‘ 𝑑 ) ⊆ ( 1st ‘ 𝑓 ) ) )
59 56 58 bitr4di ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑡 ⊆ 𝑋 ) ∧ 𝑓 ∈ 𝐻 ) → ( ( 𝑑 ∈ 𝐻 ∧ ( 1st ‘ 𝑑 ) ⊆ ( 1st ‘ 𝑓 ) ) ↔ 𝑓 𝐷 𝑑 ) )
60 54 59 bitr4d ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑡 ⊆ 𝑋 ) ∧ 𝑓 ∈ 𝐻 ) → ( 𝑑 ∈ ( ( tail ‘ 𝐷 ) ‘ 𝑓 ) ↔ ( 𝑑 ∈ 𝐻 ∧ ( 1st ‘ 𝑑 ) ⊆ ( 1st ‘ 𝑓 ) ) ) )
61 60 imbi1d ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑡 ⊆ 𝑋 ) ∧ 𝑓 ∈ 𝐻 ) → ( ( 𝑑 ∈ ( ( tail ‘ 𝐷 ) ‘ 𝑓 ) → ( ( 2nd ↾ 𝐻 ) ‘ 𝑑 ) ∈ 𝑡 ) ↔ ( ( 𝑑 ∈ 𝐻 ∧ ( 1st ‘ 𝑑 ) ⊆ ( 1st ‘ 𝑓 ) ) → ( ( 2nd ↾ 𝐻 ) ‘ 𝑑 ) ∈ 𝑡 ) ) )
62 fvres ⊢ ( 𝑑 ∈ 𝐻 → ( ( 2nd ↾ 𝐻 ) ‘ 𝑑 ) = ( 2nd ‘ 𝑑 ) )
63 62 eleq1d ⊢ ( 𝑑 ∈ 𝐻 → ( ( ( 2nd ↾ 𝐻 ) ‘ 𝑑 ) ∈ 𝑡 ↔ ( 2nd ‘ 𝑑 ) ∈ 𝑡 ) )
64 63 adantr ⊢ ( ( 𝑑 ∈ 𝐻 ∧ ( 1st ‘ 𝑑 ) ⊆ ( 1st ‘ 𝑓 ) ) → ( ( ( 2nd ↾ 𝐻 ) ‘ 𝑑 ) ∈ 𝑡 ↔ ( 2nd ‘ 𝑑 ) ∈ 𝑡 ) )
65 64 pm5.74i ⊢ ( ( ( 𝑑 ∈ 𝐻 ∧ ( 1st ‘ 𝑑 ) ⊆ ( 1st ‘ 𝑓 ) ) → ( ( 2nd ↾ 𝐻 ) ‘ 𝑑 ) ∈ 𝑡 ) ↔ ( ( 𝑑 ∈ 𝐻 ∧ ( 1st ‘ 𝑑 ) ⊆ ( 1st ‘ 𝑓 ) ) → ( 2nd ‘ 𝑑 ) ∈ 𝑡 ) )
66 impexp ⊢ ( ( ( 𝑑 ∈ 𝐻 ∧ ( 1st ‘ 𝑑 ) ⊆ ( 1st ‘ 𝑓 ) ) → ( 2nd ‘ 𝑑 ) ∈ 𝑡 ) ↔ ( 𝑑 ∈ 𝐻 → ( ( 1st ‘ 𝑑 ) ⊆ ( 1st ‘ 𝑓 ) → ( 2nd ‘ 𝑑 ) ∈ 𝑡 ) ) )
67 65 66 bitri ⊢ ( ( ( 𝑑 ∈ 𝐻 ∧ ( 1st ‘ 𝑑 ) ⊆ ( 1st ‘ 𝑓 ) ) → ( ( 2nd ↾ 𝐻 ) ‘ 𝑑 ) ∈ 𝑡 ) ↔ ( 𝑑 ∈ 𝐻 → ( ( 1st ‘ 𝑑 ) ⊆ ( 1st ‘ 𝑓 ) → ( 2nd ‘ 𝑑 ) ∈ 𝑡 ) ) )
68 61 67 bitrdi ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑡 ⊆ 𝑋 ) ∧ 𝑓 ∈ 𝐻 ) → ( ( 𝑑 ∈ ( ( tail ‘ 𝐷 ) ‘ 𝑓 ) → ( ( 2nd ↾ 𝐻 ) ‘ 𝑑 ) ∈ 𝑡 ) ↔ ( 𝑑 ∈ 𝐻 → ( ( 1st ‘ 𝑑 ) ⊆ ( 1st ‘ 𝑓 ) → ( 2nd ‘ 𝑑 ) ∈ 𝑡 ) ) ) )
69 68 ralbidv2 ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑡 ⊆ 𝑋 ) ∧ 𝑓 ∈ 𝐻 ) → ( ∀ 𝑑 ∈ ( ( tail ‘ 𝐷 ) ‘ 𝑓 ) ( ( 2nd ↾ 𝐻 ) ‘ 𝑑 ) ∈ 𝑡 ↔ ∀ 𝑑 ∈ 𝐻 ( ( 1st ‘ 𝑑 ) ⊆ ( 1st ‘ 𝑓 ) → ( 2nd ‘ 𝑑 ) ∈ 𝑡 ) ) )
70 47 69 bitrd ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑡 ⊆ 𝑋 ) ∧ 𝑓 ∈ 𝐻 ) → ( ( ( 2nd ↾ 𝐻 ) “ ( ( tail ‘ 𝐷 ) ‘ 𝑓 ) ) ⊆ 𝑡 ↔ ∀ 𝑑 ∈ 𝐻 ( ( 1st ‘ 𝑑 ) ⊆ ( 1st ‘ 𝑓 ) → ( 2nd ‘ 𝑑 ) ∈ 𝑡 ) ) )
71 70 rexbidva ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑡 ⊆ 𝑋 ) → ( ∃ 𝑓 ∈ 𝐻 ( ( 2nd ↾ 𝐻 ) “ ( ( tail ‘ 𝐷 ) ‘ 𝑓 ) ) ⊆ 𝑡 ↔ ∃ 𝑓 ∈ 𝐻 ∀ 𝑑 ∈ 𝐻 ( ( 1st ‘ 𝑑 ) ⊆ ( 1st ‘ 𝑓 ) → ( 2nd ‘ 𝑑 ) ∈ 𝑡 ) ) )
72 vex ⊢ 𝑘 ∈ V
73 vex ⊢ 𝑣 ∈ V
74 72 73 op1std ⊢ ( 𝑑 = ⟨ 𝑘 , 𝑣 ⟩ → ( 1st ‘ 𝑑 ) = 𝑘 )
75 74 sseq1d ⊢ ( 𝑑 = ⟨ 𝑘 , 𝑣 ⟩ → ( ( 1st ‘ 𝑑 ) ⊆ ( 1st ‘ 𝑓 ) ↔ 𝑘 ⊆ ( 1st ‘ 𝑓 ) ) )
76 72 73 op2ndd ⊢ ( 𝑑 = ⟨ 𝑘 , 𝑣 ⟩ → ( 2nd ‘ 𝑑 ) = 𝑣 )
77 76 eleq1d ⊢ ( 𝑑 = ⟨ 𝑘 , 𝑣 ⟩ → ( ( 2nd ‘ 𝑑 ) ∈ 𝑡 ↔ 𝑣 ∈ 𝑡 ) )
78 75 77 imbi12d ⊢ ( 𝑑 = ⟨ 𝑘 , 𝑣 ⟩ → ( ( ( 1st ‘ 𝑑 ) ⊆ ( 1st ‘ 𝑓 ) → ( 2nd ‘ 𝑑 ) ∈ 𝑡 ) ↔ ( 𝑘 ⊆ ( 1st ‘ 𝑓 ) → 𝑣 ∈ 𝑡 ) ) )
79 78 raliunxp ⊢ ( ∀ 𝑑 ∈ ∪ 𝑘 ∈ 𝐹 ( { 𝑘 } × 𝑘 ) ( ( 1st ‘ 𝑑 ) ⊆ ( 1st ‘ 𝑓 ) → ( 2nd ‘ 𝑑 ) ∈ 𝑡 ) ↔ ∀ 𝑘 ∈ 𝐹 ∀ 𝑣 ∈ 𝑘 ( 𝑘 ⊆ ( 1st ‘ 𝑓 ) → 𝑣 ∈ 𝑡 ) )
80 sneq ⊢ ( 𝑛 = 𝑘 → { 𝑛 } = { 𝑘 } )
81 id ⊢ ( 𝑛 = 𝑘 → 𝑛 = 𝑘 )
82 80 81 xpeq12d ⊢ ( 𝑛 = 𝑘 → ( { 𝑛 } × 𝑛 ) = ( { 𝑘 } × 𝑘 ) )
83 82 cbviunv ⊢ ∪ 𝑛 ∈ 𝐹 ( { 𝑛 } × 𝑛 ) = ∪ 𝑘 ∈ 𝐹 ( { 𝑘 } × 𝑘 )
84 1 83 eqtri ⊢ 𝐻 = ∪ 𝑘 ∈ 𝐹 ( { 𝑘 } × 𝑘 )
85 84 raleqi ⊢ ( ∀ 𝑑 ∈ 𝐻 ( ( 1st ‘ 𝑑 ) ⊆ ( 1st ‘ 𝑓 ) → ( 2nd ‘ 𝑑 ) ∈ 𝑡 ) ↔ ∀ 𝑑 ∈ ∪ 𝑘 ∈ 𝐹 ( { 𝑘 } × 𝑘 ) ( ( 1st ‘ 𝑑 ) ⊆ ( 1st ‘ 𝑓 ) → ( 2nd ‘ 𝑑 ) ∈ 𝑡 ) )
86 dfss3 ⊢ ( 𝑘 ⊆ 𝑡 ↔ ∀ 𝑣 ∈ 𝑘 𝑣 ∈ 𝑡 )
87 86 imbi2i ⊢ ( ( 𝑘 ⊆ ( 1st ‘ 𝑓 ) → 𝑘 ⊆ 𝑡 ) ↔ ( 𝑘 ⊆ ( 1st ‘ 𝑓 ) → ∀ 𝑣 ∈ 𝑘 𝑣 ∈ 𝑡 ) )
88 r19.21v ⊢ ( ∀ 𝑣 ∈ 𝑘 ( 𝑘 ⊆ ( 1st ‘ 𝑓 ) → 𝑣 ∈ 𝑡 ) ↔ ( 𝑘 ⊆ ( 1st ‘ 𝑓 ) → ∀ 𝑣 ∈ 𝑘 𝑣 ∈ 𝑡 ) )
89 87 88 bitr4i ⊢ ( ( 𝑘 ⊆ ( 1st ‘ 𝑓 ) → 𝑘 ⊆ 𝑡 ) ↔ ∀ 𝑣 ∈ 𝑘 ( 𝑘 ⊆ ( 1st ‘ 𝑓 ) → 𝑣 ∈ 𝑡 ) )
90 89 ralbii ⊢ ( ∀ 𝑘 ∈ 𝐹 ( 𝑘 ⊆ ( 1st ‘ 𝑓 ) → 𝑘 ⊆ 𝑡 ) ↔ ∀ 𝑘 ∈ 𝐹 ∀ 𝑣 ∈ 𝑘 ( 𝑘 ⊆ ( 1st ‘ 𝑓 ) → 𝑣 ∈ 𝑡 ) )
91 79 85 90 3bitr4i ⊢ ( ∀ 𝑑 ∈ 𝐻 ( ( 1st ‘ 𝑑 ) ⊆ ( 1st ‘ 𝑓 ) → ( 2nd ‘ 𝑑 ) ∈ 𝑡 ) ↔ ∀ 𝑘 ∈ 𝐹 ( 𝑘 ⊆ ( 1st ‘ 𝑓 ) → 𝑘 ⊆ 𝑡 ) )
92 91 rexbii ⊢ ( ∃ 𝑓 ∈ 𝐻 ∀ 𝑑 ∈ 𝐻 ( ( 1st ‘ 𝑑 ) ⊆ ( 1st ‘ 𝑓 ) → ( 2nd ‘ 𝑑 ) ∈ 𝑡 ) ↔ ∃ 𝑓 ∈ 𝐻 ∀ 𝑘 ∈ 𝐹 ( 𝑘 ⊆ ( 1st ‘ 𝑓 ) → 𝑘 ⊆ 𝑡 ) )
93 1 rexeqi ⊢ ( ∃ 𝑓 ∈ 𝐻 ∀ 𝑘 ∈ 𝐹 ( 𝑘 ⊆ ( 1st ‘ 𝑓 ) → 𝑘 ⊆ 𝑡 ) ↔ ∃ 𝑓 ∈ ∪ 𝑛 ∈ 𝐹 ( { 𝑛 } × 𝑛 ) ∀ 𝑘 ∈ 𝐹 ( 𝑘 ⊆ ( 1st ‘ 𝑓 ) → 𝑘 ⊆ 𝑡 ) )
94 vex ⊢ 𝑛 ∈ V
95 vex ⊢ 𝑚 ∈ V
96 94 95 op1std ⊢ ( 𝑓 = ⟨ 𝑛 , 𝑚 ⟩ → ( 1st ‘ 𝑓 ) = 𝑛 )
97 96 sseq2d ⊢ ( 𝑓 = ⟨ 𝑛 , 𝑚 ⟩ → ( 𝑘 ⊆ ( 1st ‘ 𝑓 ) ↔ 𝑘 ⊆ 𝑛 ) )
98 97 imbi1d ⊢ ( 𝑓 = ⟨ 𝑛 , 𝑚 ⟩ → ( ( 𝑘 ⊆ ( 1st ‘ 𝑓 ) → 𝑘 ⊆ 𝑡 ) ↔ ( 𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡 ) ) )
99 98 ralbidv ⊢ ( 𝑓 = ⟨ 𝑛 , 𝑚 ⟩ → ( ∀ 𝑘 ∈ 𝐹 ( 𝑘 ⊆ ( 1st ‘ 𝑓 ) → 𝑘 ⊆ 𝑡 ) ↔ ∀ 𝑘 ∈ 𝐹 ( 𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡 ) ) )
100 99 rexiunxp ⊢ ( ∃ 𝑓 ∈ ∪ 𝑛 ∈ 𝐹 ( { 𝑛 } × 𝑛 ) ∀ 𝑘 ∈ 𝐹 ( 𝑘 ⊆ ( 1st ‘ 𝑓 ) → 𝑘 ⊆ 𝑡 ) ↔ ∃ 𝑛 ∈ 𝐹 ∃ 𝑚 ∈ 𝑛 ∀ 𝑘 ∈ 𝐹 ( 𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡 ) )
101 92 93 100 3bitri ⊢ ( ∃ 𝑓 ∈ 𝐻 ∀ 𝑑 ∈ 𝐻 ( ( 1st ‘ 𝑑 ) ⊆ ( 1st ‘ 𝑓 ) → ( 2nd ‘ 𝑑 ) ∈ 𝑡 ) ↔ ∃ 𝑛 ∈ 𝐹 ∃ 𝑚 ∈ 𝑛 ∀ 𝑘 ∈ 𝐹 ( 𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡 ) )
102 fileln0 ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑛 ∈ 𝐹 ) → 𝑛 ≠ ∅ )
103 102 adantlr ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑡 ⊆ 𝑋 ) ∧ 𝑛 ∈ 𝐹 ) → 𝑛 ≠ ∅ )
104 r19.9rzv ⊢ ( 𝑛 ≠ ∅ → ( ∀ 𝑘 ∈ 𝐹 ( 𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡 ) ↔ ∃ 𝑚 ∈ 𝑛 ∀ 𝑘 ∈ 𝐹 ( 𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡 ) ) )
105 103 104 syl ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑡 ⊆ 𝑋 ) ∧ 𝑛 ∈ 𝐹 ) → ( ∀ 𝑘 ∈ 𝐹 ( 𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡 ) ↔ ∃ 𝑚 ∈ 𝑛 ∀ 𝑘 ∈ 𝐹 ( 𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡 ) ) )
106 ssid ⊢ 𝑛 ⊆ 𝑛
107 sseq1 ⊢ ( 𝑘 = 𝑛 → ( 𝑘 ⊆ 𝑛 ↔ 𝑛 ⊆ 𝑛 ) )
108 sseq1 ⊢ ( 𝑘 = 𝑛 → ( 𝑘 ⊆ 𝑡 ↔ 𝑛 ⊆ 𝑡 ) )
109 107 108 imbi12d ⊢ ( 𝑘 = 𝑛 → ( ( 𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡 ) ↔ ( 𝑛 ⊆ 𝑛 → 𝑛 ⊆ 𝑡 ) ) )
110 109 rspcv ⊢ ( 𝑛 ∈ 𝐹 → ( ∀ 𝑘 ∈ 𝐹 ( 𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡 ) → ( 𝑛 ⊆ 𝑛 → 𝑛 ⊆ 𝑡 ) ) )
111 106 110 mpii ⊢ ( 𝑛 ∈ 𝐹 → ( ∀ 𝑘 ∈ 𝐹 ( 𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡 ) → 𝑛 ⊆ 𝑡 ) )
112 111 adantl ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑡 ⊆ 𝑋 ) ∧ 𝑛 ∈ 𝐹 ) → ( ∀ 𝑘 ∈ 𝐹 ( 𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡 ) → 𝑛 ⊆ 𝑡 ) )
113 sstr2 ⊢ ( 𝑘 ⊆ 𝑛 → ( 𝑛 ⊆ 𝑡 → 𝑘 ⊆ 𝑡 ) )
114 113 com12 ⊢ ( 𝑛 ⊆ 𝑡 → ( 𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡 ) )
115 114 ralrimivw ⊢ ( 𝑛 ⊆ 𝑡 → ∀ 𝑘 ∈ 𝐹 ( 𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡 ) )
116 112 115 impbid1 ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑡 ⊆ 𝑋 ) ∧ 𝑛 ∈ 𝐹 ) → ( ∀ 𝑘 ∈ 𝐹 ( 𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡 ) ↔ 𝑛 ⊆ 𝑡 ) )
117 105 116 bitr3d ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑡 ⊆ 𝑋 ) ∧ 𝑛 ∈ 𝐹 ) → ( ∃ 𝑚 ∈ 𝑛 ∀ 𝑘 ∈ 𝐹 ( 𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡 ) ↔ 𝑛 ⊆ 𝑡 ) )
118 117 rexbidva ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑡 ⊆ 𝑋 ) → ( ∃ 𝑛 ∈ 𝐹 ∃ 𝑚 ∈ 𝑛 ∀ 𝑘 ∈ 𝐹 ( 𝑘 ⊆ 𝑛 → 𝑘 ⊆ 𝑡 ) ↔ ∃ 𝑛 ∈ 𝐹 𝑛 ⊆ 𝑡 ) )
119 101 118 bitrid ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑡 ⊆ 𝑋 ) → ( ∃ 𝑓 ∈ 𝐻 ∀ 𝑑 ∈ 𝐻 ( ( 1st ‘ 𝑑 ) ⊆ ( 1st ‘ 𝑓 ) → ( 2nd ‘ 𝑑 ) ∈ 𝑡 ) ↔ ∃ 𝑛 ∈ 𝐹 𝑛 ⊆ 𝑡 ) )
120 31 71 119 3bitrd ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑡 ⊆ 𝑋 ) → ( ∃ 𝑑 ∈ ran ( tail ‘ 𝐷 ) ( ( 2nd ↾ 𝐻 ) “ 𝑑 ) ⊆ 𝑡 ↔ ∃ 𝑛 ∈ 𝐹 𝑛 ⊆ 𝑡 ) )
121 120 pm5.32da ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑑 ∈ ran ( tail ‘ 𝐷 ) ( ( 2nd ↾ 𝐻 ) “ 𝑑 ) ⊆ 𝑡 ) ↔ ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑛 ∈ 𝐹 𝑛 ⊆ 𝑡 ) ) )
122 filn0 ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ≠ ∅ )
123 94 snnz ⊢ { 𝑛 } ≠ ∅
124 102 123 jctil ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑛 ∈ 𝐹 ) → ( { 𝑛 } ≠ ∅ ∧ 𝑛 ≠ ∅ ) )
125 neanior ⊢ ( ( { 𝑛 } ≠ ∅ ∧ 𝑛 ≠ ∅ ) ↔ ¬ ( { 𝑛 } = ∅ ∨ 𝑛 = ∅ ) )
126 124 125 sylib ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑛 ∈ 𝐹 ) → ¬ ( { 𝑛 } = ∅ ∨ 𝑛 = ∅ ) )
127 ss0b ⊢ ( ( { 𝑛 } × 𝑛 ) ⊆ ∅ ↔ ( { 𝑛 } × 𝑛 ) = ∅ )
128 xpeq0 ⊢ ( ( { 𝑛 } × 𝑛 ) = ∅ ↔ ( { 𝑛 } = ∅ ∨ 𝑛 = ∅ ) )
129 127 128 bitri ⊢ ( ( { 𝑛 } × 𝑛 ) ⊆ ∅ ↔ ( { 𝑛 } = ∅ ∨ 𝑛 = ∅ ) )
130 126 129 sylnibr ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑛 ∈ 𝐹 ) → ¬ ( { 𝑛 } × 𝑛 ) ⊆ ∅ )
131 130 ralrimiva ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ∀ 𝑛 ∈ 𝐹 ¬ ( { 𝑛 } × 𝑛 ) ⊆ ∅ )
132 r19.2z ⊢ ( ( 𝐹 ≠ ∅ ∧ ∀ 𝑛 ∈ 𝐹 ¬ ( { 𝑛 } × 𝑛 ) ⊆ ∅ ) → ∃ 𝑛 ∈ 𝐹 ¬ ( { 𝑛 } × 𝑛 ) ⊆ ∅ )
133 122 131 132 syl2anc ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ∃ 𝑛 ∈ 𝐹 ¬ ( { 𝑛 } × 𝑛 ) ⊆ ∅ )
134 rexnal ⊢ ( ∃ 𝑛 ∈ 𝐹 ¬ ( { 𝑛 } × 𝑛 ) ⊆ ∅ ↔ ¬ ∀ 𝑛 ∈ 𝐹 ( { 𝑛 } × 𝑛 ) ⊆ ∅ )
135 133 134 sylib ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ¬ ∀ 𝑛 ∈ 𝐹 ( { 𝑛 } × 𝑛 ) ⊆ ∅ )
136 1 sseq1i ⊢ ( 𝐻 ⊆ ∅ ↔ ∪ 𝑛 ∈ 𝐹 ( { 𝑛 } × 𝑛 ) ⊆ ∅ )
137 ss0b ⊢ ( 𝐻 ⊆ ∅ ↔ 𝐻 = ∅ )
138 iunss ⊢ ( ∪ 𝑛 ∈ 𝐹 ( { 𝑛 } × 𝑛 ) ⊆ ∅ ↔ ∀ 𝑛 ∈ 𝐹 ( { 𝑛 } × 𝑛 ) ⊆ ∅ )
139 136 137 138 3bitr3i ⊢ ( 𝐻 = ∅ ↔ ∀ 𝑛 ∈ 𝐹 ( { 𝑛 } × 𝑛 ) ⊆ ∅ )
140 139 necon3abii ⊢ ( 𝐻 ≠ ∅ ↔ ¬ ∀ 𝑛 ∈ 𝐹 ( { 𝑛 } × 𝑛 ) ⊆ ∅ )
141 135 140 sylibr ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐻 ≠ ∅ )
142 dmresi ⊢ dom ( I ↾ 𝐻 ) = 𝐻
143 1 2 filnetlem2 ⊢ ( ( I ↾ 𝐻 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ( 𝐻 × 𝐻 ) )
144 143 simpli ⊢ ( I ↾ 𝐻 ) ⊆ 𝐷
145 dmss ⊢ ( ( I ↾ 𝐻 ) ⊆ 𝐷 → dom ( I ↾ 𝐻 ) ⊆ dom 𝐷 )
146 144 145 ax-mp ⊢ dom ( I ↾ 𝐻 ) ⊆ dom 𝐷
147 142 146 eqsstrri ⊢ 𝐻 ⊆ dom 𝐷
148 143 simpri ⊢ 𝐷 ⊆ ( 𝐻 × 𝐻 )
149 dmss ⊢ ( 𝐷 ⊆ ( 𝐻 × 𝐻 ) → dom 𝐷 ⊆ dom ( 𝐻 × 𝐻 ) )
150 148 149 ax-mp ⊢ dom 𝐷 ⊆ dom ( 𝐻 × 𝐻 )
151 dmxpid ⊢ dom ( 𝐻 × 𝐻 ) = 𝐻
152 150 151 sseqtri ⊢ dom 𝐷 ⊆ 𝐻
153 147 152 eqssi ⊢ 𝐻 = dom 𝐷
154 153 tailfb ⊢ ( ( 𝐷 ∈ DirRel ∧ 𝐻 ≠ ∅ ) → ran ( tail ‘ 𝐷 ) ∈ ( fBas ‘ 𝐻 ) )
155 5 141 154 syl2anc ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ran ( tail ‘ 𝐷 ) ∈ ( fBas ‘ 𝐻 ) )
156 elfm ⊢ ( ( 𝑋 ∈ 𝐹 ∧ ran ( tail ‘ 𝐷 ) ∈ ( fBas ‘ 𝐻 ) ∧ ( 2nd ↾ 𝐻 ) : 𝐻 ⟶ 𝑋 ) → ( 𝑡 ∈ ( ( 𝑋 FilMap ( 2nd ↾ 𝐻 ) ) ‘ ran ( tail ‘ 𝐷 ) ) ↔ ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑑 ∈ ran ( tail ‘ 𝐷 ) ( ( 2nd ↾ 𝐻 ) “ 𝑑 ) ⊆ 𝑡 ) ) )
157 10 155 9 156 syl3anc ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝑡 ∈ ( ( 𝑋 FilMap ( 2nd ↾ 𝐻 ) ) ‘ ran ( tail ‘ 𝐷 ) ) ↔ ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑑 ∈ ran ( tail ‘ 𝐷 ) ( ( 2nd ↾ 𝐻 ) “ 𝑑 ) ⊆ 𝑡 ) ) )
158 filfbas ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) )
159 elfg ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( 𝑡 ∈ ( 𝑋 filGen 𝐹 ) ↔ ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑛 ∈ 𝐹 𝑛 ⊆ 𝑡 ) ) )
160 158 159 syl ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝑡 ∈ ( 𝑋 filGen 𝐹 ) ↔ ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑛 ∈ 𝐹 𝑛 ⊆ 𝑡 ) ) )
161 121 157 160 3bitr4d ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝑡 ∈ ( ( 𝑋 FilMap ( 2nd ↾ 𝐻 ) ) ‘ ran ( tail ‘ 𝐷 ) ) ↔ 𝑡 ∈ ( 𝑋 filGen 𝐹 ) ) )
162 161 eqrdv ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( ( 𝑋 FilMap ( 2nd ↾ 𝐻 ) ) ‘ ran ( tail ‘ 𝐷 ) ) = ( 𝑋 filGen 𝐹 ) )
163 fgfil ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝑋 filGen 𝐹 ) = 𝐹 )
164 162 163 eqtr2d ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 = ( ( 𝑋 FilMap ( 2nd ↾ 𝐻 ) ) ‘ ran ( tail ‘ 𝐷 ) ) )
165 20 164 jca ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( ( 2nd ↾ 𝐻 ) : dom 𝐷 ⟶ 𝑋 ∧ 𝐹 = ( ( 𝑋 FilMap ( 2nd ↾ 𝐻 ) ) ‘ ran ( tail ‘ 𝐷 ) ) ) )
166 feq1 ⊢ ( 𝑓 = ( 2nd ↾ 𝐻 ) → ( 𝑓 : dom 𝐷 ⟶ 𝑋 ↔ ( 2nd ↾ 𝐻 ) : dom 𝐷 ⟶ 𝑋 ) )
167 oveq2 ⊢ ( 𝑓 = ( 2nd ↾ 𝐻 ) → ( 𝑋 FilMap 𝑓 ) = ( 𝑋 FilMap ( 2nd ↾ 𝐻 ) ) )
168 167 fveq1d ⊢ ( 𝑓 = ( 2nd ↾ 𝐻 ) → ( ( 𝑋 FilMap 𝑓 ) ‘ ran ( tail ‘ 𝐷 ) ) = ( ( 𝑋 FilMap ( 2nd ↾ 𝐻 ) ) ‘ ran ( tail ‘ 𝐷 ) ) )
169 168 eqeq2d ⊢ ( 𝑓 = ( 2nd ↾ 𝐻 ) → ( 𝐹 = ( ( 𝑋 FilMap 𝑓 ) ‘ ran ( tail ‘ 𝐷 ) ) ↔ 𝐹 = ( ( 𝑋 FilMap ( 2nd ↾ 𝐻 ) ) ‘ ran ( tail ‘ 𝐷 ) ) ) )
170 166 169 anbi12d ⊢ ( 𝑓 = ( 2nd ↾ 𝐻 ) → ( ( 𝑓 : dom 𝐷 ⟶ 𝑋 ∧ 𝐹 = ( ( 𝑋 FilMap 𝑓 ) ‘ ran ( tail ‘ 𝐷 ) ) ) ↔ ( ( 2nd ↾ 𝐻 ) : dom 𝐷 ⟶ 𝑋 ∧ 𝐹 = ( ( 𝑋 FilMap ( 2nd ↾ 𝐻 ) ) ‘ ran ( tail ‘ 𝐷 ) ) ) ) )
171 170 spcegv ⊢ ( ( 2nd ↾ 𝐻 ) ∈ V → ( ( ( 2nd ↾ 𝐻 ) : dom 𝐷 ⟶ 𝑋 ∧ 𝐹 = ( ( 𝑋 FilMap ( 2nd ↾ 𝐻 ) ) ‘ ran ( tail ‘ 𝐷 ) ) ) → ∃ 𝑓 ( 𝑓 : dom 𝐷 ⟶ 𝑋 ∧ 𝐹 = ( ( 𝑋 FilMap 𝑓 ) ‘ ran ( tail ‘ 𝐷 ) ) ) ) )
172 14 165 171 sylc ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ∃ 𝑓 ( 𝑓 : dom 𝐷 ⟶ 𝑋 ∧ 𝐹 = ( ( 𝑋 FilMap 𝑓 ) ‘ ran ( tail ‘ 𝐷 ) ) ) )
173 dmeq ⊢ ( 𝑑 = 𝐷 → dom 𝑑 = dom 𝐷 )
174 173 feq2d ⊢ ( 𝑑 = 𝐷 → ( 𝑓 : dom 𝑑 ⟶ 𝑋 ↔ 𝑓 : dom 𝐷 ⟶ 𝑋 ) )
175 fveq2 ⊢ ( 𝑑 = 𝐷 → ( tail ‘ 𝑑 ) = ( tail ‘ 𝐷 ) )
176 175 rneqd ⊢ ( 𝑑 = 𝐷 → ran ( tail ‘ 𝑑 ) = ran ( tail ‘ 𝐷 ) )
177 176 fveq2d ⊢ ( 𝑑 = 𝐷 → ( ( 𝑋 FilMap 𝑓 ) ‘ ran ( tail ‘ 𝑑 ) ) = ( ( 𝑋 FilMap 𝑓 ) ‘ ran ( tail ‘ 𝐷 ) ) )
178 177 eqeq2d ⊢ ( 𝑑 = 𝐷 → ( 𝐹 = ( ( 𝑋 FilMap 𝑓 ) ‘ ran ( tail ‘ 𝑑 ) ) ↔ 𝐹 = ( ( 𝑋 FilMap 𝑓 ) ‘ ran ( tail ‘ 𝐷 ) ) ) )
179 174 178 anbi12d ⊢ ( 𝑑 = 𝐷 → ( ( 𝑓 : dom 𝑑 ⟶ 𝑋 ∧ 𝐹 = ( ( 𝑋 FilMap 𝑓 ) ‘ ran ( tail ‘ 𝑑 ) ) ) ↔ ( 𝑓 : dom 𝐷 ⟶ 𝑋 ∧ 𝐹 = ( ( 𝑋 FilMap 𝑓 ) ‘ ran ( tail ‘ 𝐷 ) ) ) ) )
180 179 exbidv ⊢ ( 𝑑 = 𝐷 → ( ∃ 𝑓 ( 𝑓 : dom 𝑑 ⟶ 𝑋 ∧ 𝐹 = ( ( 𝑋 FilMap 𝑓 ) ‘ ran ( tail ‘ 𝑑 ) ) ) ↔ ∃ 𝑓 ( 𝑓 : dom 𝐷 ⟶ 𝑋 ∧ 𝐹 = ( ( 𝑋 FilMap 𝑓 ) ‘ ran ( tail ‘ 𝐷 ) ) ) ) )
181 180 rspcev ⊢ ( ( 𝐷 ∈ DirRel ∧ ∃ 𝑓 ( 𝑓 : dom 𝐷 ⟶ 𝑋 ∧ 𝐹 = ( ( 𝑋 FilMap 𝑓 ) ‘ ran ( tail ‘ 𝐷 ) ) ) ) → ∃ 𝑑 ∈ DirRel ∃ 𝑓 ( 𝑓 : dom 𝑑 ⟶ 𝑋 ∧ 𝐹 = ( ( 𝑋 FilMap 𝑓 ) ‘ ran ( tail ‘ 𝑑 ) ) ) )
182 5 172 181 syl2anc ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ∃ 𝑑 ∈ DirRel ∃ 𝑓 ( 𝑓 : dom 𝑑 ⟶ 𝑋 ∧ 𝐹 = ( ( 𝑋 FilMap 𝑓 ) ‘ ran ( tail ‘ 𝑑 ) ) ) )