This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sizusglecusglem1

Description: Lemma 1 for sizusglecusg . (Contributed by Alexander van der Vekens, 12-Jan-2018) (Revised by AV, 13-Nov-2020)

Ref Expression
Hypotheses fusgrmaxsize.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
fusgrmaxsize.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
usgrsscusgra.h ⊢ 𝑉 = ( Vtx ‘ 𝐻 )
usgrsscusgra.f ⊢ 𝐹 = ( Edg ‘ 𝐻 )
Assertion sizusglecusglem1 ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph ) → ( I ↾ 𝐸 ) : 𝐸 –1-1→ 𝐹 )

Proof

Step Hyp Ref Expression
1 fusgrmaxsize.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 fusgrmaxsize.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 usgrsscusgra.h ⊢ 𝑉 = ( Vtx ‘ 𝐻 )
4 usgrsscusgra.f ⊢ 𝐹 = ( Edg ‘ 𝐻 )
5 f1oi ⊢ ( I ↾ 𝐸 ) : 𝐸 –1-1-onto→ 𝐸
6 f1of1 ⊢ ( ( I ↾ 𝐸 ) : 𝐸 –1-1-onto→ 𝐸 → ( I ↾ 𝐸 ) : 𝐸 –1-1→ 𝐸 )
7 5 6 ax-mp ⊢ ( I ↾ 𝐸 ) : 𝐸 –1-1→ 𝐸
8 1 2 3 4 usgredgsscusgredg ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph ) → 𝐸 ⊆ 𝐹 )
9 f1ss ⊢ ( ( ( I ↾ 𝐸 ) : 𝐸 –1-1→ 𝐸 ∧ 𝐸 ⊆ 𝐹 ) → ( I ↾ 𝐸 ) : 𝐸 –1-1→ 𝐹 )
10 7 8 9 sylancr ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph ) → ( I ↾ 𝐸 ) : 𝐸 –1-1→ 𝐹 )