Users' Mathboxes Mathbox for Jeff Hankins < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  filnetlem3 Structured version   Visualization version   GIF version

Theorem filnetlem3 32693
Description: Lemma for filnet 32695. (Contributed by Jeff Hankins, 13-Dec-2009.) (Revised by Mario Carneiro, 8-Aug-2015.)
Hypotheses
Ref Expression
filnet.h 𝐻 = 𝑛𝐹 ({𝑛} × 𝑛)
filnet.d 𝐷 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐻𝑦𝐻) ∧ (1st𝑦) ⊆ (1st𝑥))}
Assertion
Ref Expression
filnetlem3 (𝐻 = 𝐷 ∧ (𝐹 ∈ (Fil‘𝑋) → (𝐻 ⊆ (𝐹 × 𝑋) ∧ 𝐷 ∈ DirRel)))
Distinct variable groups:   𝑥,𝑦,𝑛,𝐹   𝑥,𝐻,𝑦   𝑛,𝑋
Allowed substitution hints:   𝐷(𝑥,𝑦,𝑛)   𝐻(𝑛)   𝑋(𝑥,𝑦)

Proof of Theorem filnetlem3
Dummy variables 𝑢 𝑣 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dmresi 5666 . . . . . 6 dom ( I ↾ 𝐻) = 𝐻
2 filnet.h . . . . . . . . 9 𝐻 = 𝑛𝐹 ({𝑛} × 𝑛)
3 filnet.d . . . . . . . . 9 𝐷 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐻𝑦𝐻) ∧ (1st𝑦) ⊆ (1st𝑥))}
42, 3filnetlem2 32692 . . . . . . . 8 (( I ↾ 𝐻) ⊆ 𝐷𝐷 ⊆ (𝐻 × 𝐻))
54simpli 472 . . . . . . 7 ( I ↾ 𝐻) ⊆ 𝐷
6 dmss 5521 . . . . . . 7 (( I ↾ 𝐻) ⊆ 𝐷 → dom ( I ↾ 𝐻) ⊆ dom 𝐷)
75, 6ax-mp 5 . . . . . 6 dom ( I ↾ 𝐻) ⊆ dom 𝐷
81, 7eqsstr3i 3830 . . . . 5 𝐻 ⊆ dom 𝐷
9 ssun1 3972 . . . . 5 dom 𝐷 ⊆ (dom 𝐷 ∪ ran 𝐷)
108, 9sstri 3804 . . . 4 𝐻 ⊆ (dom 𝐷 ∪ ran 𝐷)
11 dmrnssfld 5582 . . . 4 (dom 𝐷 ∪ ran 𝐷) ⊆ 𝐷
1210, 11sstri 3804 . . 3 𝐻 𝐷
134simpri 475 . . . . 5 𝐷 ⊆ (𝐻 × 𝐻)
14 uniss 4649 . . . . 5 (𝐷 ⊆ (𝐻 × 𝐻) → 𝐷 (𝐻 × 𝐻))
15 uniss 4649 . . . . 5 ( 𝐷 (𝐻 × 𝐻) → 𝐷 (𝐻 × 𝐻))
1613, 14, 15mp2b 10 . . . 4 𝐷 (𝐻 × 𝐻)
17 unixpss 5432 . . . . 5 (𝐻 × 𝐻) ⊆ (𝐻𝐻)
18 unidm 3952 . . . . 5 (𝐻𝐻) = 𝐻
1917, 18sseqtri 3831 . . . 4 (𝐻 × 𝐻) ⊆ 𝐻
2016, 19sstri 3804 . . 3 𝐷𝐻
2112, 20eqssi 3811 . 2 𝐻 = 𝐷
22 filelss 21865 . . . . . . . 8 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛𝐹) → 𝑛𝑋)
23 xpss2 5327 . . . . . . . 8 (𝑛𝑋 → ({𝑛} × 𝑛) ⊆ ({𝑛} × 𝑋))
2422, 23syl 17 . . . . . . 7 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛𝐹) → ({𝑛} × 𝑛) ⊆ ({𝑛} × 𝑋))
2524ralrimiva 3153 . . . . . 6 (𝐹 ∈ (Fil‘𝑋) → ∀𝑛𝐹 ({𝑛} × 𝑛) ⊆ ({𝑛} × 𝑋))
26 ss2iun 4724 . . . . . 6 (∀𝑛𝐹 ({𝑛} × 𝑛) ⊆ ({𝑛} × 𝑋) → 𝑛𝐹 ({𝑛} × 𝑛) ⊆ 𝑛𝐹 ({𝑛} × 𝑋))
2725, 26syl 17 . . . . 5 (𝐹 ∈ (Fil‘𝑋) → 𝑛𝐹 ({𝑛} × 𝑛) ⊆ 𝑛𝐹 ({𝑛} × 𝑋))
28 iunxpconst 5372 . . . . 5 𝑛𝐹 ({𝑛} × 𝑋) = (𝐹 × 𝑋)
2927, 28syl6sseq 3845 . . . 4 (𝐹 ∈ (Fil‘𝑋) → 𝑛𝐹 ({𝑛} × 𝑛) ⊆ (𝐹 × 𝑋))
302, 29syl5eqss 3843 . . 3 (𝐹 ∈ (Fil‘𝑋) → 𝐻 ⊆ (𝐹 × 𝑋))
315a1i 11 . . . . 5 (𝐹 ∈ (Fil‘𝑋) → ( I ↾ 𝐻) ⊆ 𝐷)
323relopabi 5444 . . . . 5 Rel 𝐷
3331, 32jctil 511 . . . 4 (𝐹 ∈ (Fil‘𝑋) → (Rel 𝐷 ∧ ( I ↾ 𝐻) ⊆ 𝐷))
34 simpl 470 . . . . . . . . . 10 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑣𝐻𝑧𝐻)) → 𝐹 ∈ (Fil‘𝑋))
3530adantr 468 . . . . . . . . . . . 12 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑣𝐻𝑧𝐻)) → 𝐻 ⊆ (𝐹 × 𝑋))
36 simprl 778 . . . . . . . . . . . 12 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑣𝐻𝑧𝐻)) → 𝑣𝐻)
3735, 36sseldd 3796 . . . . . . . . . . 11 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑣𝐻𝑧𝐻)) → 𝑣 ∈ (𝐹 × 𝑋))
38 xp1st 7427 . . . . . . . . . . 11 (𝑣 ∈ (𝐹 × 𝑋) → (1st𝑣) ∈ 𝐹)
3937, 38syl 17 . . . . . . . . . 10 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑣𝐻𝑧𝐻)) → (1st𝑣) ∈ 𝐹)
40 simprr 780 . . . . . . . . . . . 12 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑣𝐻𝑧𝐻)) → 𝑧𝐻)
4135, 40sseldd 3796 . . . . . . . . . . 11 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑣𝐻𝑧𝐻)) → 𝑧 ∈ (𝐹 × 𝑋))
42 xp1st 7427 . . . . . . . . . . 11 (𝑧 ∈ (𝐹 × 𝑋) → (1st𝑧) ∈ 𝐹)
4341, 42syl 17 . . . . . . . . . 10 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑣𝐻𝑧𝐻)) → (1st𝑧) ∈ 𝐹)
44 filinn0 21873 . . . . . . . . . 10 ((𝐹 ∈ (Fil‘𝑋) ∧ (1st𝑣) ∈ 𝐹 ∧ (1st𝑧) ∈ 𝐹) → ((1st𝑣) ∩ (1st𝑧)) ≠ ∅)
4534, 39, 43, 44syl3anc 1483 . . . . . . . . 9 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑣𝐻𝑧𝐻)) → ((1st𝑣) ∩ (1st𝑧)) ≠ ∅)
46 n0 4129 . . . . . . . . 9 (((1st𝑣) ∩ (1st𝑧)) ≠ ∅ ↔ ∃𝑢 𝑢 ∈ ((1st𝑣) ∩ (1st𝑧)))
4745, 46sylib 209 . . . . . . . 8 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑣𝐻𝑧𝐻)) → ∃𝑢 𝑢 ∈ ((1st𝑣) ∩ (1st𝑧)))
4836adantr 468 . . . . . . . . . 10 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝑣𝐻𝑧𝐻)) ∧ 𝑢 ∈ ((1st𝑣) ∩ (1st𝑧))) → 𝑣𝐻)
49 filin 21867 . . . . . . . . . . . . . 14 ((𝐹 ∈ (Fil‘𝑋) ∧ (1st𝑣) ∈ 𝐹 ∧ (1st𝑧) ∈ 𝐹) → ((1st𝑣) ∩ (1st𝑧)) ∈ 𝐹)
5034, 39, 43, 49syl3anc 1483 . . . . . . . . . . . . 13 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑣𝐻𝑧𝐻)) → ((1st𝑣) ∩ (1st𝑧)) ∈ 𝐹)
5150adantr 468 . . . . . . . . . . . 12 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝑣𝐻𝑧𝐻)) ∧ 𝑢 ∈ ((1st𝑣) ∩ (1st𝑧))) → ((1st𝑣) ∩ (1st𝑧)) ∈ 𝐹)
52 simpr 473 . . . . . . . . . . . 12 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝑣𝐻𝑧𝐻)) ∧ 𝑢 ∈ ((1st𝑣) ∩ (1st𝑧))) → 𝑢 ∈ ((1st𝑣) ∩ (1st𝑧)))
53 id 22 . . . . . . . . . . . . 13 (𝑛 = ((1st𝑣) ∩ (1st𝑧)) → 𝑛 = ((1st𝑣) ∩ (1st𝑧)))
5453opeliunxp2 5459 . . . . . . . . . . . 12 (⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩ ∈ 𝑛𝐹 ({𝑛} × 𝑛) ↔ (((1st𝑣) ∩ (1st𝑧)) ∈ 𝐹𝑢 ∈ ((1st𝑣) ∩ (1st𝑧))))
5551, 52, 54sylanbrc 574 . . . . . . . . . . 11 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝑣𝐻𝑧𝐻)) ∧ 𝑢 ∈ ((1st𝑣) ∩ (1st𝑧))) → ⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩ ∈ 𝑛𝐹 ({𝑛} × 𝑛))
5655, 2syl6eleqr 2895 . . . . . . . . . 10 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝑣𝐻𝑧𝐻)) ∧ 𝑢 ∈ ((1st𝑣) ∩ (1st𝑧))) → ⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩ ∈ 𝐻)
57 fvex 6418 . . . . . . . . . . . . . 14 (1st𝑣) ∈ V
5857inex1 4991 . . . . . . . . . . . . 13 ((1st𝑣) ∩ (1st𝑧)) ∈ V
59 vex 3393 . . . . . . . . . . . . 13 𝑢 ∈ V
6058, 59op1st 7403 . . . . . . . . . . . 12 (1st ‘⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩) = ((1st𝑣) ∩ (1st𝑧))
61 inss1 4026 . . . . . . . . . . . 12 ((1st𝑣) ∩ (1st𝑧)) ⊆ (1st𝑣)
6260, 61eqsstri 3829 . . . . . . . . . . 11 (1st ‘⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩) ⊆ (1st𝑣)
63 vex 3393 . . . . . . . . . . . 12 𝑣 ∈ V
64 opex 5119 . . . . . . . . . . . 12 ⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩ ∈ V
652, 3, 63, 64filnetlem1 32691 . . . . . . . . . . 11 (𝑣𝐷⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩ ↔ ((𝑣𝐻 ∧ ⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩ ∈ 𝐻) ∧ (1st ‘⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩) ⊆ (1st𝑣)))
6662, 65mpbiran2 692 . . . . . . . . . 10 (𝑣𝐷⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩ ↔ (𝑣𝐻 ∧ ⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩ ∈ 𝐻))
6748, 56, 66sylanbrc 574 . . . . . . . . 9 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝑣𝐻𝑧𝐻)) ∧ 𝑢 ∈ ((1st𝑣) ∩ (1st𝑧))) → 𝑣𝐷⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩)
6840adantr 468 . . . . . . . . . 10 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝑣𝐻𝑧𝐻)) ∧ 𝑢 ∈ ((1st𝑣) ∩ (1st𝑧))) → 𝑧𝐻)
69 inss2 4027 . . . . . . . . . . . 12 ((1st𝑣) ∩ (1st𝑧)) ⊆ (1st𝑧)
7060, 69eqsstri 3829 . . . . . . . . . . 11 (1st ‘⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩) ⊆ (1st𝑧)
71 vex 3393 . . . . . . . . . . . 12 𝑧 ∈ V
722, 3, 71, 64filnetlem1 32691 . . . . . . . . . . 11 (𝑧𝐷⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩ ↔ ((𝑧𝐻 ∧ ⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩ ∈ 𝐻) ∧ (1st ‘⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩) ⊆ (1st𝑧)))
7370, 72mpbiran2 692 . . . . . . . . . 10 (𝑧𝐷⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩ ↔ (𝑧𝐻 ∧ ⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩ ∈ 𝐻))
7468, 56, 73sylanbrc 574 . . . . . . . . 9 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝑣𝐻𝑧𝐻)) ∧ 𝑢 ∈ ((1st𝑣) ∩ (1st𝑧))) → 𝑧𝐷⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩)
75 breq2 4844 . . . . . . . . . . 11 (𝑤 = ⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩ → (𝑣𝐷𝑤𝑣𝐷⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩))
76 breq2 4844 . . . . . . . . . . 11 (𝑤 = ⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩ → (𝑧𝐷𝑤𝑧𝐷⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩))
7775, 76anbi12d 618 . . . . . . . . . 10 (𝑤 = ⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩ → ((𝑣𝐷𝑤𝑧𝐷𝑤) ↔ (𝑣𝐷⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩ ∧ 𝑧𝐷⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩)))
7864, 77spcev 3492 . . . . . . . . 9 ((𝑣𝐷⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩ ∧ 𝑧𝐷⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩) → ∃𝑤(𝑣𝐷𝑤𝑧𝐷𝑤))
7967, 74, 78syl2anc 575 . . . . . . . 8 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝑣𝐻𝑧𝐻)) ∧ 𝑢 ∈ ((1st𝑣) ∩ (1st𝑧))) → ∃𝑤(𝑣𝐷𝑤𝑧𝐷𝑤))
8047, 79exlimddv 2028 . . . . . . 7 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑣𝐻𝑧𝐻)) → ∃𝑤(𝑣𝐷𝑤𝑧𝐷𝑤))
8180ralrimivva 3158 . . . . . 6 (𝐹 ∈ (Fil‘𝑋) → ∀𝑣𝐻𝑧𝐻𝑤(𝑣𝐷𝑤𝑧𝐷𝑤))
82 codir 5724 . . . . . 6 ((𝐻 × 𝐻) ⊆ (𝐷𝐷) ↔ ∀𝑣𝐻𝑧𝐻𝑤(𝑣𝐷𝑤𝑧𝐷𝑤))
8381, 82sylibr 225 . . . . 5 (𝐹 ∈ (Fil‘𝑋) → (𝐻 × 𝐻) ⊆ (𝐷𝐷))
84 vex 3393 . . . . . . . . . . . . 13 𝑤 ∈ V
852, 3, 63, 84filnetlem1 32691 . . . . . . . . . . . 12 (𝑣𝐷𝑤 ↔ ((𝑣𝐻𝑤𝐻) ∧ (1st𝑤) ⊆ (1st𝑣)))
8685simplbi 487 . . . . . . . . . . 11 (𝑣𝐷𝑤 → (𝑣𝐻𝑤𝐻))
8786simpld 484 . . . . . . . . . 10 (𝑣𝐷𝑤𝑣𝐻)
882, 3, 84, 71filnetlem1 32691 . . . . . . . . . . . 12 (𝑤𝐷𝑧 ↔ ((𝑤𝐻𝑧𝐻) ∧ (1st𝑧) ⊆ (1st𝑤)))
8988simplbi 487 . . . . . . . . . . 11 (𝑤𝐷𝑧 → (𝑤𝐻𝑧𝐻))
9089simprd 485 . . . . . . . . . 10 (𝑤𝐷𝑧𝑧𝐻)
9187, 90anim12i 602 . . . . . . . . 9 ((𝑣𝐷𝑤𝑤𝐷𝑧) → (𝑣𝐻𝑧𝐻))
9288simprbi 486 . . . . . . . . . 10 (𝑤𝐷𝑧 → (1st𝑧) ⊆ (1st𝑤))
9385simprbi 486 . . . . . . . . . 10 (𝑣𝐷𝑤 → (1st𝑤) ⊆ (1st𝑣))
9492, 93sylan9ssr 3809 . . . . . . . . 9 ((𝑣𝐷𝑤𝑤𝐷𝑧) → (1st𝑧) ⊆ (1st𝑣))
952, 3, 63, 71filnetlem1 32691 . . . . . . . . 9 (𝑣𝐷𝑧 ↔ ((𝑣𝐻𝑧𝐻) ∧ (1st𝑧) ⊆ (1st𝑣)))
9691, 94, 95sylanbrc 574 . . . . . . . 8 ((𝑣𝐷𝑤𝑤𝐷𝑧) → 𝑣𝐷𝑧)
9796ax-gen 1880 . . . . . . 7 𝑧((𝑣𝐷𝑤𝑤𝐷𝑧) → 𝑣𝐷𝑧)
9897gen2 1881 . . . . . 6 𝑣𝑤𝑧((𝑣𝐷𝑤𝑤𝐷𝑧) → 𝑣𝐷𝑧)
99 cotr 5715 . . . . . 6 ((𝐷𝐷) ⊆ 𝐷 ↔ ∀𝑣𝑤𝑧((𝑣𝐷𝑤𝑤𝐷𝑧) → 𝑣𝐷𝑧))
10098, 99mpbir 222 . . . . 5 (𝐷𝐷) ⊆ 𝐷
10183, 100jctil 511 . . . 4 (𝐹 ∈ (Fil‘𝑋) → ((𝐷𝐷) ⊆ 𝐷 ∧ (𝐻 × 𝐻) ⊆ (𝐷𝐷)))
102 filtop 21868 . . . . . . . . 9 (𝐹 ∈ (Fil‘𝑋) → 𝑋𝐹)
103 xpexg 7187 . . . . . . . . 9 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑋𝐹) → (𝐹 × 𝑋) ∈ V)
104102, 103mpdan 670 . . . . . . . 8 (𝐹 ∈ (Fil‘𝑋) → (𝐹 × 𝑋) ∈ V)
105104, 30ssexd 4997 . . . . . . 7 (𝐹 ∈ (Fil‘𝑋) → 𝐻 ∈ V)
106 xpexg 7187 . . . . . . 7 ((𝐻 ∈ V ∧ 𝐻 ∈ V) → (𝐻 × 𝐻) ∈ V)
107105, 105, 106syl2anc 575 . . . . . 6 (𝐹 ∈ (Fil‘𝑋) → (𝐻 × 𝐻) ∈ V)
108 ssexg 4996 . . . . . 6 ((𝐷 ⊆ (𝐻 × 𝐻) ∧ (𝐻 × 𝐻) ∈ V) → 𝐷 ∈ V)
10913, 107, 108sylancr 577 . . . . 5 (𝐹 ∈ (Fil‘𝑋) → 𝐷 ∈ V)
11021isdir 17433 . . . . 5 (𝐷 ∈ V → (𝐷 ∈ DirRel ↔ ((Rel 𝐷 ∧ ( I ↾ 𝐻) ⊆ 𝐷) ∧ ((𝐷𝐷) ⊆ 𝐷 ∧ (𝐻 × 𝐻) ⊆ (𝐷𝐷)))))
111109, 110syl 17 . . . 4 (𝐹 ∈ (Fil‘𝑋) → (𝐷 ∈ DirRel ↔ ((Rel 𝐷 ∧ ( I ↾ 𝐻) ⊆ 𝐷) ∧ ((𝐷𝐷) ⊆ 𝐷 ∧ (𝐻 × 𝐻) ⊆ (𝐷𝐷)))))
11233, 101, 111mpbir2and 695 . . 3 (𝐹 ∈ (Fil‘𝑋) → 𝐷 ∈ DirRel)
11330, 112jca 503 . 2 (𝐹 ∈ (Fil‘𝑋) → (𝐻 ⊆ (𝐹 × 𝑋) ∧ 𝐷 ∈ DirRel))
11421, 113pm3.2i 458 1 (𝐻 = 𝐷 ∧ (𝐹 ∈ (Fil‘𝑋) → (𝐻 ⊆ (𝐹 × 𝑋) ∧ 𝐷 ∈ DirRel)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  wal 1635   = wceq 1637  wex 1859  wcel 2158  wne 2977  wral 3095  Vcvv 3390  cun 3764  cin 3765  wss 3766  c0 4113  {csn 4367  cop 4373   cuni 4626   ciun 4708   class class class wbr 4840  {copab 4902   I cid 5215   × cxp 5306  ccnv 5307  dom cdm 5308  ran crn 5309  cres 5310  ccom 5312  Rel wrel 5313  cfv 6098  1st c1st 7393  DirRelcdir 17429  Filcfil 21858
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-8 2160  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784  ax-sep 4971  ax-nul 4980  ax-pow 5032  ax-pr 5093  ax-un 7176
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1865  df-sb 2063  df-eu 2636  df-mo 2637  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-ne 2978  df-nel 3081  df-ral 3100  df-rex 3101  df-reu 3102  df-rab 3104  df-v 3392  df-sbc 3631  df-csb 3726  df-dif 3769  df-un 3771  df-in 3773  df-ss 3780  df-nul 4114  df-if 4277  df-pw 4350  df-sn 4368  df-pr 4370  df-op 4374  df-uni 4627  df-iun 4710  df-br 4841  df-opab 4903  df-mpt 4920  df-id 5216  df-xp 5314  df-rel 5315  df-cnv 5316  df-co 5317  df-dm 5318  df-rn 5319  df-res 5320  df-ima 5321  df-iota 6061  df-fun 6100  df-fn 6101  df-f 6102  df-f1 6103  df-fo 6104  df-f1o 6105  df-fv 6106  df-1st 7395  df-dir 17431  df-fbas 19947  df-fil 21859
This theorem is referenced by:  filnetlem4  32694
  Copyright terms: Public domain W3C validator