Step | Hyp | Ref
| Expression |
1 | | fnprb.a |
. . . . . 6
⊢ 𝐴 ∈ V |
2 | 1 | fnsnb 6751 |
. . . . 5
⊢ (𝐹 Fn {𝐴} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉}) |
3 | | dfsn2 4454 |
. . . . . 6
⊢ {𝐴} = {𝐴, 𝐴} |
4 | 3 | fneq2i 6284 |
. . . . 5
⊢ (𝐹 Fn {𝐴} ↔ 𝐹 Fn {𝐴, 𝐴}) |
5 | | dfsn2 4454 |
. . . . . 6
⊢
{〈𝐴, (𝐹‘𝐴)〉} = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐴, (𝐹‘𝐴)〉} |
6 | 5 | eqeq2i 2790 |
. . . . 5
⊢ (𝐹 = {〈𝐴, (𝐹‘𝐴)〉} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐴, (𝐹‘𝐴)〉}) |
7 | 2, 4, 6 | 3bitr3i 293 |
. . . 4
⊢ (𝐹 Fn {𝐴, 𝐴} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐴, (𝐹‘𝐴)〉}) |
8 | 7 | a1i 11 |
. . 3
⊢ (𝐴 = 𝐵 → (𝐹 Fn {𝐴, 𝐴} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐴, (𝐹‘𝐴)〉})) |
9 | | preq2 4544 |
. . . 4
⊢ (𝐴 = 𝐵 → {𝐴, 𝐴} = {𝐴, 𝐵}) |
10 | 9 | fneq2d 6280 |
. . 3
⊢ (𝐴 = 𝐵 → (𝐹 Fn {𝐴, 𝐴} ↔ 𝐹 Fn {𝐴, 𝐵})) |
11 | | id 22 |
. . . . . 6
⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵) |
12 | | fveq2 6499 |
. . . . . 6
⊢ (𝐴 = 𝐵 → (𝐹‘𝐴) = (𝐹‘𝐵)) |
13 | 11, 12 | opeq12d 4685 |
. . . . 5
⊢ (𝐴 = 𝐵 → 〈𝐴, (𝐹‘𝐴)〉 = 〈𝐵, (𝐹‘𝐵)〉) |
14 | 13 | preq2d 4550 |
. . . 4
⊢ (𝐴 = 𝐵 → {〈𝐴, (𝐹‘𝐴)〉, 〈𝐴, (𝐹‘𝐴)〉} = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}) |
15 | 14 | eqeq2d 2788 |
. . 3
⊢ (𝐴 = 𝐵 → (𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐴, (𝐹‘𝐴)〉} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉})) |
16 | 8, 10, 15 | 3bitr3d 301 |
. 2
⊢ (𝐴 = 𝐵 → (𝐹 Fn {𝐴, 𝐵} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉})) |
17 | | fndm 6288 |
. . . . . 6
⊢ (𝐹 Fn {𝐴, 𝐵} → dom 𝐹 = {𝐴, 𝐵}) |
18 | | fvex 6512 |
. . . . . . 7
⊢ (𝐹‘𝐴) ∈ V |
19 | | fvex 6512 |
. . . . . . 7
⊢ (𝐹‘𝐵) ∈ V |
20 | 18, 19 | dmprop 5913 |
. . . . . 6
⊢ dom
{〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} = {𝐴, 𝐵} |
21 | 17, 20 | syl6eqr 2832 |
. . . . 5
⊢ (𝐹 Fn {𝐴, 𝐵} → dom 𝐹 = dom {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}) |
22 | 21 | adantl 474 |
. . . 4
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → dom 𝐹 = dom {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}) |
23 | 17 | adantl 474 |
. . . . . . 7
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → dom 𝐹 = {𝐴, 𝐵}) |
24 | 23 | eleq2d 2851 |
. . . . . 6
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → (𝑥 ∈ dom 𝐹 ↔ 𝑥 ∈ {𝐴, 𝐵})) |
25 | | vex 3418 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
26 | 25 | elpr 4464 |
. . . . . . 7
⊢ (𝑥 ∈ {𝐴, 𝐵} ↔ (𝑥 = 𝐴 ∨ 𝑥 = 𝐵)) |
27 | 1, 18 | fvpr1 6779 |
. . . . . . . . . . 11
⊢ (𝐴 ≠ 𝐵 → ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐴) = (𝐹‘𝐴)) |
28 | 27 | adantr 473 |
. . . . . . . . . 10
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐴) = (𝐹‘𝐴)) |
29 | 28 | eqcomd 2784 |
. . . . . . . . 9
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → (𝐹‘𝐴) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐴)) |
30 | | fveq2 6499 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → (𝐹‘𝑥) = (𝐹‘𝐴)) |
31 | | fveq2 6499 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐴)) |
32 | 30, 31 | eqeq12d 2793 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → ((𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥) ↔ (𝐹‘𝐴) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐴))) |
33 | 29, 32 | syl5ibrcom 239 |
. . . . . . . 8
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → (𝑥 = 𝐴 → (𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥))) |
34 | | fnprb.b |
. . . . . . . . . . . 12
⊢ 𝐵 ∈ V |
35 | 34, 19 | fvpr2 6780 |
. . . . . . . . . . 11
⊢ (𝐴 ≠ 𝐵 → ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐵) = (𝐹‘𝐵)) |
36 | 35 | adantr 473 |
. . . . . . . . . 10
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐵) = (𝐹‘𝐵)) |
37 | 36 | eqcomd 2784 |
. . . . . . . . 9
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → (𝐹‘𝐵) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐵)) |
38 | | fveq2 6499 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐵 → (𝐹‘𝑥) = (𝐹‘𝐵)) |
39 | | fveq2 6499 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐵 → ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐵)) |
40 | 38, 39 | eqeq12d 2793 |
. . . . . . . . 9
⊢ (𝑥 = 𝐵 → ((𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥) ↔ (𝐹‘𝐵) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐵))) |
41 | 37, 40 | syl5ibrcom 239 |
. . . . . . . 8
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → (𝑥 = 𝐵 → (𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥))) |
42 | 33, 41 | jaod 845 |
. . . . . . 7
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → ((𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → (𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥))) |
43 | 26, 42 | syl5bi 234 |
. . . . . 6
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → (𝑥 ∈ {𝐴, 𝐵} → (𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥))) |
44 | 24, 43 | sylbid 232 |
. . . . 5
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → (𝑥 ∈ dom 𝐹 → (𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥))) |
45 | 44 | ralrimiv 3131 |
. . . 4
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → ∀𝑥 ∈ dom 𝐹(𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥)) |
46 | | fnfun 6286 |
. . . . 5
⊢ (𝐹 Fn {𝐴, 𝐵} → Fun 𝐹) |
47 | 1, 34, 18, 19 | funpr 6243 |
. . . . 5
⊢ (𝐴 ≠ 𝐵 → Fun {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}) |
48 | | eqfunfv 6632 |
. . . . 5
⊢ ((Fun
𝐹 ∧ Fun {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}) → (𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} ↔ (dom 𝐹 = dom {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} ∧ ∀𝑥 ∈ dom 𝐹(𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥)))) |
49 | 46, 47, 48 | syl2anr 587 |
. . . 4
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → (𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} ↔ (dom 𝐹 = dom {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} ∧ ∀𝑥 ∈ dom 𝐹(𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥)))) |
50 | 22, 45, 49 | mpbir2and 700 |
. . 3
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}) |
51 | | df-fn 6191 |
. . . . 5
⊢
({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} Fn {𝐴, 𝐵} ↔ (Fun {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} ∧ dom {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} = {𝐴, 𝐵})) |
52 | 47, 20, 51 | sylanblrc 581 |
. . . 4
⊢ (𝐴 ≠ 𝐵 → {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} Fn {𝐴, 𝐵}) |
53 | | fneq1 6277 |
. . . . 5
⊢ (𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} → (𝐹 Fn {𝐴, 𝐵} ↔ {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} Fn {𝐴, 𝐵})) |
54 | 53 | biimprd 240 |
. . . 4
⊢ (𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} → ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} Fn {𝐴, 𝐵} → 𝐹 Fn {𝐴, 𝐵})) |
55 | 52, 54 | mpan9 499 |
. . 3
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}) → 𝐹 Fn {𝐴, 𝐵}) |
56 | 50, 55 | impbida 788 |
. 2
⊢ (𝐴 ≠ 𝐵 → (𝐹 Fn {𝐴, 𝐵} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉})) |
57 | 16, 56 | pm2.61ine 3051 |
1
⊢ (𝐹 Fn {𝐴, 𝐵} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}) |