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

Theorem usgredgsscusgredg 28181
Description: A simple graph is a subgraph of a complete simple graph. (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 13-Nov-2020.)
Hypotheses
Ref Expression
fusgrmaxsize.v 𝑉 = (Vtx‘𝐺)
fusgrmaxsize.e 𝐸 = (Edg‘𝐺)
usgrsscusgra.h 𝑉 = (Vtx‘𝐻)
usgrsscusgra.f 𝐹 = (Edg‘𝐻)
Assertion
Ref Expression
usgredgsscusgredg ((𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph) → 𝐸𝐹)

Proof of Theorem usgredgsscusgredg
Dummy variables 𝑒 𝑎 𝑏 𝑘 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fusgrmaxsize.v . . . . 5 𝑉 = (Vtx‘𝐺)
2 fusgrmaxsize.e . . . . 5 𝐸 = (Edg‘𝐺)
31, 2usgredg 27921 . . . 4 ((𝐺 ∈ USGraph ∧ 𝑒𝐸) → ∃𝑎𝑉𝑏𝑉 (𝑎𝑏𝑒 = {𝑎, 𝑏}))
4 usgrsscusgra.h . . . . . . . 8 𝑉 = (Vtx‘𝐻)
5 usgrsscusgra.f . . . . . . . 8 𝐹 = (Edg‘𝐻)
64, 5iscusgredg 28145 . . . . . . 7 (𝐻 ∈ ComplUSGraph ↔ (𝐻 ∈ USGraph ∧ ∀𝑘𝑉𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ 𝐹))
7 sneq 4591 . . . . . . . . . . . . 13 (𝑘 = 𝑎 → {𝑘} = {𝑎})
87difeq2d 4077 . . . . . . . . . . . 12 (𝑘 = 𝑎 → (𝑉 ∖ {𝑘}) = (𝑉 ∖ {𝑎}))
9 preq2 4690 . . . . . . . . . . . . 13 (𝑘 = 𝑎 → {𝑛, 𝑘} = {𝑛, 𝑎})
109eleq1d 2822 . . . . . . . . . . . 12 (𝑘 = 𝑎 → ({𝑛, 𝑘} ∈ 𝐹 ↔ {𝑛, 𝑎} ∈ 𝐹))
118, 10raleqbidv 3317 . . . . . . . . . . 11 (𝑘 = 𝑎 → (∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ 𝐹 ↔ ∀𝑛 ∈ (𝑉 ∖ {𝑎}){𝑛, 𝑎} ∈ 𝐹))
1211rspcv 3572 . . . . . . . . . 10 (𝑎𝑉 → (∀𝑘𝑉𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ 𝐹 → ∀𝑛 ∈ (𝑉 ∖ {𝑎}){𝑛, 𝑎} ∈ 𝐹))
13 simpl 484 . . . . . . . . . . . . . . 15 ((𝑎𝑏𝑒 = {𝑎, 𝑏}) → 𝑎𝑏)
1413necomd 2997 . . . . . . . . . . . . . 14 ((𝑎𝑏𝑒 = {𝑎, 𝑏}) → 𝑏𝑎)
1514anim2i 618 . . . . . . . . . . . . 13 ((𝑏𝑉 ∧ (𝑎𝑏𝑒 = {𝑎, 𝑏})) → (𝑏𝑉𝑏𝑎))
16 eldifsn 4742 . . . . . . . . . . . . 13 (𝑏 ∈ (𝑉 ∖ {𝑎}) ↔ (𝑏𝑉𝑏𝑎))
1715, 16sylibr 233 . . . . . . . . . . . 12 ((𝑏𝑉 ∧ (𝑎𝑏𝑒 = {𝑎, 𝑏})) → 𝑏 ∈ (𝑉 ∖ {𝑎}))
18 preq1 4689 . . . . . . . . . . . . . 14 (𝑛 = 𝑏 → {𝑛, 𝑎} = {𝑏, 𝑎})
1918eleq1d 2822 . . . . . . . . . . . . 13 (𝑛 = 𝑏 → ({𝑛, 𝑎} ∈ 𝐹 ↔ {𝑏, 𝑎} ∈ 𝐹))
2019rspcv 3572 . . . . . . . . . . . 12 (𝑏 ∈ (𝑉 ∖ {𝑎}) → (∀𝑛 ∈ (𝑉 ∖ {𝑎}){𝑛, 𝑎} ∈ 𝐹 → {𝑏, 𝑎} ∈ 𝐹))
2117, 20syl 17 . . . . . . . . . . 11 ((𝑏𝑉 ∧ (𝑎𝑏𝑒 = {𝑎, 𝑏})) → (∀𝑛 ∈ (𝑉 ∖ {𝑎}){𝑛, 𝑎} ∈ 𝐹 → {𝑏, 𝑎} ∈ 𝐹))
22 prcom 4688 . . . . . . . . . . . . . . . 16 {𝑎, 𝑏} = {𝑏, 𝑎}
2322eqeq2i 2750 . . . . . . . . . . . . . . 15 (𝑒 = {𝑎, 𝑏} ↔ 𝑒 = {𝑏, 𝑎})
24 eqcom 2744 . . . . . . . . . . . . . . 15 (𝑒 = {𝑏, 𝑎} ↔ {𝑏, 𝑎} = 𝑒)
2523, 24sylbb 218 . . . . . . . . . . . . . 14 (𝑒 = {𝑎, 𝑏} → {𝑏, 𝑎} = 𝑒)
2625eleq1d 2822 . . . . . . . . . . . . 13 (𝑒 = {𝑎, 𝑏} → ({𝑏, 𝑎} ∈ 𝐹𝑒𝐹))
2726biimpd 228 . . . . . . . . . . . 12 (𝑒 = {𝑎, 𝑏} → ({𝑏, 𝑎} ∈ 𝐹𝑒𝐹))
2827ad2antll 727 . . . . . . . . . . 11 ((𝑏𝑉 ∧ (𝑎𝑏𝑒 = {𝑎, 𝑏})) → ({𝑏, 𝑎} ∈ 𝐹𝑒𝐹))
2921, 28syld 47 . . . . . . . . . 10 ((𝑏𝑉 ∧ (𝑎𝑏𝑒 = {𝑎, 𝑏})) → (∀𝑛 ∈ (𝑉 ∖ {𝑎}){𝑛, 𝑎} ∈ 𝐹𝑒𝐹))
3012, 29syl9 77 . . . . . . . . 9 (𝑎𝑉 → ((𝑏𝑉 ∧ (𝑎𝑏𝑒 = {𝑎, 𝑏})) → (∀𝑘𝑉𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ 𝐹𝑒𝐹)))
3130impl 457 . . . . . . . 8 (((𝑎𝑉𝑏𝑉) ∧ (𝑎𝑏𝑒 = {𝑎, 𝑏})) → (∀𝑘𝑉𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ 𝐹𝑒𝐹))
3231adantld 492 . . . . . . 7 (((𝑎𝑉𝑏𝑉) ∧ (𝑎𝑏𝑒 = {𝑎, 𝑏})) → ((𝐻 ∈ USGraph ∧ ∀𝑘𝑉𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ 𝐹) → 𝑒𝐹))
336, 32biimtrid 241 . . . . . 6 (((𝑎𝑉𝑏𝑉) ∧ (𝑎𝑏𝑒 = {𝑎, 𝑏})) → (𝐻 ∈ ComplUSGraph → 𝑒𝐹))
3433ex 414 . . . . 5 ((𝑎𝑉𝑏𝑉) → ((𝑎𝑏𝑒 = {𝑎, 𝑏}) → (𝐻 ∈ ComplUSGraph → 𝑒𝐹)))
3534rexlimivv 3194 . . . 4 (∃𝑎𝑉𝑏𝑉 (𝑎𝑏𝑒 = {𝑎, 𝑏}) → (𝐻 ∈ ComplUSGraph → 𝑒𝐹))
363, 35syl 17 . . 3 ((𝐺 ∈ USGraph ∧ 𝑒𝐸) → (𝐻 ∈ ComplUSGraph → 𝑒𝐹))
3736impancom 453 . 2 ((𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph) → (𝑒𝐸𝑒𝐹))
3837ssrdv 3945 1 ((𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph) → 𝐸𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1541  wcel 2106  wne 2941  wral 3062  wrex 3071  cdif 3902  wss 3905  {csn 4581  {cpr 4583  cfv 6488  Vtxcvtx 27721  Edgcedg 27772  USGraphcusgr 27874  ComplUSGraphccusgr 28132
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-sep 5251  ax-nul 5258  ax-pow 5315  ax-pr 5379  ax-un 7659  ax-cnex 11037  ax-resscn 11038  ax-1cn 11039  ax-icn 11040  ax-addcl 11041  ax-addrcl 11042  ax-mulcl 11043  ax-mulrcl 11044  ax-mulcom 11045  ax-addass 11046  ax-mulass 11047  ax-distr 11048  ax-i2m1 11049  ax-1ne0 11050  ax-1rid 11051  ax-rnegex 11052  ax-rrecex 11053  ax-cnre 11054  ax-pre-lttri 11055  ax-pre-lttrn 11056  ax-pre-ltadd 11057  ax-pre-mulgt0 11058
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3352  df-rab 3406  df-v 3445  df-sbc 3735  df-csb 3851  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3924  df-nul 4278  df-if 4482  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4861  df-int 4903  df-iun 4951  df-br 5101  df-opab 5163  df-mpt 5184  df-tr 5218  df-id 5525  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5582  df-we 5584  df-xp 5633  df-rel 5634  df-cnv 5635  df-co 5636  df-dm 5637  df-rn 5638  df-res 5639  df-ima 5640  df-pred 6246  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6440  df-fun 6490  df-fn 6491  df-f 6492  df-f1 6493  df-fo 6494  df-f1o 6495  df-fv 6496  df-riota 7302  df-ov 7349  df-oprab 7350  df-mpo 7351  df-om 7790  df-1st 7908  df-2nd 7909  df-frecs 8176  df-wrecs 8207  df-recs 8281  df-rdg 8320  df-1o 8376  df-2o 8377  df-oadd 8380  df-er 8578  df-en 8814  df-dom 8815  df-sdom 8816  df-fin 8817  df-dju 9767  df-card 9805  df-pnf 11121  df-mnf 11122  df-xr 11123  df-ltxr 11124  df-le 11125  df-sub 11317  df-neg 11318  df-nn 12084  df-2 12146  df-n0 12344  df-xnn0 12416  df-z 12430  df-uz 12693  df-fz 13350  df-hash 14155  df-edg 27773  df-upgr 27807  df-umgr 27808  df-usgr 27876  df-nbgr 28055  df-uvtx 28108  df-cplgr 28133  df-cusgr 28134
This theorem is referenced by:  usgrsscusgr  28182  sizusglecusglem1  28183
  Copyright terms: Public domain W3C validator