| Step | Hyp | Ref
| Expression |
| 1 | | c0ex 11255 |
. . . . . . 7
⊢ 0 ∈
V |
| 2 | | 1ex 11257 |
. . . . . . 7
⊢ 1 ∈
V |
| 3 | 1, 2 | pm3.2i 470 |
. . . . . 6
⊢ (0 ∈
V ∧ 1 ∈ V) |
| 4 | | prex 5437 |
. . . . . . 7
⊢ {𝐴, 𝐵} ∈ V |
| 5 | 4, 4 | pm3.2i 470 |
. . . . . 6
⊢ ({𝐴, 𝐵} ∈ V ∧ {𝐴, 𝐵} ∈ V) |
| 6 | | 0ne1 12337 |
. . . . . . 7
⊢ 0 ≠
1 |
| 7 | 6 | a1i 11 |
. . . . . 6
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → 0 ≠ 1) |
| 8 | | fprg 7175 |
. . . . . 6
⊢ (((0
∈ V ∧ 1 ∈ V) ∧ ({𝐴, 𝐵} ∈ V ∧ {𝐴, 𝐵} ∈ V) ∧ 0 ≠ 1) → {〈0,
{𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}:{0, 1}⟶{{𝐴, 𝐵}, {𝐴, 𝐵}}) |
| 9 | 3, 5, 7, 8 | mp3an12i 1467 |
. . . . 5
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}:{0, 1}⟶{{𝐴, 𝐵}, {𝐴, 𝐵}}) |
| 10 | | dfsn2 4639 |
. . . . . 6
⊢ {{𝐴, 𝐵}} = {{𝐴, 𝐵}, {𝐴, 𝐵}} |
| 11 | | fveqeq2 6915 |
. . . . . . . 8
⊢ (𝑒 = {𝐴, 𝐵} → ((♯‘𝑒) = 2 ↔ (♯‘{𝐴, 𝐵}) = 2)) |
| 12 | | prelpwi 5452 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → {𝐴, 𝐵} ∈ 𝒫 𝑉) |
| 13 | 12 | 3adant1 1131 |
. . . . . . . . . 10
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → {𝐴, 𝐵} ∈ 𝒫 𝑉) |
| 14 | | umgr2v2evtx.g |
. . . . . . . . . . . . 13
⊢ 𝐺 = 〈𝑉, {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}〉 |
| 15 | 14 | umgr2v2evtx 29539 |
. . . . . . . . . . . 12
⊢ (𝑉 ∈ 𝑊 → (Vtx‘𝐺) = 𝑉) |
| 16 | 15 | 3ad2ant1 1134 |
. . . . . . . . . . 11
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (Vtx‘𝐺) = 𝑉) |
| 17 | 16 | pweqd 4617 |
. . . . . . . . . 10
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → 𝒫 (Vtx‘𝐺) = 𝒫 𝑉) |
| 18 | 13, 17 | eleqtrrd 2844 |
. . . . . . . . 9
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → {𝐴, 𝐵} ∈ 𝒫 (Vtx‘𝐺)) |
| 19 | 18 | adantr 480 |
. . . . . . . 8
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} ∈ 𝒫 (Vtx‘𝐺)) |
| 20 | | hashprg 14434 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴 ≠ 𝐵 ↔ (♯‘{𝐴, 𝐵}) = 2)) |
| 21 | 20 | biimpd 229 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴 ≠ 𝐵 → (♯‘{𝐴, 𝐵}) = 2)) |
| 22 | 21 | 3adant1 1131 |
. . . . . . . . 9
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴 ≠ 𝐵 → (♯‘{𝐴, 𝐵}) = 2)) |
| 23 | 22 | imp 406 |
. . . . . . . 8
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (♯‘{𝐴, 𝐵}) = 2) |
| 24 | 11, 19, 23 | elrabd 3694 |
. . . . . . 7
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} ∈ {𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑒) = 2}) |
| 25 | 24 | snssd 4809 |
. . . . . 6
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → {{𝐴, 𝐵}} ⊆ {𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑒) = 2}) |
| 26 | 10, 25 | eqsstrrid 4023 |
. . . . 5
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → {{𝐴, 𝐵}, {𝐴, 𝐵}} ⊆ {𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑒) = 2}) |
| 27 | 9, 26 | fssd 6753 |
. . . 4
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}:{0, 1}⟶{𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑒) = 2}) |
| 28 | 27 | ffdmd 6766 |
. . 3
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}:dom {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}⟶{𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑒) = 2}) |
| 29 | 14 | umgr2v2eiedg 29541 |
. . . . 5
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (iEdg‘𝐺) = {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}) |
| 30 | 29 | adantr 480 |
. . . 4
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (iEdg‘𝐺) = {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}) |
| 31 | 30 | dmeqd 5916 |
. . . 4
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → dom (iEdg‘𝐺) = dom {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}) |
| 32 | 30, 31 | feq12d 6724 |
. . 3
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → ((iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑒) = 2} ↔ {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}:dom {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}⟶{𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑒) = 2})) |
| 33 | 28, 32 | mpbird 257 |
. 2
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑒) = 2}) |
| 34 | | opex 5469 |
. . . 4
⊢
〈𝑉, {〈0,
{𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}〉 ∈ V |
| 35 | 14, 34 | eqeltri 2837 |
. . 3
⊢ 𝐺 ∈ V |
| 36 | | eqid 2737 |
. . . 4
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
| 37 | | eqid 2737 |
. . . 4
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
| 38 | 36, 37 | isumgrs 29113 |
. . 3
⊢ (𝐺 ∈ V → (𝐺 ∈ UMGraph ↔
(iEdg‘𝐺):dom
(iEdg‘𝐺)⟶{𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑒) = 2})) |
| 39 | 35, 38 | mp1i 13 |
. 2
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (𝐺 ∈ UMGraph ↔ (iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑒 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑒) = 2})) |
| 40 | 33, 39 | mpbird 257 |
1
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → 𝐺 ∈ UMGraph) |