MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  uhgrspan1 Structured version   Visualization version   GIF version

Theorem uhgrspan1 27091
Description: The induced subgraph 𝑆 of a hypergraph 𝐺 obtained by removing one vertex is actually a subgraph of 𝐺. A subgraph is called induced or spanned 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.)
Hypotheses
Ref Expression
uhgrspan1.v 𝑉 = (Vtx‘𝐺)
uhgrspan1.i 𝐼 = (iEdg‘𝐺)
uhgrspan1.f 𝐹 = {𝑖 ∈ dom 𝐼𝑁 ∉ (𝐼𝑖)}
uhgrspan1.s 𝑆 = ⟨(𝑉 ∖ {𝑁}), (𝐼𝐹)⟩
Assertion
Ref Expression
uhgrspan1 ((𝐺 ∈ UHGraph ∧ 𝑁𝑉) → 𝑆 SubGraph 𝐺)
Distinct variable groups:   𝑖,𝐼   𝑖,𝑁
Allowed substitution hints:   𝑆(𝑖)   𝐹(𝑖)   𝐺(𝑖)   𝑉(𝑖)

Proof of Theorem uhgrspan1
Dummy variables 𝑐 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 difssd 4084 . 2 ((𝐺 ∈ UHGraph ∧ 𝑁𝑉) → (𝑉 ∖ {𝑁}) ⊆ 𝑉)
2 uhgrspan1.v . . . 4 𝑉 = (Vtx‘𝐺)
3 uhgrspan1.i . . . 4 𝐼 = (iEdg‘𝐺)
4 uhgrspan1.f . . . 4 𝐹 = {𝑖 ∈ dom 𝐼𝑁 ∉ (𝐼𝑖)}
5 uhgrspan1.s . . . 4 𝑆 = ⟨(𝑉 ∖ {𝑁}), (𝐼𝐹)⟩
62, 3, 4, 5uhgrspan1lem3 27090 . . 3 (iEdg‘𝑆) = (𝐼𝐹)
7 resresdm 6068 . . 3 ((iEdg‘𝑆) = (𝐼𝐹) → (iEdg‘𝑆) = (𝐼 ↾ dom (iEdg‘𝑆)))
86, 7mp1i 13 . 2 ((𝐺 ∈ UHGraph ∧ 𝑁𝑉) → (iEdg‘𝑆) = (𝐼 ↾ dom (iEdg‘𝑆)))
93uhgrfun 26857 . . . . . 6 (𝐺 ∈ UHGraph → Fun 𝐼)
10 fvelima 6713 . . . . . . 7 ((Fun 𝐼𝑐 ∈ (𝐼𝐹)) → ∃𝑗𝐹 (𝐼𝑗) = 𝑐)
1110ex 416 . . . . . 6 (Fun 𝐼 → (𝑐 ∈ (𝐼𝐹) → ∃𝑗𝐹 (𝐼𝑗) = 𝑐))
129, 11syl 17 . . . . 5 (𝐺 ∈ UHGraph → (𝑐 ∈ (𝐼𝐹) → ∃𝑗𝐹 (𝐼𝑗) = 𝑐))
1312adantr 484 . . . 4 ((𝐺 ∈ UHGraph ∧ 𝑁𝑉) → (𝑐 ∈ (𝐼𝐹) → ∃𝑗𝐹 (𝐼𝑗) = 𝑐))
14 eqidd 2823 . . . . . . . 8 (𝑖 = 𝑗𝑁 = 𝑁)
15 fveq2 6652 . . . . . . . 8 (𝑖 = 𝑗 → (𝐼𝑖) = (𝐼𝑗))
1614, 15neleq12d 3119 . . . . . . 7 (𝑖 = 𝑗 → (𝑁 ∉ (𝐼𝑖) ↔ 𝑁 ∉ (𝐼𝑗)))
1716, 4elrab2 3658 . . . . . 6 (𝑗𝐹 ↔ (𝑗 ∈ dom 𝐼𝑁 ∉ (𝐼𝑗)))
18 fvexd 6667 . . . . . . . . 9 (((𝐺 ∈ UHGraph ∧ 𝑁𝑉) ∧ (𝑗 ∈ dom 𝐼𝑁 ∉ (𝐼𝑗))) → (𝐼𝑗) ∈ V)
192, 3uhgrss 26855 . . . . . . . . . 10 ((𝐺 ∈ UHGraph ∧ 𝑗 ∈ dom 𝐼) → (𝐼𝑗) ⊆ 𝑉)
2019ad2ant2r 746 . . . . . . . . 9 (((𝐺 ∈ UHGraph ∧ 𝑁𝑉) ∧ (𝑗 ∈ dom 𝐼𝑁 ∉ (𝐼𝑗))) → (𝐼𝑗) ⊆ 𝑉)
21 simprr 772 . . . . . . . . 9 (((𝐺 ∈ UHGraph ∧ 𝑁𝑉) ∧ (𝑗 ∈ dom 𝐼𝑁 ∉ (𝐼𝑗))) → 𝑁 ∉ (𝐼𝑗))
22 elpwdifsn 4695 . . . . . . . . 9 (((𝐼𝑗) ∈ V ∧ (𝐼𝑗) ⊆ 𝑉𝑁 ∉ (𝐼𝑗)) → (𝐼𝑗) ∈ 𝒫 (𝑉 ∖ {𝑁}))
2318, 20, 21, 22syl3anc 1368 . . . . . . . 8 (((𝐺 ∈ UHGraph ∧ 𝑁𝑉) ∧ (𝑗 ∈ dom 𝐼𝑁 ∉ (𝐼𝑗))) → (𝐼𝑗) ∈ 𝒫 (𝑉 ∖ {𝑁}))
24 eleq1 2901 . . . . . . . . 9 (𝑐 = (𝐼𝑗) → (𝑐 ∈ 𝒫 (𝑉 ∖ {𝑁}) ↔ (𝐼𝑗) ∈ 𝒫 (𝑉 ∖ {𝑁})))
2524eqcoms 2830 . . . . . . . 8 ((𝐼𝑗) = 𝑐 → (𝑐 ∈ 𝒫 (𝑉 ∖ {𝑁}) ↔ (𝐼𝑗) ∈ 𝒫 (𝑉 ∖ {𝑁})))
2623, 25syl5ibrcom 250 . . . . . . 7 (((𝐺 ∈ UHGraph ∧ 𝑁𝑉) ∧ (𝑗 ∈ dom 𝐼𝑁 ∉ (𝐼𝑗))) → ((𝐼𝑗) = 𝑐𝑐 ∈ 𝒫 (𝑉 ∖ {𝑁})))
2726ex 416 . . . . . 6 ((𝐺 ∈ UHGraph ∧ 𝑁𝑉) → ((𝑗 ∈ dom 𝐼𝑁 ∉ (𝐼𝑗)) → ((𝐼𝑗) = 𝑐𝑐 ∈ 𝒫 (𝑉 ∖ {𝑁}))))
2817, 27syl5bi 245 . . . . 5 ((𝐺 ∈ UHGraph ∧ 𝑁𝑉) → (𝑗𝐹 → ((𝐼𝑗) = 𝑐𝑐 ∈ 𝒫 (𝑉 ∖ {𝑁}))))
2928rexlimdv 3269 . . . 4 ((𝐺 ∈ UHGraph ∧ 𝑁𝑉) → (∃𝑗𝐹 (𝐼𝑗) = 𝑐𝑐 ∈ 𝒫 (𝑉 ∖ {𝑁})))
3013, 29syld 47 . . 3 ((𝐺 ∈ UHGraph ∧ 𝑁𝑉) → (𝑐 ∈ (𝐼𝐹) → 𝑐 ∈ 𝒫 (𝑉 ∖ {𝑁})))
3130ssrdv 3948 . 2 ((𝐺 ∈ UHGraph ∧ 𝑁𝑉) → (𝐼𝐹) ⊆ 𝒫 (𝑉 ∖ {𝑁}))
32 opex 5333 . . . . 5 ⟨(𝑉 ∖ {𝑁}), (𝐼𝐹)⟩ ∈ V
335, 32eqeltri 2910 . . . 4 𝑆 ∈ V
3433a1i 11 . . 3 (𝑁𝑉𝑆 ∈ V)
352, 3, 4, 5uhgrspan1lem2 27089 . . . . 5 (Vtx‘𝑆) = (𝑉 ∖ {𝑁})
3635eqcomi 2831 . . . 4 (𝑉 ∖ {𝑁}) = (Vtx‘𝑆)
37 eqid 2822 . . . 4 (iEdg‘𝑆) = (iEdg‘𝑆)
386rneqi 5784 . . . . 5 ran (iEdg‘𝑆) = ran (𝐼𝐹)
39 edgval 26840 . . . . 5 (Edg‘𝑆) = ran (iEdg‘𝑆)
40 df-ima 5545 . . . . 5 (𝐼𝐹) = ran (𝐼𝐹)
4138, 39, 403eqtr4ri 2856 . . . 4 (𝐼𝐹) = (Edg‘𝑆)
4236, 2, 37, 3, 41issubgr 27059 . . 3 ((𝐺 ∈ UHGraph ∧ 𝑆 ∈ V) → (𝑆 SubGraph 𝐺 ↔ ((𝑉 ∖ {𝑁}) ⊆ 𝑉 ∧ (iEdg‘𝑆) = (𝐼 ↾ dom (iEdg‘𝑆)) ∧ (𝐼𝐹) ⊆ 𝒫 (𝑉 ∖ {𝑁}))))
4334, 42sylan2 595 . 2 ((𝐺 ∈ UHGraph ∧ 𝑁𝑉) → (𝑆 SubGraph 𝐺 ↔ ((𝑉 ∖ {𝑁}) ⊆ 𝑉 ∧ (iEdg‘𝑆) = (𝐼 ↾ dom (iEdg‘𝑆)) ∧ (𝐼𝐹) ⊆ 𝒫 (𝑉 ∖ {𝑁}))))
441, 8, 31, 43mpbir3and 1339 1 ((𝐺 ∈ UHGraph ∧ 𝑁𝑉) → 𝑆 SubGraph 𝐺)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1084   = wceq 1538  wcel 2114  wnel 3115  wrex 3131  {crab 3134  Vcvv 3469  cdif 3905  wss 3908  𝒫 cpw 4511  {csn 4539  cop 4545   class class class wbr 5042  dom cdm 5532  ran crn 5533  cres 5534  cima 5535  Fun wfun 6328  cfv 6334  Vtxcvtx 26787  iEdgciedg 26788  Edgcedg 26838  UHGraphcuhgr 26847   SubGraph csubgr 27055
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-sep 5179  ax-nul 5186  ax-pow 5243  ax-pr 5307  ax-un 7446
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ne 3012  df-nel 3116  df-ral 3135  df-rex 3136  df-rab 3139  df-v 3471  df-sbc 3748  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4266  df-if 4440  df-pw 4513  df-sn 4540  df-pr 4542  df-op 4546  df-uni 4814  df-br 5043  df-opab 5105  df-mpt 5123  df-id 5437  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545  df-iota 6293  df-fun 6336  df-fn 6337  df-f 6338  df-fv 6342  df-1st 7675  df-2nd 7676  df-vtx 26789  df-iedg 26790  df-edg 26839  df-uhgr 26849  df-subgr 27056
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator