Step | Hyp | Ref
| Expression |
1 | | prex 5390 |
. . . 4
β’ {π΄, π} β V |
2 | | prex 5390 |
. . . 4
β’ {π΅, π} β V |
3 | | prex 5390 |
. . . 4
β’ {πΆ, π} β V |
4 | | prex 5390 |
. . . 4
β’ {π·, π} β V |
5 | 1, 2, 3, 4 | preq12b 4809 |
. . 3
β’ ({{π΄, π}, {π΅, π}} = {{πΆ, π}, {π·, π}} β (({π΄, π} = {πΆ, π} β§ {π΅, π} = {π·, π}) β¨ ({π΄, π} = {π·, π} β§ {π΅, π} = {πΆ, π}))) |
6 | | opthhausdorff0.a |
. . . . . 6
β’ π΄ β V |
7 | | opthhausdorff0.c |
. . . . . 6
β’ πΆ β V |
8 | 6, 7 | preqr1 4807 |
. . . . 5
β’ ({π΄, π} = {πΆ, π} β π΄ = πΆ) |
9 | | opthhausdorff0.b |
. . . . . 6
β’ π΅ β V |
10 | | opthhausdorff0.d |
. . . . . 6
β’ π· β V |
11 | 9, 10 | preqr1 4807 |
. . . . 5
β’ ({π΅, π} = {π·, π} β π΅ = π·) |
12 | 8, 11 | anim12i 614 |
. . . 4
β’ (({π΄, π} = {πΆ, π} β§ {π΅, π} = {π·, π}) β (π΄ = πΆ β§ π΅ = π·)) |
13 | | opthhausdorff0.1 |
. . . . . . 7
β’ π β V |
14 | | opthhausdorff0.2 |
. . . . . . 7
β’ π β V |
15 | 6, 13, 10, 14 | preq12b 4809 |
. . . . . 6
β’ ({π΄, π} = {π·, π} β ((π΄ = π· β§ π = π) β¨ (π΄ = π β§ π = π·))) |
16 | | opthhausdorff0.3 |
. . . . . . . . 9
β’ π β π |
17 | | eqneqall 2951 |
. . . . . . . . 9
β’ (π = π β (π β π β ({π΅, π} = {πΆ, π} β (π΄ = πΆ β§ π΅ = π·)))) |
18 | 16, 17 | mpi 20 |
. . . . . . . 8
β’ (π = π β ({π΅, π} = {πΆ, π} β (π΄ = πΆ β§ π΅ = π·))) |
19 | 18 | adantl 483 |
. . . . . . 7
β’ ((π΄ = π· β§ π = π) β ({π΅, π} = {πΆ, π} β (π΄ = πΆ β§ π΅ = π·))) |
20 | 9, 14, 7, 13 | preq12b 4809 |
. . . . . . . . 9
β’ ({π΅, π} = {πΆ, π} β ((π΅ = πΆ β§ π = π) β¨ (π΅ = π β§ π = πΆ))) |
21 | | eqneqall 2951 |
. . . . . . . . . . . . 13
β’ (π = π β (π β π β ((π΄ = π β§ π = π·) β (π΄ = πΆ β§ π΅ = π·)))) |
22 | 16, 21 | mpi 20 |
. . . . . . . . . . . 12
β’ (π = π β ((π΄ = π β§ π = π·) β (π΄ = πΆ β§ π΅ = π·))) |
23 | 22 | eqcoms 2741 |
. . . . . . . . . . 11
β’ (π = π β ((π΄ = π β§ π = π·) β (π΄ = πΆ β§ π΅ = π·))) |
24 | 23 | adantl 483 |
. . . . . . . . . 10
β’ ((π΅ = πΆ β§ π = π) β ((π΄ = π β§ π = π·) β (π΄ = πΆ β§ π΅ = π·))) |
25 | | simpl 484 |
. . . . . . . . . . . . 13
β’ ((π΄ = π β§ π = π·) β π΄ = π) |
26 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((π΅ = π β§ π = πΆ) β π = πΆ) |
27 | 25, 26 | sylan9eqr 2795 |
. . . . . . . . . . . 12
β’ (((π΅ = π β§ π = πΆ) β§ (π΄ = π β§ π = π·)) β π΄ = πΆ) |
28 | | simpl 484 |
. . . . . . . . . . . . 13
β’ ((π΅ = π β§ π = πΆ) β π΅ = π) |
29 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((π΄ = π β§ π = π·) β π = π·) |
30 | 28, 29 | sylan9eq 2793 |
. . . . . . . . . . . 12
β’ (((π΅ = π β§ π = πΆ) β§ (π΄ = π β§ π = π·)) β π΅ = π·) |
31 | 27, 30 | jca 513 |
. . . . . . . . . . 11
β’ (((π΅ = π β§ π = πΆ) β§ (π΄ = π β§ π = π·)) β (π΄ = πΆ β§ π΅ = π·)) |
32 | 31 | ex 414 |
. . . . . . . . . 10
β’ ((π΅ = π β§ π = πΆ) β ((π΄ = π β§ π = π·) β (π΄ = πΆ β§ π΅ = π·))) |
33 | 24, 32 | jaoi 856 |
. . . . . . . . 9
β’ (((π΅ = πΆ β§ π = π) β¨ (π΅ = π β§ π = πΆ)) β ((π΄ = π β§ π = π·) β (π΄ = πΆ β§ π΅ = π·))) |
34 | 20, 33 | sylbi 216 |
. . . . . . . 8
β’ ({π΅, π} = {πΆ, π} β ((π΄ = π β§ π = π·) β (π΄ = πΆ β§ π΅ = π·))) |
35 | 34 | com12 32 |
. . . . . . 7
β’ ((π΄ = π β§ π = π·) β ({π΅, π} = {πΆ, π} β (π΄ = πΆ β§ π΅ = π·))) |
36 | 19, 35 | jaoi 856 |
. . . . . 6
β’ (((π΄ = π· β§ π = π) β¨ (π΄ = π β§ π = π·)) β ({π΅, π} = {πΆ, π} β (π΄ = πΆ β§ π΅ = π·))) |
37 | 15, 36 | sylbi 216 |
. . . . 5
β’ ({π΄, π} = {π·, π} β ({π΅, π} = {πΆ, π} β (π΄ = πΆ β§ π΅ = π·))) |
38 | 37 | imp 408 |
. . . 4
β’ (({π΄, π} = {π·, π} β§ {π΅, π} = {πΆ, π}) β (π΄ = πΆ β§ π΅ = π·)) |
39 | 12, 38 | jaoi 856 |
. . 3
β’ ((({π΄, π} = {πΆ, π} β§ {π΅, π} = {π·, π}) β¨ ({π΄, π} = {π·, π} β§ {π΅, π} = {πΆ, π})) β (π΄ = πΆ β§ π΅ = π·)) |
40 | 5, 39 | sylbi 216 |
. 2
β’ ({{π΄, π}, {π΅, π}} = {{πΆ, π}, {π·, π}} β (π΄ = πΆ β§ π΅ = π·)) |
41 | | preq1 4695 |
. . . 4
β’ (π΄ = πΆ β {π΄, π} = {πΆ, π}) |
42 | 41 | adantr 482 |
. . 3
β’ ((π΄ = πΆ β§ π΅ = π·) β {π΄, π} = {πΆ, π}) |
43 | | preq1 4695 |
. . . 4
β’ (π΅ = π· β {π΅, π} = {π·, π}) |
44 | 43 | adantl 483 |
. . 3
β’ ((π΄ = πΆ β§ π΅ = π·) β {π΅, π} = {π·, π}) |
45 | 42, 44 | preq12d 4703 |
. 2
β’ ((π΄ = πΆ β§ π΅ = π·) β {{π΄, π}, {π΅, π}} = {{πΆ, π}, {π·, π}}) |
46 | 40, 45 | impbii 208 |
1
β’ ({{π΄, π}, {π΅, π}} = {{πΆ, π}, {π·, π}} β (π΄ = πΆ β§ π΅ = π·)) |