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 36362
Description: Lemma for filnet 36364. (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 6071 . . . . . 6 dom ( I ↾ 𝐻) = 𝐻
2 filnet.h . . . . . . . . 9 𝐻 = 𝑛𝐹 ({𝑛} × 𝑛)
3 filnet.d . . . . . . . . 9 𝐷 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐻𝑦𝐻) ∧ (1st𝑦) ⊆ (1st𝑥))}
42, 3filnetlem2 36361 . . . . . . . 8 (( I ↾ 𝐻) ⊆ 𝐷𝐷 ⊆ (𝐻 × 𝐻))
54simpli 483 . . . . . . 7 ( I ↾ 𝐻) ⊆ 𝐷
6 dmss 5915 . . . . . . 7 (( I ↾ 𝐻) ⊆ 𝐷 → dom ( I ↾ 𝐻) ⊆ dom 𝐷)
75, 6ax-mp 5 . . . . . 6 dom ( I ↾ 𝐻) ⊆ dom 𝐷
81, 7eqsstrri 4030 . . . . 5 𝐻 ⊆ dom 𝐷
9 ssun1 4187 . . . . 5 dom 𝐷 ⊆ (dom 𝐷 ∪ ran 𝐷)
108, 9sstri 4004 . . . 4 𝐻 ⊆ (dom 𝐷 ∪ ran 𝐷)
11 dmrnssfld 5986 . . . 4 (dom 𝐷 ∪ ran 𝐷) ⊆ 𝐷
1210, 11sstri 4004 . . 3 𝐻 𝐷
134simpri 485 . . . . 5 𝐷 ⊆ (𝐻 × 𝐻)
14 uniss 4919 . . . . 5 (𝐷 ⊆ (𝐻 × 𝐻) → 𝐷 (𝐻 × 𝐻))
15 uniss 4919 . . . . 5 ( 𝐷 (𝐻 × 𝐻) → 𝐷 (𝐻 × 𝐻))
1613, 14, 15mp2b 10 . . . 4 𝐷 (𝐻 × 𝐻)
17 unixpss 5822 . . . . 5 (𝐻 × 𝐻) ⊆ (𝐻𝐻)
18 unidm 4166 . . . . 5 (𝐻𝐻) = 𝐻
1917, 18sseqtri 4031 . . . 4 (𝐻 × 𝐻) ⊆ 𝐻
2016, 19sstri 4004 . . 3 𝐷𝐻
2112, 20eqssi 4011 . 2 𝐻 = 𝐷
22 filelss 23875 . . . . . . . 8 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛𝐹) → 𝑛𝑋)
23 xpss2 5708 . . . . . . . 8 (𝑛𝑋 → ({𝑛} × 𝑛) ⊆ ({𝑛} × 𝑋))
2422, 23syl 17 . . . . . . 7 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑛𝐹) → ({𝑛} × 𝑛) ⊆ ({𝑛} × 𝑋))
2524ralrimiva 3143 . . . . . 6 (𝐹 ∈ (Fil‘𝑋) → ∀𝑛𝐹 ({𝑛} × 𝑛) ⊆ ({𝑛} × 𝑋))
26 ss2iun 5014 . . . . . 6 (∀𝑛𝐹 ({𝑛} × 𝑛) ⊆ ({𝑛} × 𝑋) → 𝑛𝐹 ({𝑛} × 𝑛) ⊆ 𝑛𝐹 ({𝑛} × 𝑋))
2725, 26syl 17 . . . . 5 (𝐹 ∈ (Fil‘𝑋) → 𝑛𝐹 ({𝑛} × 𝑛) ⊆ 𝑛𝐹 ({𝑛} × 𝑋))
28 iunxpconst 5760 . . . . 5 𝑛𝐹 ({𝑛} × 𝑋) = (𝐹 × 𝑋)
2927, 28sseqtrdi 4045 . . . 4 (𝐹 ∈ (Fil‘𝑋) → 𝑛𝐹 ({𝑛} × 𝑛) ⊆ (𝐹 × 𝑋))
302, 29eqsstrid 4043 . . 3 (𝐹 ∈ (Fil‘𝑋) → 𝐻 ⊆ (𝐹 × 𝑋))
315a1i 11 . . . . 5 (𝐹 ∈ (Fil‘𝑋) → ( I ↾ 𝐻) ⊆ 𝐷)
323relopabiv 5832 . . . . 5 Rel 𝐷
3331, 32jctil 519 . . . 4 (𝐹 ∈ (Fil‘𝑋) → (Rel 𝐷 ∧ ( I ↾ 𝐻) ⊆ 𝐷))
34 simpl 482 . . . . . . . . . 10 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑣𝐻𝑧𝐻)) → 𝐹 ∈ (Fil‘𝑋))
3530adantr 480 . . . . . . . . . . . 12 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑣𝐻𝑧𝐻)) → 𝐻 ⊆ (𝐹 × 𝑋))
36 simprl 771 . . . . . . . . . . . 12 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑣𝐻𝑧𝐻)) → 𝑣𝐻)
3735, 36sseldd 3995 . . . . . . . . . . 11 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑣𝐻𝑧𝐻)) → 𝑣 ∈ (𝐹 × 𝑋))
38 xp1st 8044 . . . . . . . . . . 11 (𝑣 ∈ (𝐹 × 𝑋) → (1st𝑣) ∈ 𝐹)
3937, 38syl 17 . . . . . . . . . 10 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑣𝐻𝑧𝐻)) → (1st𝑣) ∈ 𝐹)
40 simprr 773 . . . . . . . . . . . 12 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑣𝐻𝑧𝐻)) → 𝑧𝐻)
4135, 40sseldd 3995 . . . . . . . . . . 11 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑣𝐻𝑧𝐻)) → 𝑧 ∈ (𝐹 × 𝑋))
42 xp1st 8044 . . . . . . . . . . 11 (𝑧 ∈ (𝐹 × 𝑋) → (1st𝑧) ∈ 𝐹)
4341, 42syl 17 . . . . . . . . . 10 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑣𝐻𝑧𝐻)) → (1st𝑧) ∈ 𝐹)
44 filinn0 23883 . . . . . . . . . 10 ((𝐹 ∈ (Fil‘𝑋) ∧ (1st𝑣) ∈ 𝐹 ∧ (1st𝑧) ∈ 𝐹) → ((1st𝑣) ∩ (1st𝑧)) ≠ ∅)
4534, 39, 43, 44syl3anc 1370 . . . . . . . . 9 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑣𝐻𝑧𝐻)) → ((1st𝑣) ∩ (1st𝑧)) ≠ ∅)
46 n0 4358 . . . . . . . . 9 (((1st𝑣) ∩ (1st𝑧)) ≠ ∅ ↔ ∃𝑢 𝑢 ∈ ((1st𝑣) ∩ (1st𝑧)))
4745, 46sylib 218 . . . . . . . 8 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑣𝐻𝑧𝐻)) → ∃𝑢 𝑢 ∈ ((1st𝑣) ∩ (1st𝑧)))
4836adantr 480 . . . . . . . . . 10 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝑣𝐻𝑧𝐻)) ∧ 𝑢 ∈ ((1st𝑣) ∩ (1st𝑧))) → 𝑣𝐻)
49 filin 23877 . . . . . . . . . . . . . 14 ((𝐹 ∈ (Fil‘𝑋) ∧ (1st𝑣) ∈ 𝐹 ∧ (1st𝑧) ∈ 𝐹) → ((1st𝑣) ∩ (1st𝑧)) ∈ 𝐹)
5034, 39, 43, 49syl3anc 1370 . . . . . . . . . . . . 13 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑣𝐻𝑧𝐻)) → ((1st𝑣) ∩ (1st𝑧)) ∈ 𝐹)
5150adantr 480 . . . . . . . . . . . 12 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝑣𝐻𝑧𝐻)) ∧ 𝑢 ∈ ((1st𝑣) ∩ (1st𝑧))) → ((1st𝑣) ∩ (1st𝑧)) ∈ 𝐹)
52 simpr 484 . . . . . . . . . . . 12 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝑣𝐻𝑧𝐻)) ∧ 𝑢 ∈ ((1st𝑣) ∩ (1st𝑧))) → 𝑢 ∈ ((1st𝑣) ∩ (1st𝑧)))
53 id 22 . . . . . . . . . . . . 13 (𝑛 = ((1st𝑣) ∩ (1st𝑧)) → 𝑛 = ((1st𝑣) ∩ (1st𝑧)))
5453opeliunxp2 5851 . . . . . . . . . . . 12 (⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩ ∈ 𝑛𝐹 ({𝑛} × 𝑛) ↔ (((1st𝑣) ∩ (1st𝑧)) ∈ 𝐹𝑢 ∈ ((1st𝑣) ∩ (1st𝑧))))
5551, 52, 54sylanbrc 583 . . . . . . . . . . 11 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝑣𝐻𝑧𝐻)) ∧ 𝑢 ∈ ((1st𝑣) ∩ (1st𝑧))) → ⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩ ∈ 𝑛𝐹 ({𝑛} × 𝑛))
5655, 2eleqtrrdi 2849 . . . . . . . . . 10 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝑣𝐻𝑧𝐻)) ∧ 𝑢 ∈ ((1st𝑣) ∩ (1st𝑧))) → ⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩ ∈ 𝐻)
57 fvex 6919 . . . . . . . . . . . . . 14 (1st𝑣) ∈ V
5857inex1 5322 . . . . . . . . . . . . 13 ((1st𝑣) ∩ (1st𝑧)) ∈ V
59 vex 3481 . . . . . . . . . . . . 13 𝑢 ∈ V
6058, 59op1st 8020 . . . . . . . . . . . 12 (1st ‘⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩) = ((1st𝑣) ∩ (1st𝑧))
61 inss1 4244 . . . . . . . . . . . 12 ((1st𝑣) ∩ (1st𝑧)) ⊆ (1st𝑣)
6260, 61eqsstri 4029 . . . . . . . . . . 11 (1st ‘⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩) ⊆ (1st𝑣)
63 vex 3481 . . . . . . . . . . . 12 𝑣 ∈ V
64 opex 5474 . . . . . . . . . . . 12 ⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩ ∈ V
652, 3, 63, 64filnetlem1 36360 . . . . . . . . . . 11 (𝑣𝐷⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩ ↔ ((𝑣𝐻 ∧ ⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩ ∈ 𝐻) ∧ (1st ‘⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩) ⊆ (1st𝑣)))
6662, 65mpbiran2 710 . . . . . . . . . 10 (𝑣𝐷⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩ ↔ (𝑣𝐻 ∧ ⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩ ∈ 𝐻))
6748, 56, 66sylanbrc 583 . . . . . . . . 9 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝑣𝐻𝑧𝐻)) ∧ 𝑢 ∈ ((1st𝑣) ∩ (1st𝑧))) → 𝑣𝐷⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩)
6840adantr 480 . . . . . . . . . 10 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝑣𝐻𝑧𝐻)) ∧ 𝑢 ∈ ((1st𝑣) ∩ (1st𝑧))) → 𝑧𝐻)
69 inss2 4245 . . . . . . . . . . . 12 ((1st𝑣) ∩ (1st𝑧)) ⊆ (1st𝑧)
7060, 69eqsstri 4029 . . . . . . . . . . 11 (1st ‘⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩) ⊆ (1st𝑧)
71 vex 3481 . . . . . . . . . . . 12 𝑧 ∈ V
722, 3, 71, 64filnetlem1 36360 . . . . . . . . . . 11 (𝑧𝐷⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩ ↔ ((𝑧𝐻 ∧ ⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩ ∈ 𝐻) ∧ (1st ‘⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩) ⊆ (1st𝑧)))
7370, 72mpbiran2 710 . . . . . . . . . 10 (𝑧𝐷⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩ ↔ (𝑧𝐻 ∧ ⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩ ∈ 𝐻))
7468, 56, 73sylanbrc 583 . . . . . . . . 9 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝑣𝐻𝑧𝐻)) ∧ 𝑢 ∈ ((1st𝑣) ∩ (1st𝑧))) → 𝑧𝐷⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩)
75 breq2 5151 . . . . . . . . . . 11 (𝑤 = ⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩ → (𝑣𝐷𝑤𝑣𝐷⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩))
76 breq2 5151 . . . . . . . . . . 11 (𝑤 = ⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩ → (𝑧𝐷𝑤𝑧𝐷⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩))
7775, 76anbi12d 632 . . . . . . . . . 10 (𝑤 = ⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩ → ((𝑣𝐷𝑤𝑧𝐷𝑤) ↔ (𝑣𝐷⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩ ∧ 𝑧𝐷⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩)))
7864, 77spcev 3605 . . . . . . . . 9 ((𝑣𝐷⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩ ∧ 𝑧𝐷⟨((1st𝑣) ∩ (1st𝑧)), 𝑢⟩) → ∃𝑤(𝑣𝐷𝑤𝑧𝐷𝑤))
7967, 74, 78syl2anc 584 . . . . . . . 8 (((𝐹 ∈ (Fil‘𝑋) ∧ (𝑣𝐻𝑧𝐻)) ∧ 𝑢 ∈ ((1st𝑣) ∩ (1st𝑧))) → ∃𝑤(𝑣𝐷𝑤𝑧𝐷𝑤))
8047, 79exlimddv 1932 . . . . . . 7 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑣𝐻𝑧𝐻)) → ∃𝑤(𝑣𝐷𝑤𝑧𝐷𝑤))
8180ralrimivva 3199 . . . . . 6 (𝐹 ∈ (Fil‘𝑋) → ∀𝑣𝐻𝑧𝐻𝑤(𝑣𝐷𝑤𝑧𝐷𝑤))
82 codir 6142 . . . . . 6 ((𝐻 × 𝐻) ⊆ (𝐷𝐷) ↔ ∀𝑣𝐻𝑧𝐻𝑤(𝑣𝐷𝑤𝑧𝐷𝑤))
8381, 82sylibr 234 . . . . 5 (𝐹 ∈ (Fil‘𝑋) → (𝐻 × 𝐻) ⊆ (𝐷𝐷))
84 vex 3481 . . . . . . . . . . . . 13 𝑤 ∈ V
852, 3, 63, 84filnetlem1 36360 . . . . . . . . . . . 12 (𝑣𝐷𝑤 ↔ ((𝑣𝐻𝑤𝐻) ∧ (1st𝑤) ⊆ (1st𝑣)))
8685simplbi 497 . . . . . . . . . . 11 (𝑣𝐷𝑤 → (𝑣𝐻𝑤𝐻))
8786simpld 494 . . . . . . . . . 10 (𝑣𝐷𝑤𝑣𝐻)
882, 3, 84, 71filnetlem1 36360 . . . . . . . . . . . 12 (𝑤𝐷𝑧 ↔ ((𝑤𝐻𝑧𝐻) ∧ (1st𝑧) ⊆ (1st𝑤)))
8988simplbi 497 . . . . . . . . . . 11 (𝑤𝐷𝑧 → (𝑤𝐻𝑧𝐻))
9089simprd 495 . . . . . . . . . 10 (𝑤𝐷𝑧𝑧𝐻)
9187, 90anim12i 613 . . . . . . . . 9 ((𝑣𝐷𝑤𝑤𝐷𝑧) → (𝑣𝐻𝑧𝐻))
9288simprbi 496 . . . . . . . . . 10 (𝑤𝐷𝑧 → (1st𝑧) ⊆ (1st𝑤))
9385simprbi 496 . . . . . . . . . 10 (𝑣𝐷𝑤 → (1st𝑤) ⊆ (1st𝑣))
9492, 93sylan9ssr 4009 . . . . . . . . 9 ((𝑣𝐷𝑤𝑤𝐷𝑧) → (1st𝑧) ⊆ (1st𝑣))
952, 3, 63, 71filnetlem1 36360 . . . . . . . . 9 (𝑣𝐷𝑧 ↔ ((𝑣𝐻𝑧𝐻) ∧ (1st𝑧) ⊆ (1st𝑣)))
9691, 94, 95sylanbrc 583 . . . . . . . 8 ((𝑣𝐷𝑤𝑤𝐷𝑧) → 𝑣𝐷𝑧)
9796ax-gen 1791 . . . . . . 7 𝑧((𝑣𝐷𝑤𝑤𝐷𝑧) → 𝑣𝐷𝑧)
9897gen2 1792 . . . . . 6 𝑣𝑤𝑧((𝑣𝐷𝑤𝑤𝐷𝑧) → 𝑣𝐷𝑧)
99 cotr 6132 . . . . . 6 ((𝐷𝐷) ⊆ 𝐷 ↔ ∀𝑣𝑤𝑧((𝑣𝐷𝑤𝑤𝐷𝑧) → 𝑣𝐷𝑧))
10098, 99mpbir 231 . . . . 5 (𝐷𝐷) ⊆ 𝐷
10183, 100jctil 519 . . . 4 (𝐹 ∈ (Fil‘𝑋) → ((𝐷𝐷) ⊆ 𝐷 ∧ (𝐻 × 𝐻) ⊆ (𝐷𝐷)))
102 filtop 23878 . . . . . . . . 9 (𝐹 ∈ (Fil‘𝑋) → 𝑋𝐹)
103 xpexg 7768 . . . . . . . . 9 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑋𝐹) → (𝐹 × 𝑋) ∈ V)
104102, 103mpdan 687 . . . . . . . 8 (𝐹 ∈ (Fil‘𝑋) → (𝐹 × 𝑋) ∈ V)
105104, 30ssexd 5329 . . . . . . 7 (𝐹 ∈ (Fil‘𝑋) → 𝐻 ∈ V)
106105, 105xpexd 7769 . . . . . 6 (𝐹 ∈ (Fil‘𝑋) → (𝐻 × 𝐻) ∈ V)
107 ssexg 5328 . . . . . 6 ((𝐷 ⊆ (𝐻 × 𝐻) ∧ (𝐻 × 𝐻) ∈ V) → 𝐷 ∈ V)
10813, 106, 107sylancr 587 . . . . 5 (𝐹 ∈ (Fil‘𝑋) → 𝐷 ∈ V)
10921isdir 18655 . . . . 5 (𝐷 ∈ V → (𝐷 ∈ DirRel ↔ ((Rel 𝐷 ∧ ( I ↾ 𝐻) ⊆ 𝐷) ∧ ((𝐷𝐷) ⊆ 𝐷 ∧ (𝐻 × 𝐻) ⊆ (𝐷𝐷)))))
110108, 109syl 17 . . . 4 (𝐹 ∈ (Fil‘𝑋) → (𝐷 ∈ DirRel ↔ ((Rel 𝐷 ∧ ( I ↾ 𝐻) ⊆ 𝐷) ∧ ((𝐷𝐷) ⊆ 𝐷 ∧ (𝐻 × 𝐻) ⊆ (𝐷𝐷)))))
11133, 101, 110mpbir2and 713 . . 3 (𝐹 ∈ (Fil‘𝑋) → 𝐷 ∈ DirRel)
11230, 111jca 511 . 2 (𝐹 ∈ (Fil‘𝑋) → (𝐻 ⊆ (𝐹 × 𝑋) ∧ 𝐷 ∈ DirRel))
11321, 112pm3.2i 470 1 (𝐻 = 𝐷 ∧ (𝐹 ∈ (Fil‘𝑋) → (𝐻 ⊆ (𝐹 × 𝑋) ∧ 𝐷 ∈ DirRel)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wal 1534   = wceq 1536  wex 1775  wcel 2105  wne 2937  wral 3058  Vcvv 3477  cun 3960  cin 3961  wss 3962  c0 4338  {csn 4630  cop 4636   cuni 4911   ciun 4995   class class class wbr 5147  {copab 5209   I cid 5581   × cxp 5686  ccnv 5687  dom cdm 5688  ran crn 5689  cres 5690  ccom 5692  Rel wrel 5693  cfv 6562  1st c1st 8010  DirRelcdir 18651  Filcfil 23868
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-1st 8012  df-dir 18653  df-fbas 21378  df-fil 23869
This theorem is referenced by:  filnetlem4  36363
  Copyright terms: Public domain W3C validator