filnetlem2 - Mathbox for Jeff Hankins

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

Theorem filnetlem2 37294

Description: Lemma for filnet 37297. 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	⊢ 𝐷 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) ∧ (1^st ‘𝑦) ⊆ (1^st ‘𝑥))}

**Assertion**
Ref	Expression
filnetlem2	⊢ (( I ↾ 𝐻) ⊆ 𝐷 ∧ 𝐷 ⊆ (𝐻 × 𝐻))

Distinct variable groups: 𝑥,𝑦,𝑛,𝐹 𝑥,𝐻,𝑦 Allowed substitution hints: 𝐷(𝑥, 𝑦, 𝑛) 𝐻(𝑛)

Proof of Theorem filnetlem2 Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		idref 7157	. . 3 ⊢ (( I ↾ 𝐻) ⊆ 𝐷 ↔ ∀𝑧 ∈ 𝐻 𝑧𝐷𝑧)
2		ssid 3934	. . . . . 6 ⊢ (1^st ‘𝑧) ⊆ (1^st ‘𝑧)
3		filnet.h	. . . . . . 7 ⊢ 𝐻 = ∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛)
4		filnet.d	. . . . . . 7 ⊢ 𝐷 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) ∧ (1^st ‘𝑦) ⊆ (1^st ‘𝑥))}
5		vex 3457	. . . . . . 7 ⊢ 𝑧 ∈ V
6	3, 4, 5, 5	filnetlem1 37293	. . . . . 6 ⊢ (𝑧𝐷𝑧 ↔ ((𝑧 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) ∧ (1^st ‘𝑧) ⊆ (1^st ‘𝑧)))
7	2, 6	mpbiran2 723	. . . . 5 ⊢ (𝑧𝐷𝑧 ↔ (𝑧 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻))
8	7	biimpri 231	. . . 4 ⊢ ((𝑧 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → 𝑧𝐷𝑧)
9	8	anidms 577	. . 3 ⊢ (𝑧 ∈ 𝐻 → 𝑧𝐷𝑧)
10	1, 9	mprgbir 3086	. 2 ⊢ ( I ↾ 𝐻) ⊆ 𝐷
11		opabssxp 5747	. . 3 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) ∧ (1^st ‘𝑦) ⊆ (1^st ‘𝑥))} ⊆ (𝐻 × 𝐻)
12	4, 11	eqsstri 3958	. 2 ⊢ 𝐷 ⊆ (𝐻 × 𝐻)
13	10, 12	pm3.2i 476	1 ⊢ (( I ↾ 𝐻) ⊆ 𝐷 ∧ 𝐷 ⊆ (𝐻 × 𝐻))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ∧ wa 401 = wceq 1569 ∈ wcel 2146 ⊆ wss 3899 {csn 4587 ∪ ciun 4953 class class class wbr 5105 {copab 5169 I cid 5548 × cxp 5652 ↾ cres 5656 ‘cfv 6546 1^st c1st 8006

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1944 ax-6 2001 ax-7 2042 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2196 ax-12 2215 ax-ext 2735 ax-sep 5251 ax-pr 5394

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2101 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-ral 3080 df-rex 3090 df-reu 3369 df-rab 3416 df-v 3455 df-sbc 3742 df-csb 3851 df-ss 3900 df-dif 4049 df-in 4093 df-un 4153 df-nul 4281 df-if 4485 df-sn 4588 df-pr 4590 df-op 4838 df-uni 4870 df-iun 4955 df-br 5106 df-opab 5170 df-mpt 5189 df-id 5549 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-iota 6500 df-fun 6548 df-fn 6549 df-f 6550 df-f1 6551 df-fo 6552 df-f1o 6553 df-fv 6554

This theorem is used by: filnetlem3 37295 filnetlem4 37296

W3C validator