Metamath Proof Explorer

Theorem uhgrspan1

Description: The induced subgraph S of a hypergraph G obtained by removing one vertex is actually a subgraph of G . A subgraph is called induced orspanned by a subset of vertices of a graph if it contains all edges of the original graph that join two vertices of the subgraph (see section I.1 in Bollobas p. 2 and section 1.1 in Diestel p. 4). (Contributed by AV, 19-Nov-2020)

Ref Expression
Hypotheses uhgrspan1.v ⊢ V = Vtx ⁡ G
uhgrspan1.i ⊢ I = iEdg ⁡ G
uhgrspan1.f ⊢ F = i ∈ dom ⁡ I | N ∉ I ⁡ i
uhgrspan1.s ⊢ S = V ∖ N I ↾ F
Assertion uhgrspan1 ⊢ G ∈ UHGraph ∧ N ∈ V → S SubGraph G

Proof

Step Hyp Ref Expression
1 uhgrspan1.v ⊢ V = Vtx ⁡ G
2 uhgrspan1.i ⊢ I = iEdg ⁡ G
3 uhgrspan1.f ⊢ F = i ∈ dom ⁡ I | N ∉ I ⁡ i
4 uhgrspan1.s ⊢ S = V ∖ N I ↾ F
5 difssd ⊢ G ∈ UHGraph ∧ N ∈ V → V ∖ N ⊆ V
6 1 2 3 4 uhgrspan1lem3 ⊢ iEdg ⁡ S = I ↾ F
7 resresdm ⊢ iEdg ⁡ S = I ↾ F → iEdg ⁡ S = I ↾ dom ⁡ iEdg ⁡ S
8 6 7 mp1i ⊢ G ∈ UHGraph ∧ N ∈ V → iEdg ⁡ S = I ↾ dom ⁡ iEdg ⁡ S
9 2 uhgrfun ⊢ G ∈ UHGraph → Fun ⁡ I
10 fvelima ⊢ Fun ⁡ I ∧ c ∈ I F → ∃ j ∈ F I ⁡ j = c
11 10 ex ⊢ Fun ⁡ I → c ∈ I F → ∃ j ∈ F I ⁡ j = c
12 9 11 syl ⊢ G ∈ UHGraph → c ∈ I F → ∃ j ∈ F I ⁡ j = c
13 12 adantr ⊢ G ∈ UHGraph ∧ N ∈ V → c ∈ I F → ∃ j ∈ F I ⁡ j = c
14 eqidd ⊢ i = j → N = N
15 fveq2 ⊢ i = j → I ⁡ i = I ⁡ j
16 14 15 neleq12d ⊢ i = j → N ∉ I ⁡ i ↔ N ∉ I ⁡ j
17 16 3 elrab2 ⊢ j ∈ F ↔ j ∈ dom ⁡ I ∧ N ∉ I ⁡ j
18 fvexd ⊢ G ∈ UHGraph ∧ N ∈ V ∧ j ∈ dom ⁡ I ∧ N ∉ I ⁡ j → I ⁡ j ∈ V
19 1 2 uhgrss ⊢ G ∈ UHGraph ∧ j ∈ dom ⁡ I → I ⁡ j ⊆ V
20 19 ad2ant2r ⊢ G ∈ UHGraph ∧ N ∈ V ∧ j ∈ dom ⁡ I ∧ N ∉ I ⁡ j → I ⁡ j ⊆ V
21 simprr ⊢ G ∈ UHGraph ∧ N ∈ V ∧ j ∈ dom ⁡ I ∧ N ∉ I ⁡ j → N ∉ I ⁡ j
22 elpwdifsn ⊢ I ⁡ j ∈ V ∧ I ⁡ j ⊆ V ∧ N ∉ I ⁡ j → I ⁡ j ∈ 𝒫 V ∖ N
23 18 20 21 22 syl3anc ⊢ G ∈ UHGraph ∧ N ∈ V ∧ j ∈ dom ⁡ I ∧ N ∉ I ⁡ j → I ⁡ j ∈ 𝒫 V ∖ N
24 eleq1 ⊢ c = I ⁡ j → c ∈ 𝒫 V ∖ N ↔ I ⁡ j ∈ 𝒫 V ∖ N
25 24 eqcoms ⊢ I ⁡ j = c → c ∈ 𝒫 V ∖ N ↔ I ⁡ j ∈ 𝒫 V ∖ N
26 23 25 syl5ibrcom ⊢ G ∈ UHGraph ∧ N ∈ V ∧ j ∈ dom ⁡ I ∧ N ∉ I ⁡ j → I ⁡ j = c → c ∈ 𝒫 V ∖ N
27 26 ex ⊢ G ∈ UHGraph ∧ N ∈ V → j ∈ dom ⁡ I ∧ N ∉ I ⁡ j → I ⁡ j = c → c ∈ 𝒫 V ∖ N
28 17 27 syl5bi ⊢ G ∈ UHGraph ∧ N ∈ V → j ∈ F → I ⁡ j = c → c ∈ 𝒫 V ∖ N
29 28 rexlimdv ⊢ G ∈ UHGraph ∧ N ∈ V → ∃ j ∈ F I ⁡ j = c → c ∈ 𝒫 V ∖ N
30 13 29 syld ⊢ G ∈ UHGraph ∧ N ∈ V → c ∈ I F → c ∈ 𝒫 V ∖ N
31 30 ssrdv ⊢ G ∈ UHGraph ∧ N ∈ V → I F ⊆ 𝒫 V ∖ N
32 opex ⊢ V ∖ N I ↾ F ∈ V
33 4 32 eqeltri ⊢ S ∈ V
34 33 a1i ⊢ N ∈ V → S ∈ V
35 1 2 3 4 uhgrspan1lem2 ⊢ Vtx ⁡ S = V ∖ N
36 35 eqcomi ⊢ V ∖ N = Vtx ⁡ S
37 eqid ⊢ iEdg ⁡ S = iEdg ⁡ S
38 6 rneqi ⊢ ran ⁡ iEdg ⁡ S = ran ⁡ I ↾ F
39 edgval ⊢ Edg ⁡ S = ran ⁡ iEdg ⁡ S
40 df-ima ⊢ I F = ran ⁡ I ↾ F
41 38 39 40 3eqtr4ri ⊢ I F = Edg ⁡ S
42 36 1 37 2 41 issubgr ⊢ G ∈ UHGraph ∧ S ∈ V → S SubGraph G ↔ V ∖ N ⊆ V ∧ iEdg ⁡ S = I ↾ dom ⁡ iEdg ⁡ S ∧ I F ⊆ 𝒫 V ∖ N
43 34 42 sylan2 ⊢ G ∈ UHGraph ∧ N ∈ V → S SubGraph G ↔ V ∖ N ⊆ V ∧ iEdg ⁡ S = I ↾ dom ⁡ iEdg ⁡ S ∧ I F ⊆ 𝒫 V ∖ N
44 5 8 31 43 mpbir3and ⊢ G ∈ UHGraph ∧ N ∈ V → S SubGraph G