Step | Hyp | Ref
| Expression |
1 | | fodjum.z |
. 2
β’ (π β βπ€ β π (πβπ€) = β
) |
2 | | 1n0 6432 |
. . . . . . . . 9
β’
1o β β
|
3 | 2 | nesymi 2393 |
. . . . . . . 8
β’ Β¬
β
= 1o |
4 | 3 | intnan 929 |
. . . . . . 7
β’ Β¬
(Β¬ βπ§ β
π΄ (πΉβπ€) = (inlβπ§) β§ β
=
1o) |
5 | 4 | a1i 9 |
. . . . . 6
β’ ((π β§ (π€ β π β§ (πβπ€) = β
)) β Β¬ (Β¬
βπ§ β π΄ (πΉβπ€) = (inlβπ§) β§ β
=
1o)) |
6 | | simprr 531 |
. . . . . . . 8
β’ ((π β§ (π€ β π β§ (πβπ€) = β
)) β (πβπ€) = β
) |
7 | | fodjuf.p |
. . . . . . . . 9
β’ π = (π¦ β π β¦ if(βπ§ β π΄ (πΉβπ¦) = (inlβπ§), β
, 1o)) |
8 | | fveqeq2 5524 |
. . . . . . . . . . 11
β’ (π¦ = π€ β ((πΉβπ¦) = (inlβπ§) β (πΉβπ€) = (inlβπ§))) |
9 | 8 | rexbidv 2478 |
. . . . . . . . . 10
β’ (π¦ = π€ β (βπ§ β π΄ (πΉβπ¦) = (inlβπ§) β βπ§ β π΄ (πΉβπ€) = (inlβπ§))) |
10 | 9 | ifbid 3555 |
. . . . . . . . 9
β’ (π¦ = π€ β if(βπ§ β π΄ (πΉβπ¦) = (inlβπ§), β
, 1o) = if(βπ§ β π΄ (πΉβπ€) = (inlβπ§), β
, 1o)) |
11 | | simprl 529 |
. . . . . . . . 9
β’ ((π β§ (π€ β π β§ (πβπ€) = β
)) β π€ β π) |
12 | | peano1 4593 |
. . . . . . . . . . 11
β’ β
β Ο |
13 | 12 | a1i 9 |
. . . . . . . . . 10
β’ ((π β§ (π€ β π β§ (πβπ€) = β
)) β β
β
Ο) |
14 | | 1onn 6520 |
. . . . . . . . . . 11
β’
1o β Ο |
15 | 14 | a1i 9 |
. . . . . . . . . 10
β’ ((π β§ (π€ β π β§ (πβπ€) = β
)) β 1o β
Ο) |
16 | | fodjuf.fo |
. . . . . . . . . . . 12
β’ (π β πΉ:πβontoβ(π΄ β π΅)) |
17 | 16 | fodjuomnilemdc 7141 |
. . . . . . . . . . 11
β’ ((π β§ π€ β π) β DECID βπ§ β π΄ (πΉβπ€) = (inlβπ§)) |
18 | 17 | adantrr 479 |
. . . . . . . . . 10
β’ ((π β§ (π€ β π β§ (πβπ€) = β
)) β DECID
βπ§ β π΄ (πΉβπ€) = (inlβπ§)) |
19 | 13, 15, 18 | ifcldcd 3570 |
. . . . . . . . 9
β’ ((π β§ (π€ β π β§ (πβπ€) = β
)) β if(βπ§ β π΄ (πΉβπ€) = (inlβπ§), β
, 1o) β
Ο) |
20 | 7, 10, 11, 19 | fvmptd3 5609 |
. . . . . . . 8
β’ ((π β§ (π€ β π β§ (πβπ€) = β
)) β (πβπ€) = if(βπ§ β π΄ (πΉβπ€) = (inlβπ§), β
, 1o)) |
21 | 6, 20 | eqtr3d 2212 |
. . . . . . 7
β’ ((π β§ (π€ β π β§ (πβπ€) = β
)) β β
=
if(βπ§ β π΄ (πΉβπ€) = (inlβπ§), β
, 1o)) |
22 | | eqifdc 3569 |
. . . . . . . 8
β’
(DECID βπ§ β π΄ (πΉβπ€) = (inlβπ§) β (β
= if(βπ§ β π΄ (πΉβπ€) = (inlβπ§), β
, 1o) β
((βπ§ β π΄ (πΉβπ€) = (inlβπ§) β§ β
= β
) β¨ (Β¬
βπ§ β π΄ (πΉβπ€) = (inlβπ§) β§ β
=
1o)))) |
23 | 18, 22 | syl 14 |
. . . . . . 7
β’ ((π β§ (π€ β π β§ (πβπ€) = β
)) β (β
=
if(βπ§ β π΄ (πΉβπ€) = (inlβπ§), β
, 1o) β
((βπ§ β π΄ (πΉβπ€) = (inlβπ§) β§ β
= β
) β¨ (Β¬
βπ§ β π΄ (πΉβπ€) = (inlβπ§) β§ β
=
1o)))) |
24 | 21, 23 | mpbid 147 |
. . . . . 6
β’ ((π β§ (π€ β π β§ (πβπ€) = β
)) β ((βπ§ β π΄ (πΉβπ€) = (inlβπ§) β§ β
= β
) β¨ (Β¬
βπ§ β π΄ (πΉβπ€) = (inlβπ§) β§ β
=
1o))) |
25 | 5, 24 | ecased 1349 |
. . . . 5
β’ ((π β§ (π€ β π β§ (πβπ€) = β
)) β (βπ§ β π΄ (πΉβπ€) = (inlβπ§) β§ β
= β
)) |
26 | 25 | simpld 112 |
. . . 4
β’ ((π β§ (π€ β π β§ (πβπ€) = β
)) β βπ§ β π΄ (πΉβπ€) = (inlβπ§)) |
27 | | rexm 3522 |
. . . 4
β’
(βπ§ β
π΄ (πΉβπ€) = (inlβπ§) β βπ§ π§ β π΄) |
28 | 26, 27 | syl 14 |
. . 3
β’ ((π β§ (π€ β π β§ (πβπ€) = β
)) β βπ§ π§ β π΄) |
29 | | eleq1w 2238 |
. . . 4
β’ (π§ = π₯ β (π§ β π΄ β π₯ β π΄)) |
30 | 29 | cbvexv 1918 |
. . 3
β’
(βπ§ π§ β π΄ β βπ₯ π₯ β π΄) |
31 | 28, 30 | sylib 122 |
. 2
β’ ((π β§ (π€ β π β§ (πβπ€) = β
)) β βπ₯ π₯ β π΄) |
32 | 1, 31 | rexlimddv 2599 |
1
β’ (π β βπ₯ π₯ β π΄) |