Proof of Theorem constr3lem6
Step | Hyp | Ref
| Expression |
1 | | constr3cycl.f |
. . . . 5
⊢ 𝐹 = {〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉, 〈2, (◡𝐸‘{𝐶, 𝐴})〉} |
2 | | constr3cycl.p |
. . . . 5
⊢ 𝑃 = ({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉, 〈3, 𝐴〉}) |
3 | 1, 2 | constr3lem4 26175 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐴))) |
4 | | id 22 |
. . . . . . . 8
⊢ (𝐴 ≠ 𝐵 → 𝐴 ≠ 𝐵) |
5 | 4 | ancli 572 |
. . . . . . 7
⊢ (𝐴 ≠ 𝐵 → (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵)) |
6 | | necom 2835 |
. . . . . . . 8
⊢ (𝐶 ≠ 𝐴 ↔ 𝐴 ≠ 𝐶) |
7 | | id 22 |
. . . . . . . . 9
⊢ (𝐴 ≠ 𝐶 → 𝐴 ≠ 𝐶) |
8 | 7 | ancli 572 |
. . . . . . . 8
⊢ (𝐴 ≠ 𝐶 → (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐶)) |
9 | 6, 8 | sylbi 206 |
. . . . . . 7
⊢ (𝐶 ≠ 𝐴 → (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐶)) |
10 | 5, 9 | anim12i 588 |
. . . . . 6
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐴) → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐶))) |
11 | 10 | 3adant2 1073 |
. . . . 5
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐶))) |
12 | | simpl 472 |
. . . . . . . . 9
⊢ (((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) → (𝑃‘0) = 𝐴) |
13 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) → (𝑃‘1) = 𝐵) |
14 | 12, 13 | neeq12d 2843 |
. . . . . . . 8
⊢ (((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) → ((𝑃‘0) ≠ (𝑃‘1) ↔ 𝐴 ≠ 𝐵)) |
15 | 14 | adantr 480 |
. . . . . . 7
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐴)) → ((𝑃‘0) ≠ (𝑃‘1) ↔ 𝐴 ≠ 𝐵)) |
16 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐴) → (𝑃‘3) = 𝐴) |
17 | 16 | adantl 481 |
. . . . . . . 8
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐴)) → (𝑃‘3) = 𝐴) |
18 | 13 | adantr 480 |
. . . . . . . 8
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐴)) → (𝑃‘1) = 𝐵) |
19 | 17, 18 | neeq12d 2843 |
. . . . . . 7
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐴)) → ((𝑃‘3) ≠ (𝑃‘1) ↔ 𝐴 ≠ 𝐵)) |
20 | 15, 19 | anbi12d 743 |
. . . . . 6
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐴)) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘3) ≠ (𝑃‘1)) ↔ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵))) |
21 | 12 | adantr 480 |
. . . . . . . 8
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐴)) → (𝑃‘0) = 𝐴) |
22 | | simpl 472 |
. . . . . . . . 9
⊢ (((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐴) → (𝑃‘2) = 𝐶) |
23 | 22 | adantl 481 |
. . . . . . . 8
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐴)) → (𝑃‘2) = 𝐶) |
24 | 21, 23 | neeq12d 2843 |
. . . . . . 7
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐴)) → ((𝑃‘0) ≠ (𝑃‘2) ↔ 𝐴 ≠ 𝐶)) |
25 | 16, 22 | neeq12d 2843 |
. . . . . . . 8
⊢ (((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐴) → ((𝑃‘3) ≠ (𝑃‘2) ↔ 𝐴 ≠ 𝐶)) |
26 | 25 | adantl 481 |
. . . . . . 7
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐴)) → ((𝑃‘3) ≠ (𝑃‘2) ↔ 𝐴 ≠ 𝐶)) |
27 | 24, 26 | anbi12d 743 |
. . . . . 6
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐴)) → (((𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘3) ≠ (𝑃‘2)) ↔ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐶))) |
28 | 20, 27 | anbi12d 743 |
. . . . 5
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐴)) → ((((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘3) ≠ (𝑃‘1)) ∧ ((𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘3) ≠ (𝑃‘2))) ↔ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐶)))) |
29 | 11, 28 | syl5ibr 235 |
. . . 4
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐴)) → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘3) ≠ (𝑃‘1)) ∧ ((𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘3) ≠ (𝑃‘2))))) |
30 | 3, 29 | syl 17 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘3) ≠ (𝑃‘1)) ∧ ((𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘3) ≠ (𝑃‘2))))) |
31 | 30 | imp 444 |
. 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘3) ≠ (𝑃‘1)) ∧ ((𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘3) ≠ (𝑃‘2)))) |
32 | | disjpr2 4194 |
. 2
⊢ ((((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘3) ≠ (𝑃‘1)) ∧ ((𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘3) ≠ (𝑃‘2))) → ({(𝑃‘0), (𝑃‘3)} ∩ {(𝑃‘1), (𝑃‘2)}) = ∅) |
33 | 31, 32 | syl 17 |
1
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) → ({(𝑃‘0), (𝑃‘3)} ∩ {(𝑃‘1), (𝑃‘2)}) = ∅) |