Step | Hyp | Ref
| Expression |
1 | | c0ex 9913 |
. . . . . . 7
⊢ 0 ∈
V |
2 | | 1ex 9914 |
. . . . . . 7
⊢ 1 ∈
V |
3 | 1, 2 | pm3.2i 470 |
. . . . . 6
⊢ (0 ∈
V ∧ 1 ∈ V) |
4 | | prex 4836 |
. . . . . . 7
⊢ {𝐴, 𝐵} ∈ V |
5 | 4, 4 | pm3.2i 470 |
. . . . . 6
⊢ ({𝐴, 𝐵} ∈ V ∧ {𝐴, 𝐵} ∈ V) |
6 | | 0ne1 10965 |
. . . . . . 7
⊢ 0 ≠
1 |
7 | 6 | a1i 11 |
. . . . . 6
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → 0 ≠ 1) |
8 | | fprg 6327 |
. . . . . 6
⊢ (((0
∈ V ∧ 1 ∈ V) ∧ ({𝐴, 𝐵} ∈ V ∧ {𝐴, 𝐵} ∈ V) ∧ 0 ≠ 1) → {〈0,
{𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}:{0, 1}⟶{{𝐴, 𝐵}, {𝐴, 𝐵}}) |
9 | 3, 5, 7, 8 | mp3an12i 1420 |
. . . . 5
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}:{0, 1}⟶{{𝐴, 𝐵}, {𝐴, 𝐵}}) |
10 | | dfsn2 4138 |
. . . . . 6
⊢ {{𝐴, 𝐵}} = {{𝐴, 𝐵}, {𝐴, 𝐵}} |
11 | | prelpwi 4842 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → {𝐴, 𝐵} ∈ 𝒫 𝑉) |
12 | 11 | 3adant1 1072 |
. . . . . . . . . 10
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → {𝐴, 𝐵} ∈ 𝒫 𝑉) |
13 | | umgr2v2evtx.g |
. . . . . . . . . . . . 13
⊢ 𝐺 = 〈𝑉, {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}〉 |
14 | 13 | umgr2v2evtx 40737 |
. . . . . . . . . . . 12
⊢ (𝑉 ∈ 𝑊 → (Vtx‘𝐺) = 𝑉) |
15 | 14 | 3ad2ant1 1075 |
. . . . . . . . . . 11
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (Vtx‘𝐺) = 𝑉) |
16 | 15 | pweqd 4113 |
. . . . . . . . . 10
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → 𝒫 (Vtx‘𝐺) = 𝒫 𝑉) |
17 | 12, 16 | eleqtrrd 2691 |
. . . . . . . . 9
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → {𝐴, 𝐵} ∈ 𝒫 (Vtx‘𝐺)) |
18 | 17 | adantr 480 |
. . . . . . . 8
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} ∈ 𝒫 (Vtx‘𝐺)) |
19 | | hashprg 13043 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴 ≠ 𝐵 ↔ (#‘{𝐴, 𝐵}) = 2)) |
20 | 19 | biimpd 218 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴 ≠ 𝐵 → (#‘{𝐴, 𝐵}) = 2)) |
21 | 20 | 3adant1 1072 |
. . . . . . . . 9
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴 ≠ 𝐵 → (#‘{𝐴, 𝐵}) = 2)) |
22 | 21 | imp 444 |
. . . . . . . 8
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (#‘{𝐴, 𝐵}) = 2) |
23 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑒 = {𝐴, 𝐵} → (#‘𝑒) = (#‘{𝐴, 𝐵})) |
24 | 23 | eqeq1d 2612 |
. . . . . . . . 9
⊢ (𝑒 = {𝐴, 𝐵} → ((#‘𝑒) = 2 ↔ (#‘{𝐴, 𝐵}) = 2)) |
25 | 24 | elrab 3331 |
. . . . . . . 8
⊢ ({𝐴, 𝐵} ∈ {𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑒) = 2} ↔ ({𝐴, 𝐵} ∈ 𝒫 (Vtx‘𝐺) ∧ (#‘{𝐴, 𝐵}) = 2)) |
26 | 18, 22, 25 | sylanbrc 695 |
. . . . . . 7
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} ∈ {𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑒) = 2}) |
27 | 26 | snssd 4281 |
. . . . . 6
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → {{𝐴, 𝐵}} ⊆ {𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑒) = 2}) |
28 | 10, 27 | syl5eqssr 3613 |
. . . . 5
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → {{𝐴, 𝐵}, {𝐴, 𝐵}} ⊆ {𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑒) = 2}) |
29 | 9, 28 | fssd 5970 |
. . . 4
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}:{0, 1}⟶{𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑒) = 2}) |
30 | 29 | ffdmd 5976 |
. . 3
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}:dom {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}⟶{𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑒) = 2}) |
31 | 13 | umgr2v2eiedg 40739 |
. . . . 5
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (iEdg‘𝐺) = {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}) |
32 | 31 | adantr 480 |
. . . 4
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (iEdg‘𝐺) = {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}) |
33 | 32 | dmeqd 5248 |
. . . 4
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → dom (iEdg‘𝐺) = dom {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}) |
34 | 32, 33 | feq12d 5946 |
. . 3
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → ((iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑒) = 2} ↔ {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}:dom {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}⟶{𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑒) = 2})) |
35 | 30, 34 | mpbird 246 |
. 2
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑒) = 2}) |
36 | | opex 4859 |
. . . 4
⊢
〈𝑉, {〈0,
{𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}〉 ∈ V |
37 | 13, 36 | eqeltri 2684 |
. . 3
⊢ 𝐺 ∈ V |
38 | | eqid 2610 |
. . . 4
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
39 | | eqid 2610 |
. . . 4
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
40 | 38, 39 | isumgrs 25762 |
. . 3
⊢ (𝐺 ∈ V → (𝐺 ∈ UMGraph ↔
(iEdg‘𝐺):dom
(iEdg‘𝐺)⟶{𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑒) = 2})) |
41 | 37, 40 | mp1i 13 |
. 2
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (𝐺 ∈ UMGraph ↔ (iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑒) = 2})) |
42 | 35, 41 | mpbird 246 |
1
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → 𝐺 ∈ UMGraph ) |