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