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

Theorem issubgr 26073
Description: The property of a set to be a subgraph of another set. (Contributed by AV, 16-Nov-2020.)
Hypotheses
Ref Expression
issubgr.v 𝑉 = (Vtx‘𝑆)
issubgr.a 𝐴 = (Vtx‘𝐺)
issubgr.i 𝐼 = (iEdg‘𝑆)
issubgr.b 𝐵 = (iEdg‘𝐺)
issubgr.e 𝐸 = (Edg‘𝑆)
Assertion
Ref Expression
issubgr ((𝐺𝑊𝑆𝑈) → (𝑆 SubGraph 𝐺 ↔ (𝑉𝐴𝐼 = (𝐵 ↾ dom 𝐼) ∧ 𝐸 ⊆ 𝒫 𝑉)))

Proof of Theorem issubgr
Dummy variables 𝑠 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 6153 . . . . . . 7 (𝑠 = 𝑆 → (Vtx‘𝑠) = (Vtx‘𝑆))
21adantr 481 . . . . . 6 ((𝑠 = 𝑆𝑔 = 𝐺) → (Vtx‘𝑠) = (Vtx‘𝑆))
3 fveq2 6153 . . . . . . 7 (𝑔 = 𝐺 → (Vtx‘𝑔) = (Vtx‘𝐺))
43adantl 482 . . . . . 6 ((𝑠 = 𝑆𝑔 = 𝐺) → (Vtx‘𝑔) = (Vtx‘𝐺))
52, 4sseq12d 3618 . . . . 5 ((𝑠 = 𝑆𝑔 = 𝐺) → ((Vtx‘𝑠) ⊆ (Vtx‘𝑔) ↔ (Vtx‘𝑆) ⊆ (Vtx‘𝐺)))
6 fveq2 6153 . . . . . . 7 (𝑠 = 𝑆 → (iEdg‘𝑠) = (iEdg‘𝑆))
76adantr 481 . . . . . 6 ((𝑠 = 𝑆𝑔 = 𝐺) → (iEdg‘𝑠) = (iEdg‘𝑆))
8 fveq2 6153 . . . . . . . 8 (𝑔 = 𝐺 → (iEdg‘𝑔) = (iEdg‘𝐺))
98adantl 482 . . . . . . 7 ((𝑠 = 𝑆𝑔 = 𝐺) → (iEdg‘𝑔) = (iEdg‘𝐺))
106dmeqd 5291 . . . . . . . 8 (𝑠 = 𝑆 → dom (iEdg‘𝑠) = dom (iEdg‘𝑆))
1110adantr 481 . . . . . . 7 ((𝑠 = 𝑆𝑔 = 𝐺) → dom (iEdg‘𝑠) = dom (iEdg‘𝑆))
129, 11reseq12d 5362 . . . . . 6 ((𝑠 = 𝑆𝑔 = 𝐺) → ((iEdg‘𝑔) ↾ dom (iEdg‘𝑠)) = ((iEdg‘𝐺) ↾ dom (iEdg‘𝑆)))
137, 12eqeq12d 2636 . . . . 5 ((𝑠 = 𝑆𝑔 = 𝐺) → ((iEdg‘𝑠) = ((iEdg‘𝑔) ↾ dom (iEdg‘𝑠)) ↔ (iEdg‘𝑆) = ((iEdg‘𝐺) ↾ dom (iEdg‘𝑆))))
14 fveq2 6153 . . . . . . 7 (𝑠 = 𝑆 → (Edg‘𝑠) = (Edg‘𝑆))
151pweqd 4140 . . . . . . 7 (𝑠 = 𝑆 → 𝒫 (Vtx‘𝑠) = 𝒫 (Vtx‘𝑆))
1614, 15sseq12d 3618 . . . . . 6 (𝑠 = 𝑆 → ((Edg‘𝑠) ⊆ 𝒫 (Vtx‘𝑠) ↔ (Edg‘𝑆) ⊆ 𝒫 (Vtx‘𝑆)))
1716adantr 481 . . . . 5 ((𝑠 = 𝑆𝑔 = 𝐺) → ((Edg‘𝑠) ⊆ 𝒫 (Vtx‘𝑠) ↔ (Edg‘𝑆) ⊆ 𝒫 (Vtx‘𝑆)))
185, 13, 173anbi123d 1396 . . . 4 ((𝑠 = 𝑆𝑔 = 𝐺) → (((Vtx‘𝑠) ⊆ (Vtx‘𝑔) ∧ (iEdg‘𝑠) = ((iEdg‘𝑔) ↾ dom (iEdg‘𝑠)) ∧ (Edg‘𝑠) ⊆ 𝒫 (Vtx‘𝑠)) ↔ ((Vtx‘𝑆) ⊆ (Vtx‘𝐺) ∧ (iEdg‘𝑆) = ((iEdg‘𝐺) ↾ dom (iEdg‘𝑆)) ∧ (Edg‘𝑆) ⊆ 𝒫 (Vtx‘𝑆))))
19 df-subgr 26070 . . . 4 SubGraph = {⟨𝑠, 𝑔⟩ ∣ ((Vtx‘𝑠) ⊆ (Vtx‘𝑔) ∧ (iEdg‘𝑠) = ((iEdg‘𝑔) ↾ dom (iEdg‘𝑠)) ∧ (Edg‘𝑠) ⊆ 𝒫 (Vtx‘𝑠))}
2018, 19brabga 4954 . . 3 ((𝑆𝑈𝐺𝑊) → (𝑆 SubGraph 𝐺 ↔ ((Vtx‘𝑆) ⊆ (Vtx‘𝐺) ∧ (iEdg‘𝑆) = ((iEdg‘𝐺) ↾ dom (iEdg‘𝑆)) ∧ (Edg‘𝑆) ⊆ 𝒫 (Vtx‘𝑆))))
2120ancoms 469 . 2 ((𝐺𝑊𝑆𝑈) → (𝑆 SubGraph 𝐺 ↔ ((Vtx‘𝑆) ⊆ (Vtx‘𝐺) ∧ (iEdg‘𝑆) = ((iEdg‘𝐺) ↾ dom (iEdg‘𝑆)) ∧ (Edg‘𝑆) ⊆ 𝒫 (Vtx‘𝑆))))
22 issubgr.v . . . 4 𝑉 = (Vtx‘𝑆)
23 issubgr.a . . . 4 𝐴 = (Vtx‘𝐺)
2422, 23sseq12i 3615 . . 3 (𝑉𝐴 ↔ (Vtx‘𝑆) ⊆ (Vtx‘𝐺))
25 issubgr.i . . . 4 𝐼 = (iEdg‘𝑆)
26 issubgr.b . . . . 5 𝐵 = (iEdg‘𝐺)
2725dmeqi 5290 . . . . 5 dom 𝐼 = dom (iEdg‘𝑆)
2826, 27reseq12i 5359 . . . 4 (𝐵 ↾ dom 𝐼) = ((iEdg‘𝐺) ↾ dom (iEdg‘𝑆))
2925, 28eqeq12i 2635 . . 3 (𝐼 = (𝐵 ↾ dom 𝐼) ↔ (iEdg‘𝑆) = ((iEdg‘𝐺) ↾ dom (iEdg‘𝑆)))
30 issubgr.e . . . 4 𝐸 = (Edg‘𝑆)
3122pweqi 4139 . . . 4 𝒫 𝑉 = 𝒫 (Vtx‘𝑆)
3230, 31sseq12i 3615 . . 3 (𝐸 ⊆ 𝒫 𝑉 ↔ (Edg‘𝑆) ⊆ 𝒫 (Vtx‘𝑆))
3324, 29, 323anbi123i 1249 . 2 ((𝑉𝐴𝐼 = (𝐵 ↾ dom 𝐼) ∧ 𝐸 ⊆ 𝒫 𝑉) ↔ ((Vtx‘𝑆) ⊆ (Vtx‘𝐺) ∧ (iEdg‘𝑆) = ((iEdg‘𝐺) ↾ dom (iEdg‘𝑆)) ∧ (Edg‘𝑆) ⊆ 𝒫 (Vtx‘𝑆)))
3421, 33syl6bbr 278 1 ((𝐺𝑊𝑆𝑈) → (𝑆 SubGraph 𝐺 ↔ (𝑉𝐴𝐼 = (𝐵 ↾ dom 𝐼) ∧ 𝐸 ⊆ 𝒫 𝑉)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wcel 1987  wss 3559  𝒫 cpw 4135   class class class wbr 4618  dom cdm 5079  cres 5081  cfv 5852  Vtxcvtx 25791  iEdgciedg 25792  Edgcedg 25856   SubGraph csubgr 26069
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pr 4872
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rex 2913  df-rab 2916  df-v 3191  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-br 4619  df-opab 4679  df-xp 5085  df-dm 5089  df-res 5091  df-iota 5815  df-fv 5860  df-subgr 26070
This theorem is referenced by:  issubgr2  26074  subgrprop  26075  uhgrissubgr  26077  egrsubgr  26079  0grsubgr  26080  uhgrspan1  26105
  Copyright terms: Public domain W3C validator