filnetlem1

Description: Lemma for filnet . Change variables. (Contributed by Jeff Hankins, 13-Dec-2009) (Revised by Mario Carneiro, 8-Aug-2015)

Step	Hyp	Ref	Expression
1		filnet.h	⊢ 𝐻 = ∪ 𝑛 ∈ 𝐹 ( { 𝑛 } × 𝑛 )
2		filnet.d	⊢ 𝐷 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) ∧ ( 1^st ‘ 𝑦 ) ⊆ ( 1^st ‘ 𝑥 ) ) }
3		filnetlem1.a	⊢ 𝐴 ∈ V
4		filnetlem1.b	⊢ 𝐵 ∈ V
5		fveq2	⊢ ( 𝑥 = 𝐴 → ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝐴 ) )
6	5	sseq2d	⊢ ( 𝑥 = 𝐴 → ( ( 1^st ‘ 𝑦 ) ⊆ ( 1^st ‘ 𝑥 ) ↔ ( 1^st ‘ 𝑦 ) ⊆ ( 1^st ‘ 𝐴 ) ) )
7		fveq2	⊢ ( 𝑦 = 𝐵 → ( 1^st ‘ 𝑦 ) = ( 1^st ‘ 𝐵 ) )
8	7	sseq1d	⊢ ( 𝑦 = 𝐵 → ( ( 1^st ‘ 𝑦 ) ⊆ ( 1^st ‘ 𝐴 ) ↔ ( 1^st ‘ 𝐵 ) ⊆ ( 1^st ‘ 𝐴 ) ) )
9	6 8	sylan9bb	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ( 1^st ‘ 𝑦 ) ⊆ ( 1^st ‘ 𝑥 ) ↔ ( 1^st ‘ 𝐵 ) ⊆ ( 1^st ‘ 𝐴 ) ) )
10	9 2	brab2a	⊢ ( 𝐴 𝐷 𝐵 ↔ ( ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻 ) ∧ ( 1^st ‘ 𝐵 ) ⊆ ( 1^st ‘ 𝐴 ) ) )

Metamath Proof Explorer