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

Theorem cusgra2v 25991
 Description: A graph with two (different) vertices is complete if and only if there is an edge between these two vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Proof shortened by Alexander van der Vekens, 16-Dec-2017.)
Assertion
Ref Expression
cusgra2v ((𝐴𝑉𝐵𝑊𝐴𝐵) → ({𝐴, 𝐵} USGrph 𝐸 → ({𝐴, 𝐵} ComplUSGrph 𝐸 ↔ {𝐴, 𝐵} ∈ ran 𝐸)))

Proof of Theorem cusgra2v
Dummy variables 𝑘 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 usgrav 25867 . . . . 5 ({𝐴, 𝐵} USGrph 𝐸 → ({𝐴, 𝐵} ∈ V ∧ 𝐸 ∈ V))
21adantr 480 . . . 4 (({𝐴, 𝐵} USGrph 𝐸 ∧ (𝐴𝑉𝐵𝑊𝐴𝐵)) → ({𝐴, 𝐵} ∈ V ∧ 𝐸 ∈ V))
3 iscusgra 25985 . . . 4 (({𝐴, 𝐵} ∈ V ∧ 𝐸 ∈ V) → ({𝐴, 𝐵} ComplUSGrph 𝐸 ↔ ({𝐴, 𝐵} USGrph 𝐸 ∧ ∀𝑘 ∈ {𝐴, 𝐵}∀𝑛 ∈ ({𝐴, 𝐵} ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸)))
42, 3syl 17 . . 3 (({𝐴, 𝐵} USGrph 𝐸 ∧ (𝐴𝑉𝐵𝑊𝐴𝐵)) → ({𝐴, 𝐵} ComplUSGrph 𝐸 ↔ ({𝐴, 𝐵} USGrph 𝐸 ∧ ∀𝑘 ∈ {𝐴, 𝐵}∀𝑛 ∈ ({𝐴, 𝐵} ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸)))
5 3simpa 1051 . . . . . 6 ((𝐴𝑉𝐵𝑊𝐴𝐵) → (𝐴𝑉𝐵𝑊))
65adantl 481 . . . . 5 (({𝐴, 𝐵} USGrph 𝐸 ∧ (𝐴𝑉𝐵𝑊𝐴𝐵)) → (𝐴𝑉𝐵𝑊))
7 sneq 4135 . . . . . . . 8 (𝑘 = 𝐴 → {𝑘} = {𝐴})
87difeq2d 3690 . . . . . . 7 (𝑘 = 𝐴 → ({𝐴, 𝐵} ∖ {𝑘}) = ({𝐴, 𝐵} ∖ {𝐴}))
9 preq2 4213 . . . . . . . 8 (𝑘 = 𝐴 → {𝑛, 𝑘} = {𝑛, 𝐴})
109eleq1d 2672 . . . . . . 7 (𝑘 = 𝐴 → ({𝑛, 𝑘} ∈ ran 𝐸 ↔ {𝑛, 𝐴} ∈ ran 𝐸))
118, 10raleqbidv 3129 . . . . . 6 (𝑘 = 𝐴 → (∀𝑛 ∈ ({𝐴, 𝐵} ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸 ↔ ∀𝑛 ∈ ({𝐴, 𝐵} ∖ {𝐴}){𝑛, 𝐴} ∈ ran 𝐸))
12 sneq 4135 . . . . . . . 8 (𝑘 = 𝐵 → {𝑘} = {𝐵})
1312difeq2d 3690 . . . . . . 7 (𝑘 = 𝐵 → ({𝐴, 𝐵} ∖ {𝑘}) = ({𝐴, 𝐵} ∖ {𝐵}))
14 preq2 4213 . . . . . . . 8 (𝑘 = 𝐵 → {𝑛, 𝑘} = {𝑛, 𝐵})
1514eleq1d 2672 . . . . . . 7 (𝑘 = 𝐵 → ({𝑛, 𝑘} ∈ ran 𝐸 ↔ {𝑛, 𝐵} ∈ ran 𝐸))
1613, 15raleqbidv 3129 . . . . . 6 (𝑘 = 𝐵 → (∀𝑛 ∈ ({𝐴, 𝐵} ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸 ↔ ∀𝑛 ∈ ({𝐴, 𝐵} ∖ {𝐵}){𝑛, 𝐵} ∈ ran 𝐸))
1711, 16ralprg 4181 . . . . 5 ((𝐴𝑉𝐵𝑊) → (∀𝑘 ∈ {𝐴, 𝐵}∀𝑛 ∈ ({𝐴, 𝐵} ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸 ↔ (∀𝑛 ∈ ({𝐴, 𝐵} ∖ {𝐴}){𝑛, 𝐴} ∈ ran 𝐸 ∧ ∀𝑛 ∈ ({𝐴, 𝐵} ∖ {𝐵}){𝑛, 𝐵} ∈ ran 𝐸)))
186, 17syl 17 . . . 4 (({𝐴, 𝐵} USGrph 𝐸 ∧ (𝐴𝑉𝐵𝑊𝐴𝐵)) → (∀𝑘 ∈ {𝐴, 𝐵}∀𝑛 ∈ ({𝐴, 𝐵} ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸 ↔ (∀𝑛 ∈ ({𝐴, 𝐵} ∖ {𝐴}){𝑛, 𝐴} ∈ ran 𝐸 ∧ ∀𝑛 ∈ ({𝐴, 𝐵} ∖ {𝐵}){𝑛, 𝐵} ∈ ran 𝐸)))
19 ibar 524 . . . . 5 ({𝐴, 𝐵} USGrph 𝐸 → (∀𝑘 ∈ {𝐴, 𝐵}∀𝑛 ∈ ({𝐴, 𝐵} ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸 ↔ ({𝐴, 𝐵} USGrph 𝐸 ∧ ∀𝑘 ∈ {𝐴, 𝐵}∀𝑛 ∈ ({𝐴, 𝐵} ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸)))
2019adantr 480 . . . 4 (({𝐴, 𝐵} USGrph 𝐸 ∧ (𝐴𝑉𝐵𝑊𝐴𝐵)) → (∀𝑘 ∈ {𝐴, 𝐵}∀𝑛 ∈ ({𝐴, 𝐵} ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸 ↔ ({𝐴, 𝐵} USGrph 𝐸 ∧ ∀𝑘 ∈ {𝐴, 𝐵}∀𝑛 ∈ ({𝐴, 𝐵} ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸)))
21 difprsn1 4271 . . . . . . . . . 10 (𝐴𝐵 → ({𝐴, 𝐵} ∖ {𝐴}) = {𝐵})
22213ad2ant3 1077 . . . . . . . . 9 ((𝐴𝑉𝐵𝑊𝐴𝐵) → ({𝐴, 𝐵} ∖ {𝐴}) = {𝐵})
2322adantl 481 . . . . . . . 8 (({𝐴, 𝐵} USGrph 𝐸 ∧ (𝐴𝑉𝐵𝑊𝐴𝐵)) → ({𝐴, 𝐵} ∖ {𝐴}) = {𝐵})
2423raleqdv 3121 . . . . . . 7 (({𝐴, 𝐵} USGrph 𝐸 ∧ (𝐴𝑉𝐵𝑊𝐴𝐵)) → (∀𝑛 ∈ ({𝐴, 𝐵} ∖ {𝐴}){𝑛, 𝐴} ∈ ran 𝐸 ↔ ∀𝑛 ∈ {𝐵} {𝑛, 𝐴} ∈ ran 𝐸))
25 preq1 4212 . . . . . . . . . . 11 (𝑛 = 𝐵 → {𝑛, 𝐴} = {𝐵, 𝐴})
2625eleq1d 2672 . . . . . . . . . 10 (𝑛 = 𝐵 → ({𝑛, 𝐴} ∈ ran 𝐸 ↔ {𝐵, 𝐴} ∈ ran 𝐸))
2726ralsng 4165 . . . . . . . . 9 (𝐵𝑊 → (∀𝑛 ∈ {𝐵} {𝑛, 𝐴} ∈ ran 𝐸 ↔ {𝐵, 𝐴} ∈ ran 𝐸))
28273ad2ant2 1076 . . . . . . . 8 ((𝐴𝑉𝐵𝑊𝐴𝐵) → (∀𝑛 ∈ {𝐵} {𝑛, 𝐴} ∈ ran 𝐸 ↔ {𝐵, 𝐴} ∈ ran 𝐸))
2928adantl 481 . . . . . . 7 (({𝐴, 𝐵} USGrph 𝐸 ∧ (𝐴𝑉𝐵𝑊𝐴𝐵)) → (∀𝑛 ∈ {𝐵} {𝑛, 𝐴} ∈ ran 𝐸 ↔ {𝐵, 𝐴} ∈ ran 𝐸))
3024, 29bitrd 267 . . . . . 6 (({𝐴, 𝐵} USGrph 𝐸 ∧ (𝐴𝑉𝐵𝑊𝐴𝐵)) → (∀𝑛 ∈ ({𝐴, 𝐵} ∖ {𝐴}){𝑛, 𝐴} ∈ ran 𝐸 ↔ {𝐵, 𝐴} ∈ ran 𝐸))
31 difprsn2 4272 . . . . . . . . . 10 (𝐴𝐵 → ({𝐴, 𝐵} ∖ {𝐵}) = {𝐴})
32313ad2ant3 1077 . . . . . . . . 9 ((𝐴𝑉𝐵𝑊𝐴𝐵) → ({𝐴, 𝐵} ∖ {𝐵}) = {𝐴})
3332adantl 481 . . . . . . . 8 (({𝐴, 𝐵} USGrph 𝐸 ∧ (𝐴𝑉𝐵𝑊𝐴𝐵)) → ({𝐴, 𝐵} ∖ {𝐵}) = {𝐴})
3433raleqdv 3121 . . . . . . 7 (({𝐴, 𝐵} USGrph 𝐸 ∧ (𝐴𝑉𝐵𝑊𝐴𝐵)) → (∀𝑛 ∈ ({𝐴, 𝐵} ∖ {𝐵}){𝑛, 𝐵} ∈ ran 𝐸 ↔ ∀𝑛 ∈ {𝐴} {𝑛, 𝐵} ∈ ran 𝐸))
35 preq1 4212 . . . . . . . . . . 11 (𝑛 = 𝐴 → {𝑛, 𝐵} = {𝐴, 𝐵})
3635eleq1d 2672 . . . . . . . . . 10 (𝑛 = 𝐴 → ({𝑛, 𝐵} ∈ ran 𝐸 ↔ {𝐴, 𝐵} ∈ ran 𝐸))
3736ralsng 4165 . . . . . . . . 9 (𝐴𝑉 → (∀𝑛 ∈ {𝐴} {𝑛, 𝐵} ∈ ran 𝐸 ↔ {𝐴, 𝐵} ∈ ran 𝐸))
38373ad2ant1 1075 . . . . . . . 8 ((𝐴𝑉𝐵𝑊𝐴𝐵) → (∀𝑛 ∈ {𝐴} {𝑛, 𝐵} ∈ ran 𝐸 ↔ {𝐴, 𝐵} ∈ ran 𝐸))
3938adantl 481 . . . . . . 7 (({𝐴, 𝐵} USGrph 𝐸 ∧ (𝐴𝑉𝐵𝑊𝐴𝐵)) → (∀𝑛 ∈ {𝐴} {𝑛, 𝐵} ∈ ran 𝐸 ↔ {𝐴, 𝐵} ∈ ran 𝐸))
4034, 39bitrd 267 . . . . . 6 (({𝐴, 𝐵} USGrph 𝐸 ∧ (𝐴𝑉𝐵𝑊𝐴𝐵)) → (∀𝑛 ∈ ({𝐴, 𝐵} ∖ {𝐵}){𝑛, 𝐵} ∈ ran 𝐸 ↔ {𝐴, 𝐵} ∈ ran 𝐸))
4130, 40anbi12d 743 . . . . 5 (({𝐴, 𝐵} USGrph 𝐸 ∧ (𝐴𝑉𝐵𝑊𝐴𝐵)) → ((∀𝑛 ∈ ({𝐴, 𝐵} ∖ {𝐴}){𝑛, 𝐴} ∈ ran 𝐸 ∧ ∀𝑛 ∈ ({𝐴, 𝐵} ∖ {𝐵}){𝑛, 𝐵} ∈ ran 𝐸) ↔ ({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸)))
42 prcom 4211 . . . . . . . 8 {𝐵, 𝐴} = {𝐴, 𝐵}
4342eleq1i 2679 . . . . . . 7 ({𝐵, 𝐴} ∈ ran 𝐸 ↔ {𝐴, 𝐵} ∈ ran 𝐸)
4443anbi1i 727 . . . . . 6 (({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸) ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸))
45 anidm 674 . . . . . 6 (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸) ↔ {𝐴, 𝐵} ∈ ran 𝐸)
4644, 45bitri 263 . . . . 5 (({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸) ↔ {𝐴, 𝐵} ∈ ran 𝐸)
4741, 46syl6bb 275 . . . 4 (({𝐴, 𝐵} USGrph 𝐸 ∧ (𝐴𝑉𝐵𝑊𝐴𝐵)) → ((∀𝑛 ∈ ({𝐴, 𝐵} ∖ {𝐴}){𝑛, 𝐴} ∈ ran 𝐸 ∧ ∀𝑛 ∈ ({𝐴, 𝐵} ∖ {𝐵}){𝑛, 𝐵} ∈ ran 𝐸) ↔ {𝐴, 𝐵} ∈ ran 𝐸))
4818, 20, 473bitr3d 297 . . 3 (({𝐴, 𝐵} USGrph 𝐸 ∧ (𝐴𝑉𝐵𝑊𝐴𝐵)) → (({𝐴, 𝐵} USGrph 𝐸 ∧ ∀𝑘 ∈ {𝐴, 𝐵}∀𝑛 ∈ ({𝐴, 𝐵} ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝐸) ↔ {𝐴, 𝐵} ∈ ran 𝐸))
494, 48bitrd 267 . 2 (({𝐴, 𝐵} USGrph 𝐸 ∧ (𝐴𝑉𝐵𝑊𝐴𝐵)) → ({𝐴, 𝐵} ComplUSGrph 𝐸 ↔ {𝐴, 𝐵} ∈ ran 𝐸))
5049expcom 450 1 ((𝐴𝑉𝐵𝑊𝐴𝐵) → ({𝐴, 𝐵} USGrph 𝐸 → ({𝐴, 𝐵} ComplUSGrph 𝐸 ↔ {𝐴, 𝐵} ∈ ran 𝐸)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  Vcvv 3173   ∖ cdif 3537  {csn 4125  {cpr 4127   class class class wbr 4583  ran crn 5039   USGrph cusg 25859   ComplUSGrph ccusgra 25947 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644  df-xp 5044  df-rel 5045  df-cnv 5046  df-dm 5048  df-rn 5049  df-usgra 25862  df-cusgra 25950 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator