Proof of Theorem f1dom3el3dif
Step | Hyp | Ref
| Expression |
1 | | f1dom3fv3dif.f |
. . 3
⊢ (𝜑 → 𝐹:{𝐴, 𝐵, 𝐶}–1-1→𝑅) |
2 | | f1f 6662 |
. . . 4
⊢ (𝐹:{𝐴, 𝐵, 𝐶}–1-1→𝑅 → 𝐹:{𝐴, 𝐵, 𝐶}⟶𝑅) |
3 | | simpr 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐹:{𝐴, 𝐵, 𝐶}⟶𝑅) → 𝐹:{𝐴, 𝐵, 𝐶}⟶𝑅) |
4 | | eqidd 2739 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 = 𝐴) |
5 | 4 | 3mix1d 1335 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 = 𝐴 ∨ 𝐴 = 𝐵 ∨ 𝐴 = 𝐶)) |
6 | | f1dom3fv3dif.v |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍)) |
7 | 6 | simp1d 1141 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ 𝑋) |
8 | | eltpg 4621 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑋 → (𝐴 ∈ {𝐴, 𝐵, 𝐶} ↔ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵 ∨ 𝐴 = 𝐶))) |
9 | 7, 8 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 ∈ {𝐴, 𝐵, 𝐶} ↔ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵 ∨ 𝐴 = 𝐶))) |
10 | 5, 9 | mpbird 256 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ {𝐴, 𝐵, 𝐶}) |
11 | 10 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐹:{𝐴, 𝐵, 𝐶}⟶𝑅) → 𝐴 ∈ {𝐴, 𝐵, 𝐶}) |
12 | 3, 11 | ffvelrnd 6954 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐹:{𝐴, 𝐵, 𝐶}⟶𝑅) → (𝐹‘𝐴) ∈ 𝑅) |
13 | | eqidd 2739 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 = 𝐵) |
14 | 13 | 3mix2d 1336 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ∨ 𝐵 = 𝐶)) |
15 | 6 | simp2d 1142 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ 𝑌) |
16 | | eltpg 4621 |
. . . . . . . . . 10
⊢ (𝐵 ∈ 𝑌 → (𝐵 ∈ {𝐴, 𝐵, 𝐶} ↔ (𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ∨ 𝐵 = 𝐶))) |
17 | 15, 16 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 ∈ {𝐴, 𝐵, 𝐶} ↔ (𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ∨ 𝐵 = 𝐶))) |
18 | 14, 17 | mpbird 256 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ {𝐴, 𝐵, 𝐶}) |
19 | 18 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐹:{𝐴, 𝐵, 𝐶}⟶𝑅) → 𝐵 ∈ {𝐴, 𝐵, 𝐶}) |
20 | 3, 19 | ffvelrnd 6954 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐹:{𝐴, 𝐵, 𝐶}⟶𝑅) → (𝐹‘𝐵) ∈ 𝑅) |
21 | 6 | simp3d 1143 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ 𝑍) |
22 | | tpid3g 4708 |
. . . . . . . . 9
⊢ (𝐶 ∈ 𝑍 → 𝐶 ∈ {𝐴, 𝐵, 𝐶}) |
23 | 21, 22 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ {𝐴, 𝐵, 𝐶}) |
24 | 23 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐹:{𝐴, 𝐵, 𝐶}⟶𝑅) → 𝐶 ∈ {𝐴, 𝐵, 𝐶}) |
25 | 3, 24 | ffvelrnd 6954 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐹:{𝐴, 𝐵, 𝐶}⟶𝑅) → (𝐹‘𝐶) ∈ 𝑅) |
26 | 12, 20, 25 | 3jca 1127 |
. . . . 5
⊢ ((𝜑 ∧ 𝐹:{𝐴, 𝐵, 𝐶}⟶𝑅) → ((𝐹‘𝐴) ∈ 𝑅 ∧ (𝐹‘𝐵) ∈ 𝑅 ∧ (𝐹‘𝐶) ∈ 𝑅)) |
27 | 26 | expcom 414 |
. . . 4
⊢ (𝐹:{𝐴, 𝐵, 𝐶}⟶𝑅 → (𝜑 → ((𝐹‘𝐴) ∈ 𝑅 ∧ (𝐹‘𝐵) ∈ 𝑅 ∧ (𝐹‘𝐶) ∈ 𝑅))) |
28 | 2, 27 | syl 17 |
. . 3
⊢ (𝐹:{𝐴, 𝐵, 𝐶}–1-1→𝑅 → (𝜑 → ((𝐹‘𝐴) ∈ 𝑅 ∧ (𝐹‘𝐵) ∈ 𝑅 ∧ (𝐹‘𝐶) ∈ 𝑅))) |
29 | 1, 28 | mpcom 38 |
. 2
⊢ (𝜑 → ((𝐹‘𝐴) ∈ 𝑅 ∧ (𝐹‘𝐵) ∈ 𝑅 ∧ (𝐹‘𝐶) ∈ 𝑅)) |
30 | | f1dom3fv3dif.n |
. . 3
⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) |
31 | 6, 30, 1 | f1dom3fv3dif 7133 |
. 2
⊢ (𝜑 → ((𝐹‘𝐴) ≠ (𝐹‘𝐵) ∧ (𝐹‘𝐴) ≠ (𝐹‘𝐶) ∧ (𝐹‘𝐵) ≠ (𝐹‘𝐶))) |
32 | | neeq1 3006 |
. . . 4
⊢ (𝑥 = (𝐹‘𝐴) → (𝑥 ≠ 𝑦 ↔ (𝐹‘𝐴) ≠ 𝑦)) |
33 | | neeq1 3006 |
. . . 4
⊢ (𝑥 = (𝐹‘𝐴) → (𝑥 ≠ 𝑧 ↔ (𝐹‘𝐴) ≠ 𝑧)) |
34 | 32, 33 | 3anbi12d 1436 |
. . 3
⊢ (𝑥 = (𝐹‘𝐴) → ((𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧) ↔ ((𝐹‘𝐴) ≠ 𝑦 ∧ (𝐹‘𝐴) ≠ 𝑧 ∧ 𝑦 ≠ 𝑧))) |
35 | | neeq2 3007 |
. . . 4
⊢ (𝑦 = (𝐹‘𝐵) → ((𝐹‘𝐴) ≠ 𝑦 ↔ (𝐹‘𝐴) ≠ (𝐹‘𝐵))) |
36 | | neeq1 3006 |
. . . 4
⊢ (𝑦 = (𝐹‘𝐵) → (𝑦 ≠ 𝑧 ↔ (𝐹‘𝐵) ≠ 𝑧)) |
37 | 35, 36 | 3anbi13d 1437 |
. . 3
⊢ (𝑦 = (𝐹‘𝐵) → (((𝐹‘𝐴) ≠ 𝑦 ∧ (𝐹‘𝐴) ≠ 𝑧 ∧ 𝑦 ≠ 𝑧) ↔ ((𝐹‘𝐴) ≠ (𝐹‘𝐵) ∧ (𝐹‘𝐴) ≠ 𝑧 ∧ (𝐹‘𝐵) ≠ 𝑧))) |
38 | | neeq2 3007 |
. . . 4
⊢ (𝑧 = (𝐹‘𝐶) → ((𝐹‘𝐴) ≠ 𝑧 ↔ (𝐹‘𝐴) ≠ (𝐹‘𝐶))) |
39 | | neeq2 3007 |
. . . 4
⊢ (𝑧 = (𝐹‘𝐶) → ((𝐹‘𝐵) ≠ 𝑧 ↔ (𝐹‘𝐵) ≠ (𝐹‘𝐶))) |
40 | 38, 39 | 3anbi23d 1438 |
. . 3
⊢ (𝑧 = (𝐹‘𝐶) → (((𝐹‘𝐴) ≠ (𝐹‘𝐵) ∧ (𝐹‘𝐴) ≠ 𝑧 ∧ (𝐹‘𝐵) ≠ 𝑧) ↔ ((𝐹‘𝐴) ≠ (𝐹‘𝐵) ∧ (𝐹‘𝐴) ≠ (𝐹‘𝐶) ∧ (𝐹‘𝐵) ≠ (𝐹‘𝐶)))) |
41 | 34, 37, 40 | rspc3ev 3573 |
. 2
⊢ ((((𝐹‘𝐴) ∈ 𝑅 ∧ (𝐹‘𝐵) ∈ 𝑅 ∧ (𝐹‘𝐶) ∈ 𝑅) ∧ ((𝐹‘𝐴) ≠ (𝐹‘𝐵) ∧ (𝐹‘𝐴) ≠ (𝐹‘𝐶) ∧ (𝐹‘𝐵) ≠ (𝐹‘𝐶))) → ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑅 ∃𝑧 ∈ 𝑅 (𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧)) |
42 | 29, 31, 41 | syl2anc 584 |
1
⊢ (𝜑 → ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑅 ∃𝑧 ∈ 𝑅 (𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧)) |