Step | Hyp | Ref
| Expression |
1 | | dff14b 7138 |
. 2
⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦))) |
2 | | f13dfv.a |
. . . . 5
⊢ 𝐴 = {𝑋, 𝑌, 𝑍} |
3 | 2 | raleqi 3345 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ ∀𝑥 ∈ {𝑋, 𝑌, 𝑍}∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦)) |
4 | | sneq 4573 |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → {𝑥} = {𝑋}) |
5 | 4 | difeq2d 4058 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → (𝐴 ∖ {𝑥}) = (𝐴 ∖ {𝑋})) |
6 | | fveq2 6768 |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → (𝐹‘𝑥) = (𝐹‘𝑋)) |
7 | 6 | neeq1d 3003 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → ((𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑋) ≠ (𝐹‘𝑦))) |
8 | 5, 7 | raleqbidv 3335 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ ∀𝑦 ∈ (𝐴 ∖ {𝑋})(𝐹‘𝑋) ≠ (𝐹‘𝑦))) |
9 | | sneq 4573 |
. . . . . . . . 9
⊢ (𝑥 = 𝑌 → {𝑥} = {𝑌}) |
10 | 9 | difeq2d 4058 |
. . . . . . . 8
⊢ (𝑥 = 𝑌 → (𝐴 ∖ {𝑥}) = (𝐴 ∖ {𝑌})) |
11 | | fveq2 6768 |
. . . . . . . . 9
⊢ (𝑥 = 𝑌 → (𝐹‘𝑥) = (𝐹‘𝑌)) |
12 | 11 | neeq1d 3003 |
. . . . . . . 8
⊢ (𝑥 = 𝑌 → ((𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑌) ≠ (𝐹‘𝑦))) |
13 | 10, 12 | raleqbidv 3335 |
. . . . . . 7
⊢ (𝑥 = 𝑌 → (∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ ∀𝑦 ∈ (𝐴 ∖ {𝑌})(𝐹‘𝑌) ≠ (𝐹‘𝑦))) |
14 | | sneq 4573 |
. . . . . . . . 9
⊢ (𝑥 = 𝑍 → {𝑥} = {𝑍}) |
15 | 14 | difeq2d 4058 |
. . . . . . . 8
⊢ (𝑥 = 𝑍 → (𝐴 ∖ {𝑥}) = (𝐴 ∖ {𝑍})) |
16 | | fveq2 6768 |
. . . . . . . . 9
⊢ (𝑥 = 𝑍 → (𝐹‘𝑥) = (𝐹‘𝑍)) |
17 | 16 | neeq1d 3003 |
. . . . . . . 8
⊢ (𝑥 = 𝑍 → ((𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑍) ≠ (𝐹‘𝑦))) |
18 | 15, 17 | raleqbidv 3335 |
. . . . . . 7
⊢ (𝑥 = 𝑍 → (∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ ∀𝑦 ∈ (𝐴 ∖ {𝑍})(𝐹‘𝑍) ≠ (𝐹‘𝑦))) |
19 | 8, 13, 18 | raltpg 4636 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (∀𝑥 ∈ {𝑋, 𝑌, 𝑍}∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ (∀𝑦 ∈ (𝐴 ∖ {𝑋})(𝐹‘𝑋) ≠ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ {𝑌})(𝐹‘𝑌) ≠ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ {𝑍})(𝐹‘𝑍) ≠ (𝐹‘𝑦)))) |
20 | 19 | adantr 481 |
. . . . 5
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑥 ∈ {𝑋, 𝑌, 𝑍}∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ (∀𝑦 ∈ (𝐴 ∖ {𝑋})(𝐹‘𝑋) ≠ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ {𝑌})(𝐹‘𝑌) ≠ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ {𝑍})(𝐹‘𝑍) ≠ (𝐹‘𝑦)))) |
21 | 2 | difeq1i 4054 |
. . . . . . . . . . 11
⊢ (𝐴 ∖ {𝑋}) = ({𝑋, 𝑌, 𝑍} ∖ {𝑋}) |
22 | | tprot 4687 |
. . . . . . . . . . . . 13
⊢ {𝑋, 𝑌, 𝑍} = {𝑌, 𝑍, 𝑋} |
23 | 22 | difeq1i 4054 |
. . . . . . . . . . . 12
⊢ ({𝑋, 𝑌, 𝑍} ∖ {𝑋}) = ({𝑌, 𝑍, 𝑋} ∖ {𝑋}) |
24 | | necom 2997 |
. . . . . . . . . . . . . . . 16
⊢ (𝑋 ≠ 𝑌 ↔ 𝑌 ≠ 𝑋) |
25 | | necom 2997 |
. . . . . . . . . . . . . . . 16
⊢ (𝑋 ≠ 𝑍 ↔ 𝑍 ≠ 𝑋) |
26 | 24, 25 | anbi12i 627 |
. . . . . . . . . . . . . . 15
⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍) ↔ (𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋)) |
27 | 26 | biimpi 215 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍) → (𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋)) |
28 | 27 | 3adant3 1131 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → (𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋)) |
29 | | diftpsn3 4737 |
. . . . . . . . . . . . 13
⊢ ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → ({𝑌, 𝑍, 𝑋} ∖ {𝑋}) = {𝑌, 𝑍}) |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → ({𝑌, 𝑍, 𝑋} ∖ {𝑋}) = {𝑌, 𝑍}) |
31 | 23, 30 | eqtrid 2790 |
. . . . . . . . . . 11
⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → ({𝑋, 𝑌, 𝑍} ∖ {𝑋}) = {𝑌, 𝑍}) |
32 | 21, 31 | eqtrid 2790 |
. . . . . . . . . 10
⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → (𝐴 ∖ {𝑋}) = {𝑌, 𝑍}) |
33 | 32 | adantl 482 |
. . . . . . . . 9
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (𝐴 ∖ {𝑋}) = {𝑌, 𝑍}) |
34 | 33 | raleqdv 3347 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑦 ∈ (𝐴 ∖ {𝑋})(𝐹‘𝑋) ≠ (𝐹‘𝑦) ↔ ∀𝑦 ∈ {𝑌, 𝑍} (𝐹‘𝑋) ≠ (𝐹‘𝑦))) |
35 | | fveq2 6768 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑌 → (𝐹‘𝑦) = (𝐹‘𝑌)) |
36 | 35 | neeq2d 3004 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑌 → ((𝐹‘𝑋) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑋) ≠ (𝐹‘𝑌))) |
37 | | fveq2 6768 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑍 → (𝐹‘𝑦) = (𝐹‘𝑍)) |
38 | 37 | neeq2d 3004 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑍 → ((𝐹‘𝑋) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑋) ≠ (𝐹‘𝑍))) |
39 | 36, 38 | ralprg 4632 |
. . . . . . . . . 10
⊢ ((𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (∀𝑦 ∈ {𝑌, 𝑍} (𝐹‘𝑋) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍)))) |
40 | 39 | 3adant1 1129 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (∀𝑦 ∈ {𝑌, 𝑍} (𝐹‘𝑋) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍)))) |
41 | 40 | adantr 481 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑦 ∈ {𝑌, 𝑍} (𝐹‘𝑋) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍)))) |
42 | 34, 41 | bitrd 278 |
. . . . . . 7
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑦 ∈ (𝐴 ∖ {𝑋})(𝐹‘𝑋) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍)))) |
43 | 2 | difeq1i 4054 |
. . . . . . . . . . 11
⊢ (𝐴 ∖ {𝑌}) = ({𝑋, 𝑌, 𝑍} ∖ {𝑌}) |
44 | | tpcomb 4689 |
. . . . . . . . . . . . 13
⊢ {𝑋, 𝑌, 𝑍} = {𝑋, 𝑍, 𝑌} |
45 | 44 | difeq1i 4054 |
. . . . . . . . . . . 12
⊢ ({𝑋, 𝑌, 𝑍} ∖ {𝑌}) = ({𝑋, 𝑍, 𝑌} ∖ {𝑌}) |
46 | | necom 2997 |
. . . . . . . . . . . . . . . 16
⊢ (𝑌 ≠ 𝑍 ↔ 𝑍 ≠ 𝑌) |
47 | 46 | biimpi 215 |
. . . . . . . . . . . . . . 15
⊢ (𝑌 ≠ 𝑍 → 𝑍 ≠ 𝑌) |
48 | 47 | anim2i 617 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 ≠ 𝑌 ∧ 𝑌 ≠ 𝑍) → (𝑋 ≠ 𝑌 ∧ 𝑍 ≠ 𝑌)) |
49 | 48 | 3adant2 1130 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → (𝑋 ≠ 𝑌 ∧ 𝑍 ≠ 𝑌)) |
50 | | diftpsn3 4737 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ≠ 𝑌 ∧ 𝑍 ≠ 𝑌) → ({𝑋, 𝑍, 𝑌} ∖ {𝑌}) = {𝑋, 𝑍}) |
51 | 49, 50 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → ({𝑋, 𝑍, 𝑌} ∖ {𝑌}) = {𝑋, 𝑍}) |
52 | 45, 51 | eqtrid 2790 |
. . . . . . . . . . 11
⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → ({𝑋, 𝑌, 𝑍} ∖ {𝑌}) = {𝑋, 𝑍}) |
53 | 43, 52 | eqtrid 2790 |
. . . . . . . . . 10
⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → (𝐴 ∖ {𝑌}) = {𝑋, 𝑍}) |
54 | 53 | adantl 482 |
. . . . . . . . 9
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (𝐴 ∖ {𝑌}) = {𝑋, 𝑍}) |
55 | 54 | raleqdv 3347 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑦 ∈ (𝐴 ∖ {𝑌})(𝐹‘𝑌) ≠ (𝐹‘𝑦) ↔ ∀𝑦 ∈ {𝑋, 𝑍} (𝐹‘𝑌) ≠ (𝐹‘𝑦))) |
56 | | fveq2 6768 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑋 → (𝐹‘𝑦) = (𝐹‘𝑋)) |
57 | 56 | neeq2d 3004 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑋 → ((𝐹‘𝑌) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑌) ≠ (𝐹‘𝑋))) |
58 | 37 | neeq2d 3004 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑍 → ((𝐹‘𝑌) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑌) ≠ (𝐹‘𝑍))) |
59 | 57, 58 | ralprg 4632 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑍 ∈ 𝑊) → (∀𝑦 ∈ {𝑋, 𝑍} (𝐹‘𝑌) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)))) |
60 | 59 | 3adant2 1130 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (∀𝑦 ∈ {𝑋, 𝑍} (𝐹‘𝑌) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)))) |
61 | 60 | adantr 481 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑦 ∈ {𝑋, 𝑍} (𝐹‘𝑌) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)))) |
62 | 55, 61 | bitrd 278 |
. . . . . . 7
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑦 ∈ (𝐴 ∖ {𝑌})(𝐹‘𝑌) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)))) |
63 | 2 | difeq1i 4054 |
. . . . . . . . . . 11
⊢ (𝐴 ∖ {𝑍}) = ({𝑋, 𝑌, 𝑍} ∖ {𝑍}) |
64 | | diftpsn3 4737 |
. . . . . . . . . . . 12
⊢ ((𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → ({𝑋, 𝑌, 𝑍} ∖ {𝑍}) = {𝑋, 𝑌}) |
65 | 64 | 3adant1 1129 |
. . . . . . . . . . 11
⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → ({𝑋, 𝑌, 𝑍} ∖ {𝑍}) = {𝑋, 𝑌}) |
66 | 63, 65 | eqtrid 2790 |
. . . . . . . . . 10
⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → (𝐴 ∖ {𝑍}) = {𝑋, 𝑌}) |
67 | 66 | adantl 482 |
. . . . . . . . 9
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (𝐴 ∖ {𝑍}) = {𝑋, 𝑌}) |
68 | 67 | raleqdv 3347 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑦 ∈ (𝐴 ∖ {𝑍})(𝐹‘𝑍) ≠ (𝐹‘𝑦) ↔ ∀𝑦 ∈ {𝑋, 𝑌} (𝐹‘𝑍) ≠ (𝐹‘𝑦))) |
69 | 56 | neeq2d 3004 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑋 → ((𝐹‘𝑍) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑍) ≠ (𝐹‘𝑋))) |
70 | 35 | neeq2d 3004 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑌 → ((𝐹‘𝑍) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑍) ≠ (𝐹‘𝑌))) |
71 | 69, 70 | ralprg 4632 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉) → (∀𝑦 ∈ {𝑋, 𝑌} (𝐹‘𝑍) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌)))) |
72 | 71 | 3adant3 1131 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (∀𝑦 ∈ {𝑋, 𝑌} (𝐹‘𝑍) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌)))) |
73 | 72 | adantr 481 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑦 ∈ {𝑋, 𝑌} (𝐹‘𝑍) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌)))) |
74 | 68, 73 | bitrd 278 |
. . . . . . 7
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑦 ∈ (𝐴 ∖ {𝑍})(𝐹‘𝑍) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌)))) |
75 | 42, 62, 74 | 3anbi123d 1435 |
. . . . . 6
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → ((∀𝑦 ∈ (𝐴 ∖ {𝑋})(𝐹‘𝑋) ≠ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ {𝑌})(𝐹‘𝑌) ≠ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ {𝑍})(𝐹‘𝑍) ≠ (𝐹‘𝑦)) ↔ (((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍)) ∧ ((𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)) ∧ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌))))) |
76 | | ancom 461 |
. . . . . . . 8
⊢ (((𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)) ↔ ((𝐹‘𝑌) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑋))) |
77 | 76 | 3anbi2i 1157 |
. . . . . . 7
⊢ ((((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍)) ∧ ((𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)) ∧ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌))) ↔ (((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍)) ∧ ((𝐹‘𝑌) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑋)) ∧ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌)))) |
78 | | 3an6 1445 |
. . . . . . 7
⊢ ((((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍)) ∧ ((𝐹‘𝑌) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑋)) ∧ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌))) ↔ (((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑋)) ∧ ((𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌)))) |
79 | | 3anrot 1099 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑋))) |
80 | 79 | bicomi 223 |
. . . . . . . . 9
⊢ (((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑋)) ↔ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍))) |
81 | | necom 2997 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑋) ≠ (𝐹‘𝑍) ↔ (𝐹‘𝑍) ≠ (𝐹‘𝑋)) |
82 | | necom 2997 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑌) ≠ (𝐹‘𝑋) ↔ (𝐹‘𝑋) ≠ (𝐹‘𝑌)) |
83 | | necom 2997 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑍) ≠ (𝐹‘𝑌) ↔ (𝐹‘𝑌) ≠ (𝐹‘𝑍)) |
84 | 81, 82, 83 | 3anbi123i 1154 |
. . . . . . . . 9
⊢ (((𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌)) ↔ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍))) |
85 | 80, 84 | anbi12i 627 |
. . . . . . . 8
⊢ ((((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑋)) ∧ ((𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌))) ↔ (((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)) ∧ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)))) |
86 | | anidm 565 |
. . . . . . . 8
⊢ ((((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)) ∧ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍))) ↔ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍))) |
87 | | 3ancoma 1097 |
. . . . . . . . 9
⊢ (((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍))) |
88 | | necom 2997 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ↔ (𝐹‘𝑋) ≠ (𝐹‘𝑍)) |
89 | 88 | 3anbi2i 1157 |
. . . . . . . . 9
⊢ (((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍))) |
90 | 87, 89 | bitri 274 |
. . . . . . . 8
⊢ (((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍))) |
91 | 85, 86, 90 | 3bitri 297 |
. . . . . . 7
⊢ ((((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑋)) ∧ ((𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌))) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍))) |
92 | 77, 78, 91 | 3bitri 297 |
. . . . . 6
⊢ ((((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍)) ∧ ((𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)) ∧ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌))) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍))) |
93 | 75, 92 | bitrdi 287 |
. . . . 5
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → ((∀𝑦 ∈ (𝐴 ∖ {𝑋})(𝐹‘𝑋) ≠ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ {𝑌})(𝐹‘𝑌) ≠ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ {𝑍})(𝐹‘𝑍) ≠ (𝐹‘𝑦)) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)))) |
94 | 20, 93 | bitrd 278 |
. . . 4
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑥 ∈ {𝑋, 𝑌, 𝑍}∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)))) |
95 | 3, 94 | bitrid 282 |
. . 3
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)))) |
96 | 95 | anbi2d 629 |
. 2
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → ((𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦)) ↔ (𝐹:𝐴⟶𝐵 ∧ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍))))) |
97 | 1, 96 | bitrid 282 |
1
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍))))) |