Theorem filnetlem2

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

	Ref	Expression
Hypotheses	filnet.h	⊢ 𝐻 = ∪ 𝑛 ∈ 𝐹 ( { 𝑛 } × 𝑛 )
	filnet.d	⊢ 𝐷 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) ∧ ( 1st ‘ 𝑦 ) ⊆ ( 1st ‘ 𝑥 ) ) }
Assertion	filnetlem2	⊢ ( ( I ↾ 𝐻 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ( 𝐻 × 𝐻 ) )

Proof

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