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 28408 |
. 2
⊢ (𝐴 ∈ V ∧ 𝐵 ∈ V) |
6 | | hashv01gt1 13924 |
. . . 4
⊢ (𝐴 ∈ V →
((♯‘𝐴) = 0 ∨
(♯‘𝐴) = 1 ∨
1 < (♯‘𝐴))) |
7 | | hasheq0 13943 |
. . . . . 6
⊢ (𝐴 ∈ V →
((♯‘𝐴) = 0
↔ 𝐴 =
∅)) |
8 | | biidd 265 |
. . . . . 6
⊢ (𝐴 ∈ V →
((♯‘𝐴) = 1
↔ (♯‘𝐴) =
1)) |
9 | | biidd 265 |
. . . . . 6
⊢ (𝐴 ∈ V → (1 <
(♯‘𝐴) ↔ 1
< (♯‘𝐴))) |
10 | 7, 8, 9 | 3orbi123d 1437 |
. . . . 5
⊢ (𝐴 ∈ V →
(((♯‘𝐴) = 0
∨ (♯‘𝐴) = 1
∨ 1 < (♯‘𝐴)) ↔ (𝐴 = ∅ ∨ (♯‘𝐴) = 1 ∨ 1 <
(♯‘𝐴)))) |
11 | | hashv01gt1 13924 |
. . . . . . 7
⊢ (𝐵 ∈ V →
((♯‘𝐵) = 0 ∨
(♯‘𝐵) = 1 ∨
1 < (♯‘𝐵))) |
12 | | hasheq0 13943 |
. . . . . . . . 9
⊢ (𝐵 ∈ V →
((♯‘𝐵) = 0
↔ 𝐵 =
∅)) |
13 | | biidd 265 |
. . . . . . . . 9
⊢ (𝐵 ∈ V →
((♯‘𝐵) = 1
↔ (♯‘𝐵) =
1)) |
14 | | biidd 265 |
. . . . . . . . 9
⊢ (𝐵 ∈ V → (1 <
(♯‘𝐵) ↔ 1
< (♯‘𝐵))) |
15 | 12, 13, 14 | 3orbi123d 1437 |
. . . . . . . 8
⊢ (𝐵 ∈ V →
(((♯‘𝐵) = 0
∨ (♯‘𝐵) = 1
∨ 1 < (♯‘𝐵)) ↔ (𝐵 = ∅ ∨ (♯‘𝐵) = 1 ∨ 1 <
(♯‘𝐵)))) |
16 | | olc 868 |
. . . . . . . . . . 11
⊢ (𝐵 = ∅ →
((♯‘𝐵) = 1 ∨
𝐵 =
∅)) |
17 | 16 | olcd 874 |
. . . . . . . . . 10
⊢ (𝐵 = ∅ →
(((♯‘𝐴) = 1
∨ 𝐴 = ∅) ∨
((♯‘𝐵) = 1 ∨
𝐵 =
∅))) |
18 | 17 | 2a1d 26 |
. . . . . . . . 9
⊢ (𝐵 = ∅ → ((𝐴 = ∅ ∨
(♯‘𝐴) = 1 ∨
1 < (♯‘𝐴))
→ (𝐺 ∈
FriendGraph → (((♯‘𝐴) = 1 ∨ 𝐴 = ∅) ∨ ((♯‘𝐵) = 1 ∨ 𝐵 = ∅))))) |
19 | | orc 867 |
. . . . . . . . . . 11
⊢
((♯‘𝐵) =
1 → ((♯‘𝐵)
= 1 ∨ 𝐵 =
∅)) |
20 | 19 | olcd 874 |
. . . . . . . . . 10
⊢
((♯‘𝐵) =
1 → (((♯‘𝐴) = 1 ∨ 𝐴 = ∅) ∨ ((♯‘𝐵) = 1 ∨ 𝐵 = ∅))) |
21 | 20 | 2a1d 26 |
. . . . . . . . 9
⊢
((♯‘𝐵) =
1 → ((𝐴 = ∅ ∨
(♯‘𝐴) = 1 ∨
1 < (♯‘𝐴))
→ (𝐺 ∈
FriendGraph → (((♯‘𝐴) = 1 ∨ 𝐴 = ∅) ∨ ((♯‘𝐵) = 1 ∨ 𝐵 = ∅))))) |
22 | | olc 868 |
. . . . . . . . . . . . 13
⊢ (𝐴 = ∅ →
((♯‘𝐴) = 1 ∨
𝐴 =
∅)) |
23 | 22 | orcd 873 |
. . . . . . . . . . . 12
⊢ (𝐴 = ∅ →
(((♯‘𝐴) = 1
∨ 𝐴 = ∅) ∨
((♯‘𝐵) = 1 ∨
𝐵 =
∅))) |
24 | 23 | 2a1d 26 |
. . . . . . . . . . 11
⊢ (𝐴 = ∅ → (1 <
(♯‘𝐵) →
(𝐺 ∈ FriendGraph
→ (((♯‘𝐴)
= 1 ∨ 𝐴 = ∅) ∨
((♯‘𝐵) = 1 ∨
𝐵 =
∅))))) |
25 | | orc 867 |
. . . . . . . . . . . . 13
⊢
((♯‘𝐴) =
1 → ((♯‘𝐴)
= 1 ∨ 𝐴 =
∅)) |
26 | 25 | orcd 873 |
. . . . . . . . . . . 12
⊢
((♯‘𝐴) =
1 → (((♯‘𝐴) = 1 ∨ 𝐴 = ∅) ∨ ((♯‘𝐵) = 1 ∨ 𝐵 = ∅))) |
27 | 26 | 2a1d 26 |
. . . . . . . . . . 11
⊢
((♯‘𝐴) =
1 → (1 < (♯‘𝐵) → (𝐺 ∈ FriendGraph →
(((♯‘𝐴) = 1
∨ 𝐴 = ∅) ∨
((♯‘𝐵) = 1 ∨
𝐵 =
∅))))) |
28 | | eqid 2738 |
. . . . . . . . . . . . . . 15
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
29 | 1, 2, 3, 4, 28 | frgrwopreglem5 28417 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ FriendGraph ∧ 1 <
(♯‘𝐴) ∧ 1
< (♯‘𝐵))
→ ∃𝑎 ∈
𝐴 ∃𝑥 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑥} ∈ (Edg‘𝐺)) ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐺) ∧ {𝑦, 𝑎} ∈ (Edg‘𝐺)))) |
30 | | frgrusgr 28357 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ FriendGraph → 𝐺 ∈
USGraph) |
31 | | simplll 775 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐺 ∈ USGraph ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦)) → 𝐺 ∈ USGraph) |
32 | | elrabi 3603 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑎 ∈ {𝑥 ∈ 𝑉 ∣ (𝐷‘𝑥) = 𝐾} → 𝑎 ∈ 𝑉) |
33 | 32, 3 | eleq2s 2857 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑎 ∈ 𝐴 → 𝑎 ∈ 𝑉) |
34 | 33 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝑎 ∈ 𝑉) |
35 | 34 | ad3antlr 731 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐺 ∈ USGraph ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦)) → 𝑎 ∈ 𝑉) |
36 | | rabidim1 3299 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 ∈ {𝑥 ∈ 𝑉 ∣ (𝐷‘𝑥) = 𝐾} → 𝑥 ∈ 𝑉) |
37 | 36, 3 | eleq2s 2857 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑉) |
38 | 37 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝑉) |
39 | 38 | ad3antlr 731 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐺 ∈ USGraph ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦)) → 𝑥 ∈ 𝑉) |
40 | | simprl 771 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐺 ∈ USGraph ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦)) → 𝑎 ≠ 𝑥) |
41 | | eldifi 4050 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑏 ∈ (𝑉 ∖ 𝐴) → 𝑏 ∈ 𝑉) |
42 | 41, 4 | eleq2s 2857 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑏 ∈ 𝐵 → 𝑏 ∈ 𝑉) |
43 | 42 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → 𝑏 ∈ 𝑉) |
44 | 43 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐺 ∈ USGraph ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦)) → 𝑏 ∈ 𝑉) |
45 | | eldifi 4050 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 ∈ (𝑉 ∖ 𝐴) → 𝑦 ∈ 𝑉) |
46 | 45, 4 | eleq2s 2857 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝑉) |
47 | 46 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝑉) |
48 | 47 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐺 ∈ USGraph ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦)) → 𝑦 ∈ 𝑉) |
49 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐺 ∈ USGraph ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦)) → 𝑏 ≠ 𝑦) |
50 | 1, 28 | 4cyclusnfrgr 28388 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐺 ∈ USGraph ∧ (𝑎 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ 𝑎 ≠ 𝑥) ∧ (𝑏 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑏 ≠ 𝑦)) → ((({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑥} ∈ (Edg‘𝐺)) ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐺) ∧ {𝑦, 𝑎} ∈ (Edg‘𝐺))) → 𝐺 ∉ FriendGraph )) |
51 | 31, 35, 39, 40, 44, 48, 49, 50 | syl133anc 1395 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐺 ∈ USGraph ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦)) → ((({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑥} ∈ (Edg‘𝐺)) ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐺) ∧ {𝑦, 𝑎} ∈ (Edg‘𝐺))) → 𝐺 ∉ FriendGraph )) |
52 | 51 | exp4b 434 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐺 ∈ USGraph ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) → (({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑥} ∈ (Edg‘𝐺)) → (({𝑥, 𝑦} ∈ (Edg‘𝐺) ∧ {𝑦, 𝑎} ∈ (Edg‘𝐺)) → 𝐺 ∉ FriendGraph )))) |
53 | 52 | 3impd 1350 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐺 ∈ USGraph ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑥} ∈ (Edg‘𝐺)) ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐺) ∧ {𝑦, 𝑎} ∈ (Edg‘𝐺))) → 𝐺 ∉ FriendGraph )) |
54 | | df-nel 3048 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐺 ∉ FriendGraph ↔
¬ 𝐺 ∈ FriendGraph
) |
55 | | pm2.21 123 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬
𝐺 ∈ FriendGraph →
(𝐺 ∈ FriendGraph
→ (((♯‘𝐴)
= 1 ∨ 𝐴 = ∅) ∨
((♯‘𝐵) = 1 ∨
𝐵 =
∅)))) |
56 | 54, 55 | sylbi 220 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐺 ∉ FriendGraph →
(𝐺 ∈ FriendGraph
→ (((♯‘𝐴)
= 1 ∨ 𝐴 = ∅) ∨
((♯‘𝐵) = 1 ∨
𝐵 =
∅)))) |
57 | 53, 56 | syl6 35 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐺 ∈ USGraph ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑥} ∈ (Edg‘𝐺)) ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐺) ∧ {𝑦, 𝑎} ∈ (Edg‘𝐺))) → (𝐺 ∈ FriendGraph →
(((♯‘𝐴) = 1
∨ 𝐴 = ∅) ∨
((♯‘𝐵) = 1 ∨
𝐵 =
∅))))) |
58 | 57 | rexlimdvva 3220 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐺 ∈ USGraph ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) → (∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑥} ∈ (Edg‘𝐺)) ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐺) ∧ {𝑦, 𝑎} ∈ (Edg‘𝐺))) → (𝐺 ∈ FriendGraph →
(((♯‘𝐴) = 1
∨ 𝐴 = ∅) ∨
((♯‘𝐵) = 1 ∨
𝐵 =
∅))))) |
59 | 58 | rexlimdvva 3220 |
. . . . . . . . . . . . . . . . 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 1135 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ FriendGraph ∧ 1 <
(♯‘𝐴) ∧ 1
< (♯‘𝐵))
→ (∃𝑎 ∈
𝐴 ∃𝑥 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ (Edg‘𝐺) ∧ {𝑏, 𝑥} ∈ (Edg‘𝐺)) ∧ ({𝑥, 𝑦} ∈ (Edg‘𝐺) ∧ {𝑦, 𝑎} ∈ (Edg‘𝐺))) → (((♯‘𝐴) = 1 ∨ 𝐴 = ∅) ∨ ((♯‘𝐵) = 1 ∨ 𝐵 = ∅)))) |
63 | 29, 62 | mpd 15 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ FriendGraph ∧ 1 <
(♯‘𝐴) ∧ 1
< (♯‘𝐵))
→ (((♯‘𝐴)
= 1 ∨ 𝐴 = ∅) ∨
((♯‘𝐵) = 1 ∨
𝐵 =
∅))) |
64 | 63 | 3exp 1121 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ FriendGraph → (1
< (♯‘𝐴)
→ (1 < (♯‘𝐵) → (((♯‘𝐴) = 1 ∨ 𝐴 = ∅) ∨ ((♯‘𝐵) = 1 ∨ 𝐵 = ∅))))) |
65 | 64 | com3l 89 |
. . . . . . . . . . 11
⊢ (1 <
(♯‘𝐴) → (1
< (♯‘𝐵)
→ (𝐺 ∈
FriendGraph → (((♯‘𝐴) = 1 ∨ 𝐴 = ∅) ∨ ((♯‘𝐵) = 1 ∨ 𝐵 = ∅))))) |
66 | 24, 27, 65 | 3jaoi 1429 |
. . . . . . . . . 10
⊢ ((𝐴 = ∅ ∨
(♯‘𝐴) = 1 ∨
1 < (♯‘𝐴))
→ (1 < (♯‘𝐵) → (𝐺 ∈ FriendGraph →
(((♯‘𝐴) = 1
∨ 𝐴 = ∅) ∨
((♯‘𝐵) = 1 ∨
𝐵 =
∅))))) |
67 | 66 | com12 32 |
. . . . . . . . 9
⊢ (1 <
(♯‘𝐵) →
((𝐴 = ∅ ∨
(♯‘𝐴) = 1 ∨
1 < (♯‘𝐴))
→ (𝐺 ∈
FriendGraph → (((♯‘𝐴) = 1 ∨ 𝐴 = ∅) ∨ ((♯‘𝐵) = 1 ∨ 𝐵 = ∅))))) |
68 | 18, 21, 67 | 3jaoi 1429 |
. . . . . . . 8
⊢ ((𝐵 = ∅ ∨
(♯‘𝐵) = 1 ∨
1 < (♯‘𝐵))
→ ((𝐴 = ∅ ∨
(♯‘𝐴) = 1 ∨
1 < (♯‘𝐴))
→ (𝐺 ∈
FriendGraph → (((♯‘𝐴) = 1 ∨ 𝐴 = ∅) ∨ ((♯‘𝐵) = 1 ∨ 𝐵 = ∅))))) |
69 | 15, 68 | syl6bi 256 |
. . . . . . 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 256 |
. . . 4
⊢ (𝐴 ∈ V →
(((♯‘𝐴) = 0
∨ (♯‘𝐴) = 1
∨ 1 < (♯‘𝐴)) → (𝐵 ∈ V → (𝐺 ∈ FriendGraph →
(((♯‘𝐴) = 1
∨ 𝐴 = ∅) ∨
((♯‘𝐵) = 1 ∨
𝐵 =
∅)))))) |
73 | 6, 72 | mpd 15 |
. . 3
⊢ (𝐴 ∈ V → (𝐵 ∈ V → (𝐺 ∈ FriendGraph →
(((♯‘𝐴) = 1
∨ 𝐴 = ∅) ∨
((♯‘𝐵) = 1 ∨
𝐵 =
∅))))) |
74 | 73 | imp 410 |
. 2
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐺 ∈ FriendGraph →
(((♯‘𝐴) = 1
∨ 𝐴 = ∅) ∨
((♯‘𝐵) = 1 ∨
𝐵 =
∅)))) |
75 | 5, 74 | ax-mp 5 |
1
⊢ (𝐺 ∈ FriendGraph →
(((♯‘𝐴) = 1
∨ 𝐴 = ∅) ∨
((♯‘𝐵) = 1 ∨
𝐵 =
∅))) |