Step | Hyp | Ref
| Expression |
1 | | propeqop.e |
. . . 4
⊢ 𝐸 ∈ V |
2 | | propeqop.f |
. . . 4
⊢ 𝐹 ∈ V |
3 | 1, 2 | dfop 4872 |
. . 3
⊢
⟨𝐸, 𝐹⟩ = {{𝐸}, {𝐸, 𝐹}} |
4 | 3 | sseq2i 4011 |
. 2
⊢
({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ⊆ ⟨𝐸, 𝐹⟩ ↔ {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ⊆ {{𝐸}, {𝐸, 𝐹}}) |
5 | | sspr 4836 |
. . 3
⊢
({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ⊆ {{𝐸}, {𝐸, 𝐹}} ↔ (({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = ∅ ∨ {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸}}) ∨ ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸, 𝐹}} ∨ {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸}, {𝐸, 𝐹}}))) |
6 | | opex 5464 |
. . . . . . 7
⊢
⟨𝐴, 𝐵⟩ ∈ V |
7 | 6 | prnz 4781 |
. . . . . 6
⊢
{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ≠ ∅ |
8 | | eqneqall 2951 |
. . . . . 6
⊢
({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = ∅ → ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ≠ ∅ → 𝐴 = 𝐶)) |
9 | 7, 8 | mpi 20 |
. . . . 5
⊢
({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = ∅ → 𝐴 = 𝐶) |
10 | | opex 5464 |
. . . . . . 7
⊢
⟨𝐶, 𝐷⟩ ∈ V |
11 | 6, 10 | preqsn 4862 |
. . . . . 6
⊢
({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸}} ↔ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ∧ ⟨𝐶, 𝐷⟩ = {𝐸})) |
12 | | snopeqop.a |
. . . . . . . . 9
⊢ 𝐴 ∈ V |
13 | | snopeqop.b |
. . . . . . . . 9
⊢ 𝐵 ∈ V |
14 | 12, 13 | opth 5476 |
. . . . . . . 8
⊢
(⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) |
15 | | simpl 483 |
. . . . . . . 8
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → 𝐴 = 𝐶) |
16 | 14, 15 | sylbi 216 |
. . . . . . 7
⊢
(⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐴 = 𝐶) |
17 | 16 | adantr 481 |
. . . . . 6
⊢
((⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ∧ ⟨𝐶, 𝐷⟩ = {𝐸}) → 𝐴 = 𝐶) |
18 | 11, 17 | sylbi 216 |
. . . . 5
⊢
({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸}} → 𝐴 = 𝐶) |
19 | 9, 18 | jaoi 855 |
. . . 4
⊢
(({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = ∅ ∨ {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸}}) → 𝐴 = 𝐶) |
20 | 6, 10 | preqsn 4862 |
. . . . . 6
⊢
({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸, 𝐹}} ↔ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ∧ ⟨𝐶, 𝐷⟩ = {𝐸, 𝐹})) |
21 | 15 | a1d 25 |
. . . . . . . 8
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → (⟨𝐶, 𝐷⟩ = {𝐸, 𝐹} → 𝐴 = 𝐶)) |
22 | 14, 21 | sylbi 216 |
. . . . . . 7
⊢
(⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → (⟨𝐶, 𝐷⟩ = {𝐸, 𝐹} → 𝐴 = 𝐶)) |
23 | 22 | imp 407 |
. . . . . 6
⊢
((⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ∧ ⟨𝐶, 𝐷⟩ = {𝐸, 𝐹}) → 𝐴 = 𝐶) |
24 | 20, 23 | sylbi 216 |
. . . . 5
⊢
({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸, 𝐹}} → 𝐴 = 𝐶) |
25 | 3 | eqcomi 2741 |
. . . . . . . 8
⊢ {{𝐸}, {𝐸, 𝐹}} = ⟨𝐸, 𝐹⟩ |
26 | 25 | eqeq2i 2745 |
. . . . . . 7
⊢
({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸}, {𝐸, 𝐹}} ↔ {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = ⟨𝐸, 𝐹⟩) |
27 | | propeqop.c |
. . . . . . . 8
⊢ 𝐶 ∈ V |
28 | | propeqop.d |
. . . . . . . 8
⊢ 𝐷 ∈ V |
29 | 12, 13, 27, 28, 1, 2 | propeqop 5507 |
. . . . . . 7
⊢
({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = ⟨𝐸, 𝐹⟩ ↔ ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) ∧ ((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵})))) |
30 | 26, 29 | bitri 274 |
. . . . . 6
⊢
({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸}, {𝐸, 𝐹}} ↔ ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) ∧ ((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵})))) |
31 | | simpll 765 |
. . . . . 6
⊢ (((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) ∧ ((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}))) → 𝐴 = 𝐶) |
32 | 30, 31 | sylbi 216 |
. . . . 5
⊢
({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸}, {𝐸, 𝐹}} → 𝐴 = 𝐶) |
33 | 24, 32 | jaoi 855 |
. . . 4
⊢
(({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸, 𝐹}} ∨ {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸}, {𝐸, 𝐹}}) → 𝐴 = 𝐶) |
34 | 19, 33 | jaoi 855 |
. . 3
⊢
((({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = ∅ ∨ {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸}}) ∨ ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸, 𝐹}} ∨ {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {{𝐸}, {𝐸, 𝐹}})) → 𝐴 = 𝐶) |
35 | 5, 34 | sylbi 216 |
. 2
⊢
({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ⊆ {{𝐸}, {𝐸, 𝐹}} → 𝐴 = 𝐶) |
36 | 4, 35 | sylbi 216 |
1
⊢
({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ⊆ ⟨𝐸, 𝐹⟩ → 𝐴 = 𝐶) |