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