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

Theorem filnetlem2 32676
 Description: Lemma for filnet 32679. The field of the direction. (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
filnetlem2 (( I ↾ 𝐻) ⊆ 𝐷𝐷 ⊆ (𝐻 × 𝐻))
Distinct variable groups:   𝑥,𝑦,𝑛,𝐹   𝑥,𝐻,𝑦
Allowed substitution hints:   𝐷(𝑥,𝑦,𝑛)   𝐻(𝑛)

Proof of Theorem filnetlem2
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 idref 6658 . . 3 (( I ↾ 𝐻) ⊆ 𝐷 ↔ ∀𝑧𝐻 𝑧𝐷𝑧)
2 ssid 3761 . . . . . 6 (1st𝑧) ⊆ (1st𝑧)
3 filnet.h . . . . . . 7 𝐻 = 𝑛𝐹 ({𝑛} × 𝑛)
4 filnet.d . . . . . . 7 𝐷 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐻𝑦𝐻) ∧ (1st𝑦) ⊆ (1st𝑥))}
5 vex 3339 . . . . . . 7 𝑧 ∈ V
63, 4, 5, 5filnetlem1 32675 . . . . . 6 (𝑧𝐷𝑧 ↔ ((𝑧𝐻𝑧𝐻) ∧ (1st𝑧) ⊆ (1st𝑧)))
72, 6mpbiran2 992 . . . . 5 (𝑧𝐷𝑧 ↔ (𝑧𝐻𝑧𝐻))
87biimpri 218 . . . 4 ((𝑧𝐻𝑧𝐻) → 𝑧𝐷𝑧)
98anidms 680 . . 3 (𝑧𝐻𝑧𝐷𝑧)
101, 9mprgbir 3061 . 2 ( I ↾ 𝐻) ⊆ 𝐷
11 opabssxp 5346 . . 3 {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐻𝑦𝐻) ∧ (1st𝑦) ⊆ (1st𝑥))} ⊆ (𝐻 × 𝐻)
124, 11eqsstri 3772 . 2 𝐷 ⊆ (𝐻 × 𝐻)
1310, 12pm3.2i 470 1 (( I ↾ 𝐻) ⊆ 𝐷𝐷 ⊆ (𝐻 × 𝐻))
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 383   = wceq 1628   ∈ wcel 2135   ⊆ wss 3711  {csn 4317  ∪ ciun 4668   class class class wbr 4800  {copab 4860   I cid 5169   × cxp 5260   ↾ cres 5264  ‘cfv 6045  1st c1st 7327 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736  ax-sep 4929  ax-nul 4937  ax-pr 5051 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-eu 2607  df-mo 2608  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-ne 2929  df-ral 3051  df-rex 3052  df-reu 3053  df-rab 3055  df-v 3338  df-sbc 3573  df-csb 3671  df-dif 3714  df-un 3716  df-in 3718  df-ss 3725  df-nul 4055  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4585  df-iun 4670  df-br 4801  df-opab 4861  df-mpt 4878  df-id 5170  df-xp 5268  df-rel 5269  df-cnv 5270  df-co 5271  df-dm 5272  df-rn 5273  df-res 5274  df-ima 5275  df-iota 6008  df-fun 6047  df-fn 6048  df-f 6049  df-f1 6050  df-fo 6051  df-f1o 6052  df-fv 6053 This theorem is referenced by:  filnetlem3  32677  filnetlem4  32678
 Copyright terms: Public domain W3C validator