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 27176 |
. 2
⊢ (𝐴 ∈ V ∧ 𝐵 ∈ V) |
6 | | hashv01gt1 13133 |
. . . 4
⊢ (𝐴 ∈ V → ((#‘𝐴) = 0 ∨ (#‘𝐴) = 1 ∨ 1 < (#‘𝐴))) |
7 | | hasheq0 13154 |
. . . . . 6
⊢ (𝐴 ∈ V → ((#‘𝐴) = 0 ↔ 𝐴 = ∅)) |
8 | | biidd 252 |
. . . . . 6
⊢ (𝐴 ∈ V → ((#‘𝐴) = 1 ↔ (#‘𝐴) = 1)) |
9 | | biidd 252 |
. . . . . 6
⊢ (𝐴 ∈ V → (1 <
(#‘𝐴) ↔ 1 <
(#‘𝐴))) |
10 | 7, 8, 9 | 3orbi123d 1398 |
. . . . 5
⊢ (𝐴 ∈ V →
(((#‘𝐴) = 0 ∨
(#‘𝐴) = 1 ∨ 1 <
(#‘𝐴)) ↔ (𝐴 = ∅ ∨ (#‘𝐴) = 1 ∨ 1 < (#‘𝐴)))) |
11 | | hashv01gt1 13133 |
. . . . . . 7
⊢ (𝐵 ∈ V → ((#‘𝐵) = 0 ∨ (#‘𝐵) = 1 ∨ 1 < (#‘𝐵))) |
12 | | hasheq0 13154 |
. . . . . . . . 9
⊢ (𝐵 ∈ V → ((#‘𝐵) = 0 ↔ 𝐵 = ∅)) |
13 | | biidd 252 |
. . . . . . . . 9
⊢ (𝐵 ∈ V → ((#‘𝐵) = 1 ↔ (#‘𝐵) = 1)) |
14 | | biidd 252 |
. . . . . . . . 9
⊢ (𝐵 ∈ V → (1 <
(#‘𝐵) ↔ 1 <
(#‘𝐵))) |
15 | 12, 13, 14 | 3orbi123d 1398 |
. . . . . . . 8
⊢ (𝐵 ∈ V →
(((#‘𝐵) = 0 ∨
(#‘𝐵) = 1 ∨ 1 <
(#‘𝐵)) ↔ (𝐵 = ∅ ∨ (#‘𝐵) = 1 ∨ 1 < (#‘𝐵)))) |
16 | | olc 399 |
. . . . . . . . . . 11
⊢ (𝐵 = ∅ →
((#‘𝐵) = 1 ∨ 𝐵 = ∅)) |
17 | 16 | olcd 408 |
. . . . . . . . . 10
⊢ (𝐵 = ∅ →
(((#‘𝐴) = 1 ∨
𝐴 = ∅) ∨
((#‘𝐵) = 1 ∨ 𝐵 = ∅))) |
18 | 17 | 2a1d 26 |
. . . . . . . . 9
⊢ (𝐵 = ∅ → ((𝐴 = ∅ ∨ (#‘𝐴) = 1 ∨ 1 < (#‘𝐴)) → (𝐺 ∈ FriendGraph → (((#‘𝐴) = 1 ∨ 𝐴 = ∅) ∨ ((#‘𝐵) = 1 ∨ 𝐵 = ∅))))) |
19 | | orc 400 |
. . . . . . . . . . 11
⊢
((#‘𝐵) = 1
→ ((#‘𝐵) = 1
∨ 𝐵 =
∅)) |
20 | 19 | olcd 408 |
. . . . . . . . . 10
⊢
((#‘𝐵) = 1
→ (((#‘𝐴) = 1
∨ 𝐴 = ∅) ∨
((#‘𝐵) = 1 ∨ 𝐵 = ∅))) |
21 | 20 | 2a1d 26 |
. . . . . . . . 9
⊢
((#‘𝐵) = 1
→ ((𝐴 = ∅ ∨
(#‘𝐴) = 1 ∨ 1 <
(#‘𝐴)) → (𝐺 ∈ FriendGraph →
(((#‘𝐴) = 1 ∨
𝐴 = ∅) ∨
((#‘𝐵) = 1 ∨ 𝐵 = ∅))))) |
22 | | olc 399 |
. . . . . . . . . . . . 13
⊢ (𝐴 = ∅ →
((#‘𝐴) = 1 ∨ 𝐴 = ∅)) |
23 | 22 | orcd 407 |
. . . . . . . . . . . 12
⊢ (𝐴 = ∅ →
(((#‘𝐴) = 1 ∨
𝐴 = ∅) ∨
((#‘𝐵) = 1 ∨ 𝐵 = ∅))) |
24 | 23 | 2a1d 26 |
. . . . . . . . . . 11
⊢ (𝐴 = ∅ → (1 <
(#‘𝐵) → (𝐺 ∈ FriendGraph →
(((#‘𝐴) = 1 ∨
𝐴 = ∅) ∨
((#‘𝐵) = 1 ∨ 𝐵 = ∅))))) |
25 | | orc 400 |
. . . . . . . . . . . . 13
⊢
((#‘𝐴) = 1
→ ((#‘𝐴) = 1
∨ 𝐴 =
∅)) |
26 | 25 | orcd 407 |
. . . . . . . . . . . 12
⊢
((#‘𝐴) = 1
→ (((#‘𝐴) = 1
∨ 𝐴 = ∅) ∨
((#‘𝐵) = 1 ∨ 𝐵 = ∅))) |
27 | 26 | 2a1d 26 |
. . . . . . . . . . 11
⊢
((#‘𝐴) = 1
→ (1 < (#‘𝐵)
→ (𝐺 ∈
FriendGraph → (((#‘𝐴) = 1 ∨ 𝐴 = ∅) ∨ ((#‘𝐵) = 1 ∨ 𝐵 = ∅))))) |
28 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
29 | 1, 2, 3, 4, 28 | frgrwopreglem5 27185 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ FriendGraph ∧ 1 <
(#‘𝐴) ∧ 1 <
(#‘𝐵)) →
∃𝑎 ∈ 𝐴 ∃𝑥 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑥} ∈ (Edg‘𝐺)) ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐺) ∧ {𝑦, 𝑎} ∈ (Edg‘𝐺)))) |
30 | | frgrusgr 27124 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ FriendGraph → 𝐺 ∈ USGraph
) |
31 | | simplll 798 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐺 ∈ USGraph ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦)) → 𝐺 ∈ USGraph ) |
32 | | elrabi 3359 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑎 ∈ {𝑥 ∈ 𝑉 ∣ (𝐷‘𝑥) = 𝐾} → 𝑎 ∈ 𝑉) |
33 | 32, 3 | eleq2s 2719 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑎 ∈ 𝐴 → 𝑎 ∈ 𝑉) |
34 | 33 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝑎 ∈ 𝑉) |
35 | 34 | ad3antlr 767 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐺 ∈ USGraph ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦)) → 𝑎 ∈ 𝑉) |
36 | | rabidim1 3117 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 ∈ {𝑥 ∈ 𝑉 ∣ (𝐷‘𝑥) = 𝐾} → 𝑥 ∈ 𝑉) |
37 | 36, 3 | eleq2s 2719 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑉) |
38 | 37 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝑉) |
39 | 38 | ad3antlr 767 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐺 ∈ USGraph ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦)) → 𝑥 ∈ 𝑉) |
40 | | simprl 794 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐺 ∈ USGraph ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦)) → 𝑎 ≠ 𝑥) |
41 | | eldifi 3732 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑏 ∈ (𝑉 ∖ 𝐴) → 𝑏 ∈ 𝑉) |
42 | 41, 4 | eleq2s 2719 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑏 ∈ 𝐵 → 𝑏 ∈ 𝑉) |
43 | 42 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → 𝑏 ∈ 𝑉) |
44 | 43 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐺 ∈ USGraph ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦)) → 𝑏 ∈ 𝑉) |
45 | | eldifi 3732 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 ∈ (𝑉 ∖ 𝐴) → 𝑦 ∈ 𝑉) |
46 | 45, 4 | eleq2s 2719 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝑉) |
47 | 46 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝑉) |
48 | 47 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐺 ∈ USGraph ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦)) → 𝑦 ∈ 𝑉) |
49 | | simprr 796 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐺 ∈ USGraph ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦)) → 𝑏 ≠ 𝑦) |
50 | 1, 28 | 4cyclusnfrgr 27156 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐺 ∈ USGraph ∧ (𝑎 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ 𝑎 ≠ 𝑥) ∧ (𝑏 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑏 ≠ 𝑦)) → ((({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑥} ∈ (Edg‘𝐺)) ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐺) ∧ {𝑦, 𝑎} ∈ (Edg‘𝐺))) → 𝐺 ∉ FriendGraph )) |
51 | 31, 35, 39, 40, 44, 48, 49, 50 | syl133anc 1349 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐺 ∈ USGraph ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦)) → ((({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑥} ∈ (Edg‘𝐺)) ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐺) ∧ {𝑦, 𝑎} ∈ (Edg‘𝐺))) → 𝐺 ∉ FriendGraph )) |
52 | 51 | exp4b 632 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐺 ∈ USGraph ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) → (({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑥} ∈ (Edg‘𝐺)) → (({𝑥, 𝑦} ∈ (Edg‘𝐺) ∧ {𝑦, 𝑎} ∈ (Edg‘𝐺)) → 𝐺 ∉ FriendGraph )))) |
53 | 52 | 3impd 1281 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐺 ∈ USGraph ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑥} ∈ (Edg‘𝐺)) ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐺) ∧ {𝑦, 𝑎} ∈ (Edg‘𝐺))) → 𝐺 ∉ FriendGraph )) |
54 | | df-nel 2898 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐺 ∉ FriendGraph ↔
¬ 𝐺 ∈ FriendGraph
) |
55 | | pm2.21 120 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬
𝐺 ∈ FriendGraph →
(𝐺 ∈ FriendGraph
→ (((#‘𝐴) = 1
∨ 𝐴 = ∅) ∨
((#‘𝐵) = 1 ∨ 𝐵 = ∅)))) |
56 | 54, 55 | sylbi 207 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐺 ∉ FriendGraph →
(𝐺 ∈ FriendGraph
→ (((#‘𝐴) = 1
∨ 𝐴 = ∅) ∨
((#‘𝐵) = 1 ∨ 𝐵 = ∅)))) |
57 | 53, 56 | syl6 35 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐺 ∈ USGraph ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑥} ∈ (Edg‘𝐺)) ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐺) ∧ {𝑦, 𝑎} ∈ (Edg‘𝐺))) → (𝐺 ∈ FriendGraph → (((#‘𝐴) = 1 ∨ 𝐴 = ∅) ∨ ((#‘𝐵) = 1 ∨ 𝐵 = ∅))))) |
58 | 57 | rexlimdvva 3038 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐺 ∈ USGraph ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) → (∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑥} ∈ (Edg‘𝐺)) ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐺) ∧ {𝑦, 𝑎} ∈ (Edg‘𝐺))) → (𝐺 ∈ FriendGraph → (((#‘𝐴) = 1 ∨ 𝐴 = ∅) ∨ ((#‘𝐵) = 1 ∨ 𝐵 = ∅))))) |
59 | 58 | rexlimdvva 3038 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺 ∈ USGraph →
(∃𝑎 ∈ 𝐴 ∃𝑥 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑥} ∈ (Edg‘𝐺)) ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐺) ∧ {𝑦, 𝑎} ∈ (Edg‘𝐺))) → (𝐺 ∈ FriendGraph → (((#‘𝐴) = 1 ∨ 𝐴 = ∅) ∨ ((#‘𝐵) = 1 ∨ 𝐵 = ∅))))) |
60 | 59 | com23 86 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ USGraph → (𝐺 ∈ FriendGraph →
(∃𝑎 ∈ 𝐴 ∃𝑥 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑥} ∈ (Edg‘𝐺)) ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐺) ∧ {𝑦, 𝑎} ∈ (Edg‘𝐺))) → (((#‘𝐴) = 1 ∨ 𝐴 = ∅) ∨ ((#‘𝐵) = 1 ∨ 𝐵 = ∅))))) |
61 | 30, 60 | mpcom 38 |
. . . . . . . . . . . . . . 15
⊢ (𝐺 ∈ FriendGraph →
(∃𝑎 ∈ 𝐴 ∃𝑥 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑥} ∈ (Edg‘𝐺)) ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐺) ∧ {𝑦, 𝑎} ∈ (Edg‘𝐺))) → (((#‘𝐴) = 1 ∨ 𝐴 = ∅) ∨ ((#‘𝐵) = 1 ∨ 𝐵 = ∅)))) |
62 | 61 | 3ad2ant1 1082 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ FriendGraph ∧ 1 <
(#‘𝐴) ∧ 1 <
(#‘𝐵)) →
(∃𝑎 ∈ 𝐴 ∃𝑥 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑥} ∈ (Edg‘𝐺)) ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐺) ∧ {𝑦, 𝑎} ∈ (Edg‘𝐺))) → (((#‘𝐴) = 1 ∨ 𝐴 = ∅) ∨ ((#‘𝐵) = 1 ∨ 𝐵 = ∅)))) |
63 | 29, 62 | mpd 15 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ FriendGraph ∧ 1 <
(#‘𝐴) ∧ 1 <
(#‘𝐵)) →
(((#‘𝐴) = 1 ∨
𝐴 = ∅) ∨
((#‘𝐵) = 1 ∨ 𝐵 = ∅))) |
64 | 63 | 3exp 1264 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ FriendGraph → (1
< (#‘𝐴) → (1
< (#‘𝐵) →
(((#‘𝐴) = 1 ∨
𝐴 = ∅) ∨
((#‘𝐵) = 1 ∨ 𝐵 = ∅))))) |
65 | 64 | com3l 89 |
. . . . . . . . . . 11
⊢ (1 <
(#‘𝐴) → (1 <
(#‘𝐵) → (𝐺 ∈ FriendGraph →
(((#‘𝐴) = 1 ∨
𝐴 = ∅) ∨
((#‘𝐵) = 1 ∨ 𝐵 = ∅))))) |
66 | 24, 27, 65 | 3jaoi 1391 |
. . . . . . . . . 10
⊢ ((𝐴 = ∅ ∨ (#‘𝐴) = 1 ∨ 1 < (#‘𝐴)) → (1 < (#‘𝐵) → (𝐺 ∈ FriendGraph → (((#‘𝐴) = 1 ∨ 𝐴 = ∅) ∨ ((#‘𝐵) = 1 ∨ 𝐵 = ∅))))) |
67 | 66 | com12 32 |
. . . . . . . . 9
⊢ (1 <
(#‘𝐵) → ((𝐴 = ∅ ∨ (#‘𝐴) = 1 ∨ 1 < (#‘𝐴)) → (𝐺 ∈ FriendGraph → (((#‘𝐴) = 1 ∨ 𝐴 = ∅) ∨ ((#‘𝐵) = 1 ∨ 𝐵 = ∅))))) |
68 | 18, 21, 67 | 3jaoi 1391 |
. . . . . . . 8
⊢ ((𝐵 = ∅ ∨ (#‘𝐵) = 1 ∨ 1 < (#‘𝐵)) → ((𝐴 = ∅ ∨ (#‘𝐴) = 1 ∨ 1 < (#‘𝐴)) → (𝐺 ∈ FriendGraph → (((#‘𝐴) = 1 ∨ 𝐴 = ∅) ∨ ((#‘𝐵) = 1 ∨ 𝐵 = ∅))))) |
69 | 15, 68 | syl6bi 243 |
. . . . . . 7
⊢ (𝐵 ∈ V →
(((#‘𝐵) = 0 ∨
(#‘𝐵) = 1 ∨ 1 <
(#‘𝐵)) → ((𝐴 = ∅ ∨ (#‘𝐴) = 1 ∨ 1 < (#‘𝐴)) → (𝐺 ∈ FriendGraph → (((#‘𝐴) = 1 ∨ 𝐴 = ∅) ∨ ((#‘𝐵) = 1 ∨ 𝐵 = ∅)))))) |
70 | 11, 69 | mpd 15 |
. . . . . 6
⊢ (𝐵 ∈ V → ((𝐴 = ∅ ∨ (#‘𝐴) = 1 ∨ 1 < (#‘𝐴)) → (𝐺 ∈ FriendGraph → (((#‘𝐴) = 1 ∨ 𝐴 = ∅) ∨ ((#‘𝐵) = 1 ∨ 𝐵 = ∅))))) |
71 | 70 | com12 32 |
. . . . 5
⊢ ((𝐴 = ∅ ∨ (#‘𝐴) = 1 ∨ 1 < (#‘𝐴)) → (𝐵 ∈ V → (𝐺 ∈ FriendGraph → (((#‘𝐴) = 1 ∨ 𝐴 = ∅) ∨ ((#‘𝐵) = 1 ∨ 𝐵 = ∅))))) |
72 | 10, 71 | syl6bi 243 |
. . . 4
⊢ (𝐴 ∈ V →
(((#‘𝐴) = 0 ∨
(#‘𝐴) = 1 ∨ 1 <
(#‘𝐴)) → (𝐵 ∈ V → (𝐺 ∈ FriendGraph →
(((#‘𝐴) = 1 ∨
𝐴 = ∅) ∨
((#‘𝐵) = 1 ∨ 𝐵 =
∅)))))) |
73 | 6, 72 | mpd 15 |
. . 3
⊢ (𝐴 ∈ V → (𝐵 ∈ V → (𝐺 ∈ FriendGraph →
(((#‘𝐴) = 1 ∨
𝐴 = ∅) ∨
((#‘𝐵) = 1 ∨ 𝐵 = ∅))))) |
74 | 73 | imp 445 |
. 2
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐺 ∈ FriendGraph →
(((#‘𝐴) = 1 ∨
𝐴 = ∅) ∨
((#‘𝐵) = 1 ∨ 𝐵 = ∅)))) |
75 | 5, 74 | ax-mp 5 |
1
⊢ (𝐺 ∈ FriendGraph →
(((#‘𝐴) = 1 ∨
𝐴 = ∅) ∨
((#‘𝐵) = 1 ∨ 𝐵 = ∅))) |