Step | Hyp | Ref
| Expression |
1 | | c0ex 10034 |
. . . . . . 7
⊢ 0 ∈
V |
2 | | 1ex 10035 |
. . . . . . 7
⊢ 1 ∈
V |
3 | 1, 2 | pm3.2i 471 |
. . . . . 6
⊢ (0 ∈
V ∧ 1 ∈ V) |
4 | | prex 4909 |
. . . . . . 7
⊢ {𝐴, 𝐵} ∈ V |
5 | 4, 4 | pm3.2i 471 |
. . . . . 6
⊢ ({𝐴, 𝐵} ∈ V ∧ {𝐴, 𝐵} ∈ V) |
6 | | 0ne1 11088 |
. . . . . . 7
⊢ 0 ≠
1 |
7 | 6 | a1i 11 |
. . . . . 6
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → 0 ≠ 1) |
8 | | fprg 6422 |
. . . . . 6
⊢ (((0
∈ V ∧ 1 ∈ V) ∧ ({𝐴, 𝐵} ∈ V ∧ {𝐴, 𝐵} ∈ V) ∧ 0 ≠ 1) → {〈0,
{𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}:{0, 1}⟶{{𝐴, 𝐵}, {𝐴, 𝐵}}) |
9 | 3, 5, 7, 8 | mp3an12i 1428 |
. . . . 5
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}:{0, 1}⟶{{𝐴, 𝐵}, {𝐴, 𝐵}}) |
10 | | dfsn2 4190 |
. . . . . 6
⊢ {{𝐴, 𝐵}} = {{𝐴, 𝐵}, {𝐴, 𝐵}} |
11 | | prelpwi 4915 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → {𝐴, 𝐵} ∈ 𝒫 𝑉) |
12 | 11 | 3adant1 1079 |
. . . . . . . . . 10
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → {𝐴, 𝐵} ∈ 𝒫 𝑉) |
13 | | umgr2v2evtx.g |
. . . . . . . . . . . . 13
⊢ 𝐺 = 〈𝑉, {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}〉 |
14 | 13 | umgr2v2evtx 26417 |
. . . . . . . . . . . 12
⊢ (𝑉 ∈ 𝑊 → (Vtx‘𝐺) = 𝑉) |
15 | 14 | 3ad2ant1 1082 |
. . . . . . . . . . 11
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (Vtx‘𝐺) = 𝑉) |
16 | 15 | pweqd 4163 |
. . . . . . . . . 10
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → 𝒫 (Vtx‘𝐺) = 𝒫 𝑉) |
17 | 12, 16 | eleqtrrd 2704 |
. . . . . . . . 9
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → {𝐴, 𝐵} ∈ 𝒫 (Vtx‘𝐺)) |
18 | 17 | adantr 481 |
. . . . . . . 8
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} ∈ 𝒫 (Vtx‘𝐺)) |
19 | | hashprg 13182 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴 ≠ 𝐵 ↔ (#‘{𝐴, 𝐵}) = 2)) |
20 | 19 | biimpd 219 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴 ≠ 𝐵 → (#‘{𝐴, 𝐵}) = 2)) |
21 | 20 | 3adant1 1079 |
. . . . . . . . 9
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴 ≠ 𝐵 → (#‘{𝐴, 𝐵}) = 2)) |
22 | 21 | imp 445 |
. . . . . . . 8
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (#‘{𝐴, 𝐵}) = 2) |
23 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑒 = {𝐴, 𝐵} → (#‘𝑒) = (#‘{𝐴, 𝐵})) |
24 | 23 | eqeq1d 2624 |
. . . . . . . . 9
⊢ (𝑒 = {𝐴, 𝐵} → ((#‘𝑒) = 2 ↔ (#‘{𝐴, 𝐵}) = 2)) |
25 | 24 | elrab 3363 |
. . . . . . . 8
⊢ ({𝐴, 𝐵} ∈ {𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑒) = 2} ↔ ({𝐴, 𝐵} ∈ 𝒫 (Vtx‘𝐺) ∧ (#‘{𝐴, 𝐵}) = 2)) |
26 | 18, 22, 25 | sylanbrc 698 |
. . . . . . 7
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} ∈ {𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑒) = 2}) |
27 | 26 | snssd 4340 |
. . . . . 6
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → {{𝐴, 𝐵}} ⊆ {𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑒) = 2}) |
28 | 10, 27 | syl5eqssr 3650 |
. . . . 5
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → {{𝐴, 𝐵}, {𝐴, 𝐵}} ⊆ {𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑒) = 2}) |
29 | 9, 28 | fssd 6057 |
. . . 4
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}:{0, 1}⟶{𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑒) = 2}) |
30 | 29 | ffdmd 6063 |
. . 3
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}:dom {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}⟶{𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑒) = 2}) |
31 | 13 | umgr2v2eiedg 26419 |
. . . . 5
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (iEdg‘𝐺) = {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}) |
32 | 31 | adantr 481 |
. . . 4
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (iEdg‘𝐺) = {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}) |
33 | 32 | dmeqd 5326 |
. . . 4
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → dom (iEdg‘𝐺) = dom {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}) |
34 | 32, 33 | feq12d 6033 |
. . 3
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → ((iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑒) = 2} ↔ {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}:dom {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}⟶{𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑒) = 2})) |
35 | 30, 34 | mpbird 247 |
. 2
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑒) = 2}) |
36 | | opex 4932 |
. . . 4
⊢
〈𝑉, {〈0,
{𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}〉 ∈ V |
37 | 13, 36 | eqeltri 2697 |
. . 3
⊢ 𝐺 ∈ V |
38 | | eqid 2622 |
. . . 4
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
39 | | eqid 2622 |
. . . 4
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
40 | 38, 39 | isumgrs 25991 |
. . 3
⊢ (𝐺 ∈ V → (𝐺 ∈ UMGraph ↔
(iEdg‘𝐺):dom
(iEdg‘𝐺)⟶{𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑒) = 2})) |
41 | 37, 40 | mp1i 13 |
. 2
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (𝐺 ∈ UMGraph ↔ (iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑒) = 2})) |
42 | 35, 41 | mpbird 247 |
1
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → 𝐺 ∈ UMGraph ) |