Step | Hyp | Ref
| Expression |
1 | | opeq1 3549 |
. . . . 5
⊢ (𝑢 = 𝐴 → 〈𝑢, 𝑡〉 = 〈𝐴, 𝑡〉) |
2 | 1 | funeqd 4923 |
. . . 4
⊢ (𝑢 = 𝐴 → (Fun 〈𝑢, 𝑡〉 ↔ Fun 〈𝐴, 𝑡〉)) |
3 | | eqeq1 2046 |
. . . 4
⊢ (𝑢 = 𝐴 → (𝑢 = 𝑡 ↔ 𝐴 = 𝑡)) |
4 | 2, 3 | imbi12d 223 |
. . 3
⊢ (𝑢 = 𝐴 → ((Fun 〈𝑢, 𝑡〉 → 𝑢 = 𝑡) ↔ (Fun 〈𝐴, 𝑡〉 → 𝐴 = 𝑡))) |
5 | | opeq2 3550 |
. . . . 5
⊢ (𝑡 = 𝐵 → 〈𝐴, 𝑡〉 = 〈𝐴, 𝐵〉) |
6 | 5 | funeqd 4923 |
. . . 4
⊢ (𝑡 = 𝐵 → (Fun 〈𝐴, 𝑡〉 ↔ Fun 〈𝐴, 𝐵〉)) |
7 | | eqeq2 2049 |
. . . 4
⊢ (𝑡 = 𝐵 → (𝐴 = 𝑡 ↔ 𝐴 = 𝐵)) |
8 | 6, 7 | imbi12d 223 |
. . 3
⊢ (𝑡 = 𝐵 → ((Fun 〈𝐴, 𝑡〉 → 𝐴 = 𝑡) ↔ (Fun 〈𝐴, 𝐵〉 → 𝐴 = 𝐵))) |
9 | | funrel 4919 |
. . . . 5
⊢ (Fun
〈𝑢, 𝑡〉 → Rel 〈𝑢, 𝑡〉) |
10 | | vex 2560 |
. . . . . 6
⊢ 𝑢 ∈ V |
11 | | vex 2560 |
. . . . . 6
⊢ 𝑡 ∈ V |
12 | 10, 11 | relop 4486 |
. . . . 5
⊢ (Rel
〈𝑢, 𝑡〉 ↔ ∃𝑥∃𝑦(𝑢 = {𝑥} ∧ 𝑡 = {𝑥, 𝑦})) |
13 | 9, 12 | sylib 127 |
. . . 4
⊢ (Fun
〈𝑢, 𝑡〉 → ∃𝑥∃𝑦(𝑢 = {𝑥} ∧ 𝑡 = {𝑥, 𝑦})) |
14 | 10, 11 | opth 3974 |
. . . . . . . 8
⊢
(〈𝑢, 𝑡〉 = 〈{𝑥}, {𝑥, 𝑦}〉 ↔ (𝑢 = {𝑥} ∧ 𝑡 = {𝑥, 𝑦})) |
15 | | vex 2560 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
16 | 15 | opid 3567 |
. . . . . . . . . . 11
⊢
〈𝑥, 𝑥〉 = {{𝑥}} |
17 | 16 | preq1i 3450 |
. . . . . . . . . 10
⊢
{〈𝑥, 𝑥〉, {{𝑥}, {𝑥, 𝑦}}} = {{{𝑥}}, {{𝑥}, {𝑥, 𝑦}}} |
18 | | vex 2560 |
. . . . . . . . . . . 12
⊢ 𝑦 ∈ V |
19 | 15, 18 | dfop 3548 |
. . . . . . . . . . 11
⊢
〈𝑥, 𝑦〉 = {{𝑥}, {𝑥, 𝑦}} |
20 | 19 | preq2i 3451 |
. . . . . . . . . 10
⊢
{〈𝑥, 𝑥〉, 〈𝑥, 𝑦〉} = {〈𝑥, 𝑥〉, {{𝑥}, {𝑥, 𝑦}}} |
21 | | snexgOLD 3935 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ V → {𝑥} ∈ V) |
22 | 15, 21 | ax-mp 7 |
. . . . . . . . . . 11
⊢ {𝑥} ∈ V |
23 | | zfpair2 3945 |
. . . . . . . . . . 11
⊢ {𝑥, 𝑦} ∈ V |
24 | 22, 23 | dfop 3548 |
. . . . . . . . . 10
⊢
〈{𝑥}, {𝑥, 𝑦}〉 = {{{𝑥}}, {{𝑥}, {𝑥, 𝑦}}} |
25 | 17, 20, 24 | 3eqtr4ri 2071 |
. . . . . . . . 9
⊢
〈{𝑥}, {𝑥, 𝑦}〉 = {〈𝑥, 𝑥〉, 〈𝑥, 𝑦〉} |
26 | 25 | eqeq2i 2050 |
. . . . . . . 8
⊢
(〈𝑢, 𝑡〉 = 〈{𝑥}, {𝑥, 𝑦}〉 ↔ 〈𝑢, 𝑡〉 = {〈𝑥, 𝑥〉, 〈𝑥, 𝑦〉}) |
27 | 14, 26 | bitr3i 175 |
. . . . . . 7
⊢ ((𝑢 = {𝑥} ∧ 𝑡 = {𝑥, 𝑦}) ↔ 〈𝑢, 𝑡〉 = {〈𝑥, 𝑥〉, 〈𝑥, 𝑦〉}) |
28 | | dffun4 4913 |
. . . . . . . . 9
⊢ (Fun
〈𝑢, 𝑡〉 ↔ (Rel 〈𝑢, 𝑡〉 ∧ ∀𝑧∀𝑤∀𝑣((〈𝑧, 𝑤〉 ∈ 〈𝑢, 𝑡〉 ∧ 〈𝑧, 𝑣〉 ∈ 〈𝑢, 𝑡〉) → 𝑤 = 𝑣))) |
29 | 28 | simprbi 260 |
. . . . . . . 8
⊢ (Fun
〈𝑢, 𝑡〉 → ∀𝑧∀𝑤∀𝑣((〈𝑧, 𝑤〉 ∈ 〈𝑢, 𝑡〉 ∧ 〈𝑧, 𝑣〉 ∈ 〈𝑢, 𝑡〉) → 𝑤 = 𝑣)) |
30 | 15, 15 | opex 3966 |
. . . . . . . . . . 11
⊢
〈𝑥, 𝑥〉 ∈ V |
31 | 30 | prid1 3476 |
. . . . . . . . . 10
⊢
〈𝑥, 𝑥〉 ∈ {〈𝑥, 𝑥〉, 〈𝑥, 𝑦〉} |
32 | | eleq2 2101 |
. . . . . . . . . 10
⊢
(〈𝑢, 𝑡〉 = {〈𝑥, 𝑥〉, 〈𝑥, 𝑦〉} → (〈𝑥, 𝑥〉 ∈ 〈𝑢, 𝑡〉 ↔ 〈𝑥, 𝑥〉 ∈ {〈𝑥, 𝑥〉, 〈𝑥, 𝑦〉})) |
33 | 31, 32 | mpbiri 157 |
. . . . . . . . 9
⊢
(〈𝑢, 𝑡〉 = {〈𝑥, 𝑥〉, 〈𝑥, 𝑦〉} → 〈𝑥, 𝑥〉 ∈ 〈𝑢, 𝑡〉) |
34 | 15, 18 | opex 3966 |
. . . . . . . . . . 11
⊢
〈𝑥, 𝑦〉 ∈ V |
35 | 34 | prid2 3477 |
. . . . . . . . . 10
⊢
〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑥〉, 〈𝑥, 𝑦〉} |
36 | | eleq2 2101 |
. . . . . . . . . 10
⊢
(〈𝑢, 𝑡〉 = {〈𝑥, 𝑥〉, 〈𝑥, 𝑦〉} → (〈𝑥, 𝑦〉 ∈ 〈𝑢, 𝑡〉 ↔ 〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑥〉, 〈𝑥, 𝑦〉})) |
37 | 35, 36 | mpbiri 157 |
. . . . . . . . 9
⊢
(〈𝑢, 𝑡〉 = {〈𝑥, 𝑥〉, 〈𝑥, 𝑦〉} → 〈𝑥, 𝑦〉 ∈ 〈𝑢, 𝑡〉) |
38 | 33, 37 | jca 290 |
. . . . . . . 8
⊢
(〈𝑢, 𝑡〉 = {〈𝑥, 𝑥〉, 〈𝑥, 𝑦〉} → (〈𝑥, 𝑥〉 ∈ 〈𝑢, 𝑡〉 ∧ 〈𝑥, 𝑦〉 ∈ 〈𝑢, 𝑡〉)) |
39 | | opeq12 3551 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑥) → 〈𝑧, 𝑤〉 = 〈𝑥, 𝑥〉) |
40 | 39 | 3adant3 924 |
. . . . . . . . . . . . 13
⊢ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑥 ∧ 𝑣 = 𝑦) → 〈𝑧, 𝑤〉 = 〈𝑥, 𝑥〉) |
41 | 40 | eleq1d 2106 |
. . . . . . . . . . . 12
⊢ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑥 ∧ 𝑣 = 𝑦) → (〈𝑧, 𝑤〉 ∈ 〈𝑢, 𝑡〉 ↔ 〈𝑥, 𝑥〉 ∈ 〈𝑢, 𝑡〉)) |
42 | | opeq12 3551 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 = 𝑥 ∧ 𝑣 = 𝑦) → 〈𝑧, 𝑣〉 = 〈𝑥, 𝑦〉) |
43 | 42 | 3adant2 923 |
. . . . . . . . . . . . 13
⊢ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑥 ∧ 𝑣 = 𝑦) → 〈𝑧, 𝑣〉 = 〈𝑥, 𝑦〉) |
44 | 43 | eleq1d 2106 |
. . . . . . . . . . . 12
⊢ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑥 ∧ 𝑣 = 𝑦) → (〈𝑧, 𝑣〉 ∈ 〈𝑢, 𝑡〉 ↔ 〈𝑥, 𝑦〉 ∈ 〈𝑢, 𝑡〉)) |
45 | 41, 44 | anbi12d 442 |
. . . . . . . . . . 11
⊢ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑥 ∧ 𝑣 = 𝑦) → ((〈𝑧, 𝑤〉 ∈ 〈𝑢, 𝑡〉 ∧ 〈𝑧, 𝑣〉 ∈ 〈𝑢, 𝑡〉) ↔ (〈𝑥, 𝑥〉 ∈ 〈𝑢, 𝑡〉 ∧ 〈𝑥, 𝑦〉 ∈ 〈𝑢, 𝑡〉))) |
46 | | eqeq12 2052 |
. . . . . . . . . . . 12
⊢ ((𝑤 = 𝑥 ∧ 𝑣 = 𝑦) → (𝑤 = 𝑣 ↔ 𝑥 = 𝑦)) |
47 | 46 | 3adant1 922 |
. . . . . . . . . . 11
⊢ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑥 ∧ 𝑣 = 𝑦) → (𝑤 = 𝑣 ↔ 𝑥 = 𝑦)) |
48 | 45, 47 | imbi12d 223 |
. . . . . . . . . 10
⊢ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑥 ∧ 𝑣 = 𝑦) → (((〈𝑧, 𝑤〉 ∈ 〈𝑢, 𝑡〉 ∧ 〈𝑧, 𝑣〉 ∈ 〈𝑢, 𝑡〉) → 𝑤 = 𝑣) ↔ ((〈𝑥, 𝑥〉 ∈ 〈𝑢, 𝑡〉 ∧ 〈𝑥, 𝑦〉 ∈ 〈𝑢, 𝑡〉) → 𝑥 = 𝑦))) |
49 | 48 | spc3gv 2645 |
. . . . . . . . 9
⊢ ((𝑥 ∈ V ∧ 𝑥 ∈ V ∧ 𝑦 ∈ V) → (∀𝑧∀𝑤∀𝑣((〈𝑧, 𝑤〉 ∈ 〈𝑢, 𝑡〉 ∧ 〈𝑧, 𝑣〉 ∈ 〈𝑢, 𝑡〉) → 𝑤 = 𝑣) → ((〈𝑥, 𝑥〉 ∈ 〈𝑢, 𝑡〉 ∧ 〈𝑥, 𝑦〉 ∈ 〈𝑢, 𝑡〉) → 𝑥 = 𝑦))) |
50 | 15, 15, 18, 49 | mp3an 1232 |
. . . . . . . 8
⊢
(∀𝑧∀𝑤∀𝑣((〈𝑧, 𝑤〉 ∈ 〈𝑢, 𝑡〉 ∧ 〈𝑧, 𝑣〉 ∈ 〈𝑢, 𝑡〉) → 𝑤 = 𝑣) → ((〈𝑥, 𝑥〉 ∈ 〈𝑢, 𝑡〉 ∧ 〈𝑥, 𝑦〉 ∈ 〈𝑢, 𝑡〉) → 𝑥 = 𝑦)) |
51 | 29, 38, 50 | syl2im 34 |
. . . . . . 7
⊢ (Fun
〈𝑢, 𝑡〉 → (〈𝑢, 𝑡〉 = {〈𝑥, 𝑥〉, 〈𝑥, 𝑦〉} → 𝑥 = 𝑦)) |
52 | 27, 51 | syl5bi 141 |
. . . . . 6
⊢ (Fun
〈𝑢, 𝑡〉 → ((𝑢 = {𝑥} ∧ 𝑡 = {𝑥, 𝑦}) → 𝑥 = 𝑦)) |
53 | | dfsn2 3389 |
. . . . . . . . . . 11
⊢ {𝑥} = {𝑥, 𝑥} |
54 | | preq2 3448 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → {𝑥, 𝑥} = {𝑥, 𝑦}) |
55 | 53, 54 | syl5req 2085 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → {𝑥, 𝑦} = {𝑥}) |
56 | 55 | eqeq2d 2051 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑡 = {𝑥, 𝑦} ↔ 𝑡 = {𝑥})) |
57 | | eqtr3 2059 |
. . . . . . . . . 10
⊢ ((𝑢 = {𝑥} ∧ 𝑡 = {𝑥}) → 𝑢 = 𝑡) |
58 | 57 | expcom 109 |
. . . . . . . . 9
⊢ (𝑡 = {𝑥} → (𝑢 = {𝑥} → 𝑢 = 𝑡)) |
59 | 56, 58 | syl6bi 152 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑡 = {𝑥, 𝑦} → (𝑢 = {𝑥} → 𝑢 = 𝑡))) |
60 | 59 | com13 74 |
. . . . . . 7
⊢ (𝑢 = {𝑥} → (𝑡 = {𝑥, 𝑦} → (𝑥 = 𝑦 → 𝑢 = 𝑡))) |
61 | 60 | imp 115 |
. . . . . 6
⊢ ((𝑢 = {𝑥} ∧ 𝑡 = {𝑥, 𝑦}) → (𝑥 = 𝑦 → 𝑢 = 𝑡)) |
62 | 52, 61 | sylcom 25 |
. . . . 5
⊢ (Fun
〈𝑢, 𝑡〉 → ((𝑢 = {𝑥} ∧ 𝑡 = {𝑥, 𝑦}) → 𝑢 = 𝑡)) |
63 | 62 | exlimdvv 1777 |
. . . 4
⊢ (Fun
〈𝑢, 𝑡〉 → (∃𝑥∃𝑦(𝑢 = {𝑥} ∧ 𝑡 = {𝑥, 𝑦}) → 𝑢 = 𝑡)) |
64 | 13, 63 | mpd 13 |
. . 3
⊢ (Fun
〈𝑢, 𝑡〉 → 𝑢 = 𝑡) |
65 | 4, 8, 64 | vtocl2g 2617 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (Fun 〈𝐴, 𝐵〉 → 𝐴 = 𝐵)) |
66 | 65 | 3impia 1101 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ Fun 〈𝐴, 𝐵〉) → 𝐴 = 𝐵) |