Step | Hyp | Ref
| Expression |
1 | | 2pthfrgrarn2 26537 |
. . 3
⊢ (𝑉 FriendGrph 𝐸 → ∀𝑎 ∈ 𝑉 ∀𝑧 ∈ (𝑉 ∖ {𝑎})∃𝑥 ∈ 𝑉 (({𝑎, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝑧} ∈ ran 𝐸) ∧ (𝑎 ≠ 𝑥 ∧ 𝑥 ≠ 𝑧))) |
2 | | necom 2835 |
. . . . . . . . . . . 12
⊢ (𝐴 ≠ 𝐶 ↔ 𝐶 ≠ 𝐴) |
3 | | eldifsn 4260 |
. . . . . . . . . . . . 13
⊢ (𝐶 ∈ (𝑉 ∖ {𝐴}) ↔ (𝐶 ∈ 𝑉 ∧ 𝐶 ≠ 𝐴)) |
4 | 3 | simplbi2com 655 |
. . . . . . . . . . . 12
⊢ (𝐶 ≠ 𝐴 → (𝐶 ∈ 𝑉 → 𝐶 ∈ (𝑉 ∖ {𝐴}))) |
5 | 2, 4 | sylbi 206 |
. . . . . . . . . . 11
⊢ (𝐴 ≠ 𝐶 → (𝐶 ∈ 𝑉 → 𝐶 ∈ (𝑉 ∖ {𝐴}))) |
6 | 5 | com12 32 |
. . . . . . . . . 10
⊢ (𝐶 ∈ 𝑉 → (𝐴 ≠ 𝐶 → 𝐶 ∈ (𝑉 ∖ {𝐴}))) |
7 | 6 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝐴 ≠ 𝐶 → 𝐶 ∈ (𝑉 ∖ {𝐴}))) |
8 | 7 | imp 444 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐴 ≠ 𝐶) → 𝐶 ∈ (𝑉 ∖ {𝐴})) |
9 | | sneq 4135 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝐴 → {𝑎} = {𝐴}) |
10 | 9 | difeq2d 3690 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝐴 → (𝑉 ∖ {𝑎}) = (𝑉 ∖ {𝐴})) |
11 | | preq1 4212 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝐴 → {𝑎, 𝑥} = {𝐴, 𝑥}) |
12 | 11 | eleq1d 2672 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝐴 → ({𝑎, 𝑥} ∈ ran 𝐸 ↔ {𝐴, 𝑥} ∈ ran 𝐸)) |
13 | 12 | anbi1d 737 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝐴 → (({𝑎, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝑧} ∈ ran 𝐸) ↔ ({𝐴, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝑧} ∈ ran 𝐸))) |
14 | | neeq1 2844 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝐴 → (𝑎 ≠ 𝑥 ↔ 𝐴 ≠ 𝑥)) |
15 | 14 | anbi1d 737 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝐴 → ((𝑎 ≠ 𝑥 ∧ 𝑥 ≠ 𝑧) ↔ (𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝑧))) |
16 | 13, 15 | anbi12d 743 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝐴 → ((({𝑎, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝑧} ∈ ran 𝐸) ∧ (𝑎 ≠ 𝑥 ∧ 𝑥 ≠ 𝑧)) ↔ (({𝐴, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝑧} ∈ ran 𝐸) ∧ (𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝑧)))) |
17 | 16 | rexbidv 3034 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝐴 → (∃𝑥 ∈ 𝑉 (({𝑎, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝑧} ∈ ran 𝐸) ∧ (𝑎 ≠ 𝑥 ∧ 𝑥 ≠ 𝑧)) ↔ ∃𝑥 ∈ 𝑉 (({𝐴, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝑧} ∈ ran 𝐸) ∧ (𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝑧)))) |
18 | 10, 17 | raleqbidv 3129 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝐴 → (∀𝑧 ∈ (𝑉 ∖ {𝑎})∃𝑥 ∈ 𝑉 (({𝑎, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝑧} ∈ ran 𝐸) ∧ (𝑎 ≠ 𝑥 ∧ 𝑥 ≠ 𝑧)) ↔ ∀𝑧 ∈ (𝑉 ∖ {𝐴})∃𝑥 ∈ 𝑉 (({𝐴, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝑧} ∈ ran 𝐸) ∧ (𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝑧)))) |
19 | 18 | rspcv 3278 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑉 → (∀𝑎 ∈ 𝑉 ∀𝑧 ∈ (𝑉 ∖ {𝑎})∃𝑥 ∈ 𝑉 (({𝑎, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝑧} ∈ ran 𝐸) ∧ (𝑎 ≠ 𝑥 ∧ 𝑥 ≠ 𝑧)) → ∀𝑧 ∈ (𝑉 ∖ {𝐴})∃𝑥 ∈ 𝑉 (({𝐴, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝑧} ∈ ran 𝐸) ∧ (𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝑧)))) |
20 | 19 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (∀𝑎 ∈ 𝑉 ∀𝑧 ∈ (𝑉 ∖ {𝑎})∃𝑥 ∈ 𝑉 (({𝑎, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝑧} ∈ ran 𝐸) ∧ (𝑎 ≠ 𝑥 ∧ 𝑥 ≠ 𝑧)) → ∀𝑧 ∈ (𝑉 ∖ {𝐴})∃𝑥 ∈ 𝑉 (({𝐴, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝑧} ∈ ran 𝐸) ∧ (𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝑧)))) |
21 | 20 | adantr 480 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐴 ≠ 𝐶) → (∀𝑎 ∈ 𝑉 ∀𝑧 ∈ (𝑉 ∖ {𝑎})∃𝑥 ∈ 𝑉 (({𝑎, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝑧} ∈ ran 𝐸) ∧ (𝑎 ≠ 𝑥 ∧ 𝑥 ≠ 𝑧)) → ∀𝑧 ∈ (𝑉 ∖ {𝐴})∃𝑥 ∈ 𝑉 (({𝐴, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝑧} ∈ ran 𝐸) ∧ (𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝑧)))) |
22 | | preq2 4213 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝐶 → {𝑥, 𝑧} = {𝑥, 𝐶}) |
23 | 22 | eleq1d 2672 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝐶 → ({𝑥, 𝑧} ∈ ran 𝐸 ↔ {𝑥, 𝐶} ∈ ran 𝐸)) |
24 | 23 | anbi2d 736 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝐶 → (({𝐴, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝑧} ∈ ran 𝐸) ↔ ({𝐴, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝐶} ∈ ran 𝐸))) |
25 | | neeq2 2845 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝐶 → (𝑥 ≠ 𝑧 ↔ 𝑥 ≠ 𝐶)) |
26 | 25 | anbi2d 736 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝐶 → ((𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝑧) ↔ (𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝐶))) |
27 | 24, 26 | anbi12d 743 |
. . . . . . . . . 10
⊢ (𝑧 = 𝐶 → ((({𝐴, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝑧} ∈ ran 𝐸) ∧ (𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝑧)) ↔ (({𝐴, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝐶} ∈ ran 𝐸) ∧ (𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝐶)))) |
28 | 27 | rexbidv 3034 |
. . . . . . . . 9
⊢ (𝑧 = 𝐶 → (∃𝑥 ∈ 𝑉 (({𝐴, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝑧} ∈ ran 𝐸) ∧ (𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝑧)) ↔ ∃𝑥 ∈ 𝑉 (({𝐴, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝐶} ∈ ran 𝐸) ∧ (𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝐶)))) |
29 | 28 | rspcv 3278 |
. . . . . . . 8
⊢ (𝐶 ∈ (𝑉 ∖ {𝐴}) → (∀𝑧 ∈ (𝑉 ∖ {𝐴})∃𝑥 ∈ 𝑉 (({𝐴, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝑧} ∈ ran 𝐸) ∧ (𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝑧)) → ∃𝑥 ∈ 𝑉 (({𝐴, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝐶} ∈ ran 𝐸) ∧ (𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝐶)))) |
30 | 8, 21, 29 | sylsyld 59 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐴 ≠ 𝐶) → (∀𝑎 ∈ 𝑉 ∀𝑧 ∈ (𝑉 ∖ {𝑎})∃𝑥 ∈ 𝑉 (({𝑎, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝑧} ∈ ran 𝐸) ∧ (𝑎 ≠ 𝑥 ∧ 𝑥 ≠ 𝑧)) → ∃𝑥 ∈ 𝑉 (({𝐴, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝐶} ∈ ran 𝐸) ∧ (𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝐶)))) |
31 | | 2pthfrgrarn 26536 |
. . . . . . . . . 10
⊢ (𝑉 FriendGrph 𝐸 → ∀𝑢 ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {𝑢})∃𝑦 ∈ 𝑉 ({𝑢, 𝑦} ∈ ran 𝐸 ∧ {𝑦, 𝑣} ∈ ran 𝐸)) |
32 | | necom 2835 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐴 ≠ 𝑥 ↔ 𝑥 ≠ 𝐴) |
33 | | eldifsn 4260 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 ∈ (𝑉 ∖ {𝐴}) ↔ (𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 𝐴)) |
34 | 33 | simplbi2com 655 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 ≠ 𝐴 → (𝑥 ∈ 𝑉 → 𝑥 ∈ (𝑉 ∖ {𝐴}))) |
35 | 32, 34 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐴 ≠ 𝑥 → (𝑥 ∈ 𝑉 → 𝑥 ∈ (𝑉 ∖ {𝐴}))) |
36 | 35 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ≠ 𝑥 ∧ 𝐴 ∈ 𝑉) → (𝑥 ∈ 𝑉 → 𝑥 ∈ (𝑉 ∖ {𝐴}))) |
37 | 36 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ≠ 𝑥 ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 ∈ 𝑉) → 𝑥 ∈ (𝑉 ∖ {𝐴})) |
38 | | sneq 4135 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑢 = 𝐴 → {𝑢} = {𝐴}) |
39 | 38 | difeq2d 3690 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑢 = 𝐴 → (𝑉 ∖ {𝑢}) = (𝑉 ∖ {𝐴})) |
40 | | preq1 4212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑢 = 𝐴 → {𝑢, 𝑦} = {𝐴, 𝑦}) |
41 | 40 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑢 = 𝐴 → ({𝑢, 𝑦} ∈ ran 𝐸 ↔ {𝐴, 𝑦} ∈ ran 𝐸)) |
42 | 41 | anbi1d 737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑢 = 𝐴 → (({𝑢, 𝑦} ∈ ran 𝐸 ∧ {𝑦, 𝑣} ∈ ran 𝐸) ↔ ({𝐴, 𝑦} ∈ ran 𝐸 ∧ {𝑦, 𝑣} ∈ ran 𝐸))) |
43 | 42 | rexbidv 3034 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑢 = 𝐴 → (∃𝑦 ∈ 𝑉 ({𝑢, 𝑦} ∈ ran 𝐸 ∧ {𝑦, 𝑣} ∈ ran 𝐸) ↔ ∃𝑦 ∈ 𝑉 ({𝐴, 𝑦} ∈ ran 𝐸 ∧ {𝑦, 𝑣} ∈ ran 𝐸))) |
44 | 39, 43 | raleqbidv 3129 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑢 = 𝐴 → (∀𝑣 ∈ (𝑉 ∖ {𝑢})∃𝑦 ∈ 𝑉 ({𝑢, 𝑦} ∈ ran 𝐸 ∧ {𝑦, 𝑣} ∈ ran 𝐸) ↔ ∀𝑣 ∈ (𝑉 ∖ {𝐴})∃𝑦 ∈ 𝑉 ({𝐴, 𝑦} ∈ ran 𝐸 ∧ {𝑦, 𝑣} ∈ ran 𝐸))) |
45 | 44 | rspcv 3278 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐴 ∈ 𝑉 → (∀𝑢 ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {𝑢})∃𝑦 ∈ 𝑉 ({𝑢, 𝑦} ∈ ran 𝐸 ∧ {𝑦, 𝑣} ∈ ran 𝐸) → ∀𝑣 ∈ (𝑉 ∖ {𝐴})∃𝑦 ∈ 𝑉 ({𝐴, 𝑦} ∈ ran 𝐸 ∧ {𝑦, 𝑣} ∈ ran 𝐸))) |
46 | 45 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ≠ 𝑥 ∧ 𝐴 ∈ 𝑉) → (∀𝑢 ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {𝑢})∃𝑦 ∈ 𝑉 ({𝑢, 𝑦} ∈ ran 𝐸 ∧ {𝑦, 𝑣} ∈ ran 𝐸) → ∀𝑣 ∈ (𝑉 ∖ {𝐴})∃𝑦 ∈ 𝑉 ({𝐴, 𝑦} ∈ ran 𝐸 ∧ {𝑦, 𝑣} ∈ ran 𝐸))) |
47 | 46 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ≠ 𝑥 ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 ∈ 𝑉) → (∀𝑢 ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {𝑢})∃𝑦 ∈ 𝑉 ({𝑢, 𝑦} ∈ ran 𝐸 ∧ {𝑦, 𝑣} ∈ ran 𝐸) → ∀𝑣 ∈ (𝑉 ∖ {𝐴})∃𝑦 ∈ 𝑉 ({𝐴, 𝑦} ∈ ran 𝐸 ∧ {𝑦, 𝑣} ∈ ran 𝐸))) |
48 | | preq2 4213 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑣 = 𝑥 → {𝑦, 𝑣} = {𝑦, 𝑥}) |
49 | 48 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑣 = 𝑥 → ({𝑦, 𝑣} ∈ ran 𝐸 ↔ {𝑦, 𝑥} ∈ ran 𝐸)) |
50 | 49 | anbi2d 736 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑣 = 𝑥 → (({𝐴, 𝑦} ∈ ran 𝐸 ∧ {𝑦, 𝑣} ∈ ran 𝐸) ↔ ({𝐴, 𝑦} ∈ ran 𝐸 ∧ {𝑦, 𝑥} ∈ ran 𝐸))) |
51 | 50 | rexbidv 3034 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑣 = 𝑥 → (∃𝑦 ∈ 𝑉 ({𝐴, 𝑦} ∈ ran 𝐸 ∧ {𝑦, 𝑣} ∈ ran 𝐸) ↔ ∃𝑦 ∈ 𝑉 ({𝐴, 𝑦} ∈ ran 𝐸 ∧ {𝑦, 𝑥} ∈ ran 𝐸))) |
52 | 51 | rspcv 3278 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ (𝑉 ∖ {𝐴}) → (∀𝑣 ∈ (𝑉 ∖ {𝐴})∃𝑦 ∈ 𝑉 ({𝐴, 𝑦} ∈ ran 𝐸 ∧ {𝑦, 𝑣} ∈ ran 𝐸) → ∃𝑦 ∈ 𝑉 ({𝐴, 𝑦} ∈ ran 𝐸 ∧ {𝑦, 𝑥} ∈ ran 𝐸))) |
53 | 37, 47, 52 | sylsyld 59 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ≠ 𝑥 ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 ∈ 𝑉) → (∀𝑢 ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {𝑢})∃𝑦 ∈ 𝑉 ({𝑢, 𝑦} ∈ ran 𝐸 ∧ {𝑦, 𝑣} ∈ ran 𝐸) → ∃𝑦 ∈ 𝑉 ({𝐴, 𝑦} ∈ ran 𝐸 ∧ {𝑦, 𝑥} ∈ ran 𝐸))) |
54 | | prcom 4211 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ {𝐴, 𝑦} = {𝑦, 𝐴} |
55 | 54 | eleq1i 2679 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ({𝐴, 𝑦} ∈ ran 𝐸 ↔ {𝑦, 𝐴} ∈ ran 𝐸) |
56 | | prcom 4211 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ {𝑦, 𝑥} = {𝑥, 𝑦} |
57 | 56 | eleq1i 2679 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ({𝑦, 𝑥} ∈ ran 𝐸 ↔ {𝑥, 𝑦} ∈ ran 𝐸) |
58 | 55, 57 | anbi12ci 730 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (({𝐴, 𝑦} ∈ ran 𝐸 ∧ {𝑦, 𝑥} ∈ ran 𝐸) ↔ ({𝑥, 𝑦} ∈ ran 𝐸 ∧ {𝑦, 𝐴} ∈ ran 𝐸)) |
59 | | preq2 4213 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑏 = 𝑥 → {𝐴, 𝑏} = {𝐴, 𝑥}) |
60 | 59 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑏 = 𝑥 → ({𝐴, 𝑏} ∈ ran 𝐸 ↔ {𝐴, 𝑥} ∈ ran 𝐸)) |
61 | | preq1 4212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑏 = 𝑥 → {𝑏, 𝑐} = {𝑥, 𝑐}) |
62 | 61 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑏 = 𝑥 → ({𝑏, 𝑐} ∈ ran 𝐸 ↔ {𝑥, 𝑐} ∈ ran 𝐸)) |
63 | | biidd 251 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑏 = 𝑥 → ({𝑐, 𝐴} ∈ ran 𝐸 ↔ {𝑐, 𝐴} ∈ ran 𝐸)) |
64 | 60, 62, 63 | 3anbi123d 1391 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑏 = 𝑥 → (({𝐴, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝐴} ∈ ran 𝐸) ↔ ({𝐴, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝐴} ∈ ran 𝐸))) |
65 | | biidd 251 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑐 = 𝑦 → ({𝐴, 𝑥} ∈ ran 𝐸 ↔ {𝐴, 𝑥} ∈ ran 𝐸)) |
66 | | preq2 4213 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑐 = 𝑦 → {𝑥, 𝑐} = {𝑥, 𝑦}) |
67 | 66 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑐 = 𝑦 → ({𝑥, 𝑐} ∈ ran 𝐸 ↔ {𝑥, 𝑦} ∈ ran 𝐸)) |
68 | | preq1 4212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑐 = 𝑦 → {𝑐, 𝐴} = {𝑦, 𝐴}) |
69 | 68 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑐 = 𝑦 → ({𝑐, 𝐴} ∈ ran 𝐸 ↔ {𝑦, 𝐴} ∈ ran 𝐸)) |
70 | 65, 67, 69 | 3anbi123d 1391 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑐 = 𝑦 → (({𝐴, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝐴} ∈ ran 𝐸) ↔ ({𝐴, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝑦} ∈ ran 𝐸 ∧ {𝑦, 𝐴} ∈ ran 𝐸))) |
71 | 64, 70 | rspc2ev 3295 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ ({𝐴, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝑦} ∈ ran 𝐸 ∧ {𝑦, 𝐴} ∈ ran 𝐸)) → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝐴, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝐴} ∈ ran 𝐸)) |
72 | 71 | 3expa 1257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ({𝐴, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝑦} ∈ ran 𝐸 ∧ {𝑦, 𝐴} ∈ ran 𝐸)) → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝐴, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝐴} ∈ ran 𝐸)) |
73 | 72 | expcom 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (({𝐴, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝑦} ∈ ran 𝐸 ∧ {𝑦, 𝐴} ∈ ran 𝐸) → ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝐴, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝐴} ∈ ran 𝐸))) |
74 | 73 | 3expib 1260 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ({𝐴, 𝑥} ∈ ran 𝐸 → (({𝑥, 𝑦} ∈ ran 𝐸 ∧ {𝑦, 𝐴} ∈ ran 𝐸) → ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝐴, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝐴} ∈ ran 𝐸)))) |
75 | 58, 74 | syl5bi 231 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ({𝐴, 𝑥} ∈ ran 𝐸 → (({𝐴, 𝑦} ∈ ran 𝐸 ∧ {𝑦, 𝑥} ∈ ran 𝐸) → ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝐴, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝐴} ∈ ran 𝐸)))) |
76 | 75 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (({𝐴, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝐶} ∈ ran 𝐸) → (({𝐴, 𝑦} ∈ ran 𝐸 ∧ {𝑦, 𝑥} ∈ ran 𝐸) → ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝐴, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝐴} ∈ ran 𝐸)))) |
77 | 76 | com13 86 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (({𝐴, 𝑦} ∈ ran 𝐸 ∧ {𝑦, 𝑥} ∈ ran 𝐸) → (({𝐴, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝐶} ∈ ran 𝐸) → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝐴, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝐴} ∈ ran 𝐸)))) |
78 | 77 | rexlimdva 3013 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ 𝑉 → (∃𝑦 ∈ 𝑉 ({𝐴, 𝑦} ∈ ran 𝐸 ∧ {𝑦, 𝑥} ∈ ran 𝐸) → (({𝐴, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝐶} ∈ ran 𝐸) → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝐴, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝐴} ∈ ran 𝐸)))) |
79 | 78 | com13 86 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (({𝐴, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝐶} ∈ ran 𝐸) → (∃𝑦 ∈ 𝑉 ({𝐴, 𝑦} ∈ ran 𝐸 ∧ {𝑦, 𝑥} ∈ ran 𝐸) → (𝑥 ∈ 𝑉 → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝐴, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝐴} ∈ ran 𝐸)))) |
80 | 53, 79 | syl9 75 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ≠ 𝑥 ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 ∈ 𝑉) → (({𝐴, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝐶} ∈ ran 𝐸) → (∀𝑢 ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {𝑢})∃𝑦 ∈ 𝑉 ({𝑢, 𝑦} ∈ ran 𝐸 ∧ {𝑦, 𝑣} ∈ ran 𝐸) → (𝑥 ∈ 𝑉 → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝐴, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝐴} ∈ ran 𝐸))))) |
81 | 80 | exp31 628 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ≠ 𝑥 → (𝐴 ∈ 𝑉 → (𝑥 ∈ 𝑉 → (({𝐴, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝐶} ∈ ran 𝐸) → (∀𝑢 ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {𝑢})∃𝑦 ∈ 𝑉 ({𝑢, 𝑦} ∈ ran 𝐸 ∧ {𝑦, 𝑣} ∈ ran 𝐸) → (𝑥 ∈ 𝑉 → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝐴, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝐴} ∈ ran 𝐸))))))) |
82 | 81 | com24 93 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ≠ 𝑥 → (({𝐴, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝐶} ∈ ran 𝐸) → (𝑥 ∈ 𝑉 → (𝐴 ∈ 𝑉 → (∀𝑢 ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {𝑢})∃𝑦 ∈ 𝑉 ({𝑢, 𝑦} ∈ ran 𝐸 ∧ {𝑦, 𝑣} ∈ ran 𝐸) → (𝑥 ∈ 𝑉 → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝐴, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝐴} ∈ ran 𝐸))))))) |
83 | 82 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝐶) → (({𝐴, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝐶} ∈ ran 𝐸) → (𝑥 ∈ 𝑉 → (𝐴 ∈ 𝑉 → (∀𝑢 ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {𝑢})∃𝑦 ∈ 𝑉 ({𝑢, 𝑦} ∈ ran 𝐸 ∧ {𝑦, 𝑣} ∈ ran 𝐸) → (𝑥 ∈ 𝑉 → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝐴, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝐴} ∈ ran 𝐸))))))) |
84 | 83 | impcom 445 |
. . . . . . . . . . . . . . . 16
⊢ ((({𝐴, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝐶} ∈ ran 𝐸) ∧ (𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝐶)) → (𝑥 ∈ 𝑉 → (𝐴 ∈ 𝑉 → (∀𝑢 ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {𝑢})∃𝑦 ∈ 𝑉 ({𝑢, 𝑦} ∈ ran 𝐸 ∧ {𝑦, 𝑣} ∈ ran 𝐸) → (𝑥 ∈ 𝑉 → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝐴, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝐴} ∈ ran 𝐸)))))) |
85 | 84 | com15 99 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝑉 → (𝑥 ∈ 𝑉 → (𝐴 ∈ 𝑉 → (∀𝑢 ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {𝑢})∃𝑦 ∈ 𝑉 ({𝑢, 𝑦} ∈ ran 𝐸 ∧ {𝑦, 𝑣} ∈ ran 𝐸) → ((({𝐴, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝐶} ∈ ran 𝐸) ∧ (𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝐶)) → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝐴, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝐴} ∈ ran 𝐸)))))) |
86 | 85 | pm2.43i 50 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝑉 → (𝐴 ∈ 𝑉 → (∀𝑢 ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {𝑢})∃𝑦 ∈ 𝑉 ({𝑢, 𝑦} ∈ ran 𝐸 ∧ {𝑦, 𝑣} ∈ ran 𝐸) → ((({𝐴, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝐶} ∈ ran 𝐸) ∧ (𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝐶)) → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝐴, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝐴} ∈ ran 𝐸))))) |
87 | 86 | com12 32 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ 𝑉 → (∀𝑢 ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {𝑢})∃𝑦 ∈ 𝑉 ({𝑢, 𝑦} ∈ ran 𝐸 ∧ {𝑦, 𝑣} ∈ ran 𝐸) → ((({𝐴, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝐶} ∈ ran 𝐸) ∧ (𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝐶)) → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝐴, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝐴} ∈ ran 𝐸))))) |
88 | 87 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑥 ∈ 𝑉 → (∀𝑢 ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {𝑢})∃𝑦 ∈ 𝑉 ({𝑢, 𝑦} ∈ ran 𝐸 ∧ {𝑦, 𝑣} ∈ ran 𝐸) → ((({𝐴, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝐶} ∈ ran 𝐸) ∧ (𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝐶)) → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝐴, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝐴} ∈ ran 𝐸))))) |
89 | 88 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐴 ≠ 𝐶) → (𝑥 ∈ 𝑉 → (∀𝑢 ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {𝑢})∃𝑦 ∈ 𝑉 ({𝑢, 𝑦} ∈ ran 𝐸 ∧ {𝑦, 𝑣} ∈ ran 𝐸) → ((({𝐴, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝐶} ∈ ran 𝐸) ∧ (𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝐶)) → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝐴, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝐴} ∈ ran 𝐸))))) |
90 | 89 | com4t 91 |
. . . . . . . . . 10
⊢
(∀𝑢 ∈
𝑉 ∀𝑣 ∈ (𝑉 ∖ {𝑢})∃𝑦 ∈ 𝑉 ({𝑢, 𝑦} ∈ ran 𝐸 ∧ {𝑦, 𝑣} ∈ ran 𝐸) → ((({𝐴, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝐶} ∈ ran 𝐸) ∧ (𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝐶)) → (((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐴 ≠ 𝐶) → (𝑥 ∈ 𝑉 → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝐴, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝐴} ∈ ran 𝐸))))) |
91 | 31, 90 | syl 17 |
. . . . . . . . 9
⊢ (𝑉 FriendGrph 𝐸 → ((({𝐴, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝐶} ∈ ran 𝐸) ∧ (𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝐶)) → (((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐴 ≠ 𝐶) → (𝑥 ∈ 𝑉 → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝐴, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝐴} ∈ ran 𝐸))))) |
92 | 91 | com14 94 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝑉 → ((({𝐴, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝐶} ∈ ran 𝐸) ∧ (𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝐶)) → (((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐴 ≠ 𝐶) → (𝑉 FriendGrph 𝐸 → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝐴, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝐴} ∈ ran 𝐸))))) |
93 | 92 | rexlimiv 3009 |
. . . . . . 7
⊢
(∃𝑥 ∈
𝑉 (({𝐴, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝐶} ∈ ran 𝐸) ∧ (𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝐶)) → (((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐴 ≠ 𝐶) → (𝑉 FriendGrph 𝐸 → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝐴, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝐴} ∈ ran 𝐸)))) |
94 | 30, 93 | syl6 34 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐴 ≠ 𝐶) → (∀𝑎 ∈ 𝑉 ∀𝑧 ∈ (𝑉 ∖ {𝑎})∃𝑥 ∈ 𝑉 (({𝑎, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝑧} ∈ ran 𝐸) ∧ (𝑎 ≠ 𝑥 ∧ 𝑥 ≠ 𝑧)) → (((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐴 ≠ 𝐶) → (𝑉 FriendGrph 𝐸 → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝐴, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝐴} ∈ ran 𝐸))))) |
95 | 94 | pm2.43a 52 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐴 ≠ 𝐶) → (∀𝑎 ∈ 𝑉 ∀𝑧 ∈ (𝑉 ∖ {𝑎})∃𝑥 ∈ 𝑉 (({𝑎, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝑧} ∈ ran 𝐸) ∧ (𝑎 ≠ 𝑥 ∧ 𝑥 ≠ 𝑧)) → (𝑉 FriendGrph 𝐸 → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝐴, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝐴} ∈ ran 𝐸)))) |
96 | 95 | ex 449 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝐴 ≠ 𝐶 → (∀𝑎 ∈ 𝑉 ∀𝑧 ∈ (𝑉 ∖ {𝑎})∃𝑥 ∈ 𝑉 (({𝑎, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝑧} ∈ ran 𝐸) ∧ (𝑎 ≠ 𝑥 ∧ 𝑥 ≠ 𝑧)) → (𝑉 FriendGrph 𝐸 → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝐴, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝐴} ∈ ran 𝐸))))) |
97 | 96 | com4t 91 |
. . 3
⊢
(∀𝑎 ∈
𝑉 ∀𝑧 ∈ (𝑉 ∖ {𝑎})∃𝑥 ∈ 𝑉 (({𝑎, 𝑥} ∈ ran 𝐸 ∧ {𝑥, 𝑧} ∈ ran 𝐸) ∧ (𝑎 ≠ 𝑥 ∧ 𝑥 ≠ 𝑧)) → (𝑉 FriendGrph 𝐸 → ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝐴 ≠ 𝐶 → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝐴, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝐴} ∈ ran 𝐸))))) |
98 | 1, 97 | mpcom 37 |
. 2
⊢ (𝑉 FriendGrph 𝐸 → ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝐴 ≠ 𝐶 → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝐴, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝐴} ∈ ran 𝐸)))) |
99 | 98 | 3imp 1249 |
1
⊢ ((𝑉 FriendGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐴 ≠ 𝐶) → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝐴, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝐴} ∈ ran 𝐸)) |