Step | Hyp | Ref
| Expression |
1 | | isf32lem.g |
. . . 4
β’ πΏ = (π‘ β πΊ β¦ (β©π (π β Ο β§ π‘ β (πΎβπ )))) |
2 | | ssab2 4076 |
. . . . . . 7
β’ {π β£ (π β Ο β§ π‘ β (πΎβπ ))} β Ο |
3 | | iotacl 6529 |
. . . . . . 7
β’
(β!π (π β Ο β§ π‘ β (πΎβπ )) β (β©π (π β Ο β§ π‘ β (πΎβπ ))) β {π β£ (π β Ο β§ π‘ β (πΎβπ ))}) |
4 | 2, 3 | sselid 3980 |
. . . . . 6
β’
(β!π (π β Ο β§ π‘ β (πΎβπ )) β (β©π (π β Ο β§ π‘ β (πΎβπ ))) β Ο) |
5 | | iotanul 6521 |
. . . . . . 7
β’ (Β¬
β!π (π β Ο β§ π‘ β (πΎβπ )) β (β©π (π β Ο β§ π‘ β (πΎβπ ))) = β
) |
6 | | peano1 7881 |
. . . . . . 7
β’ β
β Ο |
7 | 5, 6 | eqeltrdi 2841 |
. . . . . 6
β’ (Β¬
β!π (π β Ο β§ π‘ β (πΎβπ )) β (β©π (π β Ο β§ π‘ β (πΎβπ ))) β Ο) |
8 | 4, 7 | pm2.61i 182 |
. . . . 5
β’
(β©π (π β Ο β§ π‘ β (πΎβπ ))) β Ο |
9 | 8 | a1i 11 |
. . . 4
β’ (π‘ β πΊ β (β©π (π β Ο β§ π‘ β (πΎβπ ))) β Ο) |
10 | 1, 9 | fmpti 7113 |
. . 3
β’ πΏ:πΊβΆΟ |
11 | 10 | a1i 11 |
. 2
β’ (π β πΏ:πΊβΆΟ) |
12 | | isf32lem.a |
. . . . . 6
β’ (π β πΉ:ΟβΆπ« πΊ) |
13 | | isf32lem.b |
. . . . . 6
β’ (π β βπ₯ β Ο (πΉβsuc π₯) β (πΉβπ₯)) |
14 | | isf32lem.c |
. . . . . 6
β’ (π β Β¬ β© ran πΉ β ran πΉ) |
15 | | isf32lem.d |
. . . . . 6
β’ π = {π¦ β Ο β£ (πΉβsuc π¦) β (πΉβπ¦)} |
16 | | isf32lem.e |
. . . . . 6
β’ π½ = (π’ β Ο β¦ (β©π£ β π (π£ β© π) β π’)) |
17 | | isf32lem.f |
. . . . . 6
β’ πΎ = ((π€ β π β¦ ((πΉβπ€) β (πΉβsuc π€))) β π½) |
18 | 12, 13, 14, 15, 16, 17 | isf32lem6 10355 |
. . . . 5
β’ ((π β§ π β Ο) β (πΎβπ) β β
) |
19 | | n0 4346 |
. . . . 5
β’ ((πΎβπ) β β
β βπ π β (πΎβπ)) |
20 | 18, 19 | sylib 217 |
. . . 4
β’ ((π β§ π β Ο) β βπ π β (πΎβπ)) |
21 | 12, 13, 14, 15, 16, 17 | isf32lem8 10357 |
. . . . . . . . 9
β’ ((π β§ π β Ο) β (πΎβπ) β πΊ) |
22 | 21 | sselda 3982 |
. . . . . . . 8
β’ (((π β§ π β Ο) β§ π β (πΎβπ)) β π β πΊ) |
23 | | eleq1w 2816 |
. . . . . . . . . . . . 13
β’ (π‘ = π β (π‘ β (πΎβπ ) β π β (πΎβπ ))) |
24 | 23 | anbi2d 629 |
. . . . . . . . . . . 12
β’ (π‘ = π β ((π β Ο β§ π‘ β (πΎβπ )) β (π β Ο β§ π β (πΎβπ )))) |
25 | 24 | iotabidv 6527 |
. . . . . . . . . . 11
β’ (π‘ = π β (β©π (π β Ο β§ π‘ β (πΎβπ ))) = (β©π (π β Ο β§ π β (πΎβπ )))) |
26 | | iotaex 6516 |
. . . . . . . . . . 11
β’
(β©π (π β Ο β§ π‘ β (πΎβπ ))) β V |
27 | 25, 1, 26 | fvmpt3i 7003 |
. . . . . . . . . 10
β’ (π β πΊ β (πΏβπ) = (β©π (π β Ο β§ π β (πΎβπ )))) |
28 | 22, 27 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π β Ο) β§ π β (πΎβπ)) β (πΏβπ) = (β©π (π β Ο β§ π β (πΎβπ )))) |
29 | | simp1r 1198 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (πΎβπ)) β§ π β Ο β§ π β Ο) β π β (πΎβπ)) |
30 | | simpl1 1191 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β Ο β§ π β Ο) β§ π β π) β π) |
31 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π β Ο β§ π β Ο) β§ π β π) β π β π) |
32 | 31 | necomd 2996 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β Ο β§ π β Ο) β§ π β π) β π β π ) |
33 | | simpl2 1192 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β Ο β§ π β Ο) β§ π β π) β π β Ο) |
34 | | simpl3 1193 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β Ο β§ π β Ο) β§ π β π) β π β Ο) |
35 | 12, 13, 14, 15, 16, 17 | isf32lem7 10356 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β π ) β§ (π β Ο β§ π β Ο)) β ((πΎβπ) β© (πΎβπ )) = β
) |
36 | 30, 32, 33, 34, 35 | syl22anc 837 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β Ο β§ π β Ο) β§ π β π) β ((πΎβπ) β© (πΎβπ )) = β
) |
37 | | disj1 4450 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((πΎβπ) β© (πΎβπ )) = β
β βπ(π β (πΎβπ) β Β¬ π β (πΎβπ ))) |
38 | 36, 37 | sylib 217 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β Ο β§ π β Ο) β§ π β π) β βπ(π β (πΎβπ) β Β¬ π β (πΎβπ ))) |
39 | 38 | ex 413 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β Ο β§ π β Ο) β (π β π β βπ(π β (πΎβπ) β Β¬ π β (πΎβπ )))) |
40 | | sp 2176 |
. . . . . . . . . . . . . . . . . . 19
β’
(βπ(π β (πΎβπ) β Β¬ π β (πΎβπ )) β (π β (πΎβπ) β Β¬ π β (πΎβπ ))) |
41 | 39, 40 | syl6 35 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β Ο β§ π β Ο) β (π β π β (π β (πΎβπ) β Β¬ π β (πΎβπ )))) |
42 | 41 | com23 86 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β Ο β§ π β Ο) β (π β (πΎβπ) β (π β π β Β¬ π β (πΎβπ )))) |
43 | 42 | 3adant1r 1177 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (πΎβπ)) β§ π β Ο β§ π β Ο) β (π β (πΎβπ) β (π β π β Β¬ π β (πΎβπ )))) |
44 | 29, 43 | mpd 15 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (πΎβπ)) β§ π β Ο β§ π β Ο) β (π β π β Β¬ π β (πΎβπ ))) |
45 | 44 | necon4ad 2959 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (πΎβπ)) β§ π β Ο β§ π β Ο) β (π β (πΎβπ ) β π = π)) |
46 | 45 | 3expia 1121 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (πΎβπ)) β§ π β Ο) β (π β Ο β (π β (πΎβπ ) β π = π))) |
47 | 46 | impd 411 |
. . . . . . . . . . . 12
β’ (((π β§ π β (πΎβπ)) β§ π β Ο) β ((π β Ο β§ π β (πΎβπ )) β π = π)) |
48 | | eleq1w 2816 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (π β Ο β π β Ο)) |
49 | | fveq2 6891 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (πΎβπ ) = (πΎβπ)) |
50 | 49 | eleq2d 2819 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (π β (πΎβπ ) β π β (πΎβπ))) |
51 | 48, 50 | anbi12d 631 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((π β Ο β§ π β (πΎβπ )) β (π β Ο β§ π β (πΎβπ)))) |
52 | 51 | biimprcd 249 |
. . . . . . . . . . . . . 14
β’ ((π β Ο β§ π β (πΎβπ)) β (π = π β (π β Ο β§ π β (πΎβπ )))) |
53 | 52 | ancoms 459 |
. . . . . . . . . . . . 13
β’ ((π β (πΎβπ) β§ π β Ο) β (π = π β (π β Ο β§ π β (πΎβπ )))) |
54 | 53 | adantll 712 |
. . . . . . . . . . . 12
β’ (((π β§ π β (πΎβπ)) β§ π β Ο) β (π = π β (π β Ο β§ π β (πΎβπ )))) |
55 | 47, 54 | impbid 211 |
. . . . . . . . . . 11
β’ (((π β§ π β (πΎβπ)) β§ π β Ο) β ((π β Ο β§ π β (πΎβπ )) β π = π)) |
56 | 55 | iota5 6526 |
. . . . . . . . . 10
β’ (((π β§ π β (πΎβπ)) β§ π β Ο) β (β©π (π β Ο β§ π β (πΎβπ ))) = π) |
57 | 56 | an32s 650 |
. . . . . . . . 9
β’ (((π β§ π β Ο) β§ π β (πΎβπ)) β (β©π (π β Ο β§ π β (πΎβπ ))) = π) |
58 | 28, 57 | eqtr2d 2773 |
. . . . . . . 8
β’ (((π β§ π β Ο) β§ π β (πΎβπ)) β π = (πΏβπ)) |
59 | 22, 58 | jca 512 |
. . . . . . 7
β’ (((π β§ π β Ο) β§ π β (πΎβπ)) β (π β πΊ β§ π = (πΏβπ))) |
60 | 59 | ex 413 |
. . . . . 6
β’ ((π β§ π β Ο) β (π β (πΎβπ) β (π β πΊ β§ π = (πΏβπ)))) |
61 | 60 | eximdv 1920 |
. . . . 5
β’ ((π β§ π β Ο) β (βπ π β (πΎβπ) β βπ(π β πΊ β§ π = (πΏβπ)))) |
62 | | df-rex 3071 |
. . . . 5
β’
(βπ β
πΊ π = (πΏβπ) β βπ(π β πΊ β§ π = (πΏβπ))) |
63 | 61, 62 | imbitrrdi 251 |
. . . 4
β’ ((π β§ π β Ο) β (βπ π β (πΎβπ) β βπ β πΊ π = (πΏβπ))) |
64 | 20, 63 | mpd 15 |
. . 3
β’ ((π β§ π β Ο) β βπ β πΊ π = (πΏβπ)) |
65 | 64 | ralrimiva 3146 |
. 2
β’ (π β βπ β Ο βπ β πΊ π = (πΏβπ)) |
66 | | dffo3 7103 |
. 2
β’ (πΏ:πΊβontoβΟ β (πΏ:πΊβΆΟ β§ βπ β Ο βπ β πΊ π = (πΏβπ))) |
67 | 11, 65, 66 | sylanbrc 583 |
1
β’ (π β πΏ:πΊβontoβΟ) |