Step | Hyp | Ref
| Expression |
1 | | an4 655 |
. . . . . . . . 9
β’ (((π₯ β π½ β§ π¦ β π½) β§ (π΄ β π₯ β§ π΅ β π¦)) β ((π₯ β π½ β§ π΄ β π₯) β§ (π¦ β π½ β§ π΅ β π¦))) |
2 | | nnuz 12814 |
. . . . . . . . . . . . 13
β’ β =
(β€β₯β1) |
3 | | simprr 772 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β π½ β§ π΄ β π₯)) β π΄ β π₯) |
4 | | 1zzd 12542 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β π½ β§ π΄ β π₯)) β 1 β β€) |
5 | | lmmo.4 |
. . . . . . . . . . . . . 14
β’ (π β πΉ(βπ‘βπ½)π΄) |
6 | 5 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β π½ β§ π΄ β π₯)) β πΉ(βπ‘βπ½)π΄) |
7 | | simprl 770 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β π½ β§ π΄ β π₯)) β π₯ β π½) |
8 | 2, 3, 4, 6, 7 | lmcvg 22636 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β π½ β§ π΄ β π₯)) β βπ β β βπ β (β€β₯βπ)(πΉβπ) β π₯) |
9 | 8 | ex 414 |
. . . . . . . . . . 11
β’ (π β ((π₯ β π½ β§ π΄ β π₯) β βπ β β βπ β (β€β₯βπ)(πΉβπ) β π₯)) |
10 | | simprr 772 |
. . . . . . . . . . . . 13
β’ ((π β§ (π¦ β π½ β§ π΅ β π¦)) β π΅ β π¦) |
11 | | 1zzd 12542 |
. . . . . . . . . . . . 13
β’ ((π β§ (π¦ β π½ β§ π΅ β π¦)) β 1 β β€) |
12 | | lmmo.5 |
. . . . . . . . . . . . . 14
β’ (π β πΉ(βπ‘βπ½)π΅) |
13 | 12 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ (π¦ β π½ β§ π΅ β π¦)) β πΉ(βπ‘βπ½)π΅) |
14 | | simprl 770 |
. . . . . . . . . . . . 13
β’ ((π β§ (π¦ β π½ β§ π΅ β π¦)) β π¦ β π½) |
15 | 2, 10, 11, 13, 14 | lmcvg 22636 |
. . . . . . . . . . . 12
β’ ((π β§ (π¦ β π½ β§ π΅ β π¦)) β βπ β β βπ β (β€β₯βπ)(πΉβπ) β π¦) |
16 | 15 | ex 414 |
. . . . . . . . . . 11
β’ (π β ((π¦ β π½ β§ π΅ β π¦) β βπ β β βπ β (β€β₯βπ)(πΉβπ) β π¦)) |
17 | 9, 16 | anim12d 610 |
. . . . . . . . . 10
β’ (π β (((π₯ β π½ β§ π΄ β π₯) β§ (π¦ β π½ β§ π΅ β π¦)) β (βπ β β βπ β (β€β₯βπ)(πΉβπ) β π₯ β§ βπ β β βπ β (β€β₯βπ)(πΉβπ) β π¦))) |
18 | 2 | rexanuz2 15243 |
. . . . . . . . . . 11
β’
(βπ β
β βπ β
(β€β₯βπ)((πΉβπ) β π₯ β§ (πΉβπ) β π¦) β (βπ β β βπ β (β€β₯βπ)(πΉβπ) β π₯ β§ βπ β β βπ β (β€β₯βπ)(πΉβπ) β π¦)) |
19 | | nnz 12528 |
. . . . . . . . . . . . . 14
β’ (π β β β π β
β€) |
20 | | uzid 12786 |
. . . . . . . . . . . . . 14
β’ (π β β€ β π β
(β€β₯βπ)) |
21 | | ne0i 4298 |
. . . . . . . . . . . . . 14
β’ (π β
(β€β₯βπ) β (β€β₯βπ) β β
) |
22 | 19, 20, 21 | 3syl 18 |
. . . . . . . . . . . . 13
β’ (π β β β
(β€β₯βπ) β β
) |
23 | | r19.2z 4456 |
. . . . . . . . . . . . . 14
β’
(((β€β₯βπ) β β
β§ βπ β
(β€β₯βπ)((πΉβπ) β π₯ β§ (πΉβπ) β π¦)) β βπ β (β€β₯βπ)((πΉβπ) β π₯ β§ (πΉβπ) β π¦)) |
24 | | elin 3930 |
. . . . . . . . . . . . . . . 16
β’ ((πΉβπ) β (π₯ β© π¦) β ((πΉβπ) β π₯ β§ (πΉβπ) β π¦)) |
25 | | n0i 4297 |
. . . . . . . . . . . . . . . 16
β’ ((πΉβπ) β (π₯ β© π¦) β Β¬ (π₯ β© π¦) = β
) |
26 | 24, 25 | sylbir 234 |
. . . . . . . . . . . . . . 15
β’ (((πΉβπ) β π₯ β§ (πΉβπ) β π¦) β Β¬ (π₯ β© π¦) = β
) |
27 | 26 | rexlimivw 3145 |
. . . . . . . . . . . . . 14
β’
(βπ β
(β€β₯βπ)((πΉβπ) β π₯ β§ (πΉβπ) β π¦) β Β¬ (π₯ β© π¦) = β
) |
28 | 23, 27 | syl 17 |
. . . . . . . . . . . . 13
β’
(((β€β₯βπ) β β
β§ βπ β
(β€β₯βπ)((πΉβπ) β π₯ β§ (πΉβπ) β π¦)) β Β¬ (π₯ β© π¦) = β
) |
29 | 22, 28 | sylan 581 |
. . . . . . . . . . . 12
β’ ((π β β β§
βπ β
(β€β₯βπ)((πΉβπ) β π₯ β§ (πΉβπ) β π¦)) β Β¬ (π₯ β© π¦) = β
) |
30 | 29 | rexlimiva 3141 |
. . . . . . . . . . 11
β’
(βπ β
β βπ β
(β€β₯βπ)((πΉβπ) β π₯ β§ (πΉβπ) β π¦) β Β¬ (π₯ β© π¦) = β
) |
31 | 18, 30 | sylbir 234 |
. . . . . . . . . 10
β’
((βπ β
β βπ β
(β€β₯βπ)(πΉβπ) β π₯ β§ βπ β β βπ β (β€β₯βπ)(πΉβπ) β π¦) β Β¬ (π₯ β© π¦) = β
) |
32 | 17, 31 | syl6 35 |
. . . . . . . . 9
β’ (π β (((π₯ β π½ β§ π΄ β π₯) β§ (π¦ β π½ β§ π΅ β π¦)) β Β¬ (π₯ β© π¦) = β
)) |
33 | 1, 32 | biimtrid 241 |
. . . . . . . 8
β’ (π β (((π₯ β π½ β§ π¦ β π½) β§ (π΄ β π₯ β§ π΅ β π¦)) β Β¬ (π₯ β© π¦) = β
)) |
34 | 33 | expdimp 454 |
. . . . . . 7
β’ ((π β§ (π₯ β π½ β§ π¦ β π½)) β ((π΄ β π₯ β§ π΅ β π¦) β Β¬ (π₯ β© π¦) = β
)) |
35 | | imnan 401 |
. . . . . . 7
β’ (((π΄ β π₯ β§ π΅ β π¦) β Β¬ (π₯ β© π¦) = β
) β Β¬ ((π΄ β π₯ β§ π΅ β π¦) β§ (π₯ β© π¦) = β
)) |
36 | 34, 35 | sylib 217 |
. . . . . 6
β’ ((π β§ (π₯ β π½ β§ π¦ β π½)) β Β¬ ((π΄ β π₯ β§ π΅ β π¦) β§ (π₯ β© π¦) = β
)) |
37 | | df-3an 1090 |
. . . . . 6
β’ ((π΄ β π₯ β§ π΅ β π¦ β§ (π₯ β© π¦) = β
) β ((π΄ β π₯ β§ π΅ β π¦) β§ (π₯ β© π¦) = β
)) |
38 | 36, 37 | sylnibr 329 |
. . . . 5
β’ ((π β§ (π₯ β π½ β§ π¦ β π½)) β Β¬ (π΄ β π₯ β§ π΅ β π¦ β§ (π₯ β© π¦) = β
)) |
39 | 38 | anassrs 469 |
. . . 4
β’ (((π β§ π₯ β π½) β§ π¦ β π½) β Β¬ (π΄ β π₯ β§ π΅ β π¦ β§ (π₯ β© π¦) = β
)) |
40 | 39 | nrexdv 3143 |
. . 3
β’ ((π β§ π₯ β π½) β Β¬ βπ¦ β π½ (π΄ β π₯ β§ π΅ β π¦ β§ (π₯ β© π¦) = β
)) |
41 | 40 | nrexdv 3143 |
. 2
β’ (π β Β¬ βπ₯ β π½ βπ¦ β π½ (π΄ β π₯ β§ π΅ β π¦ β§ (π₯ β© π¦) = β
)) |
42 | | lmmo.1 |
. . . 4
β’ (π β π½ β Haus) |
43 | | haustop 22705 |
. . . . . . 7
β’ (π½ β Haus β π½ β Top) |
44 | 42, 43 | syl 17 |
. . . . . 6
β’ (π β π½ β Top) |
45 | | toptopon2 22290 |
. . . . . 6
β’ (π½ β Top β π½ β (TopOnββͺ π½)) |
46 | 44, 45 | sylib 217 |
. . . . 5
β’ (π β π½ β (TopOnββͺ π½)) |
47 | | lmcl 22671 |
. . . . 5
β’ ((π½ β (TopOnββͺ π½)
β§ πΉ(βπ‘βπ½)π΄) β π΄ β βͺ π½) |
48 | 46, 5, 47 | syl2anc 585 |
. . . 4
β’ (π β π΄ β βͺ π½) |
49 | | lmcl 22671 |
. . . . 5
β’ ((π½ β (TopOnββͺ π½)
β§ πΉ(βπ‘βπ½)π΅) β π΅ β βͺ π½) |
50 | 46, 12, 49 | syl2anc 585 |
. . . 4
β’ (π β π΅ β βͺ π½) |
51 | | eqid 2733 |
. . . . . 6
β’ βͺ π½ =
βͺ π½ |
52 | 51 | hausnei 22702 |
. . . . 5
β’ ((π½ β Haus β§ (π΄ β βͺ π½
β§ π΅ β βͺ π½
β§ π΄ β π΅)) β βπ₯ β π½ βπ¦ β π½ (π΄ β π₯ β§ π΅ β π¦ β§ (π₯ β© π¦) = β
)) |
53 | 52 | 3exp2 1355 |
. . . 4
β’ (π½ β Haus β (π΄ β βͺ π½
β (π΅ β βͺ π½
β (π΄ β π΅ β βπ₯ β π½ βπ¦ β π½ (π΄ β π₯ β§ π΅ β π¦ β§ (π₯ β© π¦) = β
))))) |
54 | 42, 48, 50, 53 | syl3c 66 |
. . 3
β’ (π β (π΄ β π΅ β βπ₯ β π½ βπ¦ β π½ (π΄ β π₯ β§ π΅ β π¦ β§ (π₯ β© π¦) = β
))) |
55 | 54 | necon1bd 2958 |
. 2
β’ (π β (Β¬ βπ₯ β π½ βπ¦ β π½ (π΄ β π₯ β§ π΅ β π¦ β§ (π₯ β© π¦) = β
) β π΄ = π΅)) |
56 | 41, 55 | mpd 15 |
1
β’ (π β π΄ = π΅) |