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

Theorem uhgrspan1 29335
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 4147 . 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 29334 . . 3 (iEdg‘𝑆) = (𝐼𝐹)
7 resresdm 6255 . . 3 ((iEdg‘𝑆) = (𝐼𝐹) → (iEdg‘𝑆) = (𝐼 ↾ dom (iEdg‘𝑆)))
86, 7mp1i 13 . 2 ((𝐺 ∈ UHGraph ∧ 𝑁𝑉) → (iEdg‘𝑆) = (𝐼 ↾ dom (iEdg‘𝑆)))
93uhgrfun 29098 . . . . . 6 (𝐺 ∈ UHGraph → Fun 𝐼)
10 fvelima 6974 . . . . . . 7 ((Fun 𝐼𝑐 ∈ (𝐼𝐹)) → ∃𝑗𝐹 (𝐼𝑗) = 𝑐)
1110ex 412 . . . . . 6 (Fun 𝐼 → (𝑐 ∈ (𝐼𝐹) → ∃𝑗𝐹 (𝐼𝑗) = 𝑐))
129, 11syl 17 . . . . 5 (𝐺 ∈ UHGraph → (𝑐 ∈ (𝐼𝐹) → ∃𝑗𝐹 (𝐼𝑗) = 𝑐))
1312adantr 480 . . . 4 ((𝐺 ∈ UHGraph ∧ 𝑁𝑉) → (𝑐 ∈ (𝐼𝐹) → ∃𝑗𝐹 (𝐼𝑗) = 𝑐))
14 eqidd 2736 . . . . . . . 8 (𝑖 = 𝑗𝑁 = 𝑁)
15 fveq2 6907 . . . . . . . 8 (𝑖 = 𝑗 → (𝐼𝑖) = (𝐼𝑗))
1614, 15neleq12d 3049 . . . . . . 7 (𝑖 = 𝑗 → (𝑁 ∉ (𝐼𝑖) ↔ 𝑁 ∉ (𝐼𝑗)))
1716, 4elrab2 3698 . . . . . 6 (𝑗𝐹 ↔ (𝑗 ∈ dom 𝐼𝑁 ∉ (𝐼𝑗)))
18 fvexd 6922 . . . . . . . . 9 (((𝐺 ∈ UHGraph ∧ 𝑁𝑉) ∧ (𝑗 ∈ dom 𝐼𝑁 ∉ (𝐼𝑗))) → (𝐼𝑗) ∈ V)
192, 3uhgrss 29096 . . . . . . . . . 10 ((𝐺 ∈ UHGraph ∧ 𝑗 ∈ dom 𝐼) → (𝐼𝑗) ⊆ 𝑉)
2019ad2ant2r 747 . . . . . . . . 9 (((𝐺 ∈ UHGraph ∧ 𝑁𝑉) ∧ (𝑗 ∈ dom 𝐼𝑁 ∉ (𝐼𝑗))) → (𝐼𝑗) ⊆ 𝑉)
21 simprr 773 . . . . . . . . 9 (((𝐺 ∈ UHGraph ∧ 𝑁𝑉) ∧ (𝑗 ∈ dom 𝐼𝑁 ∉ (𝐼𝑗))) → 𝑁 ∉ (𝐼𝑗))
22 elpwdifsn 4794 . . . . . . . . 9 (((𝐼𝑗) ∈ V ∧ (𝐼𝑗) ⊆ 𝑉𝑁 ∉ (𝐼𝑗)) → (𝐼𝑗) ∈ 𝒫 (𝑉 ∖ {𝑁}))
2318, 20, 21, 22syl3anc 1370 . . . . . . . 8 (((𝐺 ∈ UHGraph ∧ 𝑁𝑉) ∧ (𝑗 ∈ dom 𝐼𝑁 ∉ (𝐼𝑗))) → (𝐼𝑗) ∈ 𝒫 (𝑉 ∖ {𝑁}))
24 eleq1 2827 . . . . . . . . 9 (𝑐 = (𝐼𝑗) → (𝑐 ∈ 𝒫 (𝑉 ∖ {𝑁}) ↔ (𝐼𝑗) ∈ 𝒫 (𝑉 ∖ {𝑁})))
2524eqcoms 2743 . . . . . . . 8 ((𝐼𝑗) = 𝑐 → (𝑐 ∈ 𝒫 (𝑉 ∖ {𝑁}) ↔ (𝐼𝑗) ∈ 𝒫 (𝑉 ∖ {𝑁})))
2623, 25syl5ibrcom 247 . . . . . . 7 (((𝐺 ∈ UHGraph ∧ 𝑁𝑉) ∧ (𝑗 ∈ dom 𝐼𝑁 ∉ (𝐼𝑗))) → ((𝐼𝑗) = 𝑐𝑐 ∈ 𝒫 (𝑉 ∖ {𝑁})))
2726ex 412 . . . . . 6 ((𝐺 ∈ UHGraph ∧ 𝑁𝑉) → ((𝑗 ∈ dom 𝐼𝑁 ∉ (𝐼𝑗)) → ((𝐼𝑗) = 𝑐𝑐 ∈ 𝒫 (𝑉 ∖ {𝑁}))))
2817, 27biimtrid 242 . . . . 5 ((𝐺 ∈ UHGraph ∧ 𝑁𝑉) → (𝑗𝐹 → ((𝐼𝑗) = 𝑐𝑐 ∈ 𝒫 (𝑉 ∖ {𝑁}))))
2928rexlimdv 3151 . . . 4 ((𝐺 ∈ UHGraph ∧ 𝑁𝑉) → (∃𝑗𝐹 (𝐼𝑗) = 𝑐𝑐 ∈ 𝒫 (𝑉 ∖ {𝑁})))
3013, 29syld 47 . . 3 ((𝐺 ∈ UHGraph ∧ 𝑁𝑉) → (𝑐 ∈ (𝐼𝐹) → 𝑐 ∈ 𝒫 (𝑉 ∖ {𝑁})))
3130ssrdv 4001 . 2 ((𝐺 ∈ UHGraph ∧ 𝑁𝑉) → (𝐼𝐹) ⊆ 𝒫 (𝑉 ∖ {𝑁}))
32 opex 5475 . . . . 5 ⟨(𝑉 ∖ {𝑁}), (𝐼𝐹)⟩ ∈ V
335, 32eqeltri 2835 . . . 4 𝑆 ∈ V
3433a1i 11 . . 3 (𝑁𝑉𝑆 ∈ V)
352, 3, 4, 5uhgrspan1lem2 29333 . . . . 5 (Vtx‘𝑆) = (𝑉 ∖ {𝑁})
3635eqcomi 2744 . . . 4 (𝑉 ∖ {𝑁}) = (Vtx‘𝑆)
37 eqid 2735 . . . 4 (iEdg‘𝑆) = (iEdg‘𝑆)
386rneqi 5951 . . . . 5 ran (iEdg‘𝑆) = ran (𝐼𝐹)
39 edgval 29081 . . . . 5 (Edg‘𝑆) = ran (iEdg‘𝑆)
40 df-ima 5702 . . . . 5 (𝐼𝐹) = ran (𝐼𝐹)
4138, 39, 403eqtr4ri 2774 . . . 4 (𝐼𝐹) = (Edg‘𝑆)
4236, 2, 37, 3, 41issubgr 29303 . . 3 ((𝐺 ∈ UHGraph ∧ 𝑆 ∈ V) → (𝑆 SubGraph 𝐺 ↔ ((𝑉 ∖ {𝑁}) ⊆ 𝑉 ∧ (iEdg‘𝑆) = (𝐼 ↾ dom (iEdg‘𝑆)) ∧ (𝐼𝐹) ⊆ 𝒫 (𝑉 ∖ {𝑁}))))
4334, 42sylan2 593 . 2 ((𝐺 ∈ UHGraph ∧ 𝑁𝑉) → (𝑆 SubGraph 𝐺 ↔ ((𝑉 ∖ {𝑁}) ⊆ 𝑉 ∧ (iEdg‘𝑆) = (𝐼 ↾ dom (iEdg‘𝑆)) ∧ (𝐼𝐹) ⊆ 𝒫 (𝑉 ∖ {𝑁}))))
441, 8, 31, 43mpbir3and 1341 1 ((𝐺 ∈ UHGraph ∧ 𝑁𝑉) → 𝑆 SubGraph 𝐺)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1086   = wceq 1537  wcel 2106  wnel 3044  wrex 3068  {crab 3433  Vcvv 3478  cdif 3960  wss 3963  𝒫 cpw 4605  {csn 4631  cop 4637   class class class wbr 5148  dom cdm 5689  ran crn 5690  cres 5691  cima 5692  Fun wfun 6557  cfv 6563  Vtxcvtx 29028  iEdgciedg 29029  Edgcedg 29079  UHGraphcuhgr 29088   SubGraph csubgr 29299
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-sbc 3792  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-fv 6571  df-1st 8013  df-2nd 8014  df-vtx 29030  df-iedg 29031  df-edg 29080  df-uhgr 29090  df-subgr 29300
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator