Step | Hyp | Ref
| Expression |
1 | | c0ex 10370 |
. . . . . . 7
⊢ 0 ∈
V |
2 | | 1ex 10372 |
. . . . . . 7
⊢ 1 ∈
V |
3 | 1, 2 | pm3.2i 464 |
. . . . . 6
⊢ (0 ∈
V ∧ 1 ∈ V) |
4 | | prex 5141 |
. . . . . . 7
⊢ {𝐴, 𝐵} ∈ V |
5 | 4, 4 | pm3.2i 464 |
. . . . . 6
⊢ ({𝐴, 𝐵} ∈ V ∧ {𝐴, 𝐵} ∈ V) |
6 | | 0ne1 11446 |
. . . . . . 7
⊢ 0 ≠
1 |
7 | 6 | a1i 11 |
. . . . . 6
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → 0 ≠ 1) |
8 | | fprg 6688 |
. . . . . 6
⊢ (((0
∈ V ∧ 1 ∈ V) ∧ ({𝐴, 𝐵} ∈ V ∧ {𝐴, 𝐵} ∈ V) ∧ 0 ≠ 1) → {〈0,
{𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}:{0, 1}⟶{{𝐴, 𝐵}, {𝐴, 𝐵}}) |
9 | 3, 5, 7, 8 | mp3an12i 1538 |
. . . . 5
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}:{0, 1}⟶{{𝐴, 𝐵}, {𝐴, 𝐵}}) |
10 | | dfsn2 4410 |
. . . . . 6
⊢ {{𝐴, 𝐵}} = {{𝐴, 𝐵}, {𝐴, 𝐵}} |
11 | | prelpwi 5147 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → {𝐴, 𝐵} ∈ 𝒫 𝑉) |
12 | 11 | 3adant1 1121 |
. . . . . . . . . 10
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → {𝐴, 𝐵} ∈ 𝒫 𝑉) |
13 | | umgr2v2evtx.g |
. . . . . . . . . . . . 13
⊢ 𝐺 = 〈𝑉, {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}〉 |
14 | 13 | umgr2v2evtx 26869 |
. . . . . . . . . . . 12
⊢ (𝑉 ∈ 𝑊 → (Vtx‘𝐺) = 𝑉) |
15 | 14 | 3ad2ant1 1124 |
. . . . . . . . . . 11
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (Vtx‘𝐺) = 𝑉) |
16 | 15 | pweqd 4383 |
. . . . . . . . . 10
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → 𝒫 (Vtx‘𝐺) = 𝒫 𝑉) |
17 | 12, 16 | eleqtrrd 2861 |
. . . . . . . . 9
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → {𝐴, 𝐵} ∈ 𝒫 (Vtx‘𝐺)) |
18 | 17 | adantr 474 |
. . . . . . . 8
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} ∈ 𝒫 (Vtx‘𝐺)) |
19 | | hashprg 13497 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴 ≠ 𝐵 ↔ (♯‘{𝐴, 𝐵}) = 2)) |
20 | 19 | biimpd 221 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴 ≠ 𝐵 → (♯‘{𝐴, 𝐵}) = 2)) |
21 | 20 | 3adant1 1121 |
. . . . . . . . 9
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴 ≠ 𝐵 → (♯‘{𝐴, 𝐵}) = 2)) |
22 | 21 | imp 397 |
. . . . . . . 8
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (♯‘{𝐴, 𝐵}) = 2) |
23 | | fveqeq2 6455 |
. . . . . . . . 9
⊢ (𝑒 = {𝐴, 𝐵} → ((♯‘𝑒) = 2 ↔ (♯‘{𝐴, 𝐵}) = 2)) |
24 | 23 | elrab 3571 |
. . . . . . . 8
⊢ ({𝐴, 𝐵} ∈ {𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑒) = 2} ↔ ({𝐴, 𝐵} ∈ 𝒫 (Vtx‘𝐺) ∧ (♯‘{𝐴, 𝐵}) = 2)) |
25 | 18, 22, 24 | sylanbrc 578 |
. . . . . . 7
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} ∈ {𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑒) = 2}) |
26 | 25 | snssd 4571 |
. . . . . 6
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → {{𝐴, 𝐵}} ⊆ {𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑒) = 2}) |
27 | 10, 26 | syl5eqssr 3868 |
. . . . 5
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → {{𝐴, 𝐵}, {𝐴, 𝐵}} ⊆ {𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑒) = 2}) |
28 | 9, 27 | fssd 6305 |
. . . 4
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}:{0, 1}⟶{𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑒) = 2}) |
29 | 28 | ffdmd 6313 |
. . 3
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}:dom {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}⟶{𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑒) = 2}) |
30 | 13 | umgr2v2eiedg 26871 |
. . . . 5
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (iEdg‘𝐺) = {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}) |
31 | 30 | adantr 474 |
. . . 4
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (iEdg‘𝐺) = {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}) |
32 | 31 | dmeqd 5571 |
. . . 4
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → dom (iEdg‘𝐺) = dom {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}) |
33 | 31, 32 | feq12d 6279 |
. . 3
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → ((iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑒) = 2} ↔ {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}:dom {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}⟶{𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑒) = 2})) |
34 | 29, 33 | mpbird 249 |
. 2
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑒) = 2}) |
35 | | opex 5164 |
. . . 4
⊢
〈𝑉, {〈0,
{𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}〉 ∈ V |
36 | 13, 35 | eqeltri 2854 |
. . 3
⊢ 𝐺 ∈ V |
37 | | eqid 2777 |
. . . 4
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
38 | | eqid 2777 |
. . . 4
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
39 | 37, 38 | isumgrs 26444 |
. . 3
⊢ (𝐺 ∈ V → (𝐺 ∈ UMGraph ↔
(iEdg‘𝐺):dom
(iEdg‘𝐺)⟶{𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑒) = 2})) |
40 | 36, 39 | mp1i 13 |
. 2
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (𝐺 ∈ UMGraph ↔ (iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑒) = 2})) |
41 | 34, 40 | mpbird 249 |
1
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → 𝐺 ∈ UMGraph) |