Theorem usgrexmpledg 29221

Description: The edges {0, 1}, {1, 2}, {2, 0}, {0, 3} of the graph 𝐺 = ⟨𝑉, 𝐸⟩. (Contributed by AV, 12-Jan-2020.) (Revised by AV, 21-Oct-2020.)

Hypotheses

Ref	Expression
usgrexmpl.v	⊢ 𝑉 = (0...4)
usgrexmpl.e	⊢ 𝐸 = ⟨“{0, 1} {1, 2} {2, 0} {0, 3}”⟩
usgrexmpl.g	⊢ 𝐺 = ⟨𝑉, 𝐸⟩

Assertion

Ref	Expression
usgrexmpledg	⊢ (Edg‘𝐺) = ({{0, 1}, {1, 2}} ∪ {{2, 0}, {0, 3}})

Proof of Theorem usgrexmpledg

Step	Hyp	Ref	Expression
1		edgval 29008	. 2 ⊢ (Edg‘𝐺) = ran (iEdg‘𝐺)
2		usgrexmpl.v	. . . . 5 ⊢ 𝑉 = (0...4)
3		usgrexmpl.e	. . . . 5 ⊢ 𝐸 = ⟨“{0, 1} {1, 2} {2, 0} {0, 3}”⟩
4		usgrexmpl.g	. . . . 5 ⊢ 𝐺 = ⟨𝑉, 𝐸⟩
5	2, 3, 4	usgrexmpllem 29219	. . . 4 ⊢ ((Vtx‘𝐺) = 𝑉 ∧ (iEdg‘𝐺) = 𝐸)
6	5	simpri 484	. . 3 ⊢ (iEdg‘𝐺) = 𝐸
7	6	rneqi 5945	. 2 ⊢ ran (iEdg‘𝐺) = ran 𝐸
8		prex 5440	. . . . . . 7 ⊢ {0, 1} ∈ V
9		prex 5440	. . . . . . 7 ⊢ {1, 2} ∈ V
10	8, 9	pm3.2i 469	. . . . . 6 ⊢ ({0, 1} ∈ V ∧ {1, 2} ∈ V)
11		prex 5440	. . . . . . 7 ⊢ {2, 0} ∈ V
12		prex 5440	. . . . . . 7 ⊢ {0, 3} ∈ V
13	11, 12	pm3.2i 469	. . . . . 6 ⊢ ({2, 0} ∈ V ∧ {0, 3} ∈ V)
14	10, 13	pm3.2i 469	. . . . 5 ⊢ (({0, 1} ∈ V ∧ {1, 2} ∈ V) ∧ ({2, 0} ∈ V ∧ {0, 3} ∈ V))
15		usgrexmpldifpr 29217	. . . . 5 ⊢ (({0, 1} ≠ {1, 2} ∧ {0, 1} ≠ {2, 0} ∧ {0, 1} ≠ {0, 3}) ∧ ({1, 2} ≠ {2, 0} ∧ {1, 2} ≠ {0, 3} ∧ {2, 0} ≠ {0, 3}))
16	14, 15	pm3.2i 469	. . . 4 ⊢ ((({0, 1} ∈ V ∧ {1, 2} ∈ V) ∧ ({2, 0} ∈ V ∧ {0, 3} ∈ V)) ∧ (({0, 1} ≠ {1, 2} ∧ {0, 1} ≠ {2, 0} ∧ {0, 1} ≠ {0, 3}) ∧ ({1, 2} ≠ {2, 0} ∧ {1, 2} ≠ {0, 3} ∧ {2, 0} ≠ {0, 3})))
17	16, 3	pm3.2i 469	. . 3 ⊢ (((({0, 1} ∈ V ∧ {1, 2} ∈ V) ∧ ({2, 0} ∈ V ∧ {0, 3} ∈ V)) ∧ (({0, 1} ≠ {1, 2} ∧ {0, 1} ≠ {2, 0} ∧ {0, 1} ≠ {0, 3}) ∧ ({1, 2} ≠ {2, 0} ∧ {1, 2} ≠ {0, 3} ∧ {2, 0} ≠ {0, 3}))) ∧ 𝐸 = ⟨“{0, 1} {1, 2} {2, 0} {0, 3}”⟩)
18		s4f1o 14948	. . . 4 ⊢ ((({0, 1} ∈ V ∧ {1, 2} ∈ V) ∧ ({2, 0} ∈ V ∧ {0, 3} ∈ V)) → ((({0, 1} ≠ {1, 2} ∧ {0, 1} ≠ {2, 0} ∧ {0, 1} ≠ {0, 3}) ∧ ({1, 2} ≠ {2, 0} ∧ {1, 2} ≠ {0, 3} ∧ {2, 0} ≠ {0, 3})) → (𝐸 = ⟨“{0, 1} {1, 2} {2, 0} {0, 3}”⟩ → 𝐸:dom 𝐸–1-1-onto→({{0, 1}, {1, 2}} ∪ {{2, 0}, {0, 3}}))))
19	18	imp31 416	. . 3 ⊢ ((((({0, 1} ∈ V ∧ {1, 2} ∈ V) ∧ ({2, 0} ∈ V ∧ {0, 3} ∈ V)) ∧ (({0, 1} ≠ {1, 2} ∧ {0, 1} ≠ {2, 0} ∧ {0, 1} ≠ {0, 3}) ∧ ({1, 2} ≠ {2, 0} ∧ {1, 2} ≠ {0, 3} ∧ {2, 0} ≠ {0, 3}))) ∧ 𝐸 = ⟨“{0, 1} {1, 2} {2, 0} {0, 3}”⟩) → 𝐸:dom 𝐸–1-1-onto→({{0, 1}, {1, 2}} ∪ {{2, 0}, {0, 3}}))
20		dff1o5 6854	. . . 4 ⊢ (𝐸:dom 𝐸–1-1-onto→({{0, 1}, {1, 2}} ∪ {{2, 0}, {0, 3}}) ↔ (𝐸:dom 𝐸–1-1→({{0, 1}, {1, 2}} ∪ {{2, 0}, {0, 3}}) ∧ ran 𝐸 = ({{0, 1}, {1, 2}} ∪ {{2, 0}, {0, 3}})))
21	20	simprbi 495	. . 3 ⊢ (𝐸:dom 𝐸–1-1-onto→({{0, 1}, {1, 2}} ∪ {{2, 0}, {0, 3}}) → ran 𝐸 = ({{0, 1}, {1, 2}} ∪ {{2, 0}, {0, 3}}))
22	17, 19, 21	mp2b 10	. 2 ⊢ ran 𝐸 = ({{0, 1}, {1, 2}} ∪ {{2, 0}, {0, 3}})
23	1, 7, 22	3eqtri 2761	1 ⊢ (Edg‘𝐺) = ({{0, 1}, {1, 2}} ∪ {{2, 0}, {0, 3}})

