Step | Hyp | Ref
| Expression |
1 | | opth1.1 |
. . . 4
⊢ A ∈
V |
2 | | opth1.2 |
. . . 4
⊢ B ∈
V |
3 | 1, 2 | opth1 3964 |
. . 3
⊢
(〈A, B〉 = 〈𝐶, 𝐷〉 → A = 𝐶) |
4 | 1, 2 | opi1 3960 |
. . . . . . 7
⊢ {A} ∈
〈A, B〉 |
5 | | id 19 |
. . . . . . 7
⊢
(〈A, B〉 = 〈𝐶, 𝐷〉 → 〈A, B〉 =
〈𝐶, 𝐷〉) |
6 | 4, 5 | syl5eleq 2123 |
. . . . . 6
⊢
(〈A, B〉 = 〈𝐶, 𝐷〉 → {A} ∈ 〈𝐶, 𝐷〉) |
7 | | oprcl 3564 |
. . . . . 6
⊢
({A} ∈ 〈𝐶, 𝐷〉 → (𝐶 ∈ V ∧ 𝐷 ∈
V)) |
8 | 6, 7 | syl 14 |
. . . . 5
⊢
(〈A, B〉 = 〈𝐶, 𝐷〉 → (𝐶 ∈ V ∧ 𝐷 ∈
V)) |
9 | 8 | simprd 107 |
. . . 4
⊢
(〈A, B〉 = 〈𝐶, 𝐷〉 → 𝐷 ∈
V) |
10 | 3 | opeq1d 3546 |
. . . . . . . 8
⊢
(〈A, B〉 = 〈𝐶, 𝐷〉 → 〈A, B〉 =
〈𝐶, B〉) |
11 | 10, 5 | eqtr3d 2071 |
. . . . . . 7
⊢
(〈A, B〉 = 〈𝐶, 𝐷〉 → 〈𝐶, B〉 = 〈𝐶, 𝐷〉) |
12 | 8 | simpld 105 |
. . . . . . . 8
⊢
(〈A, B〉 = 〈𝐶, 𝐷〉 → 𝐶 ∈
V) |
13 | | dfopg 3538 |
. . . . . . . 8
⊢ ((𝐶 ∈ V ∧ B ∈ V) →
〈𝐶, B〉 = {{𝐶}, {𝐶, B}}) |
14 | 12, 2, 13 | sylancl 392 |
. . . . . . 7
⊢
(〈A, B〉 = 〈𝐶, 𝐷〉 → 〈𝐶, B〉 = {{𝐶}, {𝐶, B}}) |
15 | 11, 14 | eqtr3d 2071 |
. . . . . 6
⊢
(〈A, B〉 = 〈𝐶, 𝐷〉 → 〈𝐶, 𝐷〉 = {{𝐶}, {𝐶, B}}) |
16 | | dfopg 3538 |
. . . . . . 7
⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → 〈𝐶, 𝐷〉 = {{𝐶}, {𝐶, 𝐷}}) |
17 | 8, 16 | syl 14 |
. . . . . 6
⊢
(〈A, B〉 = 〈𝐶, 𝐷〉 → 〈𝐶, 𝐷〉 = {{𝐶}, {𝐶, 𝐷}}) |
18 | 15, 17 | eqtr3d 2071 |
. . . . 5
⊢
(〈A, B〉 = 〈𝐶, 𝐷〉 → {{𝐶}, {𝐶, B}} =
{{𝐶}, {𝐶, 𝐷}}) |
19 | | prexgOLD 3937 |
. . . . . . 7
⊢ ((𝐶 ∈ V ∧ B ∈ V) →
{𝐶, B} ∈
V) |
20 | 12, 2, 19 | sylancl 392 |
. . . . . 6
⊢
(〈A, B〉 = 〈𝐶, 𝐷〉 → {𝐶, B}
∈ V) |
21 | | prexgOLD 3937 |
. . . . . . 7
⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → {𝐶, 𝐷} ∈
V) |
22 | 8, 21 | syl 14 |
. . . . . 6
⊢
(〈A, B〉 = 〈𝐶, 𝐷〉 → {𝐶, 𝐷} ∈
V) |
23 | | preqr2g 3529 |
. . . . . 6
⊢ (({𝐶, B} ∈ V ∧ {𝐶, 𝐷} ∈ V)
→ ({{𝐶}, {𝐶, B}} = {{𝐶}, {𝐶, 𝐷}} → {𝐶, B} =
{𝐶, 𝐷})) |
24 | 20, 22, 23 | syl2anc 391 |
. . . . 5
⊢
(〈A, B〉 = 〈𝐶, 𝐷〉 → ({{𝐶}, {𝐶, B}} =
{{𝐶}, {𝐶, 𝐷}} → {𝐶, B} =
{𝐶, 𝐷})) |
25 | 18, 24 | mpd 13 |
. . . 4
⊢
(〈A, B〉 = 〈𝐶, 𝐷〉 → {𝐶, B} =
{𝐶, 𝐷}) |
26 | | preq2 3439 |
. . . . . . 7
⊢ (x = 𝐷 → {𝐶, x} =
{𝐶, 𝐷}) |
27 | 26 | eqeq2d 2048 |
. . . . . 6
⊢ (x = 𝐷 → ({𝐶, B} =
{𝐶, x} ↔ {𝐶, B} =
{𝐶, 𝐷})) |
28 | | eqeq2 2046 |
. . . . . 6
⊢ (x = 𝐷 → (B = x ↔
B = 𝐷)) |
29 | 27, 28 | imbi12d 223 |
. . . . 5
⊢ (x = 𝐷 → (({𝐶, B} =
{𝐶, x} → B =
x) ↔ ({𝐶, B} =
{𝐶, 𝐷} → B = 𝐷))) |
30 | | vex 2554 |
. . . . . 6
⊢ x ∈
V |
31 | 2, 30 | preqr2 3531 |
. . . . 5
⊢ ({𝐶, B} = {𝐶, x}
→ B = x) |
32 | 29, 31 | vtoclg 2607 |
. . . 4
⊢ (𝐷 ∈ V → ({𝐶, B} =
{𝐶, 𝐷} → B = 𝐷)) |
33 | 9, 25, 32 | sylc 56 |
. . 3
⊢
(〈A, B〉 = 〈𝐶, 𝐷〉 → B = 𝐷) |
34 | 3, 33 | jca 290 |
. 2
⊢
(〈A, B〉 = 〈𝐶, 𝐷〉 → (A = 𝐶 ∧ B = 𝐷)) |
35 | | opeq12 3542 |
. 2
⊢
((A = 𝐶 ∧ B = 𝐷) → 〈A, B〉 =
〈𝐶, 𝐷〉) |
36 | 34, 35 | impbii 117 |
1
⊢
(〈A, B〉 = 〈𝐶, 𝐷〉 ↔ (A = 𝐶 ∧ B = 𝐷)) |