Proof of Theorem 3vfriswmgra
Step | Hyp | Ref
| Expression |
1 | | frisusgra 26519 |
. . . 4
⊢ ({𝐴, 𝐵, 𝐶} FriendGrph 𝐸 → {𝐴, 𝐵, 𝐶} USGrph 𝐸) |
2 | | frgra3v 26529 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ({𝐴, 𝐵, 𝐶} USGrph 𝐸 → ({𝐴, 𝐵, 𝐶} FriendGrph 𝐸 ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)))) |
3 | 2 | 3adant3 1074 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) → ({𝐴, 𝐵, 𝐶} USGrph 𝐸 → ({𝐴, 𝐵, 𝐶} FriendGrph 𝐸 ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)))) |
4 | 3 | imp 444 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → ({𝐴, 𝐵, 𝐶} FriendGrph 𝐸 ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) |
5 | | prcom 4211 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝐶, 𝐴} = {𝐴, 𝐶} |
6 | 5 | eleq1i 2679 |
. . . . . . . . . . . . . . . . 17
⊢ ({𝐶, 𝐴} ∈ ran 𝐸 ↔ {𝐴, 𝐶} ∈ ran 𝐸) |
7 | 6 | biimpi 205 |
. . . . . . . . . . . . . . . 16
⊢ ({𝐶, 𝐴} ∈ ran 𝐸 → {𝐴, 𝐶} ∈ ran 𝐸) |
8 | 7 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . 15
⊢ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) → {𝐴, 𝐶} ∈ ran 𝐸) |
9 | 8 | adantl 481 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → {𝐴, 𝐶} ∈ ran 𝐸) |
10 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) |
11 | 10 | 3adant3 1074 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) |
12 | 11 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) → (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) |
13 | 12 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) |
14 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ≠ 𝐵 → 𝐴 ≠ 𝐵) |
15 | 14 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → 𝐴 ≠ 𝐵) |
16 | 15 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) → 𝐴 ≠ 𝐵) |
17 | 16 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐴 ≠ 𝐵) |
18 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → {𝐴, 𝐵, 𝐶} USGrph 𝐸) |
19 | 13, 17, 18 | 3jca 1235 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸)) |
20 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ ({𝐴, 𝐵} ∈ ran 𝐸 → {𝐴, 𝐵} ∈ ran 𝐸) |
21 | 20 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . 15
⊢ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) → {𝐴, 𝐵} ∈ ran 𝐸) |
22 | | 3vfriswmgralem 26531 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → ({𝐴, 𝐵} ∈ ran 𝐸 → ∃!𝑤 ∈ {𝐴, 𝐵} {𝐴, 𝑤} ∈ ran 𝐸)) |
23 | 22 | imp 444 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → ∃!𝑤 ∈ {𝐴, 𝐵} {𝐴, 𝑤} ∈ ran 𝐸) |
24 | 19, 21, 23 | syl2an 493 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → ∃!𝑤 ∈ {𝐴, 𝐵} {𝐴, 𝑤} ∈ ran 𝐸) |
25 | 9, 24 | jca 553 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → ({𝐴, 𝐶} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝐴, 𝑤} ∈ ran 𝐸)) |
26 | | simpr2 1061 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → {𝐵, 𝐶} ∈ ran 𝐸) |
27 | | pm3.22 464 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → (𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋)) |
28 | 27 | 3adant3 1074 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋)) |
29 | 28 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) → (𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋)) |
30 | 29 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → (𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋)) |
31 | | necom 2835 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴) |
32 | 31 | biimpi 205 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ≠ 𝐵 → 𝐵 ≠ 𝐴) |
33 | 32 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → 𝐵 ≠ 𝐴) |
34 | 33 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) → 𝐵 ≠ 𝐴) |
35 | 34 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → 𝐵 ≠ 𝐴) |
36 | | tpcoma 4229 |
. . . . . . . . . . . . . . . . . . 19
⊢ {𝐴, 𝐵, 𝐶} = {𝐵, 𝐴, 𝐶} |
37 | 36 | breq1i 4590 |
. . . . . . . . . . . . . . . . . 18
⊢ ({𝐴, 𝐵, 𝐶} USGrph 𝐸 ↔ {𝐵, 𝐴, 𝐶} USGrph 𝐸) |
38 | 37 | biimpi 205 |
. . . . . . . . . . . . . . . . 17
⊢ ({𝐴, 𝐵, 𝐶} USGrph 𝐸 → {𝐵, 𝐴, 𝐶} USGrph 𝐸) |
39 | 38 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → {𝐵, 𝐴, 𝐶} USGrph 𝐸) |
40 | 30, 35, 39 | 3jca 1235 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → ((𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋) ∧ 𝐵 ≠ 𝐴 ∧ {𝐵, 𝐴, 𝐶} USGrph 𝐸)) |
41 | | prcom 4211 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝐴, 𝐵} = {𝐵, 𝐴} |
42 | 41 | eleq1i 2679 |
. . . . . . . . . . . . . . . . 17
⊢ ({𝐴, 𝐵} ∈ ran 𝐸 ↔ {𝐵, 𝐴} ∈ ran 𝐸) |
43 | 42 | biimpi 205 |
. . . . . . . . . . . . . . . 16
⊢ ({𝐴, 𝐵} ∈ ran 𝐸 → {𝐵, 𝐴} ∈ ran 𝐸) |
44 | 43 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . 15
⊢ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) → {𝐵, 𝐴} ∈ ran 𝐸) |
45 | | 3vfriswmgralem 26531 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋) ∧ 𝐵 ≠ 𝐴 ∧ {𝐵, 𝐴, 𝐶} USGrph 𝐸) → ({𝐵, 𝐴} ∈ ran 𝐸 → ∃!𝑤 ∈ {𝐵, 𝐴} {𝐵, 𝑤} ∈ ran 𝐸)) |
46 | 45 | imp 444 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋) ∧ 𝐵 ≠ 𝐴 ∧ {𝐵, 𝐴, 𝐶} USGrph 𝐸) ∧ {𝐵, 𝐴} ∈ ran 𝐸) → ∃!𝑤 ∈ {𝐵, 𝐴} {𝐵, 𝑤} ∈ ran 𝐸) |
47 | | reueq1 3117 |
. . . . . . . . . . . . . . . . 17
⊢ ({𝐴, 𝐵} = {𝐵, 𝐴} → (∃!𝑤 ∈ {𝐴, 𝐵} {𝐵, 𝑤} ∈ ran 𝐸 ↔ ∃!𝑤 ∈ {𝐵, 𝐴} {𝐵, 𝑤} ∈ ran 𝐸)) |
48 | 41, 47 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
(∃!𝑤 ∈
{𝐴, 𝐵} {𝐵, 𝑤} ∈ ran 𝐸 ↔ ∃!𝑤 ∈ {𝐵, 𝐴} {𝐵, 𝑤} ∈ ran 𝐸) |
49 | 46, 48 | sylibr 223 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋) ∧ 𝐵 ≠ 𝐴 ∧ {𝐵, 𝐴, 𝐶} USGrph 𝐸) ∧ {𝐵, 𝐴} ∈ ran 𝐸) → ∃!𝑤 ∈ {𝐴, 𝐵} {𝐵, 𝑤} ∈ ran 𝐸) |
50 | 40, 44, 49 | syl2an 493 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → ∃!𝑤 ∈ {𝐴, 𝐵} {𝐵, 𝑤} ∈ ran 𝐸) |
51 | 26, 50 | jca 553 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → ({𝐵, 𝐶} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝐵, 𝑤} ∈ ran 𝐸)) |
52 | 25, 51 | jca 553 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → (({𝐴, 𝐶} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝐴, 𝑤} ∈ ran 𝐸) ∧ ({𝐵, 𝐶} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝐵, 𝑤} ∈ ran 𝐸))) |
53 | | preq1 4212 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 = 𝐴 → {𝑣, 𝐶} = {𝐴, 𝐶}) |
54 | 53 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 = 𝐴 → ({𝑣, 𝐶} ∈ ran 𝐸 ↔ {𝐴, 𝐶} ∈ ran 𝐸)) |
55 | | preq1 4212 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑣 = 𝐴 → {𝑣, 𝑤} = {𝐴, 𝑤}) |
56 | 55 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 = 𝐴 → ({𝑣, 𝑤} ∈ ran 𝐸 ↔ {𝐴, 𝑤} ∈ ran 𝐸)) |
57 | 56 | reubidv 3103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 = 𝐴 → (∃!𝑤 ∈ {𝐴, 𝐵} {𝑣, 𝑤} ∈ ran 𝐸 ↔ ∃!𝑤 ∈ {𝐴, 𝐵} {𝐴, 𝑤} ∈ ran 𝐸)) |
58 | 54, 57 | anbi12d 743 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 = 𝐴 → (({𝑣, 𝐶} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝑣, 𝑤} ∈ ran 𝐸) ↔ ({𝐴, 𝐶} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝐴, 𝑤} ∈ ran 𝐸))) |
59 | | preq1 4212 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 = 𝐵 → {𝑣, 𝐶} = {𝐵, 𝐶}) |
60 | 59 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 = 𝐵 → ({𝑣, 𝐶} ∈ ran 𝐸 ↔ {𝐵, 𝐶} ∈ ran 𝐸)) |
61 | | preq1 4212 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑣 = 𝐵 → {𝑣, 𝑤} = {𝐵, 𝑤}) |
62 | 61 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 = 𝐵 → ({𝑣, 𝑤} ∈ ran 𝐸 ↔ {𝐵, 𝑤} ∈ ran 𝐸)) |
63 | 62 | reubidv 3103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 = 𝐵 → (∃!𝑤 ∈ {𝐴, 𝐵} {𝑣, 𝑤} ∈ ran 𝐸 ↔ ∃!𝑤 ∈ {𝐴, 𝐵} {𝐵, 𝑤} ∈ ran 𝐸)) |
64 | 60, 63 | anbi12d 743 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 = 𝐵 → (({𝑣, 𝐶} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝑣, 𝑤} ∈ ran 𝐸) ↔ ({𝐵, 𝐶} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝐵, 𝑤} ∈ ran 𝐸))) |
65 | 58, 64 | ralprg 4181 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → (∀𝑣 ∈ {𝐴, 𝐵} ({𝑣, 𝐶} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝑣, 𝑤} ∈ ran 𝐸) ↔ (({𝐴, 𝐶} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝐴, 𝑤} ∈ ran 𝐸) ∧ ({𝐵, 𝐶} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝐵, 𝑤} ∈ ran 𝐸)))) |
66 | 65 | 3adant3 1074 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (∀𝑣 ∈ {𝐴, 𝐵} ({𝑣, 𝐶} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝑣, 𝑤} ∈ ran 𝐸) ↔ (({𝐴, 𝐶} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝐴, 𝑤} ∈ ran 𝐸) ∧ ({𝐵, 𝐶} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝐵, 𝑤} ∈ ran 𝐸)))) |
67 | 66 | 3ad2ant1 1075 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) → (∀𝑣 ∈ {𝐴, 𝐵} ({𝑣, 𝐶} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝑣, 𝑤} ∈ ran 𝐸) ↔ (({𝐴, 𝐶} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝐴, 𝑤} ∈ ran 𝐸) ∧ ({𝐵, 𝐶} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝐵, 𝑤} ∈ ran 𝐸)))) |
68 | 67 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → (∀𝑣 ∈ {𝐴, 𝐵} ({𝑣, 𝐶} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝑣, 𝑤} ∈ ran 𝐸) ↔ (({𝐴, 𝐶} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝐴, 𝑤} ∈ ran 𝐸) ∧ ({𝐵, 𝐶} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝐵, 𝑤} ∈ ran 𝐸)))) |
69 | 68 | adantr 480 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → (∀𝑣 ∈ {𝐴, 𝐵} ({𝑣, 𝐶} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝑣, 𝑤} ∈ ran 𝐸) ↔ (({𝐴, 𝐶} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝐴, 𝑤} ∈ ran 𝐸) ∧ ({𝐵, 𝐶} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝐵, 𝑤} ∈ ran 𝐸)))) |
70 | 52, 69 | mpbird 246 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → ∀𝑣 ∈ {𝐴, 𝐵} ({𝑣, 𝐶} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝑣, 𝑤} ∈ ran 𝐸)) |
71 | | diftpsn3 4273 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐶}) = {𝐴, 𝐵}) |
72 | 71 | 3adant1 1072 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐶}) = {𝐴, 𝐵}) |
73 | | reueq1 3117 |
. . . . . . . . . . . . . . . . 17
⊢ (({𝐴, 𝐵, 𝐶} ∖ {𝐶}) = {𝐴, 𝐵} → (∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶}){𝑣, 𝑤} ∈ ran 𝐸 ↔ ∃!𝑤 ∈ {𝐴, 𝐵} {𝑣, 𝑤} ∈ ran 𝐸)) |
74 | 72, 73 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶}){𝑣, 𝑤} ∈ ran 𝐸 ↔ ∃!𝑤 ∈ {𝐴, 𝐵} {𝑣, 𝑤} ∈ ran 𝐸)) |
75 | 74 | anbi2d 736 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (({𝑣, 𝐶} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶}){𝑣, 𝑤} ∈ ran 𝐸) ↔ ({𝑣, 𝐶} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝑣, 𝑤} ∈ ran 𝐸))) |
76 | 72, 75 | raleqbidv 3129 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → (∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})({𝑣, 𝐶} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶}){𝑣, 𝑤} ∈ ran 𝐸) ↔ ∀𝑣 ∈ {𝐴, 𝐵} ({𝑣, 𝐶} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝑣, 𝑤} ∈ ran 𝐸))) |
77 | 76 | 3ad2ant2 1076 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) → (∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})({𝑣, 𝐶} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶}){𝑣, 𝑤} ∈ ran 𝐸) ↔ ∀𝑣 ∈ {𝐴, 𝐵} ({𝑣, 𝐶} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝑣, 𝑤} ∈ ran 𝐸))) |
78 | 77 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → (∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})({𝑣, 𝐶} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶}){𝑣, 𝑤} ∈ ran 𝐸) ↔ ∀𝑣 ∈ {𝐴, 𝐵} ({𝑣, 𝐶} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝑣, 𝑤} ∈ ran 𝐸))) |
79 | 78 | adantr 480 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → (∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})({𝑣, 𝐶} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶}){𝑣, 𝑤} ∈ ran 𝐸) ↔ ∀𝑣 ∈ {𝐴, 𝐵} ({𝑣, 𝐶} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ {𝐴, 𝐵} {𝑣, 𝑤} ∈ ran 𝐸))) |
80 | 70, 79 | mpbird 246 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → ∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})({𝑣, 𝐶} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶}){𝑣, 𝑤} ∈ ran 𝐸)) |
81 | 80 | 3mix3d 1231 |
. . . . . . . . 9
⊢
(((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → (∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})({𝑣, 𝐴} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴}){𝑣, 𝑤} ∈ ran 𝐸) ∨ ∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})({𝑣, 𝐵} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵}){𝑣, 𝑤} ∈ ran 𝐸) ∨ ∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})({𝑣, 𝐶} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶}){𝑣, 𝑤} ∈ ran 𝐸))) |
82 | | sneq 4135 |
. . . . . . . . . . . . . . 15
⊢ (ℎ = 𝐴 → {ℎ} = {𝐴}) |
83 | 82 | difeq2d 3690 |
. . . . . . . . . . . . . 14
⊢ (ℎ = 𝐴 → ({𝐴, 𝐵, 𝐶} ∖ {ℎ}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐴})) |
84 | | preq2 4213 |
. . . . . . . . . . . . . . . 16
⊢ (ℎ = 𝐴 → {𝑣, ℎ} = {𝑣, 𝐴}) |
85 | 84 | eleq1d 2672 |
. . . . . . . . . . . . . . 15
⊢ (ℎ = 𝐴 → ({𝑣, ℎ} ∈ ran 𝐸 ↔ {𝑣, 𝐴} ∈ ran 𝐸)) |
86 | | reueq1 3117 |
. . . . . . . . . . . . . . . 16
⊢ (({𝐴, 𝐵, 𝐶} ∖ {ℎ}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐴}) → (∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸 ↔ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴}){𝑣, 𝑤} ∈ ran 𝐸)) |
87 | 83, 86 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (ℎ = 𝐴 → (∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸 ↔ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴}){𝑣, 𝑤} ∈ ran 𝐸)) |
88 | 85, 87 | anbi12d 743 |
. . . . . . . . . . . . . 14
⊢ (ℎ = 𝐴 → (({𝑣, ℎ} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸) ↔ ({𝑣, 𝐴} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴}){𝑣, 𝑤} ∈ ran 𝐸))) |
89 | 83, 88 | raleqbidv 3129 |
. . . . . . . . . . . . 13
⊢ (ℎ = 𝐴 → (∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {ℎ})({𝑣, ℎ} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸) ↔ ∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})({𝑣, 𝐴} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴}){𝑣, 𝑤} ∈ ran 𝐸))) |
90 | | sneq 4135 |
. . . . . . . . . . . . . . 15
⊢ (ℎ = 𝐵 → {ℎ} = {𝐵}) |
91 | 90 | difeq2d 3690 |
. . . . . . . . . . . . . 14
⊢ (ℎ = 𝐵 → ({𝐴, 𝐵, 𝐶} ∖ {ℎ}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐵})) |
92 | | preq2 4213 |
. . . . . . . . . . . . . . . 16
⊢ (ℎ = 𝐵 → {𝑣, ℎ} = {𝑣, 𝐵}) |
93 | 92 | eleq1d 2672 |
. . . . . . . . . . . . . . 15
⊢ (ℎ = 𝐵 → ({𝑣, ℎ} ∈ ran 𝐸 ↔ {𝑣, 𝐵} ∈ ran 𝐸)) |
94 | | reueq1 3117 |
. . . . . . . . . . . . . . . 16
⊢ (({𝐴, 𝐵, 𝐶} ∖ {ℎ}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐵}) → (∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸 ↔ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵}){𝑣, 𝑤} ∈ ran 𝐸)) |
95 | 91, 94 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (ℎ = 𝐵 → (∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸 ↔ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵}){𝑣, 𝑤} ∈ ran 𝐸)) |
96 | 93, 95 | anbi12d 743 |
. . . . . . . . . . . . . 14
⊢ (ℎ = 𝐵 → (({𝑣, ℎ} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸) ↔ ({𝑣, 𝐵} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵}){𝑣, 𝑤} ∈ ran 𝐸))) |
97 | 91, 96 | raleqbidv 3129 |
. . . . . . . . . . . . 13
⊢ (ℎ = 𝐵 → (∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {ℎ})({𝑣, ℎ} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸) ↔ ∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})({𝑣, 𝐵} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵}){𝑣, 𝑤} ∈ ran 𝐸))) |
98 | | sneq 4135 |
. . . . . . . . . . . . . . 15
⊢ (ℎ = 𝐶 → {ℎ} = {𝐶}) |
99 | 98 | difeq2d 3690 |
. . . . . . . . . . . . . 14
⊢ (ℎ = 𝐶 → ({𝐴, 𝐵, 𝐶} ∖ {ℎ}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐶})) |
100 | | preq2 4213 |
. . . . . . . . . . . . . . . 16
⊢ (ℎ = 𝐶 → {𝑣, ℎ} = {𝑣, 𝐶}) |
101 | 100 | eleq1d 2672 |
. . . . . . . . . . . . . . 15
⊢ (ℎ = 𝐶 → ({𝑣, ℎ} ∈ ran 𝐸 ↔ {𝑣, 𝐶} ∈ ran 𝐸)) |
102 | | reueq1 3117 |
. . . . . . . . . . . . . . . 16
⊢ (({𝐴, 𝐵, 𝐶} ∖ {ℎ}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐶}) → (∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸 ↔ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶}){𝑣, 𝑤} ∈ ran 𝐸)) |
103 | 99, 102 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (ℎ = 𝐶 → (∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸 ↔ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶}){𝑣, 𝑤} ∈ ran 𝐸)) |
104 | 101, 103 | anbi12d 743 |
. . . . . . . . . . . . . 14
⊢ (ℎ = 𝐶 → (({𝑣, ℎ} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸) ↔ ({𝑣, 𝐶} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶}){𝑣, 𝑤} ∈ ran 𝐸))) |
105 | 99, 104 | raleqbidv 3129 |
. . . . . . . . . . . . 13
⊢ (ℎ = 𝐶 → (∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {ℎ})({𝑣, ℎ} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸) ↔ ∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})({𝑣, 𝐶} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶}){𝑣, 𝑤} ∈ ran 𝐸))) |
106 | 89, 97, 105 | rextpg 4184 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (∃ℎ ∈ {𝐴, 𝐵, 𝐶}∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {ℎ})({𝑣, ℎ} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸) ↔ (∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})({𝑣, 𝐴} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴}){𝑣, 𝑤} ∈ ran 𝐸) ∨ ∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})({𝑣, 𝐵} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵}){𝑣, 𝑤} ∈ ran 𝐸) ∨ ∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})({𝑣, 𝐶} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶}){𝑣, 𝑤} ∈ ran 𝐸)))) |
107 | 106 | 3ad2ant1 1075 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) → (∃ℎ ∈ {𝐴, 𝐵, 𝐶}∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {ℎ})({𝑣, ℎ} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸) ↔ (∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})({𝑣, 𝐴} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴}){𝑣, 𝑤} ∈ ran 𝐸) ∨ ∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})({𝑣, 𝐵} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵}){𝑣, 𝑤} ∈ ran 𝐸) ∨ ∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})({𝑣, 𝐶} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶}){𝑣, 𝑤} ∈ ran 𝐸)))) |
108 | 107 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → (∃ℎ ∈ {𝐴, 𝐵, 𝐶}∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {ℎ})({𝑣, ℎ} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸) ↔ (∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})({𝑣, 𝐴} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴}){𝑣, 𝑤} ∈ ran 𝐸) ∨ ∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})({𝑣, 𝐵} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵}){𝑣, 𝑤} ∈ ran 𝐸) ∨ ∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})({𝑣, 𝐶} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶}){𝑣, 𝑤} ∈ ran 𝐸)))) |
109 | 108 | adantr 480 |
. . . . . . . . 9
⊢
(((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → (∃ℎ ∈ {𝐴, 𝐵, 𝐶}∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {ℎ})({𝑣, ℎ} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸) ↔ (∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})({𝑣, 𝐴} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴}){𝑣, 𝑤} ∈ ran 𝐸) ∨ ∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})({𝑣, 𝐵} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵}){𝑣, 𝑤} ∈ ran 𝐸) ∨ ∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})({𝑣, 𝐶} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶}){𝑣, 𝑤} ∈ ran 𝐸)))) |
110 | 81, 109 | mpbird 246 |
. . . . . . . 8
⊢
(((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → ∃ℎ ∈ {𝐴, 𝐵, 𝐶}∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {ℎ})({𝑣, ℎ} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸)) |
111 | 110 | ex 449 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) → ∃ℎ ∈ {𝐴, 𝐵, 𝐶}∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {ℎ})({𝑣, ℎ} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸))) |
112 | 4, 111 | sylbid 229 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → ({𝐴, 𝐵, 𝐶} FriendGrph 𝐸 → ∃ℎ ∈ {𝐴, 𝐵, 𝐶}∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {ℎ})({𝑣, ℎ} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸))) |
113 | 112 | expcom 450 |
. . . . 5
⊢ ({𝐴, 𝐵, 𝐶} USGrph 𝐸 → (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) → ({𝐴, 𝐵, 𝐶} FriendGrph 𝐸 → ∃ℎ ∈ {𝐴, 𝐵, 𝐶}∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {ℎ})({𝑣, ℎ} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸)))) |
114 | 113 | com23 84 |
. . . 4
⊢ ({𝐴, 𝐵, 𝐶} USGrph 𝐸 → ({𝐴, 𝐵, 𝐶} FriendGrph 𝐸 → (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) → ∃ℎ ∈ {𝐴, 𝐵, 𝐶}∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {ℎ})({𝑣, ℎ} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸)))) |
115 | 1, 114 | mpcom 37 |
. . 3
⊢ ({𝐴, 𝐵, 𝐶} FriendGrph 𝐸 → (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) → ∃ℎ ∈ {𝐴, 𝐵, 𝐶}∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {ℎ})({𝑣, ℎ} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸))) |
116 | 115 | com12 32 |
. 2
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) → ({𝐴, 𝐵, 𝐶} FriendGrph 𝐸 → ∃ℎ ∈ {𝐴, 𝐵, 𝐶}∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {ℎ})({𝑣, ℎ} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸))) |
117 | | breq1 4586 |
. . . 4
⊢ (𝑉 = {𝐴, 𝐵, 𝐶} → (𝑉 FriendGrph 𝐸 ↔ {𝐴, 𝐵, 𝐶} FriendGrph 𝐸)) |
118 | | difeq1 3683 |
. . . . . 6
⊢ (𝑉 = {𝐴, 𝐵, 𝐶} → (𝑉 ∖ {ℎ}) = ({𝐴, 𝐵, 𝐶} ∖ {ℎ})) |
119 | | reueq1 3117 |
. . . . . . . 8
⊢ ((𝑉 ∖ {ℎ}) = ({𝐴, 𝐵, 𝐶} ∖ {ℎ}) → (∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸 ↔ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸)) |
120 | 118, 119 | syl 17 |
. . . . . . 7
⊢ (𝑉 = {𝐴, 𝐵, 𝐶} → (∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸 ↔ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸)) |
121 | 120 | anbi2d 736 |
. . . . . 6
⊢ (𝑉 = {𝐴, 𝐵, 𝐶} → (({𝑣, ℎ} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸) ↔ ({𝑣, ℎ} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸))) |
122 | 118, 121 | raleqbidv 3129 |
. . . . 5
⊢ (𝑉 = {𝐴, 𝐵, 𝐶} → (∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸) ↔ ∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {ℎ})({𝑣, ℎ} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸))) |
123 | 122 | rexeqbi1dv 3124 |
. . . 4
⊢ (𝑉 = {𝐴, 𝐵, 𝐶} → (∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸) ↔ ∃ℎ ∈ {𝐴, 𝐵, 𝐶}∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {ℎ})({𝑣, ℎ} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸))) |
124 | 117, 123 | imbi12d 333 |
. . 3
⊢ (𝑉 = {𝐴, 𝐵, 𝐶} → ((𝑉 FriendGrph 𝐸 → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸)) ↔ ({𝐴, 𝐵, 𝐶} FriendGrph 𝐸 → ∃ℎ ∈ {𝐴, 𝐵, 𝐶}∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {ℎ})({𝑣, ℎ} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸)))) |
125 | 124 | 3ad2ant3 1077 |
. 2
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) → ((𝑉 FriendGrph 𝐸 → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸)) ↔ ({𝐴, 𝐵, 𝐶} FriendGrph 𝐸 → ∃ℎ ∈ {𝐴, 𝐵, 𝐶}∀𝑣 ∈ ({𝐴, 𝐵, 𝐶} ∖ {ℎ})({𝑣, ℎ} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸)))) |
126 | 116, 125 | mpbird 246 |
1
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) → (𝑉 FriendGrph 𝐸 → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸))) |