Step | Hyp | Ref
| Expression |
1 | | frgrwopreg.v |
. . 3
⊢ 𝑉 = (Vtx‘𝐺) |
2 | | frgrwopreg.d |
. . 3
⊢ 𝐷 = (VtxDeg‘𝐺) |
3 | | frgrwopreg.a |
. . 3
⊢ 𝐴 = {𝑥 ∈ 𝑉 ∣ (𝐷‘𝑥) = 𝐾} |
4 | | frgrwopreg.b |
. . 3
⊢ 𝐵 = (𝑉 ∖ 𝐴) |
5 | 1, 2, 3, 4 | frgrwopreglem1 41481 |
. 2
⊢ (𝐴 ∈ V ∧ 𝐵 ∈ V) |
6 | | hashv01gt1 12995 |
. . . 4
⊢ (𝐴 ∈ V → ((#‘𝐴) = 0 ∨ (#‘𝐴) = 1 ∨ 1 < (#‘𝐴))) |
7 | | hashv01gt1 12995 |
. . . 4
⊢ (𝐵 ∈ V → ((#‘𝐵) = 0 ∨ (#‘𝐵) = 1 ∨ 1 < (#‘𝐵))) |
8 | 6, 7 | anim12i 588 |
. . 3
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) →
(((#‘𝐴) = 0 ∨
(#‘𝐴) = 1 ∨ 1 <
(#‘𝐴)) ∧
((#‘𝐵) = 0 ∨
(#‘𝐵) = 1 ∨ 1 <
(#‘𝐵)))) |
9 | | hasheq0 13015 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ V → ((#‘𝐴) = 0 ↔ 𝐴 = ∅)) |
10 | 9 | biimpd 218 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ V → ((#‘𝐴) = 0 → 𝐴 = ∅)) |
11 | 10 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) →
((#‘𝐴) = 0 →
𝐴 =
∅)) |
12 | 11 | impcom 445 |
. . . . . . . . . 10
⊢
(((#‘𝐴) = 0
∧ (𝐴 ∈ V ∧
𝐵 ∈ V)) → 𝐴 = ∅) |
13 | 12 | olcd 407 |
. . . . . . . . 9
⊢
(((#‘𝐴) = 0
∧ (𝐴 ∈ V ∧
𝐵 ∈ V)) →
((#‘𝐴) = 1 ∨ 𝐴 = ∅)) |
14 | 13 | orcd 406 |
. . . . . . . 8
⊢
(((#‘𝐴) = 0
∧ (𝐴 ∈ V ∧
𝐵 ∈ V)) →
(((#‘𝐴) = 1 ∨
𝐴 = ∅) ∨
((#‘𝐵) = 1 ∨ 𝐵 = ∅))) |
15 | 14 | a1d 25 |
. . . . . . 7
⊢
(((#‘𝐴) = 0
∧ (𝐴 ∈ V ∧
𝐵 ∈ V)) → (𝐺 ∈ FriendGraph →
(((#‘𝐴) = 1 ∨
𝐴 = ∅) ∨
((#‘𝐵) = 1 ∨ 𝐵 = ∅)))) |
16 | 15 | ex 449 |
. . . . . 6
⊢
((#‘𝐴) = 0
→ ((𝐴 ∈ V ∧
𝐵 ∈ V) → (𝐺 ∈ FriendGraph →
(((#‘𝐴) = 1 ∨
𝐴 = ∅) ∨
((#‘𝐵) = 1 ∨ 𝐵 = ∅))))) |
17 | 16 | a1d 25 |
. . . . 5
⊢
((#‘𝐴) = 0
→ (((#‘𝐵) = 0
∨ (#‘𝐵) = 1 ∨ 1
< (#‘𝐵)) →
((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐺 ∈ FriendGraph →
(((#‘𝐴) = 1 ∨
𝐴 = ∅) ∨
((#‘𝐵) = 1 ∨ 𝐵 =
∅)))))) |
18 | | orc 399 |
. . . . . . . . 9
⊢
((#‘𝐴) = 1
→ ((#‘𝐴) = 1
∨ 𝐴 =
∅)) |
19 | 18 | orcd 406 |
. . . . . . . 8
⊢
((#‘𝐴) = 1
→ (((#‘𝐴) = 1
∨ 𝐴 = ∅) ∨
((#‘𝐵) = 1 ∨ 𝐵 = ∅))) |
20 | 19 | a1d 25 |
. . . . . . 7
⊢
((#‘𝐴) = 1
→ (𝐺 ∈
FriendGraph → (((#‘𝐴) = 1 ∨ 𝐴 = ∅) ∨ ((#‘𝐵) = 1 ∨ 𝐵 = ∅)))) |
21 | 20 | a1d 25 |
. . . . . 6
⊢
((#‘𝐴) = 1
→ ((𝐴 ∈ V ∧
𝐵 ∈ V) → (𝐺 ∈ FriendGraph →
(((#‘𝐴) = 1 ∨
𝐴 = ∅) ∨
((#‘𝐵) = 1 ∨ 𝐵 = ∅))))) |
22 | 21 | a1d 25 |
. . . . 5
⊢
((#‘𝐴) = 1
→ (((#‘𝐵) = 0
∨ (#‘𝐵) = 1 ∨ 1
< (#‘𝐵)) →
((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐺 ∈ FriendGraph →
(((#‘𝐴) = 1 ∨
𝐴 = ∅) ∨
((#‘𝐵) = 1 ∨ 𝐵 =
∅)))))) |
23 | | hasheq0 13015 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 ∈ V → ((#‘𝐵) = 0 ↔ 𝐵 = ∅)) |
24 | 23 | biimpd 218 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ V → ((#‘𝐵) = 0 → 𝐵 = ∅)) |
25 | 24 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) →
((#‘𝐵) = 0 →
𝐵 =
∅)) |
26 | 25 | impcom 445 |
. . . . . . . . . . . 12
⊢
(((#‘𝐵) = 0
∧ (𝐴 ∈ V ∧
𝐵 ∈ V)) → 𝐵 = ∅) |
27 | 26 | olcd 407 |
. . . . . . . . . . 11
⊢
(((#‘𝐵) = 0
∧ (𝐴 ∈ V ∧
𝐵 ∈ V)) →
((#‘𝐵) = 1 ∨ 𝐵 = ∅)) |
28 | 27 | olcd 407 |
. . . . . . . . . 10
⊢
(((#‘𝐵) = 0
∧ (𝐴 ∈ V ∧
𝐵 ∈ V)) →
(((#‘𝐴) = 1 ∨
𝐴 = ∅) ∨
((#‘𝐵) = 1 ∨ 𝐵 = ∅))) |
29 | 28 | a1d 25 |
. . . . . . . . 9
⊢
(((#‘𝐵) = 0
∧ (𝐴 ∈ V ∧
𝐵 ∈ V)) → (𝐺 ∈ FriendGraph →
(((#‘𝐴) = 1 ∨
𝐴 = ∅) ∨
((#‘𝐵) = 1 ∨ 𝐵 = ∅)))) |
30 | 29 | ex 449 |
. . . . . . . 8
⊢
((#‘𝐵) = 0
→ ((𝐴 ∈ V ∧
𝐵 ∈ V) → (𝐺 ∈ FriendGraph →
(((#‘𝐴) = 1 ∨
𝐴 = ∅) ∨
((#‘𝐵) = 1 ∨ 𝐵 = ∅))))) |
31 | 30 | a1d 25 |
. . . . . . 7
⊢
((#‘𝐵) = 0
→ (1 < (#‘𝐴)
→ ((𝐴 ∈ V ∧
𝐵 ∈ V) → (𝐺 ∈ FriendGraph →
(((#‘𝐴) = 1 ∨
𝐴 = ∅) ∨
((#‘𝐵) = 1 ∨ 𝐵 =
∅)))))) |
32 | | orc 399 |
. . . . . . . . . . 11
⊢
((#‘𝐵) = 1
→ ((#‘𝐵) = 1
∨ 𝐵 =
∅)) |
33 | 32 | olcd 407 |
. . . . . . . . . 10
⊢
((#‘𝐵) = 1
→ (((#‘𝐴) = 1
∨ 𝐴 = ∅) ∨
((#‘𝐵) = 1 ∨ 𝐵 = ∅))) |
34 | 33 | a1d 25 |
. . . . . . . . 9
⊢
((#‘𝐵) = 1
→ (𝐺 ∈
FriendGraph → (((#‘𝐴) = 1 ∨ 𝐴 = ∅) ∨ ((#‘𝐵) = 1 ∨ 𝐵 = ∅)))) |
35 | 34 | a1d 25 |
. . . . . . . 8
⊢
((#‘𝐵) = 1
→ ((𝐴 ∈ V ∧
𝐵 ∈ V) → (𝐺 ∈ FriendGraph →
(((#‘𝐴) = 1 ∨
𝐴 = ∅) ∨
((#‘𝐵) = 1 ∨ 𝐵 = ∅))))) |
36 | 35 | a1d 25 |
. . . . . . 7
⊢
((#‘𝐵) = 1
→ (1 < (#‘𝐴)
→ ((𝐴 ∈ V ∧
𝐵 ∈ V) → (𝐺 ∈ FriendGraph →
(((#‘𝐴) = 1 ∨
𝐴 = ∅) ∨
((#‘𝐵) = 1 ∨ 𝐵 =
∅)))))) |
37 | | frgrwopreg.e |
. . . . . . . . . . . . 13
⊢ 𝐸 = (Edg‘𝐺) |
38 | 1, 2, 3, 4, 37 | frgrwopreglem5 41485 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ FriendGraph ∧ 1 <
(#‘𝐴) ∧ 1 <
(#‘𝐵)) →
∃𝑎 ∈ 𝐴 ∃𝑥 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑏 ≠ 𝑦 ∧ 𝑎 ≠ 𝑥) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑥, 𝑏} ∈ 𝐸) ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸))) |
39 | 38 | 3expb 1258 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ FriendGraph ∧ (1
< (#‘𝐴) ∧ 1
< (#‘𝐵))) →
∃𝑎 ∈ 𝐴 ∃𝑥 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑏 ≠ 𝑦 ∧ 𝑎 ≠ 𝑥) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑥, 𝑏} ∈ 𝐸) ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸))) |
40 | | frgrusgr 41432 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ FriendGraph → 𝐺 ∈ USGraph
) |
41 | | simplll 794 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐺 ∈ USGraph ∧ ((𝑏 ≠ 𝑦 ∧ 𝑎 ≠ 𝑥) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑥, 𝑏} ∈ 𝐸) ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐺 ∈ USGraph ) |
42 | | elrabi 3328 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑎 ∈ {𝑥 ∈ 𝑉 ∣ (𝐷‘𝑥) = 𝐾} → 𝑎 ∈ 𝑉) |
43 | 42, 3 | eleq2s 2706 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑎 ∈ 𝐴 → 𝑎 ∈ 𝑉) |
44 | 43 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐺 ∈ USGraph ∧ ((𝑏 ≠ 𝑦 ∧ 𝑎 ≠ 𝑥) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑥, 𝑏} ∈ 𝐸) ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) → 𝑎 ∈ 𝑉) |
45 | 44 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐺 ∈ USGraph ∧ ((𝑏 ≠ 𝑦 ∧ 𝑎 ≠ 𝑥) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑥, 𝑏} ∈ 𝐸) ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑎 ∈ 𝑉) |
46 | 3 | rabeq2i 3170 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝑉 ∧ (𝐷‘𝑥) = 𝐾)) |
47 | 46 | simplbi 475 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑉) |
48 | 47 | ad2antll 761 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐺 ∈ USGraph ∧ ((𝑏 ≠ 𝑦 ∧ 𝑎 ≠ 𝑥) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑥, 𝑏} ∈ 𝐸) ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) → 𝑥 ∈ 𝑉) |
49 | 48 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐺 ∈ USGraph ∧ ((𝑏 ≠ 𝑦 ∧ 𝑎 ≠ 𝑥) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑥, 𝑏} ∈ 𝐸) ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥 ∈ 𝑉) |
50 | | simpr1r 1112 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐺 ∈ USGraph ∧ ((𝑏 ≠ 𝑦 ∧ 𝑎 ≠ 𝑥) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑥, 𝑏} ∈ 𝐸) ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸))) → 𝑎 ≠ 𝑥) |
51 | 50 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐺 ∈ USGraph ∧ ((𝑏 ≠ 𝑦 ∧ 𝑎 ≠ 𝑥) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑥, 𝑏} ∈ 𝐸) ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) → 𝑎 ≠ 𝑥) |
52 | 51 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐺 ∈ USGraph ∧ ((𝑏 ≠ 𝑦 ∧ 𝑎 ≠ 𝑥) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑥, 𝑏} ∈ 𝐸) ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑎 ≠ 𝑥) |
53 | 45, 49, 52 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐺 ∈ USGraph ∧ ((𝑏 ≠ 𝑦 ∧ 𝑎 ≠ 𝑥) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑥, 𝑏} ∈ 𝐸) ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑎 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ 𝑎 ≠ 𝑥)) |
54 | 4 | eleq2i 2680 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑏 ∈ 𝐵 ↔ 𝑏 ∈ (𝑉 ∖ 𝐴)) |
55 | | eldif 3550 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑏 ∈ (𝑉 ∖ 𝐴) ↔ (𝑏 ∈ 𝑉 ∧ ¬ 𝑏 ∈ 𝐴)) |
56 | 54, 55 | bitri 263 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑏 ∈ 𝐵 ↔ (𝑏 ∈ 𝑉 ∧ ¬ 𝑏 ∈ 𝐴)) |
57 | 56 | simplbi 475 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑏 ∈ 𝐵 → 𝑏 ∈ 𝑉) |
58 | 57 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐺 ∈ USGraph ∧ ((𝑏 ≠ 𝑦 ∧ 𝑎 ≠ 𝑥) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑥, 𝑏} ∈ 𝐸) ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑏 ∈ 𝑉) |
59 | 4 | eleq2i 2680 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ (𝑉 ∖ 𝐴)) |
60 | | eldif 3550 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ (𝑉 ∖ 𝐴) ↔ (𝑦 ∈ 𝑉 ∧ ¬ 𝑦 ∈ 𝐴)) |
61 | 59, 60 | bitri 263 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ 𝐵 ↔ (𝑦 ∈ 𝑉 ∧ ¬ 𝑦 ∈ 𝐴)) |
62 | 61 | simplbi 475 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝑉) |
63 | 62 | ad2antll 761 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐺 ∈ USGraph ∧ ((𝑏 ≠ 𝑦 ∧ 𝑎 ≠ 𝑥) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑥, 𝑏} ∈ 𝐸) ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ 𝑉) |
64 | | simpr1l 1111 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐺 ∈ USGraph ∧ ((𝑏 ≠ 𝑦 ∧ 𝑎 ≠ 𝑥) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑥, 𝑏} ∈ 𝐸) ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸))) → 𝑏 ≠ 𝑦) |
65 | 64 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐺 ∈ USGraph ∧ ((𝑏 ≠ 𝑦 ∧ 𝑎 ≠ 𝑥) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑥, 𝑏} ∈ 𝐸) ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) → 𝑏 ≠ 𝑦) |
66 | 65 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐺 ∈ USGraph ∧ ((𝑏 ≠ 𝑦 ∧ 𝑎 ≠ 𝑥) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑥, 𝑏} ∈ 𝐸) ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑏 ≠ 𝑦) |
67 | 58, 63, 66 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐺 ∈ USGraph ∧ ((𝑏 ≠ 𝑦 ∧ 𝑎 ≠ 𝑥) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑥, 𝑏} ∈ 𝐸) ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑏 ≠ 𝑦)) |
68 | | prcom 4211 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ {𝑥, 𝑏} = {𝑏, 𝑥} |
69 | 68 | eleq1i 2679 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ({𝑥, 𝑏} ∈ 𝐸 ↔ {𝑏, 𝑥} ∈ 𝐸) |
70 | 69 | biimpi 205 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ({𝑥, 𝑏} ∈ 𝐸 → {𝑏, 𝑥} ∈ 𝐸) |
71 | 70 | anim2i 591 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑥, 𝑏} ∈ 𝐸) → ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸)) |
72 | | prcom 4211 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ {𝑎, 𝑦} = {𝑦, 𝑎} |
73 | 72 | eleq1i 2679 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ({𝑎, 𝑦} ∈ 𝐸 ↔ {𝑦, 𝑎} ∈ 𝐸) |
74 | 73 | biimpi 205 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ({𝑎, 𝑦} ∈ 𝐸 → {𝑦, 𝑎} ∈ 𝐸) |
75 | 74 | anim1i 590 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸) → ({𝑦, 𝑎} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸)) |
76 | 75 | ancomd 466 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸) → ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸)) |
77 | 71, 76 | anim12i 588 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑥, 𝑏} ∈ 𝐸) ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸)) → (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸))) |
78 | 77 | 3adant1 1072 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑏 ≠ 𝑦 ∧ 𝑎 ≠ 𝑥) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑥, 𝑏} ∈ 𝐸) ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸)) → (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸))) |
79 | 78 | ad3antlr 763 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐺 ∈ USGraph ∧ ((𝑏 ≠ 𝑦 ∧ 𝑎 ≠ 𝑥) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑥, 𝑏} ∈ 𝐸) ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸))) |
80 | 1, 37 | 4cyclusnfrgr 41462 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐺 ∈ USGraph ∧ (𝑎 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ 𝑎 ≠ 𝑥) ∧ (𝑏 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑏 ≠ 𝑦)) → ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸)) → 𝐺 ∉ FriendGraph )) |
81 | 80 | imp 444 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐺 ∈ USGraph ∧ (𝑎 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ 𝑎 ≠ 𝑥) ∧ (𝑏 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑏 ≠ 𝑦)) ∧ (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸))) → 𝐺 ∉ FriendGraph ) |
82 | 41, 53, 67, 79, 81 | syl31anc 1321 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐺 ∈ USGraph ∧ ((𝑏 ≠ 𝑦 ∧ 𝑎 ≠ 𝑥) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑥, 𝑏} ∈ 𝐸) ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐺 ∉ FriendGraph ) |
83 | | df-nel 2783 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐺 ∉ FriendGraph ↔
¬ 𝐺 ∈ FriendGraph
) |
84 | 82, 83 | sylib 207 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐺 ∈ USGraph ∧ ((𝑏 ≠ 𝑦 ∧ 𝑎 ≠ 𝑥) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑥, 𝑏} ∈ 𝐸) ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ¬ 𝐺 ∈ FriendGraph ) |
85 | 84 | pm2.21d 117 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐺 ∈ USGraph ∧ ((𝑏 ≠ 𝑦 ∧ 𝑎 ≠ 𝑥) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑥, 𝑏} ∈ 𝐸) ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐺 ∈ FriendGraph → (((#‘𝐴) = 1 ∨ 𝐴 = ∅) ∨ ((#‘𝐵) = 1 ∨ 𝐵 = ∅)))) |
86 | 85 | exp41 636 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺 ∈ USGraph → (((𝑏 ≠ 𝑦 ∧ 𝑎 ≠ 𝑥) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑥, 𝑏} ∈ 𝐸) ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸)) → ((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝐺 ∈ FriendGraph → (((#‘𝐴) = 1 ∨ 𝐴 = ∅) ∨ ((#‘𝐵) = 1 ∨ 𝐵 = ∅))))))) |
87 | 86 | com25 97 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ USGraph → (𝐺 ∈ FriendGraph →
((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (((𝑏 ≠ 𝑦 ∧ 𝑎 ≠ 𝑥) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑥, 𝑏} ∈ 𝐸) ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸)) → (((#‘𝐴) = 1 ∨ 𝐴 = ∅) ∨ ((#‘𝐵) = 1 ∨ 𝐵 = ∅))))))) |
88 | 40, 87 | mpcom 37 |
. . . . . . . . . . . . . . 15
⊢ (𝐺 ∈ FriendGraph →
((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (((𝑏 ≠ 𝑦 ∧ 𝑎 ≠ 𝑥) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑥, 𝑏} ∈ 𝐸) ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸)) → (((#‘𝐴) = 1 ∨ 𝐴 = ∅) ∨ ((#‘𝐵) = 1 ∨ 𝐵 = ∅)))))) |
89 | 88 | imp 444 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ FriendGraph ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) → ((𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (((𝑏 ≠ 𝑦 ∧ 𝑎 ≠ 𝑥) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑥, 𝑏} ∈ 𝐸) ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸)) → (((#‘𝐴) = 1 ∨ 𝐴 = ∅) ∨ ((#‘𝐵) = 1 ∨ 𝐵 = ∅))))) |
90 | 89 | rexlimdvv 3019 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ FriendGraph ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) → (∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑏 ≠ 𝑦 ∧ 𝑎 ≠ 𝑥) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑥, 𝑏} ∈ 𝐸) ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸)) → (((#‘𝐴) = 1 ∨ 𝐴 = ∅) ∨ ((#‘𝐵) = 1 ∨ 𝐵 = ∅)))) |
91 | 90 | rexlimdvva 3020 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ FriendGraph →
(∃𝑎 ∈ 𝐴 ∃𝑥 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑏 ≠ 𝑦 ∧ 𝑎 ≠ 𝑥) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑥, 𝑏} ∈ 𝐸) ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸)) → (((#‘𝐴) = 1 ∨ 𝐴 = ∅) ∨ ((#‘𝐵) = 1 ∨ 𝐵 = ∅)))) |
92 | 91 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ FriendGraph ∧ (1
< (#‘𝐴) ∧ 1
< (#‘𝐵))) →
(∃𝑎 ∈ 𝐴 ∃𝑥 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑏 ≠ 𝑦 ∧ 𝑎 ≠ 𝑥) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑥, 𝑏} ∈ 𝐸) ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑥, 𝑦} ∈ 𝐸)) → (((#‘𝐴) = 1 ∨ 𝐴 = ∅) ∨ ((#‘𝐵) = 1 ∨ 𝐵 = ∅)))) |
93 | 39, 92 | mpd 15 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ FriendGraph ∧ (1
< (#‘𝐴) ∧ 1
< (#‘𝐵))) →
(((#‘𝐴) = 1 ∨
𝐴 = ∅) ∨
((#‘𝐵) = 1 ∨ 𝐵 = ∅))) |
94 | 93 | expcom 450 |
. . . . . . . . 9
⊢ ((1 <
(#‘𝐴) ∧ 1 <
(#‘𝐵)) → (𝐺 ∈ FriendGraph →
(((#‘𝐴) = 1 ∨
𝐴 = ∅) ∨
((#‘𝐵) = 1 ∨ 𝐵 = ∅)))) |
95 | 94 | a1d 25 |
. . . . . . . 8
⊢ ((1 <
(#‘𝐴) ∧ 1 <
(#‘𝐵)) → ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐺 ∈ FriendGraph →
(((#‘𝐴) = 1 ∨
𝐴 = ∅) ∨
((#‘𝐵) = 1 ∨ 𝐵 = ∅))))) |
96 | 95 | expcom 450 |
. . . . . . 7
⊢ (1 <
(#‘𝐵) → (1 <
(#‘𝐴) → ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐺 ∈ FriendGraph →
(((#‘𝐴) = 1 ∨
𝐴 = ∅) ∨
((#‘𝐵) = 1 ∨ 𝐵 =
∅)))))) |
97 | 31, 36, 96 | 3jaoi 1383 |
. . . . . 6
⊢
(((#‘𝐵) = 0
∨ (#‘𝐵) = 1 ∨ 1
< (#‘𝐵)) → (1
< (#‘𝐴) →
((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐺 ∈ FriendGraph →
(((#‘𝐴) = 1 ∨
𝐴 = ∅) ∨
((#‘𝐵) = 1 ∨ 𝐵 =
∅)))))) |
98 | 97 | com12 32 |
. . . . 5
⊢ (1 <
(#‘𝐴) →
(((#‘𝐵) = 0 ∨
(#‘𝐵) = 1 ∨ 1 <
(#‘𝐵)) → ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐺 ∈ FriendGraph →
(((#‘𝐴) = 1 ∨
𝐴 = ∅) ∨
((#‘𝐵) = 1 ∨ 𝐵 =
∅)))))) |
99 | 17, 22, 98 | 3jaoi 1383 |
. . . 4
⊢
(((#‘𝐴) = 0
∨ (#‘𝐴) = 1 ∨ 1
< (#‘𝐴)) →
(((#‘𝐵) = 0 ∨
(#‘𝐵) = 1 ∨ 1 <
(#‘𝐵)) → ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐺 ∈ FriendGraph →
(((#‘𝐴) = 1 ∨
𝐴 = ∅) ∨
((#‘𝐵) = 1 ∨ 𝐵 =
∅)))))) |
100 | 99 | imp 444 |
. . 3
⊢
((((#‘𝐴) = 0
∨ (#‘𝐴) = 1 ∨ 1
< (#‘𝐴)) ∧
((#‘𝐵) = 0 ∨
(#‘𝐵) = 1 ∨ 1 <
(#‘𝐵))) →
((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐺 ∈ FriendGraph →
(((#‘𝐴) = 1 ∨
𝐴 = ∅) ∨
((#‘𝐵) = 1 ∨ 𝐵 = ∅))))) |
101 | 8, 100 | mpcom 37 |
. 2
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐺 ∈ FriendGraph →
(((#‘𝐴) = 1 ∨
𝐴 = ∅) ∨
((#‘𝐵) = 1 ∨ 𝐵 = ∅)))) |
102 | 5, 101 | ax-mp 5 |
1
⊢ (𝐺 ∈ FriendGraph →
(((#‘𝐴) = 1 ∨
𝐴 = ∅) ∨
((#‘𝐵) = 1 ∨ 𝐵 = ∅))) |