Step | Hyp | Ref
| Expression |
1 | | frisusgra 26519 |
. . . 4
⊢ (𝑉 FriendGrph 𝐸 → 𝑉 USGrph 𝐸) |
2 | | usgrav 25867 |
. . . 4
⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
3 | 1, 2 | syl 17 |
. . 3
⊢ (𝑉 FriendGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
4 | | hashgt12el2 13071 |
. . . . . . . . . . . . . 14
⊢ ((𝑉 ∈ V ∧ 1 <
(#‘𝑉) ∧ 𝑎 ∈ 𝑉) → ∃𝑥 ∈ 𝑉 𝑎 ≠ 𝑥) |
5 | 4 | 3expa 1257 |
. . . . . . . . . . . . 13
⊢ (((𝑉 ∈ V ∧ 1 <
(#‘𝑉)) ∧ 𝑎 ∈ 𝑉) → ∃𝑥 ∈ 𝑉 𝑎 ≠ 𝑥) |
6 | | 3cyclfrgrarn1 26539 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑉 FriendGrph 𝐸 ∧ (𝑎 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) ∧ 𝑎 ≠ 𝑥) → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸)) |
7 | 6 | 3expb 1258 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑉 FriendGrph 𝐸 ∧ ((𝑎 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) ∧ 𝑎 ≠ 𝑥)) → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸)) |
8 | 7 | expcom 450 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑎 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) ∧ 𝑎 ≠ 𝑥) → (𝑉 FriendGrph 𝐸 → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸))) |
9 | 8 | ex 449 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) → (𝑎 ≠ 𝑥 → (𝑉 FriendGrph 𝐸 → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸)))) |
10 | 9 | expcom 450 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ 𝑉 → (𝑎 ∈ 𝑉 → (𝑎 ≠ 𝑥 → (𝑉 FriendGrph 𝐸 → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸))))) |
11 | 10 | com23 84 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝑉 → (𝑎 ≠ 𝑥 → (𝑎 ∈ 𝑉 → (𝑉 FriendGrph 𝐸 → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸))))) |
12 | 11 | com34 89 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝑉 → (𝑎 ≠ 𝑥 → (𝑉 FriendGrph 𝐸 → (𝑎 ∈ 𝑉 → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸))))) |
13 | 12 | rexlimiv 3009 |
. . . . . . . . . . . . 13
⊢
(∃𝑥 ∈
𝑉 𝑎 ≠ 𝑥 → (𝑉 FriendGrph 𝐸 → (𝑎 ∈ 𝑉 → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸)))) |
14 | 5, 13 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝑉 ∈ V ∧ 1 <
(#‘𝑉)) ∧ 𝑎 ∈ 𝑉) → (𝑉 FriendGrph 𝐸 → (𝑎 ∈ 𝑉 → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸)))) |
15 | 14 | expcom 450 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ 𝑉 → ((𝑉 ∈ V ∧ 1 < (#‘𝑉)) → (𝑉 FriendGrph 𝐸 → (𝑎 ∈ 𝑉 → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸))))) |
16 | 15 | com24 93 |
. . . . . . . . . 10
⊢ (𝑎 ∈ 𝑉 → (𝑎 ∈ 𝑉 → (𝑉 FriendGrph 𝐸 → ((𝑉 ∈ V ∧ 1 < (#‘𝑉)) → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸))))) |
17 | 16 | pm2.43i 50 |
. . . . . . . . 9
⊢ (𝑎 ∈ 𝑉 → (𝑉 FriendGrph 𝐸 → ((𝑉 ∈ V ∧ 1 < (#‘𝑉)) → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸)))) |
18 | 17 | com13 86 |
. . . . . . . 8
⊢ ((𝑉 ∈ V ∧ 1 <
(#‘𝑉)) → (𝑉 FriendGrph 𝐸 → (𝑎 ∈ 𝑉 → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸)))) |
19 | 18 | imp 444 |
. . . . . . 7
⊢ (((𝑉 ∈ V ∧ 1 <
(#‘𝑉)) ∧ 𝑉 FriendGrph 𝐸) → (𝑎 ∈ 𝑉 → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸))) |
20 | 19 | ralrimiv 2948 |
. . . . . 6
⊢ (((𝑉 ∈ V ∧ 1 <
(#‘𝑉)) ∧ 𝑉 FriendGrph 𝐸) → ∀𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸)) |
21 | 20 | exp31 628 |
. . . . 5
⊢ (𝑉 ∈ V → (1 <
(#‘𝑉) → (𝑉 FriendGrph 𝐸 → ∀𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸)))) |
22 | 21 | com23 84 |
. . . 4
⊢ (𝑉 ∈ V → (𝑉 FriendGrph 𝐸 → (1 < (#‘𝑉) → ∀𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸)))) |
23 | 22 | adantr 480 |
. . 3
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑉 FriendGrph 𝐸 → (1 < (#‘𝑉) → ∀𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸)))) |
24 | 3, 23 | mpcom 37 |
. 2
⊢ (𝑉 FriendGrph 𝐸 → (1 < (#‘𝑉) → ∀𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸))) |
25 | 24 | imp 444 |
1
⊢ ((𝑉 FriendGrph 𝐸 ∧ 1 < (#‘𝑉)) → ∀𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸)) |