Metamath Proof Explorer


Theorem filnetlem3

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

Ref Expression
Hypotheses filnet.h 𝐻 = 𝑛𝐹 ( { 𝑛 } × 𝑛 )
filnet.d 𝐷 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥𝐻𝑦𝐻 ) ∧ ( 1st𝑦 ) ⊆ ( 1st𝑥 ) ) }
Assertion filnetlem3 ( 𝐻 = 𝐷 ∧ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝐻 ⊆ ( 𝐹 × 𝑋 ) ∧ 𝐷 ∈ DirRel ) ) )

Proof

Step Hyp Ref Expression
1 filnet.h 𝐻 = 𝑛𝐹 ( { 𝑛 } × 𝑛 )
2 filnet.d 𝐷 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥𝐻𝑦𝐻 ) ∧ ( 1st𝑦 ) ⊆ ( 1st𝑥 ) ) }
3 dmresi dom ( I ↾ 𝐻 ) = 𝐻
4 1 2 filnetlem2 ( ( I ↾ 𝐻 ) ⊆ 𝐷𝐷 ⊆ ( 𝐻 × 𝐻 ) )
5 4 simpli ( I ↾ 𝐻 ) ⊆ 𝐷
6 dmss ( ( I ↾ 𝐻 ) ⊆ 𝐷 → dom ( I ↾ 𝐻 ) ⊆ dom 𝐷 )
7 5 6 ax-mp dom ( I ↾ 𝐻 ) ⊆ dom 𝐷
8 3 7 eqsstrri 𝐻 ⊆ dom 𝐷
9 ssun1 dom 𝐷 ⊆ ( dom 𝐷 ∪ ran 𝐷 )
10 8 9 sstri 𝐻 ⊆ ( dom 𝐷 ∪ ran 𝐷 )
11 dmrnssfld ( dom 𝐷 ∪ ran 𝐷 ) ⊆ 𝐷
12 10 11 sstri 𝐻 𝐷
13 4 simpri 𝐷 ⊆ ( 𝐻 × 𝐻 )
14 uniss ( 𝐷 ⊆ ( 𝐻 × 𝐻 ) → 𝐷 ( 𝐻 × 𝐻 ) )
15 uniss ( 𝐷 ( 𝐻 × 𝐻 ) → 𝐷 ( 𝐻 × 𝐻 ) )
16 13 14 15 mp2b 𝐷 ( 𝐻 × 𝐻 )
17 unixpss ( 𝐻 × 𝐻 ) ⊆ ( 𝐻𝐻 )
18 unidm ( 𝐻𝐻 ) = 𝐻
19 17 18 sseqtri ( 𝐻 × 𝐻 ) ⊆ 𝐻
20 16 19 sstri 𝐷𝐻
21 12 20 eqssi 𝐻 = 𝐷
22 filelss ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑛𝐹 ) → 𝑛𝑋 )
23 xpss2 ( 𝑛𝑋 → ( { 𝑛 } × 𝑛 ) ⊆ ( { 𝑛 } × 𝑋 ) )
24 22 23 syl ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑛𝐹 ) → ( { 𝑛 } × 𝑛 ) ⊆ ( { 𝑛 } × 𝑋 ) )
25 24 ralrimiva ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ∀ 𝑛𝐹 ( { 𝑛 } × 𝑛 ) ⊆ ( { 𝑛 } × 𝑋 ) )
26 ss2iun ( ∀ 𝑛𝐹 ( { 𝑛 } × 𝑛 ) ⊆ ( { 𝑛 } × 𝑋 ) → 𝑛𝐹 ( { 𝑛 } × 𝑛 ) ⊆ 𝑛𝐹 ( { 𝑛 } × 𝑋 ) )
27 25 26 syl ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝑛𝐹 ( { 𝑛 } × 𝑛 ) ⊆ 𝑛𝐹 ( { 𝑛 } × 𝑋 ) )
28 iunxpconst 𝑛𝐹 ( { 𝑛 } × 𝑋 ) = ( 𝐹 × 𝑋 )
29 27 28 sseqtrdi ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝑛𝐹 ( { 𝑛 } × 𝑛 ) ⊆ ( 𝐹 × 𝑋 ) )
30 1 29 eqsstrid ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐻 ⊆ ( 𝐹 × 𝑋 ) )
31 5 a1i ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( I ↾ 𝐻 ) ⊆ 𝐷 )
32 2 relopabiv Rel 𝐷
33 31 32 jctil ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( Rel 𝐷 ∧ ( I ↾ 𝐻 ) ⊆ 𝐷 ) )
34 simpl ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑣𝐻𝑧𝐻 ) ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
35 30 adantr ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑣𝐻𝑧𝐻 ) ) → 𝐻 ⊆ ( 𝐹 × 𝑋 ) )
36 simprl ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑣𝐻𝑧𝐻 ) ) → 𝑣𝐻 )
37 35 36 sseldd ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑣𝐻𝑧𝐻 ) ) → 𝑣 ∈ ( 𝐹 × 𝑋 ) )
38 xp1st ( 𝑣 ∈ ( 𝐹 × 𝑋 ) → ( 1st𝑣 ) ∈ 𝐹 )
39 37 38 syl ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑣𝐻𝑧𝐻 ) ) → ( 1st𝑣 ) ∈ 𝐹 )
40 simprr ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑣𝐻𝑧𝐻 ) ) → 𝑧𝐻 )
41 35 40 sseldd ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑣𝐻𝑧𝐻 ) ) → 𝑧 ∈ ( 𝐹 × 𝑋 ) )
42 xp1st ( 𝑧 ∈ ( 𝐹 × 𝑋 ) → ( 1st𝑧 ) ∈ 𝐹 )
43 41 42 syl ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑣𝐻𝑧𝐻 ) ) → ( 1st𝑧 ) ∈ 𝐹 )
44 filinn0 ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 1st𝑣 ) ∈ 𝐹 ∧ ( 1st𝑧 ) ∈ 𝐹 ) → ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) ≠ ∅ )
45 34 39 43 44 syl3anc ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑣𝐻𝑧𝐻 ) ) → ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) ≠ ∅ )
46 n0 ( ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) ≠ ∅ ↔ ∃ 𝑢 𝑢 ∈ ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) )
47 45 46 sylib ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑣𝐻𝑧𝐻 ) ) → ∃ 𝑢 𝑢 ∈ ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) )
48 36 adantr ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑣𝐻𝑧𝐻 ) ) ∧ 𝑢 ∈ ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) ) → 𝑣𝐻 )
49 filin ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 1st𝑣 ) ∈ 𝐹 ∧ ( 1st𝑧 ) ∈ 𝐹 ) → ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) ∈ 𝐹 )
50 34 39 43 49 syl3anc ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑣𝐻𝑧𝐻 ) ) → ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) ∈ 𝐹 )
51 50 adantr ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑣𝐻𝑧𝐻 ) ) ∧ 𝑢 ∈ ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) ) → ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) ∈ 𝐹 )
52 simpr ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑣𝐻𝑧𝐻 ) ) ∧ 𝑢 ∈ ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) ) → 𝑢 ∈ ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) )
53 id ( 𝑛 = ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) → 𝑛 = ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) )
54 53 opeliunxp2 ( ⟨ ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) , 𝑢 ⟩ ∈ 𝑛𝐹 ( { 𝑛 } × 𝑛 ) ↔ ( ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) ∈ 𝐹𝑢 ∈ ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) ) )
55 51 52 54 sylanbrc ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑣𝐻𝑧𝐻 ) ) ∧ 𝑢 ∈ ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) ) → ⟨ ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) , 𝑢 ⟩ ∈ 𝑛𝐹 ( { 𝑛 } × 𝑛 ) )
56 55 1 eleqtrrdi ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑣𝐻𝑧𝐻 ) ) ∧ 𝑢 ∈ ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) ) → ⟨ ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) , 𝑢 ⟩ ∈ 𝐻 )
57 fvex ( 1st𝑣 ) ∈ V
58 57 inex1 ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) ∈ V
59 vex 𝑢 ∈ V
60 58 59 op1st ( 1st ‘ ⟨ ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) , 𝑢 ⟩ ) = ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) )
61 inss1 ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) ⊆ ( 1st𝑣 )
62 60 61 eqsstri ( 1st ‘ ⟨ ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) , 𝑢 ⟩ ) ⊆ ( 1st𝑣 )
63 vex 𝑣 ∈ V
64 opex ⟨ ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) , 𝑢 ⟩ ∈ V
65 1 2 63 64 filnetlem1 ( 𝑣 𝐷 ⟨ ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) , 𝑢 ⟩ ↔ ( ( 𝑣𝐻 ∧ ⟨ ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) , 𝑢 ⟩ ∈ 𝐻 ) ∧ ( 1st ‘ ⟨ ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) , 𝑢 ⟩ ) ⊆ ( 1st𝑣 ) ) )
66 62 65 mpbiran2 ( 𝑣 𝐷 ⟨ ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) , 𝑢 ⟩ ↔ ( 𝑣𝐻 ∧ ⟨ ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) , 𝑢 ⟩ ∈ 𝐻 ) )
67 48 56 66 sylanbrc ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑣𝐻𝑧𝐻 ) ) ∧ 𝑢 ∈ ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) ) → 𝑣 𝐷 ⟨ ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) , 𝑢 ⟩ )
68 40 adantr ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑣𝐻𝑧𝐻 ) ) ∧ 𝑢 ∈ ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) ) → 𝑧𝐻 )
69 inss2 ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) ⊆ ( 1st𝑧 )
70 60 69 eqsstri ( 1st ‘ ⟨ ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) , 𝑢 ⟩ ) ⊆ ( 1st𝑧 )
71 vex 𝑧 ∈ V
72 1 2 71 64 filnetlem1 ( 𝑧 𝐷 ⟨ ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) , 𝑢 ⟩ ↔ ( ( 𝑧𝐻 ∧ ⟨ ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) , 𝑢 ⟩ ∈ 𝐻 ) ∧ ( 1st ‘ ⟨ ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) , 𝑢 ⟩ ) ⊆ ( 1st𝑧 ) ) )
73 70 72 mpbiran2 ( 𝑧 𝐷 ⟨ ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) , 𝑢 ⟩ ↔ ( 𝑧𝐻 ∧ ⟨ ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) , 𝑢 ⟩ ∈ 𝐻 ) )
74 68 56 73 sylanbrc ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑣𝐻𝑧𝐻 ) ) ∧ 𝑢 ∈ ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) ) → 𝑧 𝐷 ⟨ ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) , 𝑢 ⟩ )
75 breq2 ( 𝑤 = ⟨ ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) , 𝑢 ⟩ → ( 𝑣 𝐷 𝑤𝑣 𝐷 ⟨ ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) , 𝑢 ⟩ ) )
76 breq2 ( 𝑤 = ⟨ ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) , 𝑢 ⟩ → ( 𝑧 𝐷 𝑤𝑧 𝐷 ⟨ ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) , 𝑢 ⟩ ) )
77 75 76 anbi12d ( 𝑤 = ⟨ ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) , 𝑢 ⟩ → ( ( 𝑣 𝐷 𝑤𝑧 𝐷 𝑤 ) ↔ ( 𝑣 𝐷 ⟨ ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) , 𝑢 ⟩ ∧ 𝑧 𝐷 ⟨ ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) , 𝑢 ⟩ ) ) )
78 64 77 spcev ( ( 𝑣 𝐷 ⟨ ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) , 𝑢 ⟩ ∧ 𝑧 𝐷 ⟨ ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) , 𝑢 ⟩ ) → ∃ 𝑤 ( 𝑣 𝐷 𝑤𝑧 𝐷 𝑤 ) )
79 67 74 78 syl2anc ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑣𝐻𝑧𝐻 ) ) ∧ 𝑢 ∈ ( ( 1st𝑣 ) ∩ ( 1st𝑧 ) ) ) → ∃ 𝑤 ( 𝑣 𝐷 𝑤𝑧 𝐷 𝑤 ) )
80 47 79 exlimddv ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑣𝐻𝑧𝐻 ) ) → ∃ 𝑤 ( 𝑣 𝐷 𝑤𝑧 𝐷 𝑤 ) )
81 80 ralrimivva ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ∀ 𝑣𝐻𝑧𝐻𝑤 ( 𝑣 𝐷 𝑤𝑧 𝐷 𝑤 ) )
82 codir ( ( 𝐻 × 𝐻 ) ⊆ ( 𝐷𝐷 ) ↔ ∀ 𝑣𝐻𝑧𝐻𝑤 ( 𝑣 𝐷 𝑤𝑧 𝐷 𝑤 ) )
83 81 82 sylibr ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝐻 × 𝐻 ) ⊆ ( 𝐷𝐷 ) )
84 vex 𝑤 ∈ V
85 1 2 63 84 filnetlem1 ( 𝑣 𝐷 𝑤 ↔ ( ( 𝑣𝐻𝑤𝐻 ) ∧ ( 1st𝑤 ) ⊆ ( 1st𝑣 ) ) )
86 85 simplbi ( 𝑣 𝐷 𝑤 → ( 𝑣𝐻𝑤𝐻 ) )
87 86 simpld ( 𝑣 𝐷 𝑤𝑣𝐻 )
88 1 2 84 71 filnetlem1 ( 𝑤 𝐷 𝑧 ↔ ( ( 𝑤𝐻𝑧𝐻 ) ∧ ( 1st𝑧 ) ⊆ ( 1st𝑤 ) ) )
89 88 simplbi ( 𝑤 𝐷 𝑧 → ( 𝑤𝐻𝑧𝐻 ) )
90 89 simprd ( 𝑤 𝐷 𝑧𝑧𝐻 )
91 87 90 anim12i ( ( 𝑣 𝐷 𝑤𝑤 𝐷 𝑧 ) → ( 𝑣𝐻𝑧𝐻 ) )
92 88 simprbi ( 𝑤 𝐷 𝑧 → ( 1st𝑧 ) ⊆ ( 1st𝑤 ) )
93 85 simprbi ( 𝑣 𝐷 𝑤 → ( 1st𝑤 ) ⊆ ( 1st𝑣 ) )
94 92 93 sylan9ssr ( ( 𝑣 𝐷 𝑤𝑤 𝐷 𝑧 ) → ( 1st𝑧 ) ⊆ ( 1st𝑣 ) )
95 1 2 63 71 filnetlem1 ( 𝑣 𝐷 𝑧 ↔ ( ( 𝑣𝐻𝑧𝐻 ) ∧ ( 1st𝑧 ) ⊆ ( 1st𝑣 ) ) )
96 91 94 95 sylanbrc ( ( 𝑣 𝐷 𝑤𝑤 𝐷 𝑧 ) → 𝑣 𝐷 𝑧 )
97 96 ax-gen 𝑧 ( ( 𝑣 𝐷 𝑤𝑤 𝐷 𝑧 ) → 𝑣 𝐷 𝑧 )
98 97 gen2 𝑣𝑤𝑧 ( ( 𝑣 𝐷 𝑤𝑤 𝐷 𝑧 ) → 𝑣 𝐷 𝑧 )
99 cotr ( ( 𝐷𝐷 ) ⊆ 𝐷 ↔ ∀ 𝑣𝑤𝑧 ( ( 𝑣 𝐷 𝑤𝑤 𝐷 𝑧 ) → 𝑣 𝐷 𝑧 ) )
100 98 99 mpbir ( 𝐷𝐷 ) ⊆ 𝐷
101 83 100 jctil ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( ( 𝐷𝐷 ) ⊆ 𝐷 ∧ ( 𝐻 × 𝐻 ) ⊆ ( 𝐷𝐷 ) ) )
102 filtop ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝑋𝐹 )
103 xpexg ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑋𝐹 ) → ( 𝐹 × 𝑋 ) ∈ V )
104 102 103 mpdan ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝐹 × 𝑋 ) ∈ V )
105 104 30 ssexd ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐻 ∈ V )
106 105 105 xpexd ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝐻 × 𝐻 ) ∈ V )
107 ssexg ( ( 𝐷 ⊆ ( 𝐻 × 𝐻 ) ∧ ( 𝐻 × 𝐻 ) ∈ V ) → 𝐷 ∈ V )
108 13 106 107 sylancr ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐷 ∈ V )
109 21 isdir ( 𝐷 ∈ V → ( 𝐷 ∈ DirRel ↔ ( ( Rel 𝐷 ∧ ( I ↾ 𝐻 ) ⊆ 𝐷 ) ∧ ( ( 𝐷𝐷 ) ⊆ 𝐷 ∧ ( 𝐻 × 𝐻 ) ⊆ ( 𝐷𝐷 ) ) ) ) )
110 108 109 syl ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝐷 ∈ DirRel ↔ ( ( Rel 𝐷 ∧ ( I ↾ 𝐻 ) ⊆ 𝐷 ) ∧ ( ( 𝐷𝐷 ) ⊆ 𝐷 ∧ ( 𝐻 × 𝐻 ) ⊆ ( 𝐷𝐷 ) ) ) ) )
111 33 101 110 mpbir2and ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐷 ∈ DirRel )
112 30 111 jca ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝐻 ⊆ ( 𝐹 × 𝑋 ) ∧ 𝐷 ∈ DirRel ) )
113 21 112 pm3.2i ( 𝐻 = 𝐷 ∧ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝐻 ⊆ ( 𝐹 × 𝑋 ) ∧ 𝐷 ∈ DirRel ) ) )