Step | Hyp | Ref
| Expression |
1 | | opeq1 3763 |
. . . . 5
⊢ (𝑢 = 𝐴 → 〈𝑢, 𝑡〉 = 〈𝐴, 𝑡〉) |
2 | 1 | funeqd 5218 |
. . . 4
⊢ (𝑢 = 𝐴 → (Fun 〈𝑢, 𝑡〉 ↔ Fun 〈𝐴, 𝑡〉)) |
3 | | eqeq1 2177 |
. . . 4
⊢ (𝑢 = 𝐴 → (𝑢 = 𝑡 ↔ 𝐴 = 𝑡)) |
4 | 2, 3 | imbi12d 233 |
. . 3
⊢ (𝑢 = 𝐴 → ((Fun 〈𝑢, 𝑡〉 → 𝑢 = 𝑡) ↔ (Fun 〈𝐴, 𝑡〉 → 𝐴 = 𝑡))) |
5 | | opeq2 3764 |
. . . . 5
⊢ (𝑡 = 𝐵 → 〈𝐴, 𝑡〉 = 〈𝐴, 𝐵〉) |
6 | 5 | funeqd 5218 |
. . . 4
⊢ (𝑡 = 𝐵 → (Fun 〈𝐴, 𝑡〉 ↔ Fun 〈𝐴, 𝐵〉)) |
7 | | eqeq2 2180 |
. . . 4
⊢ (𝑡 = 𝐵 → (𝐴 = 𝑡 ↔ 𝐴 = 𝐵)) |
8 | 6, 7 | imbi12d 233 |
. . 3
⊢ (𝑡 = 𝐵 → ((Fun 〈𝐴, 𝑡〉 → 𝐴 = 𝑡) ↔ (Fun 〈𝐴, 𝐵〉 → 𝐴 = 𝐵))) |
9 | | funrel 5213 |
. . . . 5
⊢ (Fun
〈𝑢, 𝑡〉 → Rel 〈𝑢, 𝑡〉) |
10 | | vex 2733 |
. . . . . 6
⊢ 𝑢 ∈ V |
11 | | vex 2733 |
. . . . . 6
⊢ 𝑡 ∈ V |
12 | 10, 11 | relop 4759 |
. . . . 5
⊢ (Rel
〈𝑢, 𝑡〉 ↔ ∃𝑥∃𝑦(𝑢 = {𝑥} ∧ 𝑡 = {𝑥, 𝑦})) |
13 | 9, 12 | sylib 121 |
. . . 4
⊢ (Fun
〈𝑢, 𝑡〉 → ∃𝑥∃𝑦(𝑢 = {𝑥} ∧ 𝑡 = {𝑥, 𝑦})) |
14 | 10, 11 | opth 4220 |
. . . . . . . 8
⊢
(〈𝑢, 𝑡〉 = 〈{𝑥}, {𝑥, 𝑦}〉 ↔ (𝑢 = {𝑥} ∧ 𝑡 = {𝑥, 𝑦})) |
15 | | vex 2733 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
16 | 15 | opid 3781 |
. . . . . . . . . . 11
⊢
〈𝑥, 𝑥〉 = {{𝑥}} |
17 | 16 | preq1i 3661 |
. . . . . . . . . 10
⊢
{〈𝑥, 𝑥〉, {{𝑥}, {𝑥, 𝑦}}} = {{{𝑥}}, {{𝑥}, {𝑥, 𝑦}}} |
18 | | vex 2733 |
. . . . . . . . . . . 12
⊢ 𝑦 ∈ V |
19 | 15, 18 | dfop 3762 |
. . . . . . . . . . 11
⊢
〈𝑥, 𝑦〉 = {{𝑥}, {𝑥, 𝑦}} |
20 | 19 | preq2i 3662 |
. . . . . . . . . 10
⊢
{〈𝑥, 𝑥〉, 〈𝑥, 𝑦〉} = {〈𝑥, 𝑥〉, {{𝑥}, {𝑥, 𝑦}}} |
21 | 15 | snex 4169 |
. . . . . . . . . . 11
⊢ {𝑥} ∈ V |
22 | | zfpair2 4193 |
. . . . . . . . . . 11
⊢ {𝑥, 𝑦} ∈ V |
23 | 21, 22 | dfop 3762 |
. . . . . . . . . 10
⊢
〈{𝑥}, {𝑥, 𝑦}〉 = {{{𝑥}}, {{𝑥}, {𝑥, 𝑦}}} |
24 | 17, 20, 23 | 3eqtr4ri 2202 |
. . . . . . . . 9
⊢
〈{𝑥}, {𝑥, 𝑦}〉 = {〈𝑥, 𝑥〉, 〈𝑥, 𝑦〉} |
25 | 24 | eqeq2i 2181 |
. . . . . . . 8
⊢
(〈𝑢, 𝑡〉 = 〈{𝑥}, {𝑥, 𝑦}〉 ↔ 〈𝑢, 𝑡〉 = {〈𝑥, 𝑥〉, 〈𝑥, 𝑦〉}) |
26 | 14, 25 | bitr3i 185 |
. . . . . . 7
⊢ ((𝑢 = {𝑥} ∧ 𝑡 = {𝑥, 𝑦}) ↔ 〈𝑢, 𝑡〉 = {〈𝑥, 𝑥〉, 〈𝑥, 𝑦〉}) |
27 | | dffun4 5207 |
. . . . . . . . 9
⊢ (Fun
〈𝑢, 𝑡〉 ↔ (Rel 〈𝑢, 𝑡〉 ∧ ∀𝑧∀𝑤∀𝑣((〈𝑧, 𝑤〉 ∈ 〈𝑢, 𝑡〉 ∧ 〈𝑧, 𝑣〉 ∈ 〈𝑢, 𝑡〉) → 𝑤 = 𝑣))) |
28 | 27 | simprbi 273 |
. . . . . . . 8
⊢ (Fun
〈𝑢, 𝑡〉 → ∀𝑧∀𝑤∀𝑣((〈𝑧, 𝑤〉 ∈ 〈𝑢, 𝑡〉 ∧ 〈𝑧, 𝑣〉 ∈ 〈𝑢, 𝑡〉) → 𝑤 = 𝑣)) |
29 | 15, 15 | opex 4212 |
. . . . . . . . . . 11
⊢
〈𝑥, 𝑥〉 ∈ V |
30 | 29 | prid1 3687 |
. . . . . . . . . 10
⊢
〈𝑥, 𝑥〉 ∈ {〈𝑥, 𝑥〉, 〈𝑥, 𝑦〉} |
31 | | eleq2 2234 |
. . . . . . . . . 10
⊢
(〈𝑢, 𝑡〉 = {〈𝑥, 𝑥〉, 〈𝑥, 𝑦〉} → (〈𝑥, 𝑥〉 ∈ 〈𝑢, 𝑡〉 ↔ 〈𝑥, 𝑥〉 ∈ {〈𝑥, 𝑥〉, 〈𝑥, 𝑦〉})) |
32 | 30, 31 | mpbiri 167 |
. . . . . . . . 9
⊢
(〈𝑢, 𝑡〉 = {〈𝑥, 𝑥〉, 〈𝑥, 𝑦〉} → 〈𝑥, 𝑥〉 ∈ 〈𝑢, 𝑡〉) |
33 | 15, 18 | opex 4212 |
. . . . . . . . . . 11
⊢
〈𝑥, 𝑦〉 ∈ V |
34 | 33 | prid2 3688 |
. . . . . . . . . 10
⊢
〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑥〉, 〈𝑥, 𝑦〉} |
35 | | eleq2 2234 |
. . . . . . . . . 10
⊢
(〈𝑢, 𝑡〉 = {〈𝑥, 𝑥〉, 〈𝑥, 𝑦〉} → (〈𝑥, 𝑦〉 ∈ 〈𝑢, 𝑡〉 ↔ 〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑥〉, 〈𝑥, 𝑦〉})) |
36 | 34, 35 | mpbiri 167 |
. . . . . . . . 9
⊢
(〈𝑢, 𝑡〉 = {〈𝑥, 𝑥〉, 〈𝑥, 𝑦〉} → 〈𝑥, 𝑦〉 ∈ 〈𝑢, 𝑡〉) |
37 | 32, 36 | jca 304 |
. . . . . . . 8
⊢
(〈𝑢, 𝑡〉 = {〈𝑥, 𝑥〉, 〈𝑥, 𝑦〉} → (〈𝑥, 𝑥〉 ∈ 〈𝑢, 𝑡〉 ∧ 〈𝑥, 𝑦〉 ∈ 〈𝑢, 𝑡〉)) |
38 | | opeq12 3765 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑥) → 〈𝑧, 𝑤〉 = 〈𝑥, 𝑥〉) |
39 | 38 | 3adant3 1012 |
. . . . . . . . . . . . 13
⊢ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑥 ∧ 𝑣 = 𝑦) → 〈𝑧, 𝑤〉 = 〈𝑥, 𝑥〉) |
40 | 39 | eleq1d 2239 |
. . . . . . . . . . . 12
⊢ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑥 ∧ 𝑣 = 𝑦) → (〈𝑧, 𝑤〉 ∈ 〈𝑢, 𝑡〉 ↔ 〈𝑥, 𝑥〉 ∈ 〈𝑢, 𝑡〉)) |
41 | | opeq12 3765 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 = 𝑥 ∧ 𝑣 = 𝑦) → 〈𝑧, 𝑣〉 = 〈𝑥, 𝑦〉) |
42 | 41 | 3adant2 1011 |
. . . . . . . . . . . . 13
⊢ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑥 ∧ 𝑣 = 𝑦) → 〈𝑧, 𝑣〉 = 〈𝑥, 𝑦〉) |
43 | 42 | eleq1d 2239 |
. . . . . . . . . . . 12
⊢ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑥 ∧ 𝑣 = 𝑦) → (〈𝑧, 𝑣〉 ∈ 〈𝑢, 𝑡〉 ↔ 〈𝑥, 𝑦〉 ∈ 〈𝑢, 𝑡〉)) |
44 | 40, 43 | anbi12d 470 |
. . . . . . . . . . 11
⊢ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑥 ∧ 𝑣 = 𝑦) → ((〈𝑧, 𝑤〉 ∈ 〈𝑢, 𝑡〉 ∧ 〈𝑧, 𝑣〉 ∈ 〈𝑢, 𝑡〉) ↔ (〈𝑥, 𝑥〉 ∈ 〈𝑢, 𝑡〉 ∧ 〈𝑥, 𝑦〉 ∈ 〈𝑢, 𝑡〉))) |
45 | | eqeq12 2183 |
. . . . . . . . . . . 12
⊢ ((𝑤 = 𝑥 ∧ 𝑣 = 𝑦) → (𝑤 = 𝑣 ↔ 𝑥 = 𝑦)) |
46 | 45 | 3adant1 1010 |
. . . . . . . . . . 11
⊢ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑥 ∧ 𝑣 = 𝑦) → (𝑤 = 𝑣 ↔ 𝑥 = 𝑦)) |
47 | 44, 46 | imbi12d 233 |
. . . . . . . . . 10
⊢ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑥 ∧ 𝑣 = 𝑦) → (((〈𝑧, 𝑤〉 ∈ 〈𝑢, 𝑡〉 ∧ 〈𝑧, 𝑣〉 ∈ 〈𝑢, 𝑡〉) → 𝑤 = 𝑣) ↔ ((〈𝑥, 𝑥〉 ∈ 〈𝑢, 𝑡〉 ∧ 〈𝑥, 𝑦〉 ∈ 〈𝑢, 𝑡〉) → 𝑥 = 𝑦))) |
48 | 47 | spc3gv 2823 |
. . . . . . . . 9
⊢ ((𝑥 ∈ V ∧ 𝑥 ∈ V ∧ 𝑦 ∈ V) → (∀𝑧∀𝑤∀𝑣((〈𝑧, 𝑤〉 ∈ 〈𝑢, 𝑡〉 ∧ 〈𝑧, 𝑣〉 ∈ 〈𝑢, 𝑡〉) → 𝑤 = 𝑣) → ((〈𝑥, 𝑥〉 ∈ 〈𝑢, 𝑡〉 ∧ 〈𝑥, 𝑦〉 ∈ 〈𝑢, 𝑡〉) → 𝑥 = 𝑦))) |
49 | 15, 15, 18, 48 | mp3an 1332 |
. . . . . . . 8
⊢
(∀𝑧∀𝑤∀𝑣((〈𝑧, 𝑤〉 ∈ 〈𝑢, 𝑡〉 ∧ 〈𝑧, 𝑣〉 ∈ 〈𝑢, 𝑡〉) → 𝑤 = 𝑣) → ((〈𝑥, 𝑥〉 ∈ 〈𝑢, 𝑡〉 ∧ 〈𝑥, 𝑦〉 ∈ 〈𝑢, 𝑡〉) → 𝑥 = 𝑦)) |
50 | 28, 37, 49 | syl2im 38 |
. . . . . . 7
⊢ (Fun
〈𝑢, 𝑡〉 → (〈𝑢, 𝑡〉 = {〈𝑥, 𝑥〉, 〈𝑥, 𝑦〉} → 𝑥 = 𝑦)) |
51 | 26, 50 | syl5bi 151 |
. . . . . 6
⊢ (Fun
〈𝑢, 𝑡〉 → ((𝑢 = {𝑥} ∧ 𝑡 = {𝑥, 𝑦}) → 𝑥 = 𝑦)) |
52 | | dfsn2 3595 |
. . . . . . . . . . 11
⊢ {𝑥} = {𝑥, 𝑥} |
53 | | preq2 3659 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → {𝑥, 𝑥} = {𝑥, 𝑦}) |
54 | 52, 53 | eqtr2id 2216 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → {𝑥, 𝑦} = {𝑥}) |
55 | 54 | eqeq2d 2182 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑡 = {𝑥, 𝑦} ↔ 𝑡 = {𝑥})) |
56 | | eqtr3 2190 |
. . . . . . . . . 10
⊢ ((𝑢 = {𝑥} ∧ 𝑡 = {𝑥}) → 𝑢 = 𝑡) |
57 | 56 | expcom 115 |
. . . . . . . . 9
⊢ (𝑡 = {𝑥} → (𝑢 = {𝑥} → 𝑢 = 𝑡)) |
58 | 55, 57 | syl6bi 162 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑡 = {𝑥, 𝑦} → (𝑢 = {𝑥} → 𝑢 = 𝑡))) |
59 | 58 | com13 80 |
. . . . . . 7
⊢ (𝑢 = {𝑥} → (𝑡 = {𝑥, 𝑦} → (𝑥 = 𝑦 → 𝑢 = 𝑡))) |
60 | 59 | imp 123 |
. . . . . 6
⊢ ((𝑢 = {𝑥} ∧ 𝑡 = {𝑥, 𝑦}) → (𝑥 = 𝑦 → 𝑢 = 𝑡)) |
61 | 51, 60 | sylcom 28 |
. . . . 5
⊢ (Fun
〈𝑢, 𝑡〉 → ((𝑢 = {𝑥} ∧ 𝑡 = {𝑥, 𝑦}) → 𝑢 = 𝑡)) |
62 | 61 | exlimdvv 1890 |
. . . 4
⊢ (Fun
〈𝑢, 𝑡〉 → (∃𝑥∃𝑦(𝑢 = {𝑥} ∧ 𝑡 = {𝑥, 𝑦}) → 𝑢 = 𝑡)) |
63 | 13, 62 | mpd 13 |
. . 3
⊢ (Fun
〈𝑢, 𝑡〉 → 𝑢 = 𝑡) |
64 | 4, 8, 63 | vtocl2g 2794 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (Fun 〈𝐴, 𝐵〉 → 𝐴 = 𝐵)) |
65 | 64 | 3impia 1195 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ Fun 〈𝐴, 𝐵〉) → 𝐴 = 𝐵) |