Step | Hyp | Ref
| Expression |
1 | | c0ex 10980 |
. . . . . . 7
⊢ 0 ∈
V |
2 | | 1ex 10982 |
. . . . . . 7
⊢ 1 ∈
V |
3 | 1, 2 | pm3.2i 471 |
. . . . . 6
⊢ (0 ∈
V ∧ 1 ∈ V) |
4 | | prex 5359 |
. . . . . . 7
⊢ {𝐴, 𝐵} ∈ V |
5 | 4, 4 | pm3.2i 471 |
. . . . . 6
⊢ ({𝐴, 𝐵} ∈ V ∧ {𝐴, 𝐵} ∈ V) |
6 | | 0ne1 12055 |
. . . . . . 7
⊢ 0 ≠
1 |
7 | 6 | a1i 11 |
. . . . . 6
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → 0 ≠ 1) |
8 | | fprg 7024 |
. . . . . 6
⊢ (((0
∈ V ∧ 1 ∈ V) ∧ ({𝐴, 𝐵} ∈ V ∧ {𝐴, 𝐵} ∈ V) ∧ 0 ≠ 1) → {〈0,
{𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}:{0, 1}⟶{{𝐴, 𝐵}, {𝐴, 𝐵}}) |
9 | 3, 5, 7, 8 | mp3an12i 1464 |
. . . . 5
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}:{0, 1}⟶{{𝐴, 𝐵}, {𝐴, 𝐵}}) |
10 | | dfsn2 4580 |
. . . . . 6
⊢ {{𝐴, 𝐵}} = {{𝐴, 𝐵}, {𝐴, 𝐵}} |
11 | | fveqeq2 6780 |
. . . . . . . 8
⊢ (𝑒 = {𝐴, 𝐵} → ((♯‘𝑒) = 2 ↔ (♯‘{𝐴, 𝐵}) = 2)) |
12 | | prelpwi 5367 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → {𝐴, 𝐵} ∈ 𝒫 𝑉) |
13 | 12 | 3adant1 1129 |
. . . . . . . . . 10
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → {𝐴, 𝐵} ∈ 𝒫 𝑉) |
14 | | umgr2v2evtx.g |
. . . . . . . . . . . . 13
⊢ 𝐺 = 〈𝑉, {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}〉 |
15 | 14 | umgr2v2evtx 27899 |
. . . . . . . . . . . 12
⊢ (𝑉 ∈ 𝑊 → (Vtx‘𝐺) = 𝑉) |
16 | 15 | 3ad2ant1 1132 |
. . . . . . . . . . 11
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (Vtx‘𝐺) = 𝑉) |
17 | 16 | pweqd 4558 |
. . . . . . . . . 10
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → 𝒫 (Vtx‘𝐺) = 𝒫 𝑉) |
18 | 13, 17 | eleqtrrd 2844 |
. . . . . . . . 9
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → {𝐴, 𝐵} ∈ 𝒫 (Vtx‘𝐺)) |
19 | 18 | adantr 481 |
. . . . . . . 8
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} ∈ 𝒫 (Vtx‘𝐺)) |
20 | | hashprg 14121 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴 ≠ 𝐵 ↔ (♯‘{𝐴, 𝐵}) = 2)) |
21 | 20 | biimpd 228 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴 ≠ 𝐵 → (♯‘{𝐴, 𝐵}) = 2)) |
22 | 21 | 3adant1 1129 |
. . . . . . . . 9
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴 ≠ 𝐵 → (♯‘{𝐴, 𝐵}) = 2)) |
23 | 22 | imp 407 |
. . . . . . . 8
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (♯‘{𝐴, 𝐵}) = 2) |
24 | 11, 19, 23 | elrabd 3628 |
. . . . . . 7
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} ∈ {𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑒) = 2}) |
25 | 24 | snssd 4748 |
. . . . . 6
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → {{𝐴, 𝐵}} ⊆ {𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑒) = 2}) |
26 | 10, 25 | eqsstrrid 3975 |
. . . . 5
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → {{𝐴, 𝐵}, {𝐴, 𝐵}} ⊆ {𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑒) = 2}) |
27 | 9, 26 | fssd 6616 |
. . . 4
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}:{0, 1}⟶{𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑒) = 2}) |
28 | 27 | ffdmd 6629 |
. . 3
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}:dom {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}⟶{𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑒) = 2}) |
29 | 14 | umgr2v2eiedg 27901 |
. . . . 5
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (iEdg‘𝐺) = {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}) |
30 | 29 | adantr 481 |
. . . 4
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (iEdg‘𝐺) = {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}) |
31 | 30 | dmeqd 5813 |
. . . 4
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → dom (iEdg‘𝐺) = dom {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}) |
32 | 30, 31 | feq12d 6586 |
. . 3
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → ((iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑒) = 2} ↔ {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}:dom {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}⟶{𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑒) = 2})) |
33 | 28, 32 | mpbird 256 |
. 2
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑒) = 2}) |
34 | | opex 5383 |
. . . 4
⊢
〈𝑉, {〈0,
{𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}〉 ∈ V |
35 | 14, 34 | eqeltri 2837 |
. . 3
⊢ 𝐺 ∈ V |
36 | | eqid 2740 |
. . . 4
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
37 | | eqid 2740 |
. . . 4
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
38 | 36, 37 | isumgrs 27477 |
. . 3
⊢ (𝐺 ∈ V → (𝐺 ∈ UMGraph ↔
(iEdg‘𝐺):dom
(iEdg‘𝐺)⟶{𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑒) = 2})) |
39 | 35, 38 | mp1i 13 |
. 2
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (𝐺 ∈ UMGraph ↔ (iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑒) = 2})) |
40 | 33, 39 | mpbird 256 |
1
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → 𝐺 ∈ UMGraph) |