Step | Hyp | Ref
| Expression |
1 | | constr3cycl.f |
. . . . . 6
⊢ 𝐹 = {〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉, 〈2, (◡𝐸‘{𝐶, 𝐴})〉} |
2 | | constr3cycl.p |
. . . . . 6
⊢ 𝑃 = ({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉, 〈3, 𝐴〉}) |
3 | 1, 2 | constr3trllem1 26178 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → 𝐹 ∈ Word dom 𝐸) |
4 | | wrdf 13165 |
. . . . 5
⊢ (𝐹 ∈ Word dom 𝐸 → 𝐹:(0..^(#‘𝐹))⟶dom 𝐸) |
5 | 3, 4 | syl 17 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → 𝐹:(0..^(#‘𝐹))⟶dom 𝐸) |
6 | 1, 2 | constr3lem2 26174 |
. . . . 5
⊢
(#‘𝐹) =
3 |
7 | | usgraf1o 25887 |
. . . . . . . . . . . 12
⊢ (𝑉 USGrph 𝐸 → 𝐸:dom 𝐸–1-1-onto→ran
𝐸) |
8 | | 3cycl3dv 26170 |
. . . . . . . . . . . . . 14
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) |
9 | | usgraedgrnv 25906 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑉 USGrph 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸) → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) |
10 | 9 | ex 449 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑉 USGrph 𝐸 → ({𝐴, 𝐵} ∈ ran 𝐸 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))) |
11 | | usgraedgrnv 25906 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑉 USGrph 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) → (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) |
12 | 11 | ex 449 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑉 USGrph 𝐸 → ({𝐶, 𝐴} ∈ ran 𝐸 → (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉))) |
13 | 10, 12 | anim12d 584 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑉 USGrph 𝐸 → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)))) |
14 | 13 | com12 32 |
. . . . . . . . . . . . . . . . 17
⊢ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) → (𝑉 USGrph 𝐸 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)))) |
15 | 14 | 3adant2 1073 |
. . . . . . . . . . . . . . . 16
⊢ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) → (𝑉 USGrph 𝐸 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)))) |
16 | 15 | impcom 445 |
. . . . . . . . . . . . . . 15
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉))) |
17 | 1, 2 | constr3lem5 26176 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) |
18 | 17 | jctl 562 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸) → (((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) ∧ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸))) |
19 | 18 | exp31 628 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → (𝐸:dom 𝐸–1-1-onto→ran
𝐸 → (((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) ∧ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸))))) |
20 | 16, 19 | mpancom 700 |
. . . . . . . . . . . . . 14
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → (𝐸:dom 𝐸–1-1-onto→ran
𝐸 → (((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) ∧ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸))))) |
21 | 8, 20 | mpd 15 |
. . . . . . . . . . . . 13
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → (𝐸:dom 𝐸–1-1-onto→ran
𝐸 → (((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) ∧ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸)))) |
22 | 21 | ex 449 |
. . . . . . . . . . . 12
⊢ (𝑉 USGrph 𝐸 → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) → (𝐸:dom 𝐸–1-1-onto→ran
𝐸 → (((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) ∧ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸))))) |
23 | 7, 22 | mpid 43 |
. . . . . . . . . . 11
⊢ (𝑉 USGrph 𝐸 → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) → (((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) ∧ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸)))) |
24 | 23 | imp 444 |
. . . . . . . . . 10
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → (((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) ∧ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸))) |
25 | 24 | adantl 481 |
. . . . . . . . 9
⊢
(((#‘𝐹) = 3
∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) → (((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) ∧ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸))) |
26 | | c0ex 9913 |
. . . . . . . . . . 11
⊢ 0 ∈
V |
27 | | 1ex 9914 |
. . . . . . . . . . 11
⊢ 1 ∈
V |
28 | | 2z 11286 |
. . . . . . . . . . 11
⊢ 2 ∈
ℤ |
29 | 26, 27, 28 | 3pm3.2i 1232 |
. . . . . . . . . 10
⊢ (0 ∈
V ∧ 1 ∈ V ∧ 2 ∈ ℤ) |
30 | | eqidd 2611 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘0) = (𝐹‘0) → 0 = 0) |
31 | 30 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) ∧ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸)) → ((𝐹‘0) = (𝐹‘0) → 0 = 0)) |
32 | | f1of1 6049 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐸:dom 𝐸–1-1-onto→ran
𝐸 → 𝐸:dom 𝐸–1-1→ran 𝐸) |
33 | 32 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸) → 𝐸:dom 𝐸–1-1→ran 𝐸) |
34 | | 3simpa 1051 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) → ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) |
35 | 34 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) |
36 | 35 | ad3antlr 763 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸) → ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) |
37 | | f1ocnvfvrneq 6441 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) → ((◡𝐸‘{𝐴, 𝐵}) = (◡𝐸‘{𝐵, 𝐶}) → {𝐴, 𝐵} = {𝐵, 𝐶})) |
38 | 33, 36, 37 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸) → ((◡𝐸‘{𝐴, 𝐵}) = (◡𝐸‘{𝐵, 𝐶}) → {𝐴, 𝐵} = {𝐵, 𝐶})) |
39 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) |
40 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ 𝑉) |
41 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) → 𝐶 ∈ 𝑉) |
42 | 40, 41 | anim12i 588 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) → (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) |
43 | | preq12bg 4326 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ({𝐴, 𝐵} = {𝐵, 𝐶} ↔ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐵)))) |
44 | 39, 42, 43 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) → ({𝐴, 𝐵} = {𝐵, 𝐶} ↔ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐵)))) |
45 | | df-ne 2782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) |
46 | | pm2.21 119 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (¬
𝐴 = 𝐵 → (𝐴 = 𝐵 → 0 = 1)) |
47 | 45, 46 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐴 ≠ 𝐵 → (𝐴 = 𝐵 → 0 = 1)) |
48 | 47 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → (𝐴 = 𝐵 → 0 = 1)) |
49 | 48 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐴 = 𝐵 → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → 0 = 1)) |
50 | 49 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → 0 = 1)) |
51 | | df-ne 2782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐶 ≠ 𝐴 ↔ ¬ 𝐶 = 𝐴) |
52 | | pm2.21 119 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (¬
𝐶 = 𝐴 → (𝐶 = 𝐴 → 0 = 1)) |
53 | 51, 52 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐶 ≠ 𝐴 → (𝐶 = 𝐴 → 0 = 1)) |
54 | 53 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → (𝐶 = 𝐴 → 0 = 1)) |
55 | 54 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐶 = 𝐴 → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → 0 = 1)) |
56 | 55 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐴 = 𝐶 → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → 0 = 1)) |
57 | 56 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐵) → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → 0 = 1)) |
58 | 50, 57 | jaoi 393 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐵)) → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → 0 = 1)) |
59 | 44, 58 | syl6bi 242 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) → ({𝐴, 𝐵} = {𝐵, 𝐶} → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → 0 = 1))) |
60 | 59 | com23 84 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → ({𝐴, 𝐵} = {𝐵, 𝐶} → 0 = 1))) |
61 | 60 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → ({𝐴, 𝐵} = {𝐵, 𝐶} → 0 = 1))) |
62 | 61 | imp 444 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) → ({𝐴, 𝐵} = {𝐵, 𝐶} → 0 = 1)) |
63 | 62 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸) → ({𝐴, 𝐵} = {𝐵, 𝐶} → 0 = 1)) |
64 | 38, 63 | syld 46 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸) → ((◡𝐸‘{𝐴, 𝐵}) = (◡𝐸‘{𝐵, 𝐶}) → 0 = 1)) |
65 | 64 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) ∧ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸)) → ((◡𝐸‘{𝐴, 𝐵}) = (◡𝐸‘{𝐵, 𝐶}) → 0 = 1)) |
66 | | eqeq12 2623 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶})) → ((𝐹‘0) = (𝐹‘1) ↔ (◡𝐸‘{𝐴, 𝐵}) = (◡𝐸‘{𝐵, 𝐶}))) |
67 | 66 | 3adant3 1074 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) → ((𝐹‘0) = (𝐹‘1) ↔ (◡𝐸‘{𝐴, 𝐵}) = (◡𝐸‘{𝐵, 𝐶}))) |
68 | 67 | imbi1d 330 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) → (((𝐹‘0) = (𝐹‘1) → 0 = 1) ↔ ((◡𝐸‘{𝐴, 𝐵}) = (◡𝐸‘{𝐵, 𝐶}) → 0 = 1))) |
69 | 68 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) ∧ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸)) → (((𝐹‘0) = (𝐹‘1) → 0 = 1) ↔ ((◡𝐸‘{𝐴, 𝐵}) = (◡𝐸‘{𝐵, 𝐶}) → 0 = 1))) |
70 | 65, 69 | mpbird 246 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) ∧ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸)) → ((𝐹‘0) = (𝐹‘1) → 0 = 1)) |
71 | | 3simpb 1052 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) → ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) |
72 | 71 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) |
73 | 72 | ad3antlr 763 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸) → ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) |
74 | | f1ocnvfvrneq 6441 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → ((◡𝐸‘{𝐴, 𝐵}) = (◡𝐸‘{𝐶, 𝐴}) → {𝐴, 𝐵} = {𝐶, 𝐴})) |
75 | 33, 73, 74 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸) → ((◡𝐸‘{𝐴, 𝐵}) = (◡𝐸‘{𝐶, 𝐴}) → {𝐴, 𝐵} = {𝐶, 𝐴})) |
76 | | preq12bg 4326 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) → ({𝐴, 𝐵} = {𝐶, 𝐴} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐴) ∨ (𝐴 = 𝐴 ∧ 𝐵 = 𝐶)))) |
77 | | pm2.21 119 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (¬
𝐴 = 𝐵 → (𝐴 = 𝐵 → 0 = 2)) |
78 | 45, 77 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐴 ≠ 𝐵 → (𝐴 = 𝐵 → 0 = 2)) |
79 | 78 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → (𝐴 = 𝐵 → 0 = 2)) |
80 | 79 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐴 = 𝐵 → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → 0 = 2)) |
81 | 80 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐵 = 𝐴 → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → 0 = 2)) |
82 | 81 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐴) → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → 0 = 2)) |
83 | | df-ne 2782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐵 ≠ 𝐶 ↔ ¬ 𝐵 = 𝐶) |
84 | | pm2.21 119 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (¬
𝐵 = 𝐶 → (𝐵 = 𝐶 → 0 = 2)) |
85 | 83, 84 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐵 ≠ 𝐶 → (𝐵 = 𝐶 → 0 = 2)) |
86 | 85 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → (𝐵 = 𝐶 → 0 = 2)) |
87 | 86 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐵 = 𝐶 → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → 0 = 2)) |
88 | 87 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 = 𝐴 ∧ 𝐵 = 𝐶) → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → 0 = 2)) |
89 | 82, 88 | jaoi 393 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 = 𝐶 ∧ 𝐵 = 𝐴) ∨ (𝐴 = 𝐴 ∧ 𝐵 = 𝐶)) → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → 0 = 2)) |
90 | 76, 89 | syl6bi 242 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) → ({𝐴, 𝐵} = {𝐶, 𝐴} → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → 0 = 2))) |
91 | 90 | com23 84 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → ({𝐴, 𝐵} = {𝐶, 𝐴} → 0 = 2))) |
92 | 91 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → ({𝐴, 𝐵} = {𝐶, 𝐴} → 0 = 2))) |
93 | 92 | imp 444 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) → ({𝐴, 𝐵} = {𝐶, 𝐴} → 0 = 2)) |
94 | 93 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸) → ({𝐴, 𝐵} = {𝐶, 𝐴} → 0 = 2)) |
95 | 75, 94 | syld 46 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸) → ((◡𝐸‘{𝐴, 𝐵}) = (◡𝐸‘{𝐶, 𝐴}) → 0 = 2)) |
96 | 95 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) ∧ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸)) → ((◡𝐸‘{𝐴, 𝐵}) = (◡𝐸‘{𝐶, 𝐴}) → 0 = 2)) |
97 | | eqeq12 2623 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) → ((𝐹‘0) = (𝐹‘2) ↔ (◡𝐸‘{𝐴, 𝐵}) = (◡𝐸‘{𝐶, 𝐴}))) |
98 | 97 | 3adant2 1073 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) → ((𝐹‘0) = (𝐹‘2) ↔ (◡𝐸‘{𝐴, 𝐵}) = (◡𝐸‘{𝐶, 𝐴}))) |
99 | 98 | imbi1d 330 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) → (((𝐹‘0) = (𝐹‘2) → 0 = 2) ↔ ((◡𝐸‘{𝐴, 𝐵}) = (◡𝐸‘{𝐶, 𝐴}) → 0 = 2))) |
100 | 99 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) ∧ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸)) → (((𝐹‘0) = (𝐹‘2) → 0 = 2) ↔ ((◡𝐸‘{𝐴, 𝐵}) = (◡𝐸‘{𝐶, 𝐴}) → 0 = 2))) |
101 | 96, 100 | mpbird 246 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) ∧ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸)) → ((𝐹‘0) = (𝐹‘2) → 0 = 2)) |
102 | 31, 70, 101 | 3jca 1235 |
. . . . . . . . . . . . 13
⊢ ((((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) ∧ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸)) → (((𝐹‘0) = (𝐹‘0) → 0 = 0) ∧ ((𝐹‘0) = (𝐹‘1) → 0 = 1) ∧ ((𝐹‘0) = (𝐹‘2) → 0 = 2))) |
103 | 102 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((0
∈ V ∧ 1 ∈ V ∧ 2 ∈ ℤ) ∧ (((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) ∧ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸))) → (((𝐹‘0) = (𝐹‘0) → 0 = 0) ∧ ((𝐹‘0) = (𝐹‘1) → 0 = 1) ∧ ((𝐹‘0) = (𝐹‘2) → 0 = 2))) |
104 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 0 → (𝐹‘𝑦) = (𝐹‘0)) |
105 | 104 | eqeq2d 2620 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 0 → ((𝐹‘0) = (𝐹‘𝑦) ↔ (𝐹‘0) = (𝐹‘0))) |
106 | | eqeq2 2621 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 0 → (0 = 𝑦 ↔ 0 = 0)) |
107 | 105, 106 | imbi12d 333 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 0 → (((𝐹‘0) = (𝐹‘𝑦) → 0 = 𝑦) ↔ ((𝐹‘0) = (𝐹‘0) → 0 = 0))) |
108 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 1 → (𝐹‘𝑦) = (𝐹‘1)) |
109 | 108 | eqeq2d 2620 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 1 → ((𝐹‘0) = (𝐹‘𝑦) ↔ (𝐹‘0) = (𝐹‘1))) |
110 | | eqeq2 2621 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 1 → (0 = 𝑦 ↔ 0 = 1)) |
111 | 109, 110 | imbi12d 333 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 1 → (((𝐹‘0) = (𝐹‘𝑦) → 0 = 𝑦) ↔ ((𝐹‘0) = (𝐹‘1) → 0 = 1))) |
112 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 2 → (𝐹‘𝑦) = (𝐹‘2)) |
113 | 112 | eqeq2d 2620 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 2 → ((𝐹‘0) = (𝐹‘𝑦) ↔ (𝐹‘0) = (𝐹‘2))) |
114 | | eqeq2 2621 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 2 → (0 = 𝑦 ↔ 0 = 2)) |
115 | 113, 114 | imbi12d 333 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 2 → (((𝐹‘0) = (𝐹‘𝑦) → 0 = 𝑦) ↔ ((𝐹‘0) = (𝐹‘2) → 0 = 2))) |
116 | 107, 111,
115 | raltpg 4183 |
. . . . . . . . . . . . 13
⊢ ((0
∈ V ∧ 1 ∈ V ∧ 2 ∈ ℤ) → (∀𝑦 ∈ {0, 1, 2} ((𝐹‘0) = (𝐹‘𝑦) → 0 = 𝑦) ↔ (((𝐹‘0) = (𝐹‘0) → 0 = 0) ∧ ((𝐹‘0) = (𝐹‘1) → 0 = 1) ∧ ((𝐹‘0) = (𝐹‘2) → 0 = 2)))) |
117 | 116 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((0
∈ V ∧ 1 ∈ V ∧ 2 ∈ ℤ) ∧ (((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) ∧ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸))) → (∀𝑦 ∈ {0, 1, 2} ((𝐹‘0) = (𝐹‘𝑦) → 0 = 𝑦) ↔ (((𝐹‘0) = (𝐹‘0) → 0 = 0) ∧ ((𝐹‘0) = (𝐹‘1) → 0 = 1) ∧ ((𝐹‘0) = (𝐹‘2) → 0 = 2)))) |
118 | 103, 117 | mpbird 246 |
. . . . . . . . . . 11
⊢ (((0
∈ V ∧ 1 ∈ V ∧ 2 ∈ ℤ) ∧ (((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) ∧ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸))) → ∀𝑦 ∈ {0, 1, 2} ((𝐹‘0) = (𝐹‘𝑦) → 0 = 𝑦)) |
119 | | pm3.22 464 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) → ({𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸)) |
120 | 119 | 3adant3 1074 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) → ({𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸)) |
121 | 120 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → ({𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸)) |
122 | 121 | ad3antlr 763 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸) → ({𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸)) |
123 | | f1ocnvfvrneq 6441 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ ({𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸)) → ((◡𝐸‘{𝐵, 𝐶}) = (◡𝐸‘{𝐴, 𝐵}) → {𝐵, 𝐶} = {𝐴, 𝐵})) |
124 | 33, 122, 123 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸) → ((◡𝐸‘{𝐵, 𝐶}) = (◡𝐸‘{𝐴, 𝐵}) → {𝐵, 𝐶} = {𝐴, 𝐵})) |
125 | | preq12bg 4326 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → ({𝐵, 𝐶} = {𝐴, 𝐵} ↔ ((𝐵 = 𝐴 ∧ 𝐶 = 𝐵) ∨ (𝐵 = 𝐵 ∧ 𝐶 = 𝐴)))) |
126 | 42, 39, 125 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) → ({𝐵, 𝐶} = {𝐴, 𝐵} ↔ ((𝐵 = 𝐴 ∧ 𝐶 = 𝐵) ∨ (𝐵 = 𝐵 ∧ 𝐶 = 𝐴)))) |
127 | | pm2.21 119 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (¬
𝐴 = 𝐵 → (𝐴 = 𝐵 → 1 = 0)) |
128 | 45, 127 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐴 ≠ 𝐵 → (𝐴 = 𝐵 → 1 = 0)) |
129 | 128 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → (𝐴 = 𝐵 → 1 = 0)) |
130 | 129 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐴 = 𝐵 → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → 1 = 0)) |
131 | 130 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐵 = 𝐴 → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → 1 = 0)) |
132 | 131 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐵 = 𝐴 ∧ 𝐶 = 𝐵) → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → 1 = 0)) |
133 | | pm2.21 119 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (¬
𝐶 = 𝐴 → (𝐶 = 𝐴 → 1 = 0)) |
134 | 51, 133 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐶 ≠ 𝐴 → (𝐶 = 𝐴 → 1 = 0)) |
135 | 134 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → (𝐶 = 𝐴 → 1 = 0)) |
136 | 135 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐶 = 𝐴 → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → 1 = 0)) |
137 | 136 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐵 = 𝐵 ∧ 𝐶 = 𝐴) → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → 1 = 0)) |
138 | 132, 137 | jaoi 393 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐵 = 𝐴 ∧ 𝐶 = 𝐵) ∨ (𝐵 = 𝐵 ∧ 𝐶 = 𝐴)) → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → 1 = 0)) |
139 | 126, 138 | syl6bi 242 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) → ({𝐵, 𝐶} = {𝐴, 𝐵} → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → 1 = 0))) |
140 | 139 | com23 84 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → ({𝐵, 𝐶} = {𝐴, 𝐵} → 1 = 0))) |
141 | 140 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → ({𝐵, 𝐶} = {𝐴, 𝐵} → 1 = 0))) |
142 | 141 | imp 444 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) → ({𝐵, 𝐶} = {𝐴, 𝐵} → 1 = 0)) |
143 | 142 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸) → ({𝐵, 𝐶} = {𝐴, 𝐵} → 1 = 0)) |
144 | 124, 143 | syld 46 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸) → ((◡𝐸‘{𝐵, 𝐶}) = (◡𝐸‘{𝐴, 𝐵}) → 1 = 0)) |
145 | 144 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) ∧ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸)) → ((◡𝐸‘{𝐵, 𝐶}) = (◡𝐸‘{𝐴, 𝐵}) → 1 = 0)) |
146 | | eqeq12 2623 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘0) = (◡𝐸‘{𝐴, 𝐵})) → ((𝐹‘1) = (𝐹‘0) ↔ (◡𝐸‘{𝐵, 𝐶}) = (◡𝐸‘{𝐴, 𝐵}))) |
147 | 146 | ancoms 468 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶})) → ((𝐹‘1) = (𝐹‘0) ↔ (◡𝐸‘{𝐵, 𝐶}) = (◡𝐸‘{𝐴, 𝐵}))) |
148 | 147 | 3adant3 1074 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) → ((𝐹‘1) = (𝐹‘0) ↔ (◡𝐸‘{𝐵, 𝐶}) = (◡𝐸‘{𝐴, 𝐵}))) |
149 | 148 | imbi1d 330 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) → (((𝐹‘1) = (𝐹‘0) → 1 = 0) ↔ ((◡𝐸‘{𝐵, 𝐶}) = (◡𝐸‘{𝐴, 𝐵}) → 1 = 0))) |
150 | 149 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) ∧ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸)) → (((𝐹‘1) = (𝐹‘0) → 1 = 0) ↔ ((◡𝐸‘{𝐵, 𝐶}) = (◡𝐸‘{𝐴, 𝐵}) → 1 = 0))) |
151 | 145, 150 | mpbird 246 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) ∧ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸)) → ((𝐹‘1) = (𝐹‘0) → 1 = 0)) |
152 | | eqidd 2611 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘1) = (𝐹‘1) → 1 = 1) |
153 | 152 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) ∧ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸)) → ((𝐹‘1) = (𝐹‘1) → 1 = 1)) |
154 | | 3simpc 1053 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) → ({𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) |
155 | 154 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → ({𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) |
156 | 155 | ad3antlr 763 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸) → ({𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) |
157 | | f1ocnvfvrneq 6441 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ ({𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → ((◡𝐸‘{𝐵, 𝐶}) = (◡𝐸‘{𝐶, 𝐴}) → {𝐵, 𝐶} = {𝐶, 𝐴})) |
158 | 33, 156, 157 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸) → ((◡𝐸‘{𝐵, 𝐶}) = (◡𝐸‘{𝐶, 𝐴}) → {𝐵, 𝐶} = {𝐶, 𝐴})) |
159 | | preq12bg 4326 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) → ({𝐵, 𝐶} = {𝐶, 𝐴} ↔ ((𝐵 = 𝐶 ∧ 𝐶 = 𝐴) ∨ (𝐵 = 𝐴 ∧ 𝐶 = 𝐶)))) |
160 | 42, 159 | sylancom 698 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) → ({𝐵, 𝐶} = {𝐶, 𝐴} ↔ ((𝐵 = 𝐶 ∧ 𝐶 = 𝐴) ∨ (𝐵 = 𝐴 ∧ 𝐶 = 𝐶)))) |
161 | | pm2.21 119 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (¬
𝐵 = 𝐶 → (𝐵 = 𝐶 → 1 = 2)) |
162 | 83, 161 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐵 ≠ 𝐶 → (𝐵 = 𝐶 → 1 = 2)) |
163 | 162 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → (𝐵 = 𝐶 → 1 = 2)) |
164 | 163 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐵 = 𝐶 → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → 1 = 2)) |
165 | 164 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐵 = 𝐶 ∧ 𝐶 = 𝐴) → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → 1 = 2)) |
166 | | pm2.21 119 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (¬
𝐴 = 𝐵 → (𝐴 = 𝐵 → 1 = 2)) |
167 | 45, 166 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐴 ≠ 𝐵 → (𝐴 = 𝐵 → 1 = 2)) |
168 | 167 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → (𝐴 = 𝐵 → 1 = 2)) |
169 | 168 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐴 = 𝐵 → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → 1 = 2)) |
170 | 169 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐵 = 𝐴 → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → 1 = 2)) |
171 | 170 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐵 = 𝐴 ∧ 𝐶 = 𝐶) → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → 1 = 2)) |
172 | 165, 171 | jaoi 393 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐵 = 𝐶 ∧ 𝐶 = 𝐴) ∨ (𝐵 = 𝐴 ∧ 𝐶 = 𝐶)) → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → 1 = 2)) |
173 | 160, 172 | syl6bi 242 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) → ({𝐵, 𝐶} = {𝐶, 𝐴} → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → 1 = 2))) |
174 | 173 | com23 84 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → ({𝐵, 𝐶} = {𝐶, 𝐴} → 1 = 2))) |
175 | 174 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → ({𝐵, 𝐶} = {𝐶, 𝐴} → 1 = 2))) |
176 | 175 | imp 444 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) → ({𝐵, 𝐶} = {𝐶, 𝐴} → 1 = 2)) |
177 | 176 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸) → ({𝐵, 𝐶} = {𝐶, 𝐴} → 1 = 2)) |
178 | 158, 177 | syld 46 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸) → ((◡𝐸‘{𝐵, 𝐶}) = (◡𝐸‘{𝐶, 𝐴}) → 1 = 2)) |
179 | 178 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) ∧ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸)) → ((◡𝐸‘{𝐵, 𝐶}) = (◡𝐸‘{𝐶, 𝐴}) → 1 = 2)) |
180 | | eqeq12 2623 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) → ((𝐹‘1) = (𝐹‘2) ↔ (◡𝐸‘{𝐵, 𝐶}) = (◡𝐸‘{𝐶, 𝐴}))) |
181 | 180 | 3adant1 1072 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) → ((𝐹‘1) = (𝐹‘2) ↔ (◡𝐸‘{𝐵, 𝐶}) = (◡𝐸‘{𝐶, 𝐴}))) |
182 | 181 | imbi1d 330 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) → (((𝐹‘1) = (𝐹‘2) → 1 = 2) ↔ ((◡𝐸‘{𝐵, 𝐶}) = (◡𝐸‘{𝐶, 𝐴}) → 1 = 2))) |
183 | 182 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) ∧ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸)) → (((𝐹‘1) = (𝐹‘2) → 1 = 2) ↔ ((◡𝐸‘{𝐵, 𝐶}) = (◡𝐸‘{𝐶, 𝐴}) → 1 = 2))) |
184 | 179, 183 | mpbird 246 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) ∧ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸)) → ((𝐹‘1) = (𝐹‘2) → 1 = 2)) |
185 | 151, 153,
184 | 3jca 1235 |
. . . . . . . . . . . . 13
⊢ ((((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) ∧ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸)) → (((𝐹‘1) = (𝐹‘0) → 1 = 0) ∧ ((𝐹‘1) = (𝐹‘1) → 1 = 1) ∧ ((𝐹‘1) = (𝐹‘2) → 1 = 2))) |
186 | 185 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((0
∈ V ∧ 1 ∈ V ∧ 2 ∈ ℤ) ∧ (((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) ∧ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸))) → (((𝐹‘1) = (𝐹‘0) → 1 = 0) ∧ ((𝐹‘1) = (𝐹‘1) → 1 = 1) ∧ ((𝐹‘1) = (𝐹‘2) → 1 = 2))) |
187 | 104 | eqeq2d 2620 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 0 → ((𝐹‘1) = (𝐹‘𝑦) ↔ (𝐹‘1) = (𝐹‘0))) |
188 | | eqeq2 2621 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 0 → (1 = 𝑦 ↔ 1 = 0)) |
189 | 187, 188 | imbi12d 333 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 0 → (((𝐹‘1) = (𝐹‘𝑦) → 1 = 𝑦) ↔ ((𝐹‘1) = (𝐹‘0) → 1 = 0))) |
190 | 108 | eqeq2d 2620 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 1 → ((𝐹‘1) = (𝐹‘𝑦) ↔ (𝐹‘1) = (𝐹‘1))) |
191 | | eqeq2 2621 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 1 → (1 = 𝑦 ↔ 1 = 1)) |
192 | 190, 191 | imbi12d 333 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 1 → (((𝐹‘1) = (𝐹‘𝑦) → 1 = 𝑦) ↔ ((𝐹‘1) = (𝐹‘1) → 1 = 1))) |
193 | 112 | eqeq2d 2620 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 2 → ((𝐹‘1) = (𝐹‘𝑦) ↔ (𝐹‘1) = (𝐹‘2))) |
194 | | eqeq2 2621 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 2 → (1 = 𝑦 ↔ 1 = 2)) |
195 | 193, 194 | imbi12d 333 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 2 → (((𝐹‘1) = (𝐹‘𝑦) → 1 = 𝑦) ↔ ((𝐹‘1) = (𝐹‘2) → 1 = 2))) |
196 | 189, 192,
195 | raltpg 4183 |
. . . . . . . . . . . . 13
⊢ ((0
∈ V ∧ 1 ∈ V ∧ 2 ∈ ℤ) → (∀𝑦 ∈ {0, 1, 2} ((𝐹‘1) = (𝐹‘𝑦) → 1 = 𝑦) ↔ (((𝐹‘1) = (𝐹‘0) → 1 = 0) ∧ ((𝐹‘1) = (𝐹‘1) → 1 = 1) ∧ ((𝐹‘1) = (𝐹‘2) → 1 = 2)))) |
197 | 196 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((0
∈ V ∧ 1 ∈ V ∧ 2 ∈ ℤ) ∧ (((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) ∧ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸))) → (∀𝑦 ∈ {0, 1, 2} ((𝐹‘1) = (𝐹‘𝑦) → 1 = 𝑦) ↔ (((𝐹‘1) = (𝐹‘0) → 1 = 0) ∧ ((𝐹‘1) = (𝐹‘1) → 1 = 1) ∧ ((𝐹‘1) = (𝐹‘2) → 1 = 2)))) |
198 | 186, 197 | mpbird 246 |
. . . . . . . . . . 11
⊢ (((0
∈ V ∧ 1 ∈ V ∧ 2 ∈ ℤ) ∧ (((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) ∧ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸))) → ∀𝑦 ∈ {0, 1, 2} ((𝐹‘1) = (𝐹‘𝑦) → 1 = 𝑦)) |
199 | | pm3.22 464 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) → ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸)) |
200 | 199 | 3adant2 1073 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) → ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸)) |
201 | 200 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸)) |
202 | 201 | ad3antlr 763 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸) → ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸)) |
203 | | f1ocnvfvrneq 6441 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸)) → ((◡𝐸‘{𝐶, 𝐴}) = (◡𝐸‘{𝐴, 𝐵}) → {𝐶, 𝐴} = {𝐴, 𝐵})) |
204 | 33, 202, 203 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸) → ((◡𝐸‘{𝐶, 𝐴}) = (◡𝐸‘{𝐴, 𝐵}) → {𝐶, 𝐴} = {𝐴, 𝐵})) |
205 | | preq12bg 4326 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → ({𝐶, 𝐴} = {𝐴, 𝐵} ↔ ((𝐶 = 𝐴 ∧ 𝐴 = 𝐵) ∨ (𝐶 = 𝐵 ∧ 𝐴 = 𝐴)))) |
206 | 205 | ancoms 468 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) → ({𝐶, 𝐴} = {𝐴, 𝐵} ↔ ((𝐶 = 𝐴 ∧ 𝐴 = 𝐵) ∨ (𝐶 = 𝐵 ∧ 𝐴 = 𝐴)))) |
207 | | pm2.21 119 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (¬
𝐴 = 𝐵 → (𝐴 = 𝐵 → 2 = 0)) |
208 | 45, 207 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐴 ≠ 𝐵 → (𝐴 = 𝐵 → 2 = 0)) |
209 | 208 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → (𝐴 = 𝐵 → 2 = 0)) |
210 | 209 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐴 = 𝐵 → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → 2 = 0)) |
211 | 210 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐶 = 𝐴 ∧ 𝐴 = 𝐵) → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → 2 = 0)) |
212 | | pm2.21 119 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (¬
𝐵 = 𝐶 → (𝐵 = 𝐶 → 2 = 0)) |
213 | 83, 212 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐵 ≠ 𝐶 → (𝐵 = 𝐶 → 2 = 0)) |
214 | 213 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → (𝐵 = 𝐶 → 2 = 0)) |
215 | 214 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐵 = 𝐶 → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → 2 = 0)) |
216 | 215 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐶 = 𝐵 → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → 2 = 0)) |
217 | 216 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐶 = 𝐵 ∧ 𝐴 = 𝐴) → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → 2 = 0)) |
218 | 211, 217 | jaoi 393 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐶 = 𝐴 ∧ 𝐴 = 𝐵) ∨ (𝐶 = 𝐵 ∧ 𝐴 = 𝐴)) → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → 2 = 0)) |
219 | 206, 218 | syl6bi 242 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) → ({𝐶, 𝐴} = {𝐴, 𝐵} → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → 2 = 0))) |
220 | 219 | com23 84 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → ({𝐶, 𝐴} = {𝐴, 𝐵} → 2 = 0))) |
221 | 220 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → ({𝐶, 𝐴} = {𝐴, 𝐵} → 2 = 0))) |
222 | 221 | imp 444 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) → ({𝐶, 𝐴} = {𝐴, 𝐵} → 2 = 0)) |
223 | 222 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸) → ({𝐶, 𝐴} = {𝐴, 𝐵} → 2 = 0)) |
224 | 204, 223 | syld 46 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸) → ((◡𝐸‘{𝐶, 𝐴}) = (◡𝐸‘{𝐴, 𝐵}) → 2 = 0)) |
225 | 224 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) ∧ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸)) → ((◡𝐸‘{𝐶, 𝐴}) = (◡𝐸‘{𝐴, 𝐵}) → 2 = 0)) |
226 | | eqeq12 2623 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹‘2) = (◡𝐸‘{𝐶, 𝐴}) ∧ (𝐹‘0) = (◡𝐸‘{𝐴, 𝐵})) → ((𝐹‘2) = (𝐹‘0) ↔ (◡𝐸‘{𝐶, 𝐴}) = (◡𝐸‘{𝐴, 𝐵}))) |
227 | 226 | ancoms 468 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) → ((𝐹‘2) = (𝐹‘0) ↔ (◡𝐸‘{𝐶, 𝐴}) = (◡𝐸‘{𝐴, 𝐵}))) |
228 | 227 | 3adant2 1073 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) → ((𝐹‘2) = (𝐹‘0) ↔ (◡𝐸‘{𝐶, 𝐴}) = (◡𝐸‘{𝐴, 𝐵}))) |
229 | 228 | imbi1d 330 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) → (((𝐹‘2) = (𝐹‘0) → 2 = 0) ↔ ((◡𝐸‘{𝐶, 𝐴}) = (◡𝐸‘{𝐴, 𝐵}) → 2 = 0))) |
230 | 229 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) ∧ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸)) → (((𝐹‘2) = (𝐹‘0) → 2 = 0) ↔ ((◡𝐸‘{𝐶, 𝐴}) = (◡𝐸‘{𝐴, 𝐵}) → 2 = 0))) |
231 | 225, 230 | mpbird 246 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) ∧ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸)) → ((𝐹‘2) = (𝐹‘0) → 2 = 0)) |
232 | | pm3.22 464 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (({𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) → ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) |
233 | 232 | 3adant1 1072 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) → ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) |
234 | 233 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) |
235 | 234 | ad3antlr 763 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸) → ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) |
236 | | f1ocnvfvrneq 6441 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐸:dom 𝐸–1-1→ran 𝐸 ∧ ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) → ((◡𝐸‘{𝐶, 𝐴}) = (◡𝐸‘{𝐵, 𝐶}) → {𝐶, 𝐴} = {𝐵, 𝐶})) |
237 | 33, 235, 236 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸) → ((◡𝐸‘{𝐶, 𝐴}) = (◡𝐸‘{𝐵, 𝐶}) → {𝐶, 𝐴} = {𝐵, 𝐶})) |
238 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) → (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) |
239 | | preq12bg 4326 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ({𝐶, 𝐴} = {𝐵, 𝐶} ↔ ((𝐶 = 𝐵 ∧ 𝐴 = 𝐶) ∨ (𝐶 = 𝐶 ∧ 𝐴 = 𝐵)))) |
240 | 238, 42, 239 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) → ({𝐶, 𝐴} = {𝐵, 𝐶} ↔ ((𝐶 = 𝐵 ∧ 𝐴 = 𝐶) ∨ (𝐶 = 𝐶 ∧ 𝐴 = 𝐵)))) |
241 | | pm2.21 119 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (¬
𝐶 = 𝐴 → (𝐶 = 𝐴 → 2 = 1)) |
242 | 51, 241 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐶 ≠ 𝐴 → (𝐶 = 𝐴 → 2 = 1)) |
243 | 242 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → (𝐶 = 𝐴 → 2 = 1)) |
244 | 243 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐶 = 𝐴 → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → 2 = 1)) |
245 | 244 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐴 = 𝐶 → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → 2 = 1)) |
246 | 245 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐶 = 𝐵 ∧ 𝐴 = 𝐶) → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → 2 = 1)) |
247 | | pm2.21 119 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (¬
𝐴 = 𝐵 → (𝐴 = 𝐵 → 2 = 1)) |
248 | 45, 247 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐴 ≠ 𝐵 → (𝐴 = 𝐵 → 2 = 1)) |
249 | 248 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → (𝐴 = 𝐵 → 2 = 1)) |
250 | 249 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐴 = 𝐵 → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → 2 = 1)) |
251 | 250 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐶 = 𝐶 ∧ 𝐴 = 𝐵) → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → 2 = 1)) |
252 | 246, 251 | jaoi 393 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐶 = 𝐵 ∧ 𝐴 = 𝐶) ∨ (𝐶 = 𝐶 ∧ 𝐴 = 𝐵)) → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → 2 = 1)) |
253 | 240, 252 | syl6bi 242 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) → ({𝐶, 𝐴} = {𝐵, 𝐶} → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → 2 = 1))) |
254 | 253 | com23 84 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → ({𝐶, 𝐴} = {𝐵, 𝐶} → 2 = 1))) |
255 | 254 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → ({𝐶, 𝐴} = {𝐵, 𝐶} → 2 = 1))) |
256 | 255 | imp 444 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) → ({𝐶, 𝐴} = {𝐵, 𝐶} → 2 = 1)) |
257 | 256 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸) → ({𝐶, 𝐴} = {𝐵, 𝐶} → 2 = 1)) |
258 | 237, 257 | syld 46 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸) → ((◡𝐸‘{𝐶, 𝐴}) = (◡𝐸‘{𝐵, 𝐶}) → 2 = 1)) |
259 | 258 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) ∧ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸)) → ((◡𝐸‘{𝐶, 𝐴}) = (◡𝐸‘{𝐵, 𝐶}) → 2 = 1)) |
260 | | eqeq12 2623 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹‘2) = (◡𝐸‘{𝐶, 𝐴}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶})) → ((𝐹‘2) = (𝐹‘1) ↔ (◡𝐸‘{𝐶, 𝐴}) = (◡𝐸‘{𝐵, 𝐶}))) |
261 | 260 | ancoms 468 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) → ((𝐹‘2) = (𝐹‘1) ↔ (◡𝐸‘{𝐶, 𝐴}) = (◡𝐸‘{𝐵, 𝐶}))) |
262 | 261 | 3adant1 1072 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) → ((𝐹‘2) = (𝐹‘1) ↔ (◡𝐸‘{𝐶, 𝐴}) = (◡𝐸‘{𝐵, 𝐶}))) |
263 | 262 | imbi1d 330 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) → (((𝐹‘2) = (𝐹‘1) → 2 = 1) ↔ ((◡𝐸‘{𝐶, 𝐴}) = (◡𝐸‘{𝐵, 𝐶}) → 2 = 1))) |
264 | 263 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) ∧ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸)) → (((𝐹‘2) = (𝐹‘1) → 2 = 1) ↔ ((◡𝐸‘{𝐶, 𝐴}) = (◡𝐸‘{𝐵, 𝐶}) → 2 = 1))) |
265 | 259, 264 | mpbird 246 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) ∧ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸)) → ((𝐹‘2) = (𝐹‘1) → 2 = 1)) |
266 | | eqidd 2611 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘2) = (𝐹‘2) → 2 = 2) |
267 | 266 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) ∧ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸)) → ((𝐹‘2) = (𝐹‘2) → 2 = 2)) |
268 | 231, 265,
267 | 3jca 1235 |
. . . . . . . . . . . . 13
⊢ ((((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) ∧ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸)) → (((𝐹‘2) = (𝐹‘0) → 2 = 0) ∧ ((𝐹‘2) = (𝐹‘1) → 2 = 1) ∧ ((𝐹‘2) = (𝐹‘2) → 2 = 2))) |
269 | 268 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((0
∈ V ∧ 1 ∈ V ∧ 2 ∈ ℤ) ∧ (((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) ∧ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸))) → (((𝐹‘2) = (𝐹‘0) → 2 = 0) ∧ ((𝐹‘2) = (𝐹‘1) → 2 = 1) ∧ ((𝐹‘2) = (𝐹‘2) → 2 = 2))) |
270 | 104 | eqeq2d 2620 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 0 → ((𝐹‘2) = (𝐹‘𝑦) ↔ (𝐹‘2) = (𝐹‘0))) |
271 | | eqeq2 2621 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 0 → (2 = 𝑦 ↔ 2 = 0)) |
272 | 270, 271 | imbi12d 333 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 0 → (((𝐹‘2) = (𝐹‘𝑦) → 2 = 𝑦) ↔ ((𝐹‘2) = (𝐹‘0) → 2 = 0))) |
273 | 108 | eqeq2d 2620 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 1 → ((𝐹‘2) = (𝐹‘𝑦) ↔ (𝐹‘2) = (𝐹‘1))) |
274 | | eqeq2 2621 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 1 → (2 = 𝑦 ↔ 2 = 1)) |
275 | 273, 274 | imbi12d 333 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 1 → (((𝐹‘2) = (𝐹‘𝑦) → 2 = 𝑦) ↔ ((𝐹‘2) = (𝐹‘1) → 2 = 1))) |
276 | 112 | eqeq2d 2620 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 2 → ((𝐹‘2) = (𝐹‘𝑦) ↔ (𝐹‘2) = (𝐹‘2))) |
277 | | eqeq2 2621 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 2 → (2 = 𝑦 ↔ 2 = 2)) |
278 | 276, 277 | imbi12d 333 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 2 → (((𝐹‘2) = (𝐹‘𝑦) → 2 = 𝑦) ↔ ((𝐹‘2) = (𝐹‘2) → 2 = 2))) |
279 | 272, 275,
278 | raltpg 4183 |
. . . . . . . . . . . . 13
⊢ ((0
∈ V ∧ 1 ∈ V ∧ 2 ∈ ℤ) → (∀𝑦 ∈ {0, 1, 2} ((𝐹‘2) = (𝐹‘𝑦) → 2 = 𝑦) ↔ (((𝐹‘2) = (𝐹‘0) → 2 = 0) ∧ ((𝐹‘2) = (𝐹‘1) → 2 = 1) ∧ ((𝐹‘2) = (𝐹‘2) → 2 = 2)))) |
280 | 279 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((0
∈ V ∧ 1 ∈ V ∧ 2 ∈ ℤ) ∧ (((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) ∧ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸))) → (∀𝑦 ∈ {0, 1, 2} ((𝐹‘2) = (𝐹‘𝑦) → 2 = 𝑦) ↔ (((𝐹‘2) = (𝐹‘0) → 2 = 0) ∧ ((𝐹‘2) = (𝐹‘1) → 2 = 1) ∧ ((𝐹‘2) = (𝐹‘2) → 2 = 2)))) |
281 | 269, 280 | mpbird 246 |
. . . . . . . . . . 11
⊢ (((0
∈ V ∧ 1 ∈ V ∧ 2 ∈ ℤ) ∧ (((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) ∧ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸))) → ∀𝑦 ∈ {0, 1, 2} ((𝐹‘2) = (𝐹‘𝑦) → 2 = 𝑦)) |
282 | 118, 198,
281 | 3jca 1235 |
. . . . . . . . . 10
⊢ (((0
∈ V ∧ 1 ∈ V ∧ 2 ∈ ℤ) ∧ (((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) ∧ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸))) → (∀𝑦 ∈ {0, 1, 2} ((𝐹‘0) = (𝐹‘𝑦) → 0 = 𝑦) ∧ ∀𝑦 ∈ {0, 1, 2} ((𝐹‘1) = (𝐹‘𝑦) → 1 = 𝑦) ∧ ∀𝑦 ∈ {0, 1, 2} ((𝐹‘2) = (𝐹‘𝑦) → 2 = 𝑦))) |
283 | 29, 282 | mpan 702 |
. . . . . . . . 9
⊢ ((((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) ∧ (((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) ∧ 𝐸:dom 𝐸–1-1-onto→ran
𝐸)) → (∀𝑦 ∈ {0, 1, 2} ((𝐹‘0) = (𝐹‘𝑦) → 0 = 𝑦) ∧ ∀𝑦 ∈ {0, 1, 2} ((𝐹‘1) = (𝐹‘𝑦) → 1 = 𝑦) ∧ ∀𝑦 ∈ {0, 1, 2} ((𝐹‘2) = (𝐹‘𝑦) → 2 = 𝑦))) |
284 | 25, 283 | syl 17 |
. . . . . . . 8
⊢
(((#‘𝐹) = 3
∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) → (∀𝑦 ∈ {0, 1, 2} ((𝐹‘0) = (𝐹‘𝑦) → 0 = 𝑦) ∧ ∀𝑦 ∈ {0, 1, 2} ((𝐹‘1) = (𝐹‘𝑦) → 1 = 𝑦) ∧ ∀𝑦 ∈ {0, 1, 2} ((𝐹‘2) = (𝐹‘𝑦) → 2 = 𝑦))) |
285 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 0 → (𝐹‘𝑥) = (𝐹‘0)) |
286 | 285 | eqeq1d 2612 |
. . . . . . . . . . . 12
⊢ (𝑥 = 0 → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ (𝐹‘0) = (𝐹‘𝑦))) |
287 | | eqeq1 2614 |
. . . . . . . . . . . 12
⊢ (𝑥 = 0 → (𝑥 = 𝑦 ↔ 0 = 𝑦)) |
288 | 286, 287 | imbi12d 333 |
. . . . . . . . . . 11
⊢ (𝑥 = 0 → (((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ ((𝐹‘0) = (𝐹‘𝑦) → 0 = 𝑦))) |
289 | 288 | ralbidv 2969 |
. . . . . . . . . 10
⊢ (𝑥 = 0 → (∀𝑦 ∈ {0, 1, 2} ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ ∀𝑦 ∈ {0, 1, 2} ((𝐹‘0) = (𝐹‘𝑦) → 0 = 𝑦))) |
290 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 1 → (𝐹‘𝑥) = (𝐹‘1)) |
291 | 290 | eqeq1d 2612 |
. . . . . . . . . . . 12
⊢ (𝑥 = 1 → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ (𝐹‘1) = (𝐹‘𝑦))) |
292 | | eqeq1 2614 |
. . . . . . . . . . . 12
⊢ (𝑥 = 1 → (𝑥 = 𝑦 ↔ 1 = 𝑦)) |
293 | 291, 292 | imbi12d 333 |
. . . . . . . . . . 11
⊢ (𝑥 = 1 → (((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ ((𝐹‘1) = (𝐹‘𝑦) → 1 = 𝑦))) |
294 | 293 | ralbidv 2969 |
. . . . . . . . . 10
⊢ (𝑥 = 1 → (∀𝑦 ∈ {0, 1, 2} ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ ∀𝑦 ∈ {0, 1, 2} ((𝐹‘1) = (𝐹‘𝑦) → 1 = 𝑦))) |
295 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 2 → (𝐹‘𝑥) = (𝐹‘2)) |
296 | 295 | eqeq1d 2612 |
. . . . . . . . . . . 12
⊢ (𝑥 = 2 → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ (𝐹‘2) = (𝐹‘𝑦))) |
297 | | eqeq1 2614 |
. . . . . . . . . . . 12
⊢ (𝑥 = 2 → (𝑥 = 𝑦 ↔ 2 = 𝑦)) |
298 | 296, 297 | imbi12d 333 |
. . . . . . . . . . 11
⊢ (𝑥 = 2 → (((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ ((𝐹‘2) = (𝐹‘𝑦) → 2 = 𝑦))) |
299 | 298 | ralbidv 2969 |
. . . . . . . . . 10
⊢ (𝑥 = 2 → (∀𝑦 ∈ {0, 1, 2} ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ ∀𝑦 ∈ {0, 1, 2} ((𝐹‘2) = (𝐹‘𝑦) → 2 = 𝑦))) |
300 | 289, 294,
299 | raltpg 4183 |
. . . . . . . . 9
⊢ ((0
∈ V ∧ 1 ∈ V ∧ 2 ∈ ℤ) → (∀𝑥 ∈ {0, 1, 2}∀𝑦 ∈ {0, 1, 2} ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ (∀𝑦 ∈ {0, 1, 2} ((𝐹‘0) = (𝐹‘𝑦) → 0 = 𝑦) ∧ ∀𝑦 ∈ {0, 1, 2} ((𝐹‘1) = (𝐹‘𝑦) → 1 = 𝑦) ∧ ∀𝑦 ∈ {0, 1, 2} ((𝐹‘2) = (𝐹‘𝑦) → 2 = 𝑦)))) |
301 | 29, 300 | ax-mp 5 |
. . . . . . . 8
⊢
(∀𝑥 ∈
{0, 1, 2}∀𝑦 ∈
{0, 1, 2} ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ (∀𝑦 ∈ {0, 1, 2} ((𝐹‘0) = (𝐹‘𝑦) → 0 = 𝑦) ∧ ∀𝑦 ∈ {0, 1, 2} ((𝐹‘1) = (𝐹‘𝑦) → 1 = 𝑦) ∧ ∀𝑦 ∈ {0, 1, 2} ((𝐹‘2) = (𝐹‘𝑦) → 2 = 𝑦))) |
302 | 284, 301 | sylibr 223 |
. . . . . . 7
⊢
(((#‘𝐹) = 3
∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) → ∀𝑥 ∈ {0, 1, 2}∀𝑦 ∈ {0, 1, 2} ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
303 | | fzo0to3tp 12421 |
. . . . . . . . 9
⊢ (0..^3) =
{0, 1, 2} |
304 | 303 | a1i 11 |
. . . . . . . 8
⊢
(((#‘𝐹) = 3
∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) → (0..^3) = {0, 1,
2}) |
305 | 304 | raleqdv 3121 |
. . . . . . . 8
⊢
(((#‘𝐹) = 3
∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) → (∀𝑦 ∈ (0..^3)((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ ∀𝑦 ∈ {0, 1, 2} ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
306 | 304, 305 | raleqbidv 3129 |
. . . . . . 7
⊢
(((#‘𝐹) = 3
∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) → (∀𝑥 ∈ (0..^3)∀𝑦 ∈ (0..^3)((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ ∀𝑥 ∈ {0, 1, 2}∀𝑦 ∈ {0, 1, 2} ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
307 | 302, 306 | mpbird 246 |
. . . . . 6
⊢
(((#‘𝐹) = 3
∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) → ∀𝑥 ∈ (0..^3)∀𝑦 ∈ (0..^3)((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
308 | | oveq2 6557 |
. . . . . . . 8
⊢
((#‘𝐹) = 3
→ (0..^(#‘𝐹)) =
(0..^3)) |
309 | 308 | raleqdv 3121 |
. . . . . . . 8
⊢
((#‘𝐹) = 3
→ (∀𝑦 ∈
(0..^(#‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ ∀𝑦 ∈ (0..^3)((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
310 | 308, 309 | raleqbidv 3129 |
. . . . . . 7
⊢
((#‘𝐹) = 3
→ (∀𝑥 ∈
(0..^(#‘𝐹))∀𝑦 ∈ (0..^(#‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ ∀𝑥 ∈ (0..^3)∀𝑦 ∈ (0..^3)((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
311 | 310 | adantr 480 |
. . . . . 6
⊢
(((#‘𝐹) = 3
∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) → (∀𝑥 ∈ (0..^(#‘𝐹))∀𝑦 ∈ (0..^(#‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ ∀𝑥 ∈ (0..^3)∀𝑦 ∈ (0..^3)((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
312 | 307, 311 | mpbird 246 |
. . . . 5
⊢
(((#‘𝐹) = 3
∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) → ∀𝑥 ∈ (0..^(#‘𝐹))∀𝑦 ∈ (0..^(#‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
313 | 6, 312 | mpan 702 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → ∀𝑥 ∈ (0..^(#‘𝐹))∀𝑦 ∈ (0..^(#‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
314 | | dff13 6416 |
. . . 4
⊢ (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 ↔ (𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ∧ ∀𝑥 ∈ (0..^(#‘𝐹))∀𝑦 ∈ (0..^(#‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
315 | 5, 313, 314 | sylanbrc 695 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → 𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸) |
316 | | df-f1 5809 |
. . 3
⊢ (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 ↔ (𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ∧ Fun ◡𝐹)) |
317 | 315, 316 | sylib 207 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → (𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ∧ Fun ◡𝐹)) |
318 | 317 | simprd 478 |
1
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → Fun ◡𝐹) |