Step | Hyp | Ref
| Expression |
1 | | nninffeq.f |
. . 3
β’ (π β πΉ:βββΆβ0) |
2 | 1 | ffnd 5366 |
. 2
β’ (π β πΉ Fn
ββ) |
3 | | nninffeq.g |
. . 3
β’ (π β πΊ:βββΆβ0) |
4 | 3 | ffnd 5366 |
. 2
β’ (π β πΊ Fn
ββ) |
5 | | eqid 2177 |
. . . . . . . 8
β’ (π₯ β
ββ β¦ if((πΉβπ₯) = (πΊβπ₯), 1o, β
)) = (π₯ β
ββ β¦ if((πΉβπ₯) = (πΊβπ₯), 1o, β
)) |
6 | | fveq2 5515 |
. . . . . . . . . 10
β’ (π₯ = π§ β (πΉβπ₯) = (πΉβπ§)) |
7 | | fveq2 5515 |
. . . . . . . . . 10
β’ (π₯ = π§ β (πΊβπ₯) = (πΊβπ§)) |
8 | 6, 7 | eqeq12d 2192 |
. . . . . . . . 9
β’ (π₯ = π§ β ((πΉβπ₯) = (πΊβπ₯) β (πΉβπ§) = (πΊβπ§))) |
9 | 8 | ifbid 3555 |
. . . . . . . 8
β’ (π₯ = π§ β if((πΉβπ₯) = (πΊβπ₯), 1o, β
) = if((πΉβπ§) = (πΊβπ§), 1o, β
)) |
10 | | simpr 110 |
. . . . . . . 8
β’ ((π β§ π§ β ββ) β
π§ β
ββ) |
11 | | 1onn 6520 |
. . . . . . . . . 10
β’
1o β Ο |
12 | 11 | a1i 9 |
. . . . . . . . 9
β’ ((π β§ π§ β ββ) β
1o β Ο) |
13 | | peano1 4593 |
. . . . . . . . . 10
β’ β
β Ο |
14 | 13 | a1i 9 |
. . . . . . . . 9
β’ ((π β§ π§ β ββ) β
β
β Ο) |
15 | 1 | ffvelcdmda 5651 |
. . . . . . . . . . 11
β’ ((π β§ π§ β ββ) β
(πΉβπ§) β
β0) |
16 | 15 | nn0zd 9372 |
. . . . . . . . . 10
β’ ((π β§ π§ β ββ) β
(πΉβπ§) β β€) |
17 | 3 | ffvelcdmda 5651 |
. . . . . . . . . . 11
β’ ((π β§ π§ β ββ) β
(πΊβπ§) β
β0) |
18 | 17 | nn0zd 9372 |
. . . . . . . . . 10
β’ ((π β§ π§ β ββ) β
(πΊβπ§) β β€) |
19 | | zdceq 9327 |
. . . . . . . . . 10
β’ (((πΉβπ§) β β€ β§ (πΊβπ§) β β€) β DECID
(πΉβπ§) = (πΊβπ§)) |
20 | 16, 18, 19 | syl2anc 411 |
. . . . . . . . 9
β’ ((π β§ π§ β ββ) β
DECID (πΉβπ§) = (πΊβπ§)) |
21 | 12, 14, 20 | ifcldcd 3570 |
. . . . . . . 8
β’ ((π β§ π§ β ββ) β
if((πΉβπ§) = (πΊβπ§), 1o, β
) β
Ο) |
22 | 5, 9, 10, 21 | fvmptd3 5609 |
. . . . . . 7
β’ ((π β§ π§ β ββ) β
((π₯ β
ββ β¦ if((πΉβπ₯) = (πΊβπ₯), 1o, β
))βπ§) = if((πΉβπ§) = (πΊβπ§), 1o, β
)) |
23 | | 1lt2o 6442 |
. . . . . . . . . . . . 13
β’
1o β 2o |
24 | 23 | a1i 9 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β ββ) β
1o β 2o) |
25 | | 0lt2o 6441 |
. . . . . . . . . . . . 13
β’ β
β 2o |
26 | 25 | a1i 9 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β ββ) β
β
β 2o) |
27 | 1 | ffvelcdmda 5651 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β ββ) β
(πΉβπ₯) β
β0) |
28 | 27 | nn0zd 9372 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β ββ) β
(πΉβπ₯) β β€) |
29 | 3 | ffvelcdmda 5651 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β ββ) β
(πΊβπ₯) β
β0) |
30 | 29 | nn0zd 9372 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β ββ) β
(πΊβπ₯) β β€) |
31 | | zdceq 9327 |
. . . . . . . . . . . . 13
β’ (((πΉβπ₯) β β€ β§ (πΊβπ₯) β β€) β DECID
(πΉβπ₯) = (πΊβπ₯)) |
32 | 28, 30, 31 | syl2anc 411 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β ββ) β
DECID (πΉβπ₯) = (πΊβπ₯)) |
33 | 24, 26, 32 | ifcldcd 3570 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β ββ) β
if((πΉβπ₯) = (πΊβπ₯), 1o, β
) β
2o) |
34 | 33 | fmpttd 5671 |
. . . . . . . . . 10
β’ (π β (π₯ β ββ β¦
if((πΉβπ₯) = (πΊβπ₯), 1o,
β
)):βββΆ2o) |
35 | | 2onn 6521 |
. . . . . . . . . . . 12
β’
2o β Ο |
36 | 35 | elexi 2749 |
. . . . . . . . . . 11
β’
2o β V |
37 | | nninfex 7119 |
. . . . . . . . . . 11
β’
ββ β V |
38 | 36, 37 | elmap 6676 |
. . . . . . . . . 10
β’ ((π₯ β
ββ β¦ if((πΉβπ₯) = (πΊβπ₯), 1o, β
)) β
(2o βπ ββ) β
(π₯ β
ββ β¦ if((πΉβπ₯) = (πΊβπ₯), 1o,
β
)):βββΆ2o) |
39 | 34, 38 | sylibr 134 |
. . . . . . . . 9
β’ (π β (π₯ β ββ β¦
if((πΉβπ₯) = (πΊβπ₯), 1o, β
)) β
(2o βπ
ββ)) |
40 | | fveq2 5515 |
. . . . . . . . . . . . 13
β’ (π₯ = (π€ β Ο β¦ 1o) β
(πΉβπ₯) = (πΉβ(π€ β Ο β¦
1o))) |
41 | | fveq2 5515 |
. . . . . . . . . . . . 13
β’ (π₯ = (π€ β Ο β¦ 1o) β
(πΊβπ₯) = (πΊβ(π€ β Ο β¦
1o))) |
42 | 40, 41 | eqeq12d 2192 |
. . . . . . . . . . . 12
β’ (π₯ = (π€ β Ο β¦ 1o) β
((πΉβπ₯) = (πΊβπ₯) β (πΉβ(π€ β Ο β¦ 1o)) =
(πΊβ(π€ β Ο β¦
1o)))) |
43 | 42 | ifbid 3555 |
. . . . . . . . . . 11
β’ (π₯ = (π€ β Ο β¦ 1o) β
if((πΉβπ₯) = (πΊβπ₯), 1o, β
) = if((πΉβ(π€ β Ο β¦ 1o)) =
(πΊβ(π€ β Ο β¦
1o)), 1o, β
)) |
44 | | infnninf 7121 |
. . . . . . . . . . . 12
β’ (π€ β Ο β¦
1o) β ββ |
45 | 44 | a1i 9 |
. . . . . . . . . . 11
β’ (π β (π€ β Ο β¦ 1o) β
ββ) |
46 | | nninffeq.oo |
. . . . . . . . . . . . . 14
β’ (π β (πΉβ(π₯ β Ο β¦ 1o)) =
(πΊβ(π₯ β Ο β¦
1o))) |
47 | | eqidd 2178 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π€ β 1o =
1o) |
48 | 47 | cbvmptv 4099 |
. . . . . . . . . . . . . . 15
β’ (π₯ β Ο β¦
1o) = (π€ β
Ο β¦ 1o) |
49 | 48 | fveq2i 5518 |
. . . . . . . . . . . . . 14
β’ (πΉβ(π₯ β Ο β¦ 1o)) =
(πΉβ(π€ β Ο β¦
1o)) |
50 | 48 | fveq2i 5518 |
. . . . . . . . . . . . . 14
β’ (πΊβ(π₯ β Ο β¦ 1o)) =
(πΊβ(π€ β Ο β¦
1o)) |
51 | 46, 49, 50 | 3eqtr3g 2233 |
. . . . . . . . . . . . 13
β’ (π β (πΉβ(π€ β Ο β¦ 1o)) =
(πΊβ(π€ β Ο β¦
1o))) |
52 | 51 | iftrued 3541 |
. . . . . . . . . . . 12
β’ (π β if((πΉβ(π€ β Ο β¦ 1o)) =
(πΊβ(π€ β Ο β¦
1o)), 1o, β
) = 1o) |
53 | 52, 11 | eqeltrdi 2268 |
. . . . . . . . . . 11
β’ (π β if((πΉβ(π€ β Ο β¦ 1o)) =
(πΊβ(π€ β Ο β¦
1o)), 1o, β
) β Ο) |
54 | 5, 43, 45, 53 | fvmptd3 5609 |
. . . . . . . . . 10
β’ (π β ((π₯ β ββ β¦
if((πΉβπ₯) = (πΊβπ₯), 1o, β
))β(π€ β Ο β¦
1o)) = if((πΉβ(π€ β Ο β¦ 1o)) =
(πΊβ(π€ β Ο β¦
1o)), 1o, β
)) |
55 | 54, 52 | eqtrd 2210 |
. . . . . . . . 9
β’ (π β ((π₯ β ββ β¦
if((πΉβπ₯) = (πΊβπ₯), 1o, β
))β(π€ β Ο β¦
1o)) = 1o) |
56 | | nninffeq.n |
. . . . . . . . . 10
β’ (π β βπ β Ο (πΉβ(π β Ο β¦ if(π β π, 1o, β
))) = (πΊβ(π β Ο β¦ if(π β π, 1o, β
)))) |
57 | | fveq2 5515 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = (π β Ο β¦ if(π β π, 1o, β
)) β (πΉβπ₯) = (πΉβ(π β Ο β¦ if(π β π, 1o, β
)))) |
58 | | fveq2 5515 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = (π β Ο β¦ if(π β π, 1o, β
)) β (πΊβπ₯) = (πΊβ(π β Ο β¦ if(π β π, 1o, β
)))) |
59 | 57, 58 | eqeq12d 2192 |
. . . . . . . . . . . . . . 15
β’ (π₯ = (π β Ο β¦ if(π β π, 1o, β
)) β ((πΉβπ₯) = (πΊβπ₯) β (πΉβ(π β Ο β¦ if(π β π, 1o, β
))) = (πΊβ(π β Ο β¦ if(π β π, 1o,
β
))))) |
60 | 59 | ifbid 3555 |
. . . . . . . . . . . . . 14
β’ (π₯ = (π β Ο β¦ if(π β π, 1o, β
)) β if((πΉβπ₯) = (πΊβπ₯), 1o, β
) = if((πΉβ(π β Ο β¦ if(π β π, 1o, β
))) = (πΊβ(π β Ο β¦ if(π β π, 1o, β
))), 1o,
β
)) |
61 | | nnnninf 7123 |
. . . . . . . . . . . . . . 15
β’ (π β Ο β (π β Ο β¦ if(π β π, 1o, β
)) β
ββ) |
62 | 61 | ad2antlr 489 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β Ο) β§ (πΉβ(π β Ο β¦ if(π β π, 1o, β
))) = (πΊβ(π β Ο β¦ if(π β π, 1o, β
)))) β (π β Ο β¦ if(π β π, 1o, β
)) β
ββ) |
63 | | simpr 110 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β Ο) β§ (πΉβ(π β Ο β¦ if(π β π, 1o, β
))) = (πΊβ(π β Ο β¦ if(π β π, 1o, β
)))) β (πΉβ(π β Ο β¦ if(π β π, 1o, β
))) = (πΊβ(π β Ο β¦ if(π β π, 1o, β
)))) |
64 | 63 | iftrued 3541 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β Ο) β§ (πΉβ(π β Ο β¦ if(π β π, 1o, β
))) = (πΊβ(π β Ο β¦ if(π β π, 1o, β
)))) β if((πΉβ(π β Ο β¦ if(π β π, 1o, β
))) = (πΊβ(π β Ο β¦ if(π β π, 1o, β
))), 1o,
β
) = 1o) |
65 | 64, 11 | eqeltrdi 2268 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β Ο) β§ (πΉβ(π β Ο β¦ if(π β π, 1o, β
))) = (πΊβ(π β Ο β¦ if(π β π, 1o, β
)))) β if((πΉβ(π β Ο β¦ if(π β π, 1o, β
))) = (πΊβ(π β Ο β¦ if(π β π, 1o, β
))), 1o,
β
) β Ο) |
66 | 5, 60, 62, 65 | fvmptd3 5609 |
. . . . . . . . . . . . 13
β’ (((π β§ π β Ο) β§ (πΉβ(π β Ο β¦ if(π β π, 1o, β
))) = (πΊβ(π β Ο β¦ if(π β π, 1o, β
)))) β ((π₯ β
ββ β¦ if((πΉβπ₯) = (πΊβπ₯), 1o, β
))β(π β Ο β¦ if(π β π, 1o, β
))) = if((πΉβ(π β Ο β¦ if(π β π, 1o, β
))) = (πΊβ(π β Ο β¦ if(π β π, 1o, β
))), 1o,
β
)) |
67 | 66, 64 | eqtrd 2210 |
. . . . . . . . . . . 12
β’ (((π β§ π β Ο) β§ (πΉβ(π β Ο β¦ if(π β π, 1o, β
))) = (πΊβ(π β Ο β¦ if(π β π, 1o, β
)))) β ((π₯ β
ββ β¦ if((πΉβπ₯) = (πΊβπ₯), 1o, β
))β(π β Ο β¦ if(π β π, 1o, β
))) =
1o) |
68 | 67 | ex 115 |
. . . . . . . . . . 11
β’ ((π β§ π β Ο) β ((πΉβ(π β Ο β¦ if(π β π, 1o, β
))) = (πΊβ(π β Ο β¦ if(π β π, 1o, β
))) β ((π₯ β
ββ β¦ if((πΉβπ₯) = (πΊβπ₯), 1o, β
))β(π β Ο β¦ if(π β π, 1o, β
))) =
1o)) |
69 | 68 | ralimdva 2544 |
. . . . . . . . . 10
β’ (π β (βπ β Ο (πΉβ(π β Ο β¦ if(π β π, 1o, β
))) = (πΊβ(π β Ο β¦ if(π β π, 1o, β
))) β
βπ β Ο
((π₯ β
ββ β¦ if((πΉβπ₯) = (πΊβπ₯), 1o, β
))β(π β Ο β¦ if(π β π, 1o, β
))) =
1o)) |
70 | 56, 69 | mpd 13 |
. . . . . . . . 9
β’ (π β βπ β Ο ((π₯ β ββ β¦
if((πΉβπ₯) = (πΊβπ₯), 1o, β
))β(π β Ο β¦ if(π β π, 1o, β
))) =
1o) |
71 | 39, 55, 70 | nninfall 14728 |
. . . . . . . 8
β’ (π β βπ§ β ββ ((π₯ β
ββ β¦ if((πΉβπ₯) = (πΊβπ₯), 1o, β
))βπ§) =
1o) |
72 | 71 | r19.21bi 2565 |
. . . . . . 7
β’ ((π β§ π§ β ββ) β
((π₯ β
ββ β¦ if((πΉβπ₯) = (πΊβπ₯), 1o, β
))βπ§) =
1o) |
73 | 22, 72 | eqtr3d 2212 |
. . . . . 6
β’ ((π β§ π§ β ββ) β
if((πΉβπ§) = (πΊβπ§), 1o, β
) =
1o) |
74 | 73 | adantr 276 |
. . . . 5
β’ (((π β§ π§ β ββ) β§
Β¬ (πΉβπ§) = (πΊβπ§)) β if((πΉβπ§) = (πΊβπ§), 1o, β
) =
1o) |
75 | | simpr 110 |
. . . . . 6
β’ (((π β§ π§ β ββ) β§
Β¬ (πΉβπ§) = (πΊβπ§)) β Β¬ (πΉβπ§) = (πΊβπ§)) |
76 | 75 | iffalsed 3544 |
. . . . 5
β’ (((π β§ π§ β ββ) β§
Β¬ (πΉβπ§) = (πΊβπ§)) β if((πΉβπ§) = (πΊβπ§), 1o, β
) =
β
) |
77 | 74, 76 | eqtr3d 2212 |
. . . 4
β’ (((π β§ π§ β ββ) β§
Β¬ (πΉβπ§) = (πΊβπ§)) β 1o =
β
) |
78 | | 1n0 6432 |
. . . . . 6
β’
1o β β
|
79 | 78 | neii 2349 |
. . . . 5
β’ Β¬
1o = β
|
80 | 79 | a1i 9 |
. . . 4
β’ (((π β§ π§ β ββ) β§
Β¬ (πΉβπ§) = (πΊβπ§)) β Β¬ 1o =
β
) |
81 | 77, 80 | pm2.65da 661 |
. . 3
β’ ((π β§ π§ β ββ) β
Β¬ Β¬ (πΉβπ§) = (πΊβπ§)) |
82 | | exmiddc 836 |
. . . 4
β’
(DECID (πΉβπ§) = (πΊβπ§) β ((πΉβπ§) = (πΊβπ§) β¨ Β¬ (πΉβπ§) = (πΊβπ§))) |
83 | 20, 82 | syl 14 |
. . 3
β’ ((π β§ π§ β ββ) β
((πΉβπ§) = (πΊβπ§) β¨ Β¬ (πΉβπ§) = (πΊβπ§))) |
84 | 81, 83 | ecased 1349 |
. 2
β’ ((π β§ π§ β ββ) β
(πΉβπ§) = (πΊβπ§)) |
85 | 2, 4, 84 | eqfnfvd 5616 |
1
β’ (π β πΉ = πΊ) |