| Step | Hyp | Ref
| Expression |
| 1 | | frgrusgr 30280 |
. . . . . 6
⊢ (𝐺 ∈ FriendGraph → 𝐺 ∈
USGraph) |
| 2 | 1 | anim1i 615 |
. . . . 5
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑁 ∈ 𝑉) → (𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉)) |
| 3 | 2 | adantr 480 |
. . . 4
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑁 ∈ 𝑉) ∧ 1 < (♯‘𝑉)) → (𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉)) |
| 4 | | vdn1frgrv2.v |
. . . . 5
⊢ 𝑉 = (Vtx‘𝐺) |
| 5 | | eqid 2737 |
. . . . 5
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
| 6 | | eqid 2737 |
. . . . 5
⊢ dom
(iEdg‘𝐺) = dom
(iEdg‘𝐺) |
| 7 | | eqid 2737 |
. . . . 5
⊢
(VtxDeg‘𝐺) =
(VtxDeg‘𝐺) |
| 8 | 4, 5, 6, 7 | vtxdusgrval 29505 |
. . . 4
⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉) → ((VtxDeg‘𝐺)‘𝑁) = (♯‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝑁 ∈ ((iEdg‘𝐺)‘𝑥)})) |
| 9 | 3, 8 | syl 17 |
. . 3
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑁 ∈ 𝑉) ∧ 1 < (♯‘𝑉)) → ((VtxDeg‘𝐺)‘𝑁) = (♯‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝑁 ∈ ((iEdg‘𝐺)‘𝑥)})) |
| 10 | | eqid 2737 |
. . . . . . 7
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
| 11 | 4, 10 | 3cyclfrgrrn2 30306 |
. . . . . 6
⊢ ((𝐺 ∈ FriendGraph ∧ 1 <
(♯‘𝑉)) →
∀𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑏 ≠ 𝑐 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑐, 𝑎} ∈ (Edg‘𝐺)))) |
| 12 | 11 | adantlr 715 |
. . . . 5
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑁 ∈ 𝑉) ∧ 1 < (♯‘𝑉)) → ∀𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑏 ≠ 𝑐 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑐, 𝑎} ∈ (Edg‘𝐺)))) |
| 13 | | preq1 4733 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑁 → {𝑎, 𝑏} = {𝑁, 𝑏}) |
| 14 | 13 | eleq1d 2826 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑁 → ({𝑎, 𝑏} ∈ (Edg‘𝐺) ↔ {𝑁, 𝑏} ∈ (Edg‘𝐺))) |
| 15 | | preq2 4734 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑁 → {𝑐, 𝑎} = {𝑐, 𝑁}) |
| 16 | 15 | eleq1d 2826 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑁 → ({𝑐, 𝑎} ∈ (Edg‘𝐺) ↔ {𝑐, 𝑁} ∈ (Edg‘𝐺))) |
| 17 | 14, 16 | 3anbi13d 1440 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑁 → (({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑐, 𝑎} ∈ (Edg‘𝐺)) ↔ ({𝑁, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑐, 𝑁} ∈ (Edg‘𝐺)))) |
| 18 | 17 | anbi2d 630 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑁 → ((𝑏 ≠ 𝑐 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑐, 𝑎} ∈ (Edg‘𝐺))) ↔ (𝑏 ≠ 𝑐 ∧ ({𝑁, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑐, 𝑁} ∈ (Edg‘𝐺))))) |
| 19 | 18 | 2rexbidv 3222 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑁 → (∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑏 ≠ 𝑐 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑐, 𝑎} ∈ (Edg‘𝐺))) ↔ ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑏 ≠ 𝑐 ∧ ({𝑁, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑐, 𝑁} ∈ (Edg‘𝐺))))) |
| 20 | 19 | rspcva 3620 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ 𝑉 ∧ ∀𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑏 ≠ 𝑐 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑐, 𝑎} ∈ (Edg‘𝐺)))) → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑏 ≠ 𝑐 ∧ ({𝑁, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑐, 𝑁} ∈ (Edg‘𝐺)))) |
| 21 | 1 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑏 ≠ 𝑐 ∧ ({𝑁, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑐, 𝑁} ∈ (Edg‘𝐺))) ∧ 𝑁 ∈ 𝑉) ∧ 𝐺 ∈ FriendGraph ) → 𝐺 ∈
USGraph) |
| 22 | | simplll 775 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑏 ≠ 𝑐 ∧ ({𝑁, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑐, 𝑁} ∈ (Edg‘𝐺))) ∧ 𝑁 ∈ 𝑉) ∧ 𝐺 ∈ FriendGraph ) → 𝑏 ≠ 𝑐) |
| 23 | | 3simpb 1150 |
. . . . . . . . . . . . . . . . . 18
⊢ (({𝑁, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑐, 𝑁} ∈ (Edg‘𝐺)) → ({𝑁, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑐, 𝑁} ∈ (Edg‘𝐺))) |
| 24 | 23 | ad3antlr 731 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑏 ≠ 𝑐 ∧ ({𝑁, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑐, 𝑁} ∈ (Edg‘𝐺))) ∧ 𝑁 ∈ 𝑉) ∧ 𝐺 ∈ FriendGraph ) → ({𝑁, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑐, 𝑁} ∈ (Edg‘𝐺))) |
| 25 | 5, 10 | usgr2edg1 29229 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐺 ∈ USGraph ∧ 𝑏 ≠ 𝑐) ∧ ({𝑁, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑐, 𝑁} ∈ (Edg‘𝐺))) → ¬ ∃!𝑥 ∈ dom (iEdg‘𝐺)𝑁 ∈ ((iEdg‘𝐺)‘𝑥)) |
| 26 | 21, 22, 24, 25 | syl21anc 838 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑏 ≠ 𝑐 ∧ ({𝑁, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑐, 𝑁} ∈ (Edg‘𝐺))) ∧ 𝑁 ∈ 𝑉) ∧ 𝐺 ∈ FriendGraph ) → ¬
∃!𝑥 ∈ dom
(iEdg‘𝐺)𝑁 ∈ ((iEdg‘𝐺)‘𝑥)) |
| 27 | 26 | a1d 25 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑏 ≠ 𝑐 ∧ ({𝑁, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑐, 𝑁} ∈ (Edg‘𝐺))) ∧ 𝑁 ∈ 𝑉) ∧ 𝐺 ∈ FriendGraph ) → (1 <
(♯‘𝑉) →
¬ ∃!𝑥 ∈ dom
(iEdg‘𝐺)𝑁 ∈ ((iEdg‘𝐺)‘𝑥))) |
| 28 | 27 | ex 412 |
. . . . . . . . . . . . . 14
⊢ (((𝑏 ≠ 𝑐 ∧ ({𝑁, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑐, 𝑁} ∈ (Edg‘𝐺))) ∧ 𝑁 ∈ 𝑉) → (𝐺 ∈ FriendGraph → (1 <
(♯‘𝑉) →
¬ ∃!𝑥 ∈ dom
(iEdg‘𝐺)𝑁 ∈ ((iEdg‘𝐺)‘𝑥)))) |
| 29 | 28 | ex 412 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ≠ 𝑐 ∧ ({𝑁, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑐, 𝑁} ∈ (Edg‘𝐺))) → (𝑁 ∈ 𝑉 → (𝐺 ∈ FriendGraph → (1 <
(♯‘𝑉) →
¬ ∃!𝑥 ∈ dom
(iEdg‘𝐺)𝑁 ∈ ((iEdg‘𝐺)‘𝑥))))) |
| 30 | 29 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → ((𝑏 ≠ 𝑐 ∧ ({𝑁, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑐, 𝑁} ∈ (Edg‘𝐺))) → (𝑁 ∈ 𝑉 → (𝐺 ∈ FriendGraph → (1 <
(♯‘𝑉) →
¬ ∃!𝑥 ∈ dom
(iEdg‘𝐺)𝑁 ∈ ((iEdg‘𝐺)‘𝑥)))))) |
| 31 | 30 | rexlimivv 3201 |
. . . . . . . . . . 11
⊢
(∃𝑏 ∈
𝑉 ∃𝑐 ∈ 𝑉 (𝑏 ≠ 𝑐 ∧ ({𝑁, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑐, 𝑁} ∈ (Edg‘𝐺))) → (𝑁 ∈ 𝑉 → (𝐺 ∈ FriendGraph → (1 <
(♯‘𝑉) →
¬ ∃!𝑥 ∈ dom
(iEdg‘𝐺)𝑁 ∈ ((iEdg‘𝐺)‘𝑥))))) |
| 32 | 20, 31 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ 𝑉 ∧ ∀𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑏 ≠ 𝑐 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑐, 𝑎} ∈ (Edg‘𝐺)))) → (𝑁 ∈ 𝑉 → (𝐺 ∈ FriendGraph → (1 <
(♯‘𝑉) →
¬ ∃!𝑥 ∈ dom
(iEdg‘𝐺)𝑁 ∈ ((iEdg‘𝐺)‘𝑥))))) |
| 33 | 32 | ex 412 |
. . . . . . . . 9
⊢ (𝑁 ∈ 𝑉 → (∀𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑏 ≠ 𝑐 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑐, 𝑎} ∈ (Edg‘𝐺))) → (𝑁 ∈ 𝑉 → (𝐺 ∈ FriendGraph → (1 <
(♯‘𝑉) →
¬ ∃!𝑥 ∈ dom
(iEdg‘𝐺)𝑁 ∈ ((iEdg‘𝐺)‘𝑥)))))) |
| 34 | 33 | pm2.43a 54 |
. . . . . . . 8
⊢ (𝑁 ∈ 𝑉 → (∀𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑏 ≠ 𝑐 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑐, 𝑎} ∈ (Edg‘𝐺))) → (𝐺 ∈ FriendGraph → (1 <
(♯‘𝑉) →
¬ ∃!𝑥 ∈ dom
(iEdg‘𝐺)𝑁 ∈ ((iEdg‘𝐺)‘𝑥))))) |
| 35 | 34 | com24 95 |
. . . . . . 7
⊢ (𝑁 ∈ 𝑉 → (1 < (♯‘𝑉) → (𝐺 ∈ FriendGraph → (∀𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑏 ≠ 𝑐 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑐, 𝑎} ∈ (Edg‘𝐺))) → ¬ ∃!𝑥 ∈ dom (iEdg‘𝐺)𝑁 ∈ ((iEdg‘𝐺)‘𝑥))))) |
| 36 | 35 | com3r 87 |
. . . . . 6
⊢ (𝐺 ∈ FriendGraph →
(𝑁 ∈ 𝑉 → (1 < (♯‘𝑉) → (∀𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑏 ≠ 𝑐 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑐, 𝑎} ∈ (Edg‘𝐺))) → ¬ ∃!𝑥 ∈ dom (iEdg‘𝐺)𝑁 ∈ ((iEdg‘𝐺)‘𝑥))))) |
| 37 | 36 | imp31 417 |
. . . . 5
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑁 ∈ 𝑉) ∧ 1 < (♯‘𝑉)) → (∀𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑏 ≠ 𝑐 ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑐} ∈ (Edg‘𝐺) ∧ {𝑐, 𝑎} ∈ (Edg‘𝐺))) → ¬ ∃!𝑥 ∈ dom (iEdg‘𝐺)𝑁 ∈ ((iEdg‘𝐺)‘𝑥))) |
| 38 | 12, 37 | mpd 15 |
. . . 4
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑁 ∈ 𝑉) ∧ 1 < (♯‘𝑉)) → ¬ ∃!𝑥 ∈ dom (iEdg‘𝐺)𝑁 ∈ ((iEdg‘𝐺)‘𝑥)) |
| 39 | | fvex 6919 |
. . . . . . . . 9
⊢
(iEdg‘𝐺)
∈ V |
| 40 | 39 | dmex 7931 |
. . . . . . . 8
⊢ dom
(iEdg‘𝐺) ∈
V |
| 41 | 40 | a1i 11 |
. . . . . . 7
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑁 ∈ 𝑉) ∧ 1 < (♯‘𝑉)) → dom (iEdg‘𝐺) ∈ V) |
| 42 | | rabexg 5337 |
. . . . . . 7
⊢ (dom
(iEdg‘𝐺) ∈ V
→ {𝑥 ∈ dom
(iEdg‘𝐺) ∣
𝑁 ∈ ((iEdg‘𝐺)‘𝑥)} ∈ V) |
| 43 | | hash1snb 14458 |
. . . . . . 7
⊢ ({𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝑁 ∈ ((iEdg‘𝐺)‘𝑥)} ∈ V → ((♯‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝑁 ∈ ((iEdg‘𝐺)‘𝑥)}) = 1 ↔ ∃𝑖{𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝑁 ∈ ((iEdg‘𝐺)‘𝑥)} = {𝑖})) |
| 44 | 41, 42, 43 | 3syl 18 |
. . . . . 6
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑁 ∈ 𝑉) ∧ 1 < (♯‘𝑉)) → ((♯‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝑁 ∈ ((iEdg‘𝐺)‘𝑥)}) = 1 ↔ ∃𝑖{𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝑁 ∈ ((iEdg‘𝐺)‘𝑥)} = {𝑖})) |
| 45 | | reusn 4727 |
. . . . . 6
⊢
(∃!𝑥 ∈
dom (iEdg‘𝐺)𝑁 ∈ ((iEdg‘𝐺)‘𝑥) ↔ ∃𝑖{𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝑁 ∈ ((iEdg‘𝐺)‘𝑥)} = {𝑖}) |
| 46 | 44, 45 | bitr4di 289 |
. . . . 5
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑁 ∈ 𝑉) ∧ 1 < (♯‘𝑉)) → ((♯‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝑁 ∈ ((iEdg‘𝐺)‘𝑥)}) = 1 ↔ ∃!𝑥 ∈ dom (iEdg‘𝐺)𝑁 ∈ ((iEdg‘𝐺)‘𝑥))) |
| 47 | 46 | necon3abid 2977 |
. . . 4
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑁 ∈ 𝑉) ∧ 1 < (♯‘𝑉)) → ((♯‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝑁 ∈ ((iEdg‘𝐺)‘𝑥)}) ≠ 1 ↔ ¬ ∃!𝑥 ∈ dom (iEdg‘𝐺)𝑁 ∈ ((iEdg‘𝐺)‘𝑥))) |
| 48 | 38, 47 | mpbird 257 |
. . 3
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑁 ∈ 𝑉) ∧ 1 < (♯‘𝑉)) → (♯‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝑁 ∈ ((iEdg‘𝐺)‘𝑥)}) ≠ 1) |
| 49 | 9, 48 | eqnetrd 3008 |
. 2
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑁 ∈ 𝑉) ∧ 1 < (♯‘𝑉)) → ((VtxDeg‘𝐺)‘𝑁) ≠ 1) |
| 50 | 49 | ex 412 |
1
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑁 ∈ 𝑉) → (1 < (♯‘𝑉) → ((VtxDeg‘𝐺)‘𝑁) ≠ 1)) |