| Step | Hyp | Ref
| Expression |
| 1 | | dff14b 7291 |
. 2
⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦))) |
| 2 | | f12dfv.a |
. . . . 5
⊢ 𝐴 = {𝑋, 𝑌} |
| 3 | 2 | raleqi 3324 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ ∀𝑥 ∈ {𝑋, 𝑌}∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦)) |
| 4 | | sneq 4636 |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → {𝑥} = {𝑋}) |
| 5 | 4 | difeq2d 4126 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → (𝐴 ∖ {𝑥}) = (𝐴 ∖ {𝑋})) |
| 6 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → (𝐹‘𝑥) = (𝐹‘𝑋)) |
| 7 | 6 | neeq1d 3000 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → ((𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑋) ≠ (𝐹‘𝑦))) |
| 8 | 5, 7 | raleqbidv 3346 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ ∀𝑦 ∈ (𝐴 ∖ {𝑋})(𝐹‘𝑋) ≠ (𝐹‘𝑦))) |
| 9 | | sneq 4636 |
. . . . . . . . 9
⊢ (𝑥 = 𝑌 → {𝑥} = {𝑌}) |
| 10 | 9 | difeq2d 4126 |
. . . . . . . 8
⊢ (𝑥 = 𝑌 → (𝐴 ∖ {𝑥}) = (𝐴 ∖ {𝑌})) |
| 11 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑥 = 𝑌 → (𝐹‘𝑥) = (𝐹‘𝑌)) |
| 12 | 11 | neeq1d 3000 |
. . . . . . . 8
⊢ (𝑥 = 𝑌 → ((𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑌) ≠ (𝐹‘𝑦))) |
| 13 | 10, 12 | raleqbidv 3346 |
. . . . . . 7
⊢ (𝑥 = 𝑌 → (∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ ∀𝑦 ∈ (𝐴 ∖ {𝑌})(𝐹‘𝑌) ≠ (𝐹‘𝑦))) |
| 14 | 8, 13 | ralprg 4696 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉) → (∀𝑥 ∈ {𝑋, 𝑌}∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ (∀𝑦 ∈ (𝐴 ∖ {𝑋})(𝐹‘𝑋) ≠ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ {𝑌})(𝐹‘𝑌) ≠ (𝐹‘𝑦)))) |
| 15 | 14 | adantr 480 |
. . . . 5
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉) ∧ 𝑋 ≠ 𝑌) → (∀𝑥 ∈ {𝑋, 𝑌}∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ (∀𝑦 ∈ (𝐴 ∖ {𝑋})(𝐹‘𝑋) ≠ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ {𝑌})(𝐹‘𝑌) ≠ (𝐹‘𝑦)))) |
| 16 | 2 | difeq1i 4122 |
. . . . . . . . . . 11
⊢ (𝐴 ∖ {𝑋}) = ({𝑋, 𝑌} ∖ {𝑋}) |
| 17 | | difprsn1 4800 |
. . . . . . . . . . 11
⊢ (𝑋 ≠ 𝑌 → ({𝑋, 𝑌} ∖ {𝑋}) = {𝑌}) |
| 18 | 16, 17 | eqtrid 2789 |
. . . . . . . . . 10
⊢ (𝑋 ≠ 𝑌 → (𝐴 ∖ {𝑋}) = {𝑌}) |
| 19 | 18 | adantl 481 |
. . . . . . . . 9
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉) ∧ 𝑋 ≠ 𝑌) → (𝐴 ∖ {𝑋}) = {𝑌}) |
| 20 | 19 | raleqdv 3326 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉) ∧ 𝑋 ≠ 𝑌) → (∀𝑦 ∈ (𝐴 ∖ {𝑋})(𝐹‘𝑋) ≠ (𝐹‘𝑦) ↔ ∀𝑦 ∈ {𝑌} (𝐹‘𝑋) ≠ (𝐹‘𝑦))) |
| 21 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑌 → (𝐹‘𝑦) = (𝐹‘𝑌)) |
| 22 | 21 | neeq2d 3001 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑌 → ((𝐹‘𝑋) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑋) ≠ (𝐹‘𝑌))) |
| 23 | 22 | ralsng 4675 |
. . . . . . . . . 10
⊢ (𝑌 ∈ 𝑉 → (∀𝑦 ∈ {𝑌} (𝐹‘𝑋) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑋) ≠ (𝐹‘𝑌))) |
| 24 | 23 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉) → (∀𝑦 ∈ {𝑌} (𝐹‘𝑋) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑋) ≠ (𝐹‘𝑌))) |
| 25 | 24 | adantr 480 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉) ∧ 𝑋 ≠ 𝑌) → (∀𝑦 ∈ {𝑌} (𝐹‘𝑋) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑋) ≠ (𝐹‘𝑌))) |
| 26 | 20, 25 | bitrd 279 |
. . . . . . 7
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉) ∧ 𝑋 ≠ 𝑌) → (∀𝑦 ∈ (𝐴 ∖ {𝑋})(𝐹‘𝑋) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑋) ≠ (𝐹‘𝑌))) |
| 27 | 2 | difeq1i 4122 |
. . . . . . . . . . 11
⊢ (𝐴 ∖ {𝑌}) = ({𝑋, 𝑌} ∖ {𝑌}) |
| 28 | | difprsn2 4801 |
. . . . . . . . . . 11
⊢ (𝑋 ≠ 𝑌 → ({𝑋, 𝑌} ∖ {𝑌}) = {𝑋}) |
| 29 | 27, 28 | eqtrid 2789 |
. . . . . . . . . 10
⊢ (𝑋 ≠ 𝑌 → (𝐴 ∖ {𝑌}) = {𝑋}) |
| 30 | 29 | adantl 481 |
. . . . . . . . 9
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉) ∧ 𝑋 ≠ 𝑌) → (𝐴 ∖ {𝑌}) = {𝑋}) |
| 31 | 30 | raleqdv 3326 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉) ∧ 𝑋 ≠ 𝑌) → (∀𝑦 ∈ (𝐴 ∖ {𝑌})(𝐹‘𝑌) ≠ (𝐹‘𝑦) ↔ ∀𝑦 ∈ {𝑋} (𝐹‘𝑌) ≠ (𝐹‘𝑦))) |
| 32 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑋 → (𝐹‘𝑦) = (𝐹‘𝑋)) |
| 33 | 32 | neeq2d 3001 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑋 → ((𝐹‘𝑌) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑌) ≠ (𝐹‘𝑋))) |
| 34 | 33 | ralsng 4675 |
. . . . . . . . . 10
⊢ (𝑋 ∈ 𝑈 → (∀𝑦 ∈ {𝑋} (𝐹‘𝑌) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑌) ≠ (𝐹‘𝑋))) |
| 35 | 34 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉) → (∀𝑦 ∈ {𝑋} (𝐹‘𝑌) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑌) ≠ (𝐹‘𝑋))) |
| 36 | 35 | adantr 480 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉) ∧ 𝑋 ≠ 𝑌) → (∀𝑦 ∈ {𝑋} (𝐹‘𝑌) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑌) ≠ (𝐹‘𝑋))) |
| 37 | 31, 36 | bitrd 279 |
. . . . . . 7
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉) ∧ 𝑋 ≠ 𝑌) → (∀𝑦 ∈ (𝐴 ∖ {𝑌})(𝐹‘𝑌) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑌) ≠ (𝐹‘𝑋))) |
| 38 | 26, 37 | anbi12d 632 |
. . . . . 6
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉) ∧ 𝑋 ≠ 𝑌) → ((∀𝑦 ∈ (𝐴 ∖ {𝑋})(𝐹‘𝑋) ≠ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ {𝑌})(𝐹‘𝑌) ≠ (𝐹‘𝑦)) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑋)))) |
| 39 | | necom 2994 |
. . . . . . . 8
⊢ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ↔ (𝐹‘𝑌) ≠ (𝐹‘𝑋)) |
| 40 | 39 | biimpi 216 |
. . . . . . 7
⊢ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) → (𝐹‘𝑌) ≠ (𝐹‘𝑋)) |
| 41 | 40 | pm4.71i 559 |
. . . . . 6
⊢ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑋))) |
| 42 | 38, 41 | bitr4di 289 |
. . . . 5
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉) ∧ 𝑋 ≠ 𝑌) → ((∀𝑦 ∈ (𝐴 ∖ {𝑋})(𝐹‘𝑋) ≠ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ {𝑌})(𝐹‘𝑌) ≠ (𝐹‘𝑦)) ↔ (𝐹‘𝑋) ≠ (𝐹‘𝑌))) |
| 43 | 15, 42 | bitrd 279 |
. . . 4
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉) ∧ 𝑋 ≠ 𝑌) → (∀𝑥 ∈ {𝑋, 𝑌}∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑋) ≠ (𝐹‘𝑌))) |
| 44 | 3, 43 | bitrid 283 |
. . 3
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉) ∧ 𝑋 ≠ 𝑌) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑋) ≠ (𝐹‘𝑌))) |
| 45 | 44 | anbi2d 630 |
. 2
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉) ∧ 𝑋 ≠ 𝑌) → ((𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦)) ↔ (𝐹:𝐴⟶𝐵 ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌)))) |
| 46 | 1, 45 | bitrid 283 |
1
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉) ∧ 𝑋 ≠ 𝑌) → (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌)))) |