| Step | Hyp | Ref | Expression | 
						
							| 1 |  | isubgredg.v | ⊢ 𝑉  =  ( Vtx ‘ 𝐺 ) | 
						
							| 2 |  | isubgredg.e | ⊢ 𝐸  =  ( Edg ‘ 𝐺 ) | 
						
							| 3 |  | isubgredg.h | ⊢ 𝐻  =  ( 𝐺  ISubGr  𝑆 ) | 
						
							| 4 |  | isubgredg.i | ⊢ 𝐼  =  ( Edg ‘ 𝐻 ) | 
						
							| 5 | 3 | fveq2i | ⊢ ( iEdg ‘ 𝐻 )  =  ( iEdg ‘ ( 𝐺  ISubGr  𝑆 ) ) | 
						
							| 6 |  | eqid | ⊢ ( iEdg ‘ 𝐺 )  =  ( iEdg ‘ 𝐺 ) | 
						
							| 7 | 1 6 | isubgriedg | ⊢ ( ( 𝐺  ∈  𝑊  ∧  𝑆  ⊆  𝑉 )  →  ( iEdg ‘ ( 𝐺  ISubGr  𝑆 ) )  =  ( ( iEdg ‘ 𝐺 )  ↾  { 𝑥  ∈  dom  ( iEdg ‘ 𝐺 )  ∣  ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 )  ⊆  𝑆 } ) ) | 
						
							| 8 | 5 7 | eqtrid | ⊢ ( ( 𝐺  ∈  𝑊  ∧  𝑆  ⊆  𝑉 )  →  ( iEdg ‘ 𝐻 )  =  ( ( iEdg ‘ 𝐺 )  ↾  { 𝑥  ∈  dom  ( iEdg ‘ 𝐺 )  ∣  ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 )  ⊆  𝑆 } ) ) | 
						
							| 9 | 8 | rneqd | ⊢ ( ( 𝐺  ∈  𝑊  ∧  𝑆  ⊆  𝑉 )  →  ran  ( iEdg ‘ 𝐻 )  =  ran  ( ( iEdg ‘ 𝐺 )  ↾  { 𝑥  ∈  dom  ( iEdg ‘ 𝐺 )  ∣  ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 )  ⊆  𝑆 } ) ) | 
						
							| 10 |  | resss | ⊢ ( ( iEdg ‘ 𝐺 )  ↾  { 𝑥  ∈  dom  ( iEdg ‘ 𝐺 )  ∣  ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 )  ⊆  𝑆 } )  ⊆  ( iEdg ‘ 𝐺 ) | 
						
							| 11 |  | rnss | ⊢ ( ( ( iEdg ‘ 𝐺 )  ↾  { 𝑥  ∈  dom  ( iEdg ‘ 𝐺 )  ∣  ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 )  ⊆  𝑆 } )  ⊆  ( iEdg ‘ 𝐺 )  →  ran  ( ( iEdg ‘ 𝐺 )  ↾  { 𝑥  ∈  dom  ( iEdg ‘ 𝐺 )  ∣  ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 )  ⊆  𝑆 } )  ⊆  ran  ( iEdg ‘ 𝐺 ) ) | 
						
							| 12 | 10 11 | mp1i | ⊢ ( ( 𝐺  ∈  𝑊  ∧  𝑆  ⊆  𝑉 )  →  ran  ( ( iEdg ‘ 𝐺 )  ↾  { 𝑥  ∈  dom  ( iEdg ‘ 𝐺 )  ∣  ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 )  ⊆  𝑆 } )  ⊆  ran  ( iEdg ‘ 𝐺 ) ) | 
						
							| 13 | 9 12 | eqsstrd | ⊢ ( ( 𝐺  ∈  𝑊  ∧  𝑆  ⊆  𝑉 )  →  ran  ( iEdg ‘ 𝐻 )  ⊆  ran  ( iEdg ‘ 𝐺 ) ) | 
						
							| 14 |  | edgval | ⊢ ( Edg ‘ 𝐻 )  =  ran  ( iEdg ‘ 𝐻 ) | 
						
							| 15 | 4 14 | eqtri | ⊢ 𝐼  =  ran  ( iEdg ‘ 𝐻 ) | 
						
							| 16 |  | edgval | ⊢ ( Edg ‘ 𝐺 )  =  ran  ( iEdg ‘ 𝐺 ) | 
						
							| 17 | 2 16 | eqtri | ⊢ 𝐸  =  ran  ( iEdg ‘ 𝐺 ) | 
						
							| 18 | 13 15 17 | 3sstr4g | ⊢ ( ( 𝐺  ∈  𝑊  ∧  𝑆  ⊆  𝑉 )  →  𝐼  ⊆  𝐸 ) |