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

Theorem usgraedg4 25916
 Description: The value of the "edge function" of a graph is a set containing two elements (the endvertices of the corresponding edge). (Contributed by Alexander van der Vekens, 18-Dec-2017.)
Assertion
Ref Expression
usgraedg4 ((𝑉 USGrph 𝐸𝑋 ∈ dom 𝐸𝑌 ∈ (𝐸𝑋)) → ∃𝑦𝑉 (𝐸𝑋) = {𝑌, 𝑦})
Distinct variable groups:   𝑦,𝐸   𝑦,𝑉   𝑦,𝑋   𝑦,𝑌

Proof of Theorem usgraedg4
Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 usgraf0 25877 . . 3 (𝑉 USGrph 𝐸𝐸:dom 𝐸1-1→{𝑦 ∈ 𝒫 𝑉 ∣ (#‘𝑦) = 2})
2 f1f 6014 . . 3 (𝐸:dom 𝐸1-1→{𝑦 ∈ 𝒫 𝑉 ∣ (#‘𝑦) = 2} → 𝐸:dom 𝐸⟶{𝑦 ∈ 𝒫 𝑉 ∣ (#‘𝑦) = 2})
3 ffvelrn 6265 . . . . 5 ((𝐸:dom 𝐸⟶{𝑦 ∈ 𝒫 𝑉 ∣ (#‘𝑦) = 2} ∧ 𝑋 ∈ dom 𝐸) → (𝐸𝑋) ∈ {𝑦 ∈ 𝒫 𝑉 ∣ (#‘𝑦) = 2})
4 fveq2 6103 . . . . . . . 8 (𝑦 = (𝐸𝑋) → (#‘𝑦) = (#‘(𝐸𝑋)))
54eqeq1d 2612 . . . . . . 7 (𝑦 = (𝐸𝑋) → ((#‘𝑦) = 2 ↔ (#‘(𝐸𝑋)) = 2))
65elrab 3331 . . . . . 6 ((𝐸𝑋) ∈ {𝑦 ∈ 𝒫 𝑉 ∣ (#‘𝑦) = 2} ↔ ((𝐸𝑋) ∈ 𝒫 𝑉 ∧ (#‘(𝐸𝑋)) = 2))
7 hash2pr 13108 . . . . . . 7 (((𝐸𝑋) ∈ 𝒫 𝑉 ∧ (#‘(𝐸𝑋)) = 2) → ∃𝑎𝑏(𝐸𝑋) = {𝑎, 𝑏})
8 19.42vv 1907 . . . . . . . . . . 11 (∃𝑎𝑏(𝑌 ∈ (𝐸𝑋) ∧ (𝐸𝑋) = {𝑎, 𝑏}) ↔ (𝑌 ∈ (𝐸𝑋) ∧ ∃𝑎𝑏(𝐸𝑋) = {𝑎, 𝑏}))
9 eleq2 2677 . . . . . . . . . . . . . . . 16 ((𝐸𝑋) = {𝑎, 𝑏} → (𝑌 ∈ (𝐸𝑋) ↔ 𝑌 ∈ {𝑎, 𝑏}))
10 elpri 4145 . . . . . . . . . . . . . . . . 17 (𝑌 ∈ {𝑎, 𝑏} → (𝑌 = 𝑎𝑌 = 𝑏))
11 andir 908 . . . . . . . . . . . . . . . . . . 19 (((𝑌 = 𝑎𝑌 = 𝑏) ∧ (𝐸𝑋) = {𝑎, 𝑏}) ↔ ((𝑌 = 𝑎 ∧ (𝐸𝑋) = {𝑎, 𝑏}) ∨ (𝑌 = 𝑏 ∧ (𝐸𝑋) = {𝑎, 𝑏})))
1211biimpi 205 . . . . . . . . . . . . . . . . . 18 (((𝑌 = 𝑎𝑌 = 𝑏) ∧ (𝐸𝑋) = {𝑎, 𝑏}) → ((𝑌 = 𝑎 ∧ (𝐸𝑋) = {𝑎, 𝑏}) ∨ (𝑌 = 𝑏 ∧ (𝐸𝑋) = {𝑎, 𝑏})))
1312ex 449 . . . . . . . . . . . . . . . . 17 ((𝑌 = 𝑎𝑌 = 𝑏) → ((𝐸𝑋) = {𝑎, 𝑏} → ((𝑌 = 𝑎 ∧ (𝐸𝑋) = {𝑎, 𝑏}) ∨ (𝑌 = 𝑏 ∧ (𝐸𝑋) = {𝑎, 𝑏}))))
1410, 13syl 17 . . . . . . . . . . . . . . . 16 (𝑌 ∈ {𝑎, 𝑏} → ((𝐸𝑋) = {𝑎, 𝑏} → ((𝑌 = 𝑎 ∧ (𝐸𝑋) = {𝑎, 𝑏}) ∨ (𝑌 = 𝑏 ∧ (𝐸𝑋) = {𝑎, 𝑏}))))
159, 14syl6bi 242 . . . . . . . . . . . . . . 15 ((𝐸𝑋) = {𝑎, 𝑏} → (𝑌 ∈ (𝐸𝑋) → ((𝐸𝑋) = {𝑎, 𝑏} → ((𝑌 = 𝑎 ∧ (𝐸𝑋) = {𝑎, 𝑏}) ∨ (𝑌 = 𝑏 ∧ (𝐸𝑋) = {𝑎, 𝑏})))))
1615pm2.43a 52 . . . . . . . . . . . . . 14 ((𝐸𝑋) = {𝑎, 𝑏} → (𝑌 ∈ (𝐸𝑋) → ((𝑌 = 𝑎 ∧ (𝐸𝑋) = {𝑎, 𝑏}) ∨ (𝑌 = 𝑏 ∧ (𝐸𝑋) = {𝑎, 𝑏}))))
1716impcom 445 . . . . . . . . . . . . 13 ((𝑌 ∈ (𝐸𝑋) ∧ (𝐸𝑋) = {𝑎, 𝑏}) → ((𝑌 = 𝑎 ∧ (𝐸𝑋) = {𝑎, 𝑏}) ∨ (𝑌 = 𝑏 ∧ (𝐸𝑋) = {𝑎, 𝑏})))
18172eximi 1753 . . . . . . . . . . . 12 (∃𝑎𝑏(𝑌 ∈ (𝐸𝑋) ∧ (𝐸𝑋) = {𝑎, 𝑏}) → ∃𝑎𝑏((𝑌 = 𝑎 ∧ (𝐸𝑋) = {𝑎, 𝑏}) ∨ (𝑌 = 𝑏 ∧ (𝐸𝑋) = {𝑎, 𝑏})))
19 19.43 1799 . . . . . . . . . . . . . . 15 (∃𝑏((𝑌 = 𝑎 ∧ (𝐸𝑋) = {𝑎, 𝑏}) ∨ (𝑌 = 𝑏 ∧ (𝐸𝑋) = {𝑎, 𝑏})) ↔ (∃𝑏(𝑌 = 𝑎 ∧ (𝐸𝑋) = {𝑎, 𝑏}) ∨ ∃𝑏(𝑌 = 𝑏 ∧ (𝐸𝑋) = {𝑎, 𝑏})))
2019exbii 1764 . . . . . . . . . . . . . 14 (∃𝑎𝑏((𝑌 = 𝑎 ∧ (𝐸𝑋) = {𝑎, 𝑏}) ∨ (𝑌 = 𝑏 ∧ (𝐸𝑋) = {𝑎, 𝑏})) ↔ ∃𝑎(∃𝑏(𝑌 = 𝑎 ∧ (𝐸𝑋) = {𝑎, 𝑏}) ∨ ∃𝑏(𝑌 = 𝑏 ∧ (𝐸𝑋) = {𝑎, 𝑏})))
21 19.43 1799 . . . . . . . . . . . . . 14 (∃𝑎(∃𝑏(𝑌 = 𝑎 ∧ (𝐸𝑋) = {𝑎, 𝑏}) ∨ ∃𝑏(𝑌 = 𝑏 ∧ (𝐸𝑋) = {𝑎, 𝑏})) ↔ (∃𝑎𝑏(𝑌 = 𝑎 ∧ (𝐸𝑋) = {𝑎, 𝑏}) ∨ ∃𝑎𝑏(𝑌 = 𝑏 ∧ (𝐸𝑋) = {𝑎, 𝑏})))
2220, 21bitri 263 . . . . . . . . . . . . 13 (∃𝑎𝑏((𝑌 = 𝑎 ∧ (𝐸𝑋) = {𝑎, 𝑏}) ∨ (𝑌 = 𝑏 ∧ (𝐸𝑋) = {𝑎, 𝑏})) ↔ (∃𝑎𝑏(𝑌 = 𝑎 ∧ (𝐸𝑋) = {𝑎, 𝑏}) ∨ ∃𝑎𝑏(𝑌 = 𝑏 ∧ (𝐸𝑋) = {𝑎, 𝑏})))
23 preq2 4213 . . . . . . . . . . . . . . . . . . 19 (𝑏 = 𝑦 → {𝑎, 𝑏} = {𝑎, 𝑦})
2423eqeq2d 2620 . . . . . . . . . . . . . . . . . 18 (𝑏 = 𝑦 → ((𝐸𝑋) = {𝑎, 𝑏} ↔ (𝐸𝑋) = {𝑎, 𝑦}))
2524anbi2d 736 . . . . . . . . . . . . . . . . 17 (𝑏 = 𝑦 → ((𝑌 = 𝑎 ∧ (𝐸𝑋) = {𝑎, 𝑏}) ↔ (𝑌 = 𝑎 ∧ (𝐸𝑋) = {𝑎, 𝑦})))
2625cbvexv 2263 . . . . . . . . . . . . . . . 16 (∃𝑏(𝑌 = 𝑎 ∧ (𝐸𝑋) = {𝑎, 𝑏}) ↔ ∃𝑦(𝑌 = 𝑎 ∧ (𝐸𝑋) = {𝑎, 𝑦}))
27 preq1 4212 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = 𝑌 → {𝑎, 𝑦} = {𝑌, 𝑦})
2827eqcoms 2618 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑌 = 𝑎 → {𝑎, 𝑦} = {𝑌, 𝑦})
2928eqeq2d 2620 . . . . . . . . . . . . . . . . . . . . . 22 (𝑌 = 𝑎 → ((𝐸𝑋) = {𝑎, 𝑦} ↔ (𝐸𝑋) = {𝑌, 𝑦}))
3029biimpa 500 . . . . . . . . . . . . . . . . . . . . 21 ((𝑌 = 𝑎 ∧ (𝐸𝑋) = {𝑎, 𝑦}) → (𝐸𝑋) = {𝑌, 𝑦})
31 vex 3176 . . . . . . . . . . . . . . . . . . . . . . 23 𝑎 ∈ V
32 eleq1 2676 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑌 = 𝑎 → (𝑌 ∈ V ↔ 𝑎 ∈ V))
3331, 32mpbiri 247 . . . . . . . . . . . . . . . . . . . . . 22 (𝑌 = 𝑎𝑌 ∈ V)
3433adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝑌 = 𝑎 ∧ (𝐸𝑋) = {𝑎, 𝑦}) → 𝑌 ∈ V)
35 eleq1 2676 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐸𝑋) = {𝑌, 𝑦} → ((𝐸𝑋) ∈ 𝒫 𝑉 ↔ {𝑌, 𝑦} ∈ 𝒫 𝑉))
36 prex 4836 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 {𝑌, 𝑦} ∈ V
3736elpw 4114 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ({𝑌, 𝑦} ∈ 𝒫 𝑉 ↔ {𝑌, 𝑦} ⊆ 𝑉)
38 vex 3176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑦 ∈ V
39 prssg 4290 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑌 ∈ V ∧ 𝑦 ∈ V) → ((𝑌𝑉𝑦𝑉) ↔ {𝑌, 𝑦} ⊆ 𝑉))
4039bicomd 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑌 ∈ V ∧ 𝑦 ∈ V) → ({𝑌, 𝑦} ⊆ 𝑉 ↔ (𝑌𝑉𝑦𝑉)))
4138, 40mpan2 703 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑌 ∈ V → ({𝑌, 𝑦} ⊆ 𝑉 ↔ (𝑌𝑉𝑦𝑉)))
42 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑌𝑉𝑦𝑉) → 𝑦𝑉)
4341, 42syl6bi 242 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑌 ∈ V → ({𝑌, 𝑦} ⊆ 𝑉𝑦𝑉))
4443com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ({𝑌, 𝑦} ⊆ 𝑉 → (𝑌 ∈ V → 𝑦𝑉))
4537, 44sylbi 206 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ({𝑌, 𝑦} ∈ 𝒫 𝑉 → (𝑌 ∈ V → 𝑦𝑉))
4635, 45syl6bi 242 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐸𝑋) = {𝑌, 𝑦} → ((𝐸𝑋) ∈ 𝒫 𝑉 → (𝑌 ∈ V → 𝑦𝑉)))
4746com23 84 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐸𝑋) = {𝑌, 𝑦} → (𝑌 ∈ V → ((𝐸𝑋) ∈ 𝒫 𝑉𝑦𝑉)))
4847imp 444 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐸𝑋) = {𝑌, 𝑦} ∧ 𝑌 ∈ V) → ((𝐸𝑋) ∈ 𝒫 𝑉𝑦𝑉))
4948imp 444 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐸𝑋) = {𝑌, 𝑦} ∧ 𝑌 ∈ V) ∧ (𝐸𝑋) ∈ 𝒫 𝑉) → 𝑦𝑉)
50 simpll 786 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐸𝑋) = {𝑌, 𝑦} ∧ 𝑌 ∈ V) ∧ (𝐸𝑋) ∈ 𝒫 𝑉) → (𝐸𝑋) = {𝑌, 𝑦})
5149, 50jca 553 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐸𝑋) = {𝑌, 𝑦} ∧ 𝑌 ∈ V) ∧ (𝐸𝑋) ∈ 𝒫 𝑉) → (𝑦𝑉 ∧ (𝐸𝑋) = {𝑌, 𝑦}))
5251ex 449 . . . . . . . . . . . . . . . . . . . . 21 (((𝐸𝑋) = {𝑌, 𝑦} ∧ 𝑌 ∈ V) → ((𝐸𝑋) ∈ 𝒫 𝑉 → (𝑦𝑉 ∧ (𝐸𝑋) = {𝑌, 𝑦})))
5330, 34, 52syl2anc 691 . . . . . . . . . . . . . . . . . . . 20 ((𝑌 = 𝑎 ∧ (𝐸𝑋) = {𝑎, 𝑦}) → ((𝐸𝑋) ∈ 𝒫 𝑉 → (𝑦𝑉 ∧ (𝐸𝑋) = {𝑌, 𝑦})))
5453com12 32 . . . . . . . . . . . . . . . . . . 19 ((𝐸𝑋) ∈ 𝒫 𝑉 → ((𝑌 = 𝑎 ∧ (𝐸𝑋) = {𝑎, 𝑦}) → (𝑦𝑉 ∧ (𝐸𝑋) = {𝑌, 𝑦})))
5554eximdv 1833 . . . . . . . . . . . . . . . . . 18 ((𝐸𝑋) ∈ 𝒫 𝑉 → (∃𝑦(𝑌 = 𝑎 ∧ (𝐸𝑋) = {𝑎, 𝑦}) → ∃𝑦(𝑦𝑉 ∧ (𝐸𝑋) = {𝑌, 𝑦})))
56 df-rex 2902 . . . . . . . . . . . . . . . . . 18 (∃𝑦𝑉 (𝐸𝑋) = {𝑌, 𝑦} ↔ ∃𝑦(𝑦𝑉 ∧ (𝐸𝑋) = {𝑌, 𝑦}))
5755, 56syl6ibr 241 . . . . . . . . . . . . . . . . 17 ((𝐸𝑋) ∈ 𝒫 𝑉 → (∃𝑦(𝑌 = 𝑎 ∧ (𝐸𝑋) = {𝑎, 𝑦}) → ∃𝑦𝑉 (𝐸𝑋) = {𝑌, 𝑦}))
5857com12 32 . . . . . . . . . . . . . . . 16 (∃𝑦(𝑌 = 𝑎 ∧ (𝐸𝑋) = {𝑎, 𝑦}) → ((𝐸𝑋) ∈ 𝒫 𝑉 → ∃𝑦𝑉 (𝐸𝑋) = {𝑌, 𝑦}))
5926, 58sylbi 206 . . . . . . . . . . . . . . 15 (∃𝑏(𝑌 = 𝑎 ∧ (𝐸𝑋) = {𝑎, 𝑏}) → ((𝐸𝑋) ∈ 𝒫 𝑉 → ∃𝑦𝑉 (𝐸𝑋) = {𝑌, 𝑦}))
6059exlimiv 1845 . . . . . . . . . . . . . 14 (∃𝑎𝑏(𝑌 = 𝑎 ∧ (𝐸𝑋) = {𝑎, 𝑏}) → ((𝐸𝑋) ∈ 𝒫 𝑉 → ∃𝑦𝑉 (𝐸𝑋) = {𝑌, 𝑦}))
61 excom 2029 . . . . . . . . . . . . . . 15 (∃𝑎𝑏(𝑌 = 𝑏 ∧ (𝐸𝑋) = {𝑎, 𝑏}) ↔ ∃𝑏𝑎(𝑌 = 𝑏 ∧ (𝐸𝑋) = {𝑎, 𝑏}))
62 preq1 4212 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑦 → {𝑎, 𝑏} = {𝑦, 𝑏})
6362eqeq2d 2620 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑦 → ((𝐸𝑋) = {𝑎, 𝑏} ↔ (𝐸𝑋) = {𝑦, 𝑏}))
6463anbi2d 736 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑦 → ((𝑌 = 𝑏 ∧ (𝐸𝑋) = {𝑎, 𝑏}) ↔ (𝑌 = 𝑏 ∧ (𝐸𝑋) = {𝑦, 𝑏})))
6564cbvexv 2263 . . . . . . . . . . . . . . . . 17 (∃𝑎(𝑌 = 𝑏 ∧ (𝐸𝑋) = {𝑎, 𝑏}) ↔ ∃𝑦(𝑌 = 𝑏 ∧ (𝐸𝑋) = {𝑦, 𝑏}))
66 preq2 4213 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑏 = 𝑌 → {𝑦, 𝑏} = {𝑦, 𝑌})
6766eqcoms 2618 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑌 = 𝑏 → {𝑦, 𝑏} = {𝑦, 𝑌})
6867eqeq2d 2620 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑌 = 𝑏 → ((𝐸𝑋) = {𝑦, 𝑏} ↔ (𝐸𝑋) = {𝑦, 𝑌}))
6968biimpa 500 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑌 = 𝑏 ∧ (𝐸𝑋) = {𝑦, 𝑏}) → (𝐸𝑋) = {𝑦, 𝑌})
70 vex 3176 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑏 ∈ V
71 eleq1 2676 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑌 = 𝑏 → (𝑌 ∈ V ↔ 𝑏 ∈ V))
7270, 71mpbiri 247 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑌 = 𝑏𝑌 ∈ V)
7372adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑌 = 𝑏 ∧ (𝐸𝑋) = {𝑦, 𝑏}) → 𝑌 ∈ V)
74 eleq1 2676 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐸𝑋) = {𝑦, 𝑌} → ((𝐸𝑋) ∈ 𝒫 𝑉 ↔ {𝑦, 𝑌} ∈ 𝒫 𝑉))
75 prex 4836 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 {𝑦, 𝑌} ∈ V
7675elpw 4114 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ({𝑦, 𝑌} ∈ 𝒫 𝑉 ↔ {𝑦, 𝑌} ⊆ 𝑉)
77 prssg 4290 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑦 ∈ V ∧ 𝑌 ∈ V) → ((𝑦𝑉𝑌𝑉) ↔ {𝑦, 𝑌} ⊆ 𝑉))
7877bicomd 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑦 ∈ V ∧ 𝑌 ∈ V) → ({𝑦, 𝑌} ⊆ 𝑉 ↔ (𝑦𝑉𝑌𝑉)))
7938, 78mpan 702 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑌 ∈ V → ({𝑦, 𝑌} ⊆ 𝑉 ↔ (𝑦𝑉𝑌𝑉)))
80 simpl 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑦𝑉𝑌𝑉) → 𝑦𝑉)
8179, 80syl6bi 242 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑌 ∈ V → ({𝑦, 𝑌} ⊆ 𝑉𝑦𝑉))
8281com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ({𝑦, 𝑌} ⊆ 𝑉 → (𝑌 ∈ V → 𝑦𝑉))
8376, 82sylbi 206 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ({𝑦, 𝑌} ∈ 𝒫 𝑉 → (𝑌 ∈ V → 𝑦𝑉))
8474, 83syl6bi 242 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐸𝑋) = {𝑦, 𝑌} → ((𝐸𝑋) ∈ 𝒫 𝑉 → (𝑌 ∈ V → 𝑦𝑉)))
8584com23 84 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐸𝑋) = {𝑦, 𝑌} → (𝑌 ∈ V → ((𝐸𝑋) ∈ 𝒫 𝑉𝑦𝑉)))
8685imp 444 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐸𝑋) = {𝑦, 𝑌} ∧ 𝑌 ∈ V) → ((𝐸𝑋) ∈ 𝒫 𝑉𝑦𝑉))
87 prcom 4211 . . . . . . . . . . . . . . . . . . . . . . . . . 26 {𝑦, 𝑌} = {𝑌, 𝑦}
8887eqeq2i 2622 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐸𝑋) = {𝑦, 𝑌} ↔ (𝐸𝑋) = {𝑌, 𝑦})
8988biimpi 205 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐸𝑋) = {𝑦, 𝑌} → (𝐸𝑋) = {𝑌, 𝑦})
9089adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐸𝑋) = {𝑦, 𝑌} ∧ 𝑌 ∈ V) → (𝐸𝑋) = {𝑌, 𝑦})
9186, 90jctird 565 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐸𝑋) = {𝑦, 𝑌} ∧ 𝑌 ∈ V) → ((𝐸𝑋) ∈ 𝒫 𝑉 → (𝑦𝑉 ∧ (𝐸𝑋) = {𝑌, 𝑦})))
9269, 73, 91syl2anc 691 . . . . . . . . . . . . . . . . . . . . 21 ((𝑌 = 𝑏 ∧ (𝐸𝑋) = {𝑦, 𝑏}) → ((𝐸𝑋) ∈ 𝒫 𝑉 → (𝑦𝑉 ∧ (𝐸𝑋) = {𝑌, 𝑦})))
9392com12 32 . . . . . . . . . . . . . . . . . . . 20 ((𝐸𝑋) ∈ 𝒫 𝑉 → ((𝑌 = 𝑏 ∧ (𝐸𝑋) = {𝑦, 𝑏}) → (𝑦𝑉 ∧ (𝐸𝑋) = {𝑌, 𝑦})))
9493eximdv 1833 . . . . . . . . . . . . . . . . . . 19 ((𝐸𝑋) ∈ 𝒫 𝑉 → (∃𝑦(𝑌 = 𝑏 ∧ (𝐸𝑋) = {𝑦, 𝑏}) → ∃𝑦(𝑦𝑉 ∧ (𝐸𝑋) = {𝑌, 𝑦})))
9594, 56syl6ibr 241 . . . . . . . . . . . . . . . . . 18 ((𝐸𝑋) ∈ 𝒫 𝑉 → (∃𝑦(𝑌 = 𝑏 ∧ (𝐸𝑋) = {𝑦, 𝑏}) → ∃𝑦𝑉 (𝐸𝑋) = {𝑌, 𝑦}))
9695com12 32 . . . . . . . . . . . . . . . . 17 (∃𝑦(𝑌 = 𝑏 ∧ (𝐸𝑋) = {𝑦, 𝑏}) → ((𝐸𝑋) ∈ 𝒫 𝑉 → ∃𝑦𝑉 (𝐸𝑋) = {𝑌, 𝑦}))
9765, 96sylbi 206 . . . . . . . . . . . . . . . 16 (∃𝑎(𝑌 = 𝑏 ∧ (𝐸𝑋) = {𝑎, 𝑏}) → ((𝐸𝑋) ∈ 𝒫 𝑉 → ∃𝑦𝑉 (𝐸𝑋) = {𝑌, 𝑦}))
9897exlimiv 1845 . . . . . . . . . . . . . . 15 (∃𝑏𝑎(𝑌 = 𝑏 ∧ (𝐸𝑋) = {𝑎, 𝑏}) → ((𝐸𝑋) ∈ 𝒫 𝑉 → ∃𝑦𝑉 (𝐸𝑋) = {𝑌, 𝑦}))
9961, 98sylbi 206 . . . . . . . . . . . . . 14 (∃𝑎𝑏(𝑌 = 𝑏 ∧ (𝐸𝑋) = {𝑎, 𝑏}) → ((𝐸𝑋) ∈ 𝒫 𝑉 → ∃𝑦𝑉 (𝐸𝑋) = {𝑌, 𝑦}))
10060, 99jaoi 393 . . . . . . . . . . . . 13 ((∃𝑎𝑏(𝑌 = 𝑎 ∧ (𝐸𝑋) = {𝑎, 𝑏}) ∨ ∃𝑎𝑏(𝑌 = 𝑏 ∧ (𝐸𝑋) = {𝑎, 𝑏})) → ((𝐸𝑋) ∈ 𝒫 𝑉 → ∃𝑦𝑉 (𝐸𝑋) = {𝑌, 𝑦}))
10122, 100sylbi 206 . . . . . . . . . . . 12 (∃𝑎𝑏((𝑌 = 𝑎 ∧ (𝐸𝑋) = {𝑎, 𝑏}) ∨ (𝑌 = 𝑏 ∧ (𝐸𝑋) = {𝑎, 𝑏})) → ((𝐸𝑋) ∈ 𝒫 𝑉 → ∃𝑦𝑉 (𝐸𝑋) = {𝑌, 𝑦}))
10218, 101syl 17 . . . . . . . . . . 11 (∃𝑎𝑏(𝑌 ∈ (𝐸𝑋) ∧ (𝐸𝑋) = {𝑎, 𝑏}) → ((𝐸𝑋) ∈ 𝒫 𝑉 → ∃𝑦𝑉 (𝐸𝑋) = {𝑌, 𝑦}))
1038, 102sylbir 224 . . . . . . . . . 10 ((𝑌 ∈ (𝐸𝑋) ∧ ∃𝑎𝑏(𝐸𝑋) = {𝑎, 𝑏}) → ((𝐸𝑋) ∈ 𝒫 𝑉 → ∃𝑦𝑉 (𝐸𝑋) = {𝑌, 𝑦}))
104103ex 449 . . . . . . . . 9 (𝑌 ∈ (𝐸𝑋) → (∃𝑎𝑏(𝐸𝑋) = {𝑎, 𝑏} → ((𝐸𝑋) ∈ 𝒫 𝑉 → ∃𝑦𝑉 (𝐸𝑋) = {𝑌, 𝑦})))
105104com13 86 . . . . . . . 8 ((𝐸𝑋) ∈ 𝒫 𝑉 → (∃𝑎𝑏(𝐸𝑋) = {𝑎, 𝑏} → (𝑌 ∈ (𝐸𝑋) → ∃𝑦𝑉 (𝐸𝑋) = {𝑌, 𝑦})))
106105adantr 480 . . . . . . 7 (((𝐸𝑋) ∈ 𝒫 𝑉 ∧ (#‘(𝐸𝑋)) = 2) → (∃𝑎𝑏(𝐸𝑋) = {𝑎, 𝑏} → (𝑌 ∈ (𝐸𝑋) → ∃𝑦𝑉 (𝐸𝑋) = {𝑌, 𝑦})))
1077, 106mpd 15 . . . . . 6 (((𝐸𝑋) ∈ 𝒫 𝑉 ∧ (#‘(𝐸𝑋)) = 2) → (𝑌 ∈ (𝐸𝑋) → ∃𝑦𝑉 (𝐸𝑋) = {𝑌, 𝑦}))
1086, 107sylbi 206 . . . . 5 ((𝐸𝑋) ∈ {𝑦 ∈ 𝒫 𝑉 ∣ (#‘𝑦) = 2} → (𝑌 ∈ (𝐸𝑋) → ∃𝑦𝑉 (𝐸𝑋) = {𝑌, 𝑦}))
1093, 108syl 17 . . . 4 ((𝐸:dom 𝐸⟶{𝑦 ∈ 𝒫 𝑉 ∣ (#‘𝑦) = 2} ∧ 𝑋 ∈ dom 𝐸) → (𝑌 ∈ (𝐸𝑋) → ∃𝑦𝑉 (𝐸𝑋) = {𝑌, 𝑦}))
110109ex 449 . . 3 (𝐸:dom 𝐸⟶{𝑦 ∈ 𝒫 𝑉 ∣ (#‘𝑦) = 2} → (𝑋 ∈ dom 𝐸 → (𝑌 ∈ (𝐸𝑋) → ∃𝑦𝑉 (𝐸𝑋) = {𝑌, 𝑦})))
1111, 2, 1103syl 18 . 2 (𝑉 USGrph 𝐸 → (𝑋 ∈ dom 𝐸 → (𝑌 ∈ (𝐸𝑋) → ∃𝑦𝑉 (𝐸𝑋) = {𝑌, 𝑦})))
1121113imp 1249 1 ((𝑉 USGrph 𝐸𝑋 ∈ dom 𝐸𝑌 ∈ (𝐸𝑋)) → ∃𝑦𝑉 (𝐸𝑋) = {𝑌, 𝑦})
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   ∧ w3a 1031   = wceq 1475  ∃wex 1695   ∈ wcel 1977  ∃wrex 2897  {crab 2900  Vcvv 3173   ⊆ wss 3540  𝒫 cpw 4108  {cpr 4127   class class class wbr 4583  dom cdm 5038  ⟶wf 5800  –1-1→wf1 5801  ‘cfv 5804  2c2 10947  #chash 12979   USGrph cusg 25859 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-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  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-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-card 8648  df-cda 8873  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-2 10956  df-n0 11170  df-z 11255  df-uz 11564  df-fz 12198  df-hash 12980  df-usgra 25862 This theorem is referenced by:  usgraedgreu  25917  nbgraf1olem5  25974
 Copyright terms: Public domain W3C validator