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→ 𝐹 )