Proof of Theorem propssopi
Step | Hyp | Ref
| Expression |
1 | | propeqop.e |
. . . 4
⊢ 𝐸 ∈ V |
2 | | propeqop.f |
. . . 4
⊢ 𝐹 ∈ V |
3 | 1, 2 | dfop 4401 |
. . 3
⊢
〈𝐸, 𝐹〉 = {{𝐸}, {𝐸, 𝐹}} |
4 | 3 | sseq2i 3630 |
. 2
⊢
({〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} ⊆ 〈𝐸, 𝐹〉 ↔ {〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} ⊆ {{𝐸}, {𝐸, 𝐹}}) |
5 | | sspr 4366 |
. . 3
⊢
({〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} ⊆ {{𝐸}, {𝐸, 𝐹}} ↔ (({〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = ∅ ∨ {〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = {{𝐸}}) ∨ ({〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = {{𝐸, 𝐹}} ∨ {〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = {{𝐸}, {𝐸, 𝐹}}))) |
6 | | opex 4932 |
. . . . . . 7
⊢
〈𝐴, 𝐵〉 ∈ V |
7 | 6 | prnz 4310 |
. . . . . 6
⊢
{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} ≠ ∅ |
8 | | eqneqall 2805 |
. . . . . 6
⊢
({〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = ∅ → ({〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} ≠ ∅ → 𝐴 = 𝐶)) |
9 | 7, 8 | mpi 20 |
. . . . 5
⊢
({〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = ∅ → 𝐴 = 𝐶) |
10 | | opex 4932 |
. . . . . . 7
⊢
〈𝐶, 𝐷〉 ∈ V |
11 | | snex 4908 |
. . . . . . 7
⊢ {𝐸} ∈ V |
12 | 6, 10, 11 | preqsn 4393 |
. . . . . 6
⊢
({〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = {{𝐸}} ↔ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 ∧ 〈𝐶, 𝐷〉 = {𝐸})) |
13 | | snopeqop.a |
. . . . . . . . 9
⊢ 𝐴 ∈ V |
14 | | snopeqop.b |
. . . . . . . . 9
⊢ 𝐵 ∈ V |
15 | 13, 14 | opth 4945 |
. . . . . . . 8
⊢
(〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) |
16 | | simpl 473 |
. . . . . . . 8
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → 𝐴 = 𝐶) |
17 | 15, 16 | sylbi 207 |
. . . . . . 7
⊢
(〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 𝐴 = 𝐶) |
18 | 17 | adantr 481 |
. . . . . 6
⊢
((〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 ∧ 〈𝐶, 𝐷〉 = {𝐸}) → 𝐴 = 𝐶) |
19 | 12, 18 | sylbi 207 |
. . . . 5
⊢
({〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = {{𝐸}} → 𝐴 = 𝐶) |
20 | 9, 19 | jaoi 394 |
. . . 4
⊢
(({〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = ∅ ∨ {〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = {{𝐸}}) → 𝐴 = 𝐶) |
21 | | prex 4909 |
. . . . . . 7
⊢ {𝐸, 𝐹} ∈ V |
22 | 6, 10, 21 | preqsn 4393 |
. . . . . 6
⊢
({〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = {{𝐸, 𝐹}} ↔ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 ∧ 〈𝐶, 𝐷〉 = {𝐸, 𝐹})) |
23 | 16 | a1d 25 |
. . . . . . . 8
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → (〈𝐶, 𝐷〉 = {𝐸, 𝐹} → 𝐴 = 𝐶)) |
24 | 15, 23 | sylbi 207 |
. . . . . . 7
⊢
(〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → (〈𝐶, 𝐷〉 = {𝐸, 𝐹} → 𝐴 = 𝐶)) |
25 | 24 | imp 445 |
. . . . . 6
⊢
((〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 ∧ 〈𝐶, 𝐷〉 = {𝐸, 𝐹}) → 𝐴 = 𝐶) |
26 | 22, 25 | sylbi 207 |
. . . . 5
⊢
({〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = {{𝐸, 𝐹}} → 𝐴 = 𝐶) |
27 | 3 | eqcomi 2631 |
. . . . . . . 8
⊢ {{𝐸}, {𝐸, 𝐹}} = 〈𝐸, 𝐹〉 |
28 | 27 | eqeq2i 2634 |
. . . . . . 7
⊢
({〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = {{𝐸}, {𝐸, 𝐹}} ↔ {〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = 〈𝐸, 𝐹〉) |
29 | | snopeqop.c |
. . . . . . . 8
⊢ 𝐶 ∈ V |
30 | | snopeqop.d |
. . . . . . . 8
⊢ 𝐷 ∈ V |
31 | 13, 14, 29, 30, 1, 2 | propeqop 4970 |
. . . . . . 7
⊢
({〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = 〈𝐸, 𝐹〉 ↔ ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) ∧ ((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵})))) |
32 | 28, 31 | bitri 264 |
. . . . . 6
⊢
({〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = {{𝐸}, {𝐸, 𝐹}} ↔ ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) ∧ ((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵})))) |
33 | | simpll 790 |
. . . . . 6
⊢ (((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) ∧ ((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}))) → 𝐴 = 𝐶) |
34 | 32, 33 | sylbi 207 |
. . . . 5
⊢
({〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = {{𝐸}, {𝐸, 𝐹}} → 𝐴 = 𝐶) |
35 | 26, 34 | jaoi 394 |
. . . 4
⊢
(({〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = {{𝐸, 𝐹}} ∨ {〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = {{𝐸}, {𝐸, 𝐹}}) → 𝐴 = 𝐶) |
36 | 20, 35 | jaoi 394 |
. . 3
⊢
((({〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = ∅ ∨ {〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = {{𝐸}}) ∨ ({〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = {{𝐸, 𝐹}} ∨ {〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = {{𝐸}, {𝐸, 𝐹}})) → 𝐴 = 𝐶) |
37 | 5, 36 | sylbi 207 |
. 2
⊢
({〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} ⊆ {{𝐸}, {𝐸, 𝐹}} → 𝐴 = 𝐶) |
38 | 4, 37 | sylbi 207 |
1
⊢
({〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} ⊆ 〈𝐸, 𝐹〉 → 𝐴 = 𝐶) |