Step | Hyp | Ref
| Expression |
1 | | fnprb.a |
. . . . . 6
⊢ 𝐴 ∈ V |
2 | 1 | fnsnb 7038 |
. . . . 5
⊢ (𝐹 Fn {𝐴} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉}) |
3 | | dfsn2 4574 |
. . . . . 6
⊢ {𝐴} = {𝐴, 𝐴} |
4 | 3 | fneq2i 6531 |
. . . . 5
⊢ (𝐹 Fn {𝐴} ↔ 𝐹 Fn {𝐴, 𝐴}) |
5 | | dfsn2 4574 |
. . . . . 6
⊢
{〈𝐴, (𝐹‘𝐴)〉} = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐴, (𝐹‘𝐴)〉} |
6 | 5 | eqeq2i 2751 |
. . . . 5
⊢ (𝐹 = {〈𝐴, (𝐹‘𝐴)〉} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐴, (𝐹‘𝐴)〉}) |
7 | 2, 4, 6 | 3bitr3i 301 |
. . . 4
⊢ (𝐹 Fn {𝐴, 𝐴} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐴, (𝐹‘𝐴)〉}) |
8 | 7 | a1i 11 |
. . 3
⊢ (𝐴 = 𝐵 → (𝐹 Fn {𝐴, 𝐴} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐴, (𝐹‘𝐴)〉})) |
9 | | preq2 4670 |
. . . 4
⊢ (𝐴 = 𝐵 → {𝐴, 𝐴} = {𝐴, 𝐵}) |
10 | 9 | fneq2d 6527 |
. . 3
⊢ (𝐴 = 𝐵 → (𝐹 Fn {𝐴, 𝐴} ↔ 𝐹 Fn {𝐴, 𝐵})) |
11 | | id 22 |
. . . . . 6
⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵) |
12 | | fveq2 6774 |
. . . . . 6
⊢ (𝐴 = 𝐵 → (𝐹‘𝐴) = (𝐹‘𝐵)) |
13 | 11, 12 | opeq12d 4812 |
. . . . 5
⊢ (𝐴 = 𝐵 → 〈𝐴, (𝐹‘𝐴)〉 = 〈𝐵, (𝐹‘𝐵)〉) |
14 | 13 | preq2d 4676 |
. . . 4
⊢ (𝐴 = 𝐵 → {〈𝐴, (𝐹‘𝐴)〉, 〈𝐴, (𝐹‘𝐴)〉} = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}) |
15 | 14 | eqeq2d 2749 |
. . 3
⊢ (𝐴 = 𝐵 → (𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐴, (𝐹‘𝐴)〉} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉})) |
16 | 8, 10, 15 | 3bitr3d 309 |
. 2
⊢ (𝐴 = 𝐵 → (𝐹 Fn {𝐴, 𝐵} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉})) |
17 | | fndm 6536 |
. . . . . 6
⊢ (𝐹 Fn {𝐴, 𝐵} → dom 𝐹 = {𝐴, 𝐵}) |
18 | | fvex 6787 |
. . . . . . 7
⊢ (𝐹‘𝐴) ∈ V |
19 | | fvex 6787 |
. . . . . . 7
⊢ (𝐹‘𝐵) ∈ V |
20 | 18, 19 | dmprop 6120 |
. . . . . 6
⊢ dom
{〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} = {𝐴, 𝐵} |
21 | 17, 20 | eqtr4di 2796 |
. . . . 5
⊢ (𝐹 Fn {𝐴, 𝐵} → dom 𝐹 = dom {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}) |
22 | 21 | adantl 482 |
. . . 4
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → dom 𝐹 = dom {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}) |
23 | 17 | adantl 482 |
. . . . . . 7
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → dom 𝐹 = {𝐴, 𝐵}) |
24 | 23 | eleq2d 2824 |
. . . . . 6
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → (𝑥 ∈ dom 𝐹 ↔ 𝑥 ∈ {𝐴, 𝐵})) |
25 | | vex 3436 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
26 | 25 | elpr 4584 |
. . . . . . 7
⊢ (𝑥 ∈ {𝐴, 𝐵} ↔ (𝑥 = 𝐴 ∨ 𝑥 = 𝐵)) |
27 | 1, 18 | fvpr1 7065 |
. . . . . . . . . . 11
⊢ (𝐴 ≠ 𝐵 → ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐴) = (𝐹‘𝐴)) |
28 | 27 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐴) = (𝐹‘𝐴)) |
29 | 28 | eqcomd 2744 |
. . . . . . . . 9
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → (𝐹‘𝐴) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐴)) |
30 | | fveq2 6774 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → (𝐹‘𝑥) = (𝐹‘𝐴)) |
31 | | fveq2 6774 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐴)) |
32 | 30, 31 | eqeq12d 2754 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → ((𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥) ↔ (𝐹‘𝐴) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐴))) |
33 | 29, 32 | syl5ibrcom 246 |
. . . . . . . 8
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → (𝑥 = 𝐴 → (𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥))) |
34 | | fnprb.b |
. . . . . . . . . . . 12
⊢ 𝐵 ∈ V |
35 | 34, 19 | fvpr2 7067 |
. . . . . . . . . . 11
⊢ (𝐴 ≠ 𝐵 → ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐵) = (𝐹‘𝐵)) |
36 | 35 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐵) = (𝐹‘𝐵)) |
37 | 36 | eqcomd 2744 |
. . . . . . . . 9
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → (𝐹‘𝐵) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐵)) |
38 | | fveq2 6774 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐵 → (𝐹‘𝑥) = (𝐹‘𝐵)) |
39 | | fveq2 6774 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐵 → ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐵)) |
40 | 38, 39 | eqeq12d 2754 |
. . . . . . . . 9
⊢ (𝑥 = 𝐵 → ((𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥) ↔ (𝐹‘𝐵) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐵))) |
41 | 37, 40 | syl5ibrcom 246 |
. . . . . . . 8
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → (𝑥 = 𝐵 → (𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥))) |
42 | 33, 41 | jaod 856 |
. . . . . . 7
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → ((𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → (𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥))) |
43 | 26, 42 | syl5bi 241 |
. . . . . 6
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → (𝑥 ∈ {𝐴, 𝐵} → (𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥))) |
44 | 24, 43 | sylbid 239 |
. . . . 5
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → (𝑥 ∈ dom 𝐹 → (𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥))) |
45 | 44 | ralrimiv 3102 |
. . . 4
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → ∀𝑥 ∈ dom 𝐹(𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥)) |
46 | | fnfun 6533 |
. . . . 5
⊢ (𝐹 Fn {𝐴, 𝐵} → Fun 𝐹) |
47 | 1, 34, 18, 19 | funpr 6490 |
. . . . 5
⊢ (𝐴 ≠ 𝐵 → Fun {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}) |
48 | | eqfunfv 6914 |
. . . . 5
⊢ ((Fun
𝐹 ∧ Fun {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}) → (𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} ↔ (dom 𝐹 = dom {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} ∧ ∀𝑥 ∈ dom 𝐹(𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥)))) |
49 | 46, 47, 48 | syl2anr 597 |
. . . 4
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → (𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} ↔ (dom 𝐹 = dom {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} ∧ ∀𝑥 ∈ dom 𝐹(𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥)))) |
50 | 22, 45, 49 | mpbir2and 710 |
. . 3
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 Fn {𝐴, 𝐵}) → 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}) |
51 | | df-fn 6436 |
. . . . 5
⊢
({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} Fn {𝐴, 𝐵} ↔ (Fun {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} ∧ dom {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} = {𝐴, 𝐵})) |
52 | 47, 20, 51 | sylanblrc 590 |
. . . 4
⊢ (𝐴 ≠ 𝐵 → {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} Fn {𝐴, 𝐵}) |
53 | | fneq1 6524 |
. . . . 5
⊢ (𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} → (𝐹 Fn {𝐴, 𝐵} ↔ {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} Fn {𝐴, 𝐵})) |
54 | 53 | biimprd 247 |
. . . 4
⊢ (𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} → ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} Fn {𝐴, 𝐵} → 𝐹 Fn {𝐴, 𝐵})) |
55 | 52, 54 | mpan9 507 |
. . 3
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}) → 𝐹 Fn {𝐴, 𝐵}) |
56 | 50, 55 | impbida 798 |
. 2
⊢ (𝐴 ≠ 𝐵 → (𝐹 Fn {𝐴, 𝐵} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉})) |
57 | 16, 56 | pm2.61ine 3028 |
1
⊢ (𝐹 Fn {𝐴, 𝐵} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}) |