Step | Hyp | Ref
| Expression |
1 | | simpr 476 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → {𝐴, 𝐵} ∈ ran 𝐸) |
2 | 1 | olcd 407 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → ({𝐴, 𝐴} ∈ ran 𝐸 ∨ {𝐴, 𝐵} ∈ ran 𝐸)) |
3 | | preq2 4213 |
. . . . . . . . . 10
⊢ (𝑤 = 𝐴 → {𝐴, 𝑤} = {𝐴, 𝐴}) |
4 | 3 | eleq1d 2672 |
. . . . . . . . 9
⊢ (𝑤 = 𝐴 → ({𝐴, 𝑤} ∈ ran 𝐸 ↔ {𝐴, 𝐴} ∈ ran 𝐸)) |
5 | | preq2 4213 |
. . . . . . . . . 10
⊢ (𝑤 = 𝐵 → {𝐴, 𝑤} = {𝐴, 𝐵}) |
6 | 5 | eleq1d 2672 |
. . . . . . . . 9
⊢ (𝑤 = 𝐵 → ({𝐴, 𝑤} ∈ ran 𝐸 ↔ {𝐴, 𝐵} ∈ ran 𝐸)) |
7 | 4, 6 | rexprg 4182 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → (∃𝑤 ∈ {𝐴, 𝐵} {𝐴, 𝑤} ∈ ran 𝐸 ↔ ({𝐴, 𝐴} ∈ ran 𝐸 ∨ {𝐴, 𝐵} ∈ ran 𝐸))) |
8 | 7 | 3ad2ant1 1075 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → (∃𝑤 ∈ {𝐴, 𝐵} {𝐴, 𝑤} ∈ ran 𝐸 ↔ ({𝐴, 𝐴} ∈ ran 𝐸 ∨ {𝐴, 𝐵} ∈ ran 𝐸))) |
9 | 8 | adantr 480 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → (∃𝑤 ∈ {𝐴, 𝐵} {𝐴, 𝑤} ∈ ran 𝐸 ↔ ({𝐴, 𝐴} ∈ ran 𝐸 ∨ {𝐴, 𝐵} ∈ ran 𝐸))) |
10 | 2, 9 | mpbird 246 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → ∃𝑤 ∈ {𝐴, 𝐵} {𝐴, 𝑤} ∈ ran 𝐸) |
11 | | df-rex 2902 |
. . . . 5
⊢
(∃𝑤 ∈
{𝐴, 𝐵} {𝐴, 𝑤} ∈ ran 𝐸 ↔ ∃𝑤(𝑤 ∈ {𝐴, 𝐵} ∧ {𝐴, 𝑤} ∈ ran 𝐸)) |
12 | 10, 11 | sylib 207 |
. . . 4
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → ∃𝑤(𝑤 ∈ {𝐴, 𝐵} ∧ {𝐴, 𝑤} ∈ ran 𝐸)) |
13 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑤 ∈ V |
14 | 13 | elpr 4146 |
. . . . . . . 8
⊢ (𝑤 ∈ {𝐴, 𝐵} ↔ (𝑤 = 𝐴 ∨ 𝑤 = 𝐵)) |
15 | | vex 3176 |
. . . . . . . . . . . 12
⊢ 𝑦 ∈ V |
16 | 15 | elpr 4146 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ {𝐴, 𝐵} ↔ (𝑦 = 𝐴 ∨ 𝑦 = 𝐵)) |
17 | | eqidd 2611 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝐴 = 𝐴) |
18 | 17 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ({𝐴, 𝐴} ∈ ran 𝐸 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝐴 = 𝐴)) |
19 | 18 | 2a1i 12 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝐴 → ({𝐴, 𝐴} ∈ ran 𝐸 → ({𝐴, 𝐴} ∈ ran 𝐸 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝐴 = 𝐴)))) |
20 | | preq2 4213 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝐴 → {𝐴, 𝑦} = {𝐴, 𝐴}) |
21 | 20 | eleq1d 2672 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝐴 → ({𝐴, 𝑦} ∈ ran 𝐸 ↔ {𝐴, 𝐴} ∈ ran 𝐸)) |
22 | | eqeq2 2621 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝐴 → (𝐴 = 𝑦 ↔ 𝐴 = 𝐴)) |
23 | 22 | imbi2d 329 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝐴 → (((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝐴 = 𝑦) ↔ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝐴 = 𝐴))) |
24 | 23 | imbi2d 329 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝐴 → (({𝐴, 𝐴} ∈ ran 𝐸 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝐴 = 𝑦)) ↔ ({𝐴, 𝐴} ∈ ran 𝐸 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝐴 = 𝐴)))) |
25 | 19, 21, 24 | 3imtr4d 282 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝐴 → ({𝐴, 𝑦} ∈ ran 𝐸 → ({𝐴, 𝐴} ∈ ran 𝐸 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝐴 = 𝑦)))) |
26 | | usgraedgrn 25910 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (({𝐴, 𝐵, 𝐶} USGrph 𝐸 ∧ {𝐴, 𝐴} ∈ ran 𝐸) → 𝐴 ≠ 𝐴) |
27 | | df-ne 2782 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐴 ≠ 𝐴 ↔ ¬ 𝐴 = 𝐴) |
28 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝐴 = 𝐴 |
29 | 28 | pm2.24i 145 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (¬
𝐴 = 𝐴 → 𝐴 = 𝐵) |
30 | 27, 29 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐴 ≠ 𝐴 → 𝐴 = 𝐵) |
31 | 26, 30 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (({𝐴, 𝐵, 𝐶} USGrph 𝐸 ∧ {𝐴, 𝐴} ∈ ran 𝐸) → 𝐴 = 𝐵) |
32 | 31 | ex 449 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ({𝐴, 𝐵, 𝐶} USGrph 𝐸 → ({𝐴, 𝐴} ∈ ran 𝐸 → 𝐴 = 𝐵)) |
33 | 32 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → ({𝐴, 𝐴} ∈ ran 𝐸 → 𝐴 = 𝐵)) |
34 | 33 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → ({𝐴, 𝐴} ∈ ran 𝐸 → 𝐴 = 𝐵)) |
35 | 34 | com12 32 |
. . . . . . . . . . . . . . . . 17
⊢ ({𝐴, 𝐴} ∈ ran 𝐸 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝐴 = 𝐵)) |
36 | 35 | 2a1i 12 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝐵 → ({𝐴, 𝐵} ∈ ran 𝐸 → ({𝐴, 𝐴} ∈ ran 𝐸 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝐴 = 𝐵)))) |
37 | | preq2 4213 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝐵 → {𝐴, 𝑦} = {𝐴, 𝐵}) |
38 | 37 | eleq1d 2672 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝐵 → ({𝐴, 𝑦} ∈ ran 𝐸 ↔ {𝐴, 𝐵} ∈ ran 𝐸)) |
39 | | eqeq2 2621 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝐵 → (𝐴 = 𝑦 ↔ 𝐴 = 𝐵)) |
40 | 39 | imbi2d 329 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝐵 → (((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝐴 = 𝑦) ↔ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝐴 = 𝐵))) |
41 | 40 | imbi2d 329 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝐵 → (({𝐴, 𝐴} ∈ ran 𝐸 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝐴 = 𝑦)) ↔ ({𝐴, 𝐴} ∈ ran 𝐸 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝐴 = 𝐵)))) |
42 | 36, 38, 41 | 3imtr4d 282 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝐵 → ({𝐴, 𝑦} ∈ ran 𝐸 → ({𝐴, 𝐴} ∈ ran 𝐸 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝐴 = 𝑦)))) |
43 | 25, 42 | jaoi 393 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 = 𝐴 ∨ 𝑦 = 𝐵) → ({𝐴, 𝑦} ∈ ran 𝐸 → ({𝐴, 𝐴} ∈ ran 𝐸 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝐴 = 𝑦)))) |
44 | | eqeq1 2614 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 𝐴 → (𝑤 = 𝑦 ↔ 𝐴 = 𝑦)) |
45 | 44 | imbi2d 329 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝐴 → (((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝑤 = 𝑦) ↔ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝐴 = 𝑦))) |
46 | 4, 45 | imbi12d 333 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 𝐴 → (({𝐴, 𝑤} ∈ ran 𝐸 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝑤 = 𝑦)) ↔ ({𝐴, 𝐴} ∈ ran 𝐸 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝐴 = 𝑦)))) |
47 | 46 | imbi2d 329 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝐴 → (({𝐴, 𝑦} ∈ ran 𝐸 → ({𝐴, 𝑤} ∈ ran 𝐸 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝑤 = 𝑦))) ↔ ({𝐴, 𝑦} ∈ ran 𝐸 → ({𝐴, 𝐴} ∈ ran 𝐸 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝐴 = 𝑦))))) |
48 | 43, 47 | syl5ibr 235 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝐴 → ((𝑦 = 𝐴 ∨ 𝑦 = 𝐵) → ({𝐴, 𝑦} ∈ ran 𝐸 → ({𝐴, 𝑤} ∈ ran 𝐸 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝑤 = 𝑦))))) |
49 | 28 | pm2.24i 145 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (¬
𝐴 = 𝐴 → 𝐵 = 𝐴) |
50 | 27, 49 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐴 ≠ 𝐴 → 𝐵 = 𝐴) |
51 | 26, 50 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (({𝐴, 𝐵, 𝐶} USGrph 𝐸 ∧ {𝐴, 𝐴} ∈ ran 𝐸) → 𝐵 = 𝐴) |
52 | 51 | ex 449 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ({𝐴, 𝐵, 𝐶} USGrph 𝐸 → ({𝐴, 𝐴} ∈ ran 𝐸 → 𝐵 = 𝐴)) |
53 | 52 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → ({𝐴, 𝐴} ∈ ran 𝐸 → 𝐵 = 𝐴)) |
54 | 53 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → ({𝐴, 𝐴} ∈ ran 𝐸 → 𝐵 = 𝐴)) |
55 | 54 | com12 32 |
. . . . . . . . . . . . . . . . . 18
⊢ ({𝐴, 𝐴} ∈ ran 𝐸 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝐵 = 𝐴)) |
56 | 55 | a1d 25 |
. . . . . . . . . . . . . . . . 17
⊢ ({𝐴, 𝐴} ∈ ran 𝐸 → ({𝐴, 𝐵} ∈ ran 𝐸 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝐵 = 𝐴))) |
57 | 56 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝐴 → ({𝐴, 𝐴} ∈ ran 𝐸 → ({𝐴, 𝐵} ∈ ran 𝐸 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝐵 = 𝐴)))) |
58 | | eqeq2 2621 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝐴 → (𝐵 = 𝑦 ↔ 𝐵 = 𝐴)) |
59 | 58 | imbi2d 329 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝐴 → (((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝐵 = 𝑦) ↔ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝐵 = 𝐴))) |
60 | 59 | imbi2d 329 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝐴 → (({𝐴, 𝐵} ∈ ran 𝐸 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝐵 = 𝑦)) ↔ ({𝐴, 𝐵} ∈ ran 𝐸 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝐵 = 𝐴)))) |
61 | 57, 21, 60 | 3imtr4d 282 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝐴 → ({𝐴, 𝑦} ∈ ran 𝐸 → ({𝐴, 𝐵} ∈ ran 𝐸 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝐵 = 𝑦)))) |
62 | | eqidd 2611 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝐵 = 𝐵) |
63 | 62 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ({𝐴, 𝐵} ∈ ran 𝐸 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝐵 = 𝐵)) |
64 | 63 | 2a1i 12 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝐵 → ({𝐴, 𝐵} ∈ ran 𝐸 → ({𝐴, 𝐵} ∈ ran 𝐸 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝐵 = 𝐵)))) |
65 | | eqeq2 2621 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝐵 → (𝐵 = 𝑦 ↔ 𝐵 = 𝐵)) |
66 | 65 | imbi2d 329 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝐵 → (((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝐵 = 𝑦) ↔ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝐵 = 𝐵))) |
67 | 66 | imbi2d 329 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝐵 → (({𝐴, 𝐵} ∈ ran 𝐸 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝐵 = 𝑦)) ↔ ({𝐴, 𝐵} ∈ ran 𝐸 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝐵 = 𝐵)))) |
68 | 64, 38, 67 | 3imtr4d 282 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝐵 → ({𝐴, 𝑦} ∈ ran 𝐸 → ({𝐴, 𝐵} ∈ ran 𝐸 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝐵 = 𝑦)))) |
69 | 61, 68 | jaoi 393 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 = 𝐴 ∨ 𝑦 = 𝐵) → ({𝐴, 𝑦} ∈ ran 𝐸 → ({𝐴, 𝐵} ∈ ran 𝐸 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝐵 = 𝑦)))) |
70 | | eqeq1 2614 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 𝐵 → (𝑤 = 𝑦 ↔ 𝐵 = 𝑦)) |
71 | 70 | imbi2d 329 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝐵 → (((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝑤 = 𝑦) ↔ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝐵 = 𝑦))) |
72 | 6, 71 | imbi12d 333 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 𝐵 → (({𝐴, 𝑤} ∈ ran 𝐸 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝑤 = 𝑦)) ↔ ({𝐴, 𝐵} ∈ ran 𝐸 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝐵 = 𝑦)))) |
73 | 72 | imbi2d 329 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝐵 → (({𝐴, 𝑦} ∈ ran 𝐸 → ({𝐴, 𝑤} ∈ ran 𝐸 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝑤 = 𝑦))) ↔ ({𝐴, 𝑦} ∈ ran 𝐸 → ({𝐴, 𝐵} ∈ ran 𝐸 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝐵 = 𝑦))))) |
74 | 69, 73 | syl5ibr 235 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝐵 → ((𝑦 = 𝐴 ∨ 𝑦 = 𝐵) → ({𝐴, 𝑦} ∈ ran 𝐸 → ({𝐴, 𝑤} ∈ ran 𝐸 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝑤 = 𝑦))))) |
75 | 48, 74 | jaoi 393 |
. . . . . . . . . . . 12
⊢ ((𝑤 = 𝐴 ∨ 𝑤 = 𝐵) → ((𝑦 = 𝐴 ∨ 𝑦 = 𝐵) → ({𝐴, 𝑦} ∈ ran 𝐸 → ({𝐴, 𝑤} ∈ ran 𝐸 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝑤 = 𝑦))))) |
76 | 75 | com3l 87 |
. . . . . . . . . . 11
⊢ ((𝑦 = 𝐴 ∨ 𝑦 = 𝐵) → ({𝐴, 𝑦} ∈ ran 𝐸 → ((𝑤 = 𝐴 ∨ 𝑤 = 𝐵) → ({𝐴, 𝑤} ∈ ran 𝐸 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝑤 = 𝑦))))) |
77 | 16, 76 | sylbi 206 |
. . . . . . . . . 10
⊢ (𝑦 ∈ {𝐴, 𝐵} → ({𝐴, 𝑦} ∈ ran 𝐸 → ((𝑤 = 𝐴 ∨ 𝑤 = 𝐵) → ({𝐴, 𝑤} ∈ ran 𝐸 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝑤 = 𝑦))))) |
78 | 77 | imp 444 |
. . . . . . . . 9
⊢ ((𝑦 ∈ {𝐴, 𝐵} ∧ {𝐴, 𝑦} ∈ ran 𝐸) → ((𝑤 = 𝐴 ∨ 𝑤 = 𝐵) → ({𝐴, 𝑤} ∈ ran 𝐸 → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝑤 = 𝑦)))) |
79 | 78 | com3l 87 |
. . . . . . . 8
⊢ ((𝑤 = 𝐴 ∨ 𝑤 = 𝐵) → ({𝐴, 𝑤} ∈ ran 𝐸 → ((𝑦 ∈ {𝐴, 𝐵} ∧ {𝐴, 𝑦} ∈ ran 𝐸) → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝑤 = 𝑦)))) |
80 | 14, 79 | sylbi 206 |
. . . . . . 7
⊢ (𝑤 ∈ {𝐴, 𝐵} → ({𝐴, 𝑤} ∈ ran 𝐸 → ((𝑦 ∈ {𝐴, 𝐵} ∧ {𝐴, 𝑦} ∈ ran 𝐸) → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝑤 = 𝑦)))) |
81 | 80 | imp31 447 |
. . . . . 6
⊢ (((𝑤 ∈ {𝐴, 𝐵} ∧ {𝐴, 𝑤} ∈ ran 𝐸) ∧ (𝑦 ∈ {𝐴, 𝐵} ∧ {𝐴, 𝑦} ∈ ran 𝐸)) → ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → 𝑤 = 𝑦)) |
82 | 81 | com12 32 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → (((𝑤 ∈ {𝐴, 𝐵} ∧ {𝐴, 𝑤} ∈ ran 𝐸) ∧ (𝑦 ∈ {𝐴, 𝐵} ∧ {𝐴, 𝑦} ∈ ran 𝐸)) → 𝑤 = 𝑦)) |
83 | 82 | alrimivv 1843 |
. . . 4
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → ∀𝑤∀𝑦(((𝑤 ∈ {𝐴, 𝐵} ∧ {𝐴, 𝑤} ∈ ran 𝐸) ∧ (𝑦 ∈ {𝐴, 𝐵} ∧ {𝐴, 𝑦} ∈ ran 𝐸)) → 𝑤 = 𝑦)) |
84 | | eleq1 2676 |
. . . . . 6
⊢ (𝑤 = 𝑦 → (𝑤 ∈ {𝐴, 𝐵} ↔ 𝑦 ∈ {𝐴, 𝐵})) |
85 | | preq2 4213 |
. . . . . . 7
⊢ (𝑤 = 𝑦 → {𝐴, 𝑤} = {𝐴, 𝑦}) |
86 | 85 | eleq1d 2672 |
. . . . . 6
⊢ (𝑤 = 𝑦 → ({𝐴, 𝑤} ∈ ran 𝐸 ↔ {𝐴, 𝑦} ∈ ran 𝐸)) |
87 | 84, 86 | anbi12d 743 |
. . . . 5
⊢ (𝑤 = 𝑦 → ((𝑤 ∈ {𝐴, 𝐵} ∧ {𝐴, 𝑤} ∈ ran 𝐸) ↔ (𝑦 ∈ {𝐴, 𝐵} ∧ {𝐴, 𝑦} ∈ ran 𝐸))) |
88 | 87 | eu4 2506 |
. . . 4
⊢
(∃!𝑤(𝑤 ∈ {𝐴, 𝐵} ∧ {𝐴, 𝑤} ∈ ran 𝐸) ↔ (∃𝑤(𝑤 ∈ {𝐴, 𝐵} ∧ {𝐴, 𝑤} ∈ ran 𝐸) ∧ ∀𝑤∀𝑦(((𝑤 ∈ {𝐴, 𝐵} ∧ {𝐴, 𝑤} ∈ ran 𝐸) ∧ (𝑦 ∈ {𝐴, 𝐵} ∧ {𝐴, 𝑦} ∈ ran 𝐸)) → 𝑤 = 𝑦))) |
89 | 12, 83, 88 | sylanbrc 695 |
. . 3
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → ∃!𝑤(𝑤 ∈ {𝐴, 𝐵} ∧ {𝐴, 𝑤} ∈ ran 𝐸)) |
90 | | df-reu 2903 |
. . 3
⊢
(∃!𝑤 ∈
{𝐴, 𝐵} {𝐴, 𝑤} ∈ ran 𝐸 ↔ ∃!𝑤(𝑤 ∈ {𝐴, 𝐵} ∧ {𝐴, 𝑤} ∈ ran 𝐸)) |
91 | 89, 90 | sylibr 223 |
. 2
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) ∧ {𝐴, 𝐵} ∈ ran 𝐸) → ∃!𝑤 ∈ {𝐴, 𝐵} {𝐴, 𝑤} ∈ ran 𝐸) |
92 | 91 | ex 449 |
1
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → ({𝐴, 𝐵} ∈ ran 𝐸 → ∃!𝑤 ∈ {𝐴, 𝐵} {𝐴, 𝑤} ∈ ran 𝐸)) |