Step | Hyp | Ref
| Expression |
1 | | opeq1 4830 |
. . . . 5
⊢ (𝑢 = 𝐴 → ⟨𝑢, 𝑡⟩ = ⟨𝐴, 𝑡⟩) |
2 | 1 | funeqd 6523 |
. . . 4
⊢ (𝑢 = 𝐴 → (Fun ⟨𝑢, 𝑡⟩ ↔ Fun ⟨𝐴, 𝑡⟩)) |
3 | | eqeq1 2740 |
. . . 4
⊢ (𝑢 = 𝐴 → (𝑢 = 𝑡 ↔ 𝐴 = 𝑡)) |
4 | 2, 3 | imbi12d 344 |
. . 3
⊢ (𝑢 = 𝐴 → ((Fun ⟨𝑢, 𝑡⟩ → 𝑢 = 𝑡) ↔ (Fun ⟨𝐴, 𝑡⟩ → 𝐴 = 𝑡))) |
5 | | opeq2 4831 |
. . . . 5
⊢ (𝑡 = 𝐵 → ⟨𝐴, 𝑡⟩ = ⟨𝐴, 𝐵⟩) |
6 | 5 | funeqd 6523 |
. . . 4
⊢ (𝑡 = 𝐵 → (Fun ⟨𝐴, 𝑡⟩ ↔ Fun ⟨𝐴, 𝐵⟩)) |
7 | | eqeq2 2748 |
. . . 4
⊢ (𝑡 = 𝐵 → (𝐴 = 𝑡 ↔ 𝐴 = 𝐵)) |
8 | 6, 7 | imbi12d 344 |
. . 3
⊢ (𝑡 = 𝐵 → ((Fun ⟨𝐴, 𝑡⟩ → 𝐴 = 𝑡) ↔ (Fun ⟨𝐴, 𝐵⟩ → 𝐴 = 𝐵))) |
9 | | funrel 6518 |
. . . . 5
⊢ (Fun
⟨𝑢, 𝑡⟩ → Rel ⟨𝑢, 𝑡⟩) |
10 | | vex 3449 |
. . . . . 6
⊢ 𝑢 ∈ V |
11 | | vex 3449 |
. . . . . 6
⊢ 𝑡 ∈ V |
12 | 10, 11 | relop 5806 |
. . . . 5
⊢ (Rel
⟨𝑢, 𝑡⟩ ↔ ∃𝑥∃𝑦(𝑢 = {𝑥} ∧ 𝑡 = {𝑥, 𝑦})) |
13 | 9, 12 | sylib 217 |
. . . 4
⊢ (Fun
⟨𝑢, 𝑡⟩ → ∃𝑥∃𝑦(𝑢 = {𝑥} ∧ 𝑡 = {𝑥, 𝑦})) |
14 | 10, 11 | opth 5433 |
. . . . . . . 8
⊢
(⟨𝑢, 𝑡⟩ = ⟨{𝑥}, {𝑥, 𝑦}⟩ ↔ (𝑢 = {𝑥} ∧ 𝑡 = {𝑥, 𝑦})) |
15 | | vex 3449 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
16 | 15 | opid 4850 |
. . . . . . . . . . 11
⊢
⟨𝑥, 𝑥⟩ = {{𝑥}} |
17 | 16 | preq1i 4697 |
. . . . . . . . . 10
⊢
{⟨𝑥, 𝑥⟩, {{𝑥}, {𝑥, 𝑦}}} = {{{𝑥}}, {{𝑥}, {𝑥, 𝑦}}} |
18 | | vex 3449 |
. . . . . . . . . . . 12
⊢ 𝑦 ∈ V |
19 | 15, 18 | dfop 4829 |
. . . . . . . . . . 11
⊢
⟨𝑥, 𝑦⟩ = {{𝑥}, {𝑥, 𝑦}} |
20 | 19 | preq2i 4698 |
. . . . . . . . . 10
⊢
{⟨𝑥, 𝑥⟩, ⟨𝑥, 𝑦⟩} = {⟨𝑥, 𝑥⟩, {{𝑥}, {𝑥, 𝑦}}} |
21 | | vsnex 5386 |
. . . . . . . . . . 11
⊢ {𝑥} ∈ V |
22 | | zfpair2 5385 |
. . . . . . . . . . 11
⊢ {𝑥, 𝑦} ∈ V |
23 | 21, 22 | dfop 4829 |
. . . . . . . . . 10
⊢
⟨{𝑥}, {𝑥, 𝑦}⟩ = {{{𝑥}}, {{𝑥}, {𝑥, 𝑦}}} |
24 | 17, 20, 23 | 3eqtr4ri 2775 |
. . . . . . . . 9
⊢
⟨{𝑥}, {𝑥, 𝑦}⟩ = {⟨𝑥, 𝑥⟩, ⟨𝑥, 𝑦⟩} |
25 | 24 | eqeq2i 2749 |
. . . . . . . 8
⊢
(⟨𝑢, 𝑡⟩ = ⟨{𝑥}, {𝑥, 𝑦}⟩ ↔ ⟨𝑢, 𝑡⟩ = {⟨𝑥, 𝑥⟩, ⟨𝑥, 𝑦⟩}) |
26 | 14, 25 | bitr3i 276 |
. . . . . . 7
⊢ ((𝑢 = {𝑥} ∧ 𝑡 = {𝑥, 𝑦}) ↔ ⟨𝑢, 𝑡⟩ = {⟨𝑥, 𝑥⟩, ⟨𝑥, 𝑦⟩}) |
27 | | dffun4 6512 |
. . . . . . . . 9
⊢ (Fun
⟨𝑢, 𝑡⟩ ↔ (Rel ⟨𝑢, 𝑡⟩ ∧ ∀𝑧∀𝑤∀𝑣((⟨𝑧, 𝑤⟩ ∈ ⟨𝑢, 𝑡⟩ ∧ ⟨𝑧, 𝑣⟩ ∈ ⟨𝑢, 𝑡⟩) → 𝑤 = 𝑣))) |
28 | 27 | simprbi 497 |
. . . . . . . 8
⊢ (Fun
⟨𝑢, 𝑡⟩ → ∀𝑧∀𝑤∀𝑣((⟨𝑧, 𝑤⟩ ∈ ⟨𝑢, 𝑡⟩ ∧ ⟨𝑧, 𝑣⟩ ∈ ⟨𝑢, 𝑡⟩) → 𝑤 = 𝑣)) |
29 | | opex 5421 |
. . . . . . . . . . 11
⊢
⟨𝑥, 𝑥⟩ ∈ V |
30 | 29 | prid1 4723 |
. . . . . . . . . 10
⊢
⟨𝑥, 𝑥⟩ ∈ {⟨𝑥, 𝑥⟩, ⟨𝑥, 𝑦⟩} |
31 | | eleq2 2826 |
. . . . . . . . . 10
⊢
(⟨𝑢, 𝑡⟩ = {⟨𝑥, 𝑥⟩, ⟨𝑥, 𝑦⟩} → (⟨𝑥, 𝑥⟩ ∈ ⟨𝑢, 𝑡⟩ ↔ ⟨𝑥, 𝑥⟩ ∈ {⟨𝑥, 𝑥⟩, ⟨𝑥, 𝑦⟩})) |
32 | 30, 31 | mpbiri 257 |
. . . . . . . . 9
⊢
(⟨𝑢, 𝑡⟩ = {⟨𝑥, 𝑥⟩, ⟨𝑥, 𝑦⟩} → ⟨𝑥, 𝑥⟩ ∈ ⟨𝑢, 𝑡⟩) |
33 | | opex 5421 |
. . . . . . . . . . 11
⊢
⟨𝑥, 𝑦⟩ ∈ V |
34 | 33 | prid2 4724 |
. . . . . . . . . 10
⊢
⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑥⟩, ⟨𝑥, 𝑦⟩} |
35 | | eleq2 2826 |
. . . . . . . . . 10
⊢
(⟨𝑢, 𝑡⟩ = {⟨𝑥, 𝑥⟩, ⟨𝑥, 𝑦⟩} → (⟨𝑥, 𝑦⟩ ∈ ⟨𝑢, 𝑡⟩ ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑥⟩, ⟨𝑥, 𝑦⟩})) |
36 | 34, 35 | mpbiri 257 |
. . . . . . . . 9
⊢
(⟨𝑢, 𝑡⟩ = {⟨𝑥, 𝑥⟩, ⟨𝑥, 𝑦⟩} → ⟨𝑥, 𝑦⟩ ∈ ⟨𝑢, 𝑡⟩) |
37 | 32, 36 | jca 512 |
. . . . . . . 8
⊢
(⟨𝑢, 𝑡⟩ = {⟨𝑥, 𝑥⟩, ⟨𝑥, 𝑦⟩} → (⟨𝑥, 𝑥⟩ ∈ ⟨𝑢, 𝑡⟩ ∧ ⟨𝑥, 𝑦⟩ ∈ ⟨𝑢, 𝑡⟩)) |
38 | | opeq12 4832 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑥) → ⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑥⟩) |
39 | 38 | 3adant3 1132 |
. . . . . . . . . . . . 13
⊢ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑥 ∧ 𝑣 = 𝑦) → ⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑥⟩) |
40 | 39 | eleq1d 2822 |
. . . . . . . . . . . 12
⊢ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑥 ∧ 𝑣 = 𝑦) → (⟨𝑧, 𝑤⟩ ∈ ⟨𝑢, 𝑡⟩ ↔ ⟨𝑥, 𝑥⟩ ∈ ⟨𝑢, 𝑡⟩)) |
41 | | opeq12 4832 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 = 𝑥 ∧ 𝑣 = 𝑦) → ⟨𝑧, 𝑣⟩ = ⟨𝑥, 𝑦⟩) |
42 | 41 | 3adant2 1131 |
. . . . . . . . . . . . 13
⊢ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑥 ∧ 𝑣 = 𝑦) → ⟨𝑧, 𝑣⟩ = ⟨𝑥, 𝑦⟩) |
43 | 42 | eleq1d 2822 |
. . . . . . . . . . . 12
⊢ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑥 ∧ 𝑣 = 𝑦) → (⟨𝑧, 𝑣⟩ ∈ ⟨𝑢, 𝑡⟩ ↔ ⟨𝑥, 𝑦⟩ ∈ ⟨𝑢, 𝑡⟩)) |
44 | 40, 43 | anbi12d 631 |
. . . . . . . . . . 11
⊢ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑥 ∧ 𝑣 = 𝑦) → ((⟨𝑧, 𝑤⟩ ∈ ⟨𝑢, 𝑡⟩ ∧ ⟨𝑧, 𝑣⟩ ∈ ⟨𝑢, 𝑡⟩) ↔ (⟨𝑥, 𝑥⟩ ∈ ⟨𝑢, 𝑡⟩ ∧ ⟨𝑥, 𝑦⟩ ∈ ⟨𝑢, 𝑡⟩))) |
45 | | eqeq12 2753 |
. . . . . . . . . . . 12
⊢ ((𝑤 = 𝑥 ∧ 𝑣 = 𝑦) → (𝑤 = 𝑣 ↔ 𝑥 = 𝑦)) |
46 | 45 | 3adant1 1130 |
. . . . . . . . . . 11
⊢ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑥 ∧ 𝑣 = 𝑦) → (𝑤 = 𝑣 ↔ 𝑥 = 𝑦)) |
47 | 44, 46 | imbi12d 344 |
. . . . . . . . . 10
⊢ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑥 ∧ 𝑣 = 𝑦) → (((⟨𝑧, 𝑤⟩ ∈ ⟨𝑢, 𝑡⟩ ∧ ⟨𝑧, 𝑣⟩ ∈ ⟨𝑢, 𝑡⟩) → 𝑤 = 𝑣) ↔ ((⟨𝑥, 𝑥⟩ ∈ ⟨𝑢, 𝑡⟩ ∧ ⟨𝑥, 𝑦⟩ ∈ ⟨𝑢, 𝑡⟩) → 𝑥 = 𝑦))) |
48 | 47 | spc3gv 3563 |
. . . . . . . . 9
⊢ ((𝑥 ∈ V ∧ 𝑥 ∈ V ∧ 𝑦 ∈ V) → (∀𝑧∀𝑤∀𝑣((⟨𝑧, 𝑤⟩ ∈ ⟨𝑢, 𝑡⟩ ∧ ⟨𝑧, 𝑣⟩ ∈ ⟨𝑢, 𝑡⟩) → 𝑤 = 𝑣) → ((⟨𝑥, 𝑥⟩ ∈ ⟨𝑢, 𝑡⟩ ∧ ⟨𝑥, 𝑦⟩ ∈ ⟨𝑢, 𝑡⟩) → 𝑥 = 𝑦))) |
49 | 15, 15, 18, 48 | mp3an 1461 |
. . . . . . . 8
⊢
(∀𝑧∀𝑤∀𝑣((⟨𝑧, 𝑤⟩ ∈ ⟨𝑢, 𝑡⟩ ∧ ⟨𝑧, 𝑣⟩ ∈ ⟨𝑢, 𝑡⟩) → 𝑤 = 𝑣) → ((⟨𝑥, 𝑥⟩ ∈ ⟨𝑢, 𝑡⟩ ∧ ⟨𝑥, 𝑦⟩ ∈ ⟨𝑢, 𝑡⟩) → 𝑥 = 𝑦)) |
50 | 28, 37, 49 | syl2im 40 |
. . . . . . 7
⊢ (Fun
⟨𝑢, 𝑡⟩ → (⟨𝑢, 𝑡⟩ = {⟨𝑥, 𝑥⟩, ⟨𝑥, 𝑦⟩} → 𝑥 = 𝑦)) |
51 | 26, 50 | biimtrid 241 |
. . . . . 6
⊢ (Fun
⟨𝑢, 𝑡⟩ → ((𝑢 = {𝑥} ∧ 𝑡 = {𝑥, 𝑦}) → 𝑥 = 𝑦)) |
52 | | dfsn2 4599 |
. . . . . . . . . . 11
⊢ {𝑥} = {𝑥, 𝑥} |
53 | | preq2 4695 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → {𝑥, 𝑥} = {𝑥, 𝑦}) |
54 | 52, 53 | eqtr2id 2789 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → {𝑥, 𝑦} = {𝑥}) |
55 | 54 | eqeq2d 2747 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑡 = {𝑥, 𝑦} ↔ 𝑡 = {𝑥})) |
56 | | eqtr3 2762 |
. . . . . . . . . 10
⊢ ((𝑢 = {𝑥} ∧ 𝑡 = {𝑥}) → 𝑢 = 𝑡) |
57 | 56 | expcom 414 |
. . . . . . . . 9
⊢ (𝑡 = {𝑥} → (𝑢 = {𝑥} → 𝑢 = 𝑡)) |
58 | 55, 57 | syl6bi 252 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑡 = {𝑥, 𝑦} → (𝑢 = {𝑥} → 𝑢 = 𝑡))) |
59 | 58 | com13 88 |
. . . . . . 7
⊢ (𝑢 = {𝑥} → (𝑡 = {𝑥, 𝑦} → (𝑥 = 𝑦 → 𝑢 = 𝑡))) |
60 | 59 | imp 407 |
. . . . . 6
⊢ ((𝑢 = {𝑥} ∧ 𝑡 = {𝑥, 𝑦}) → (𝑥 = 𝑦 → 𝑢 = 𝑡)) |
61 | 51, 60 | sylcom 30 |
. . . . 5
⊢ (Fun
⟨𝑢, 𝑡⟩ → ((𝑢 = {𝑥} ∧ 𝑡 = {𝑥, 𝑦}) → 𝑢 = 𝑡)) |
62 | 61 | exlimdvv 1937 |
. . . 4
⊢ (Fun
⟨𝑢, 𝑡⟩ → (∃𝑥∃𝑦(𝑢 = {𝑥} ∧ 𝑡 = {𝑥, 𝑦}) → 𝑢 = 𝑡)) |
63 | 13, 62 | mpd 15 |
. . 3
⊢ (Fun
⟨𝑢, 𝑡⟩ → 𝑢 = 𝑡) |
64 | 4, 8, 63 | vtocl2g 3531 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (Fun ⟨𝐴, 𝐵⟩ → 𝐴 = 𝐵)) |
65 | 64 | 3impia 1117 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ Fun ⟨𝐴, 𝐵⟩) → 𝐴 = 𝐵) |