Syntax hints:   ∧ wa 394   ∧ w3a 1084   = wceq 1534   ∈ wcel 2100   ≠ wne 2933  Vcvv 3472   ∪ cun 3955  {cpr 4636  ⟨cop 4640  dom cdm 5684  ran crn 5685  –1-1→wf1 6553  –1-1-onto→wf1o 6555  ‘cfv 6556  (class class class)co 7428  0cc0 11165  1c1 11166  2c2 12329  3c3 12330  4c4 12331  ...cfz 13548  ⟨“cs4 14873  Vtxcvtx 28955  iEdgciedg 28956  Edgcedg 29006

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-10 2133  ax-11 2150  ax-12 2170  ax-ext 2700  ax-rep 5291  ax-sep 5305  ax-nul 5312  ax-pow 5371  ax-pr 5435  ax-un 7749  ax-cnex 11221  ax-resscn 11222  ax-1cn 11223  ax-icn 11224  ax-addcl 11225  ax-addrcl 11226  ax-mulcl 11227  ax-mulrcl 11228  ax-mulcom 11229  ax-addass 11230  ax-mulass 11231  ax-distr 11232  ax-i2m1 11233  ax-1ne0 11234  ax-1rid 11235  ax-rnegex 11236  ax-rrecex 11237  ax-cnre 11238  ax-pre-lttri 11239  ax-pre-lttrn 11240  ax-pre-ltadd 11241  ax-pre-mulgt0 11242

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2062  df-mo 2532  df-eu 2561  df-clab 2707  df-cleq 2721  df-clel 2806  df-nfc 2881  df-ne 2934  df-nel 3040  df-ral 3055  df-rex 3064  df-reu 3374  df-rab 3429  df-v 3474  df-sbc 3787  df-csb 3903  df-dif 3960  df-un 3962  df-in 3964  df-ss 3974  df-pss 3977  df-nul 4334  df-if 4535  df-pw 4610  df-sn 4635  df-pr 4637  df-op 4641  df-uni 4917  df-int 4958  df-iun 5006  df-br 5155  df-opab 5217  df-mpt 5238  df-tr 5272  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5639  df-we 5641  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-pred 6315  df-ord 6381  df-on 6382  df-lim 6383  df-suc 6384  df-iota 6508  df-fun 6558  df-fn 6559  df-f 6560  df-f1 6561  df-fo 6562  df-f1o 6563  df-fv 6564  df-riota 7384  df-ov 7431  df-oprab 7432  df-mpo 7433  df-om 7883  df-1st 8009  df-2nd 8010  df-frecs 8302  df-wrecs 8333  df-recs 8407  df-rdg 8446  df-1o 8502  df-er 8740  df-en 8981  df-dom 8982  df-sdom 8983  df-fin 8984  df-card 9989  df-pnf 11307  df-mnf 11308  df-xr 11309  df-ltxr 11310  df-le 11311  df-sub 11503  df-neg 11504  df-nn 12275  df-2 12337  df-3 12338  df-n0 12535  df-z 12621  df-uz 12885  df-fz 13549  df-fzo 13692  df-hash 14360  df-word 14544  df-concat 14600  df-s1 14625  df-s2 14878  df-s3 14879  df-s4 14880  df-vtx 28957  df-iedg 28958  df-edg 29007

This theorem is referenced by: (None)