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

Metamath Proof Explorer

Theorem issubgr

Description: The property of a set to be a subgraph of another set. (Contributed by AV, 16-Nov-2020)

Ref Expression
Hypotheses issubgr.v ⊢ 𝑉 = ( Vtx ‘ 𝑆 )
issubgr.a ⊢ 𝐴 = ( Vtx ‘ 𝐺 )
issubgr.i ⊢ 𝐼 = ( iEdg ‘ 𝑆 )
issubgr.b ⊢ 𝐵 = ( iEdg ‘ 𝐺 )
issubgr.e ⊢ 𝐸 = ( Edg ‘ 𝑆 )
Assertion issubgr ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ 𝑈 ) → ( 𝑆 SubGraph 𝐺 ↔ ( 𝑉 ⊆ 𝐴 ∧ 𝐼 = ( 𝐵 ↾ dom 𝐼 ) ∧ 𝐸 ⊆ 𝒫 𝑉 ) ) )

Proof

Step Hyp Ref Expression
1 issubgr.v ⊢ 𝑉 = ( Vtx ‘ 𝑆 )
2 issubgr.a ⊢ 𝐴 = ( Vtx ‘ 𝐺 )
3 issubgr.i ⊢ 𝐼 = ( iEdg ‘ 𝑆 )
4 issubgr.b ⊢ 𝐵 = ( iEdg ‘ 𝐺 )
5 issubgr.e ⊢ 𝐸 = ( Edg ‘ 𝑆 )
6 fveq2 ⊢ ( 𝑠 = 𝑆 → ( Vtx ‘ 𝑠 ) = ( Vtx ‘ 𝑆 ) )
7 6 adantr ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑔 = 𝐺 ) → ( Vtx ‘ 𝑠 ) = ( Vtx ‘ 𝑆 ) )
8 fveq2 ⊢ ( 𝑔 = 𝐺 → ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) )
9 8 adantl ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑔 = 𝐺 ) → ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) )
10 7 9 sseq12d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑔 = 𝐺 ) → ( ( Vtx ‘ 𝑠 ) ⊆ ( Vtx ‘ 𝑔 ) ↔ ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ) )
11 fveq2 ⊢ ( 𝑠 = 𝑆 → ( iEdg ‘ 𝑠 ) = ( iEdg ‘ 𝑆 ) )
12 11 adantr ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑔 = 𝐺 ) → ( iEdg ‘ 𝑠 ) = ( iEdg ‘ 𝑆 ) )
13 fveq2 ⊢ ( 𝑔 = 𝐺 → ( iEdg ‘ 𝑔 ) = ( iEdg ‘ 𝐺 ) )
14 13 adantl ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑔 = 𝐺 ) → ( iEdg ‘ 𝑔 ) = ( iEdg ‘ 𝐺 ) )
15 11 dmeqd ⊢ ( 𝑠 = 𝑆 → dom ( iEdg ‘ 𝑠 ) = dom ( iEdg ‘ 𝑆 ) )
16 15 adantr ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑔 = 𝐺 ) → dom ( iEdg ‘ 𝑠 ) = dom ( iEdg ‘ 𝑆 ) )
17 14 16 reseq12d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑔 = 𝐺 ) → ( ( iEdg ‘ 𝑔 ) ↾ dom ( iEdg ‘ 𝑠 ) ) = ( ( iEdg ‘ 𝐺 ) ↾ dom ( iEdg ‘ 𝑆 ) ) )
18 12 17 eqeq12d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑔 = 𝐺 ) → ( ( iEdg ‘ 𝑠 ) = ( ( iEdg ‘ 𝑔 ) ↾ dom ( iEdg ‘ 𝑠 ) ) ↔ ( iEdg ‘ 𝑆 ) = ( ( iEdg ‘ 𝐺 ) ↾ dom ( iEdg ‘ 𝑆 ) ) ) )
19 fveq2 ⊢ ( 𝑠 = 𝑆 → ( Edg ‘ 𝑠 ) = ( Edg ‘ 𝑆 ) )
20 6 pweqd ⊢ ( 𝑠 = 𝑆 → 𝒫 ( Vtx ‘ 𝑠 ) = 𝒫 ( Vtx ‘ 𝑆 ) )
21 19 20 sseq12d ⊢ ( 𝑠 = 𝑆 → ( ( Edg ‘ 𝑠 ) ⊆ 𝒫 ( Vtx ‘ 𝑠 ) ↔ ( Edg ‘ 𝑆 ) ⊆ 𝒫 ( Vtx ‘ 𝑆 ) ) )
22 21 adantr ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑔 = 𝐺 ) → ( ( Edg ‘ 𝑠 ) ⊆ 𝒫 ( Vtx ‘ 𝑠 ) ↔ ( Edg ‘ 𝑆 ) ⊆ 𝒫 ( Vtx ‘ 𝑆 ) ) )
23 10 18 22 3anbi123d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑔 = 𝐺 ) → ( ( ( Vtx ‘ 𝑠 ) ⊆ ( Vtx ‘ 𝑔 ) ∧ ( iEdg ‘ 𝑠 ) = ( ( iEdg ‘ 𝑔 ) ↾ dom ( iEdg ‘ 𝑠 ) ) ∧ ( Edg ‘ 𝑠 ) ⊆ 𝒫 ( Vtx ‘ 𝑠 ) ) ↔ ( ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑆 ) = ( ( iEdg ‘ 𝐺 ) ↾ dom ( iEdg ‘ 𝑆 ) ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 ( Vtx ‘ 𝑆 ) ) ) )
24 df-subgr ⊢ SubGraph = { ⟨ 𝑠 , 𝑔 ⟩ ∣ ( ( Vtx ‘ 𝑠 ) ⊆ ( Vtx ‘ 𝑔 ) ∧ ( iEdg ‘ 𝑠 ) = ( ( iEdg ‘ 𝑔 ) ↾ dom ( iEdg ‘ 𝑠 ) ) ∧ ( Edg ‘ 𝑠 ) ⊆ 𝒫 ( Vtx ‘ 𝑠 ) ) }
25 23 24 brabga ⊢ ( ( 𝑆 ∈ 𝑈 ∧ 𝐺 ∈ 𝑊 ) → ( 𝑆 SubGraph 𝐺 ↔ ( ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑆 ) = ( ( iEdg ‘ 𝐺 ) ↾ dom ( iEdg ‘ 𝑆 ) ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 ( Vtx ‘ 𝑆 ) ) ) )
26 25 ancoms ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ 𝑈 ) → ( 𝑆 SubGraph 𝐺 ↔ ( ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑆 ) = ( ( iEdg ‘ 𝐺 ) ↾ dom ( iEdg ‘ 𝑆 ) ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 ( Vtx ‘ 𝑆 ) ) ) )
27 1 2 sseq12i ⊢ ( 𝑉 ⊆ 𝐴 ↔ ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) )
28 3 dmeqi ⊢ dom 𝐼 = dom ( iEdg ‘ 𝑆 )
29 4 28 reseq12i ⊢ ( 𝐵 ↾ dom 𝐼 ) = ( ( iEdg ‘ 𝐺 ) ↾ dom ( iEdg ‘ 𝑆 ) )
30 3 29 eqeq12i ⊢ ( 𝐼 = ( 𝐵 ↾ dom 𝐼 ) ↔ ( iEdg ‘ 𝑆 ) = ( ( iEdg ‘ 𝐺 ) ↾ dom ( iEdg ‘ 𝑆 ) ) )
31 1 pweqi ⊢ 𝒫 𝑉 = 𝒫 ( Vtx ‘ 𝑆 )
32 5 31 sseq12i ⊢ ( 𝐸 ⊆ 𝒫 𝑉 ↔ ( Edg ‘ 𝑆 ) ⊆ 𝒫 ( Vtx ‘ 𝑆 ) )
33 27 30 32 3anbi123i ⊢ ( ( 𝑉 ⊆ 𝐴 ∧ 𝐼 = ( 𝐵 ↾ dom 𝐼 ) ∧ 𝐸 ⊆ 𝒫 𝑉 ) ↔ ( ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑆 ) = ( ( iEdg ‘ 𝐺 ) ↾ dom ( iEdg ‘ 𝑆 ) ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 ( Vtx ‘ 𝑆 ) ) )
34 26 33 bitr4di ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ 𝑈 ) → ( 𝑆 SubGraph 𝐺 ↔ ( 𝑉 ⊆ 𝐴 ∧ 𝐼 = ( 𝐵 ↾ dom 𝐼 ) ∧ 𝐸 ⊆ 𝒫 𝑉 ) ) )