Step | Hyp | Ref
| Expression |
1 | | omp1eom.f |
. . 3
β’ πΉ = (π₯ β Ο β¦ if(π₯ = β
, (inrβπ₯), (inlββͺ
π₯))) |
2 | | el1o 6440 |
. . . . . . 7
β’ (π₯ β 1o β
π₯ =
β
) |
3 | 2 | biimpri 133 |
. . . . . 6
β’ (π₯ = β
β π₯ β
1o) |
4 | 3 | adantl 277 |
. . . . 5
β’
(((β€ β§ π₯
β Ο) β§ π₯ =
β
) β π₯ β
1o) |
5 | | djurcl 7053 |
. . . . 5
β’ (π₯ β 1o β
(inrβπ₯) β
(Ο β 1o)) |
6 | 4, 5 | syl 14 |
. . . 4
β’
(((β€ β§ π₯
β Ο) β§ π₯ =
β
) β (inrβπ₯) β (Ο β
1o)) |
7 | | nnpredcl 4624 |
. . . . . 6
β’ (π₯ β Ο β βͺ π₯
β Ο) |
8 | 7 | ad2antlr 489 |
. . . . 5
β’
(((β€ β§ π₯
β Ο) β§ Β¬ π₯ = β
) β βͺ π₯
β Ο) |
9 | | djulcl 7052 |
. . . . 5
β’ (βͺ π₯
β Ο β (inlββͺ π₯) β (Ο β
1o)) |
10 | 8, 9 | syl 14 |
. . . 4
β’
(((β€ β§ π₯
β Ο) β§ Β¬ π₯ = β
) β (inlββͺ π₯)
β (Ο β 1o)) |
11 | | nndceq0 4619 |
. . . . 5
β’ (π₯ β Ο β
DECID π₯ =
β
) |
12 | 11 | adantl 277 |
. . . 4
β’
((β€ β§ π₯
β Ο) β DECID π₯ = β
) |
13 | 6, 10, 12 | ifcldadc 3565 |
. . 3
β’
((β€ β§ π₯
β Ο) β if(π₯
= β
, (inrβπ₯),
(inlββͺ π₯)) β (Ο β
1o)) |
14 | | omp1eom.s |
. . . . . . . 8
β’ π = (π₯ β Ο β¦ suc π₯) |
15 | | peano2 4596 |
. . . . . . . 8
β’ (π₯ β Ο β suc π₯ β
Ο) |
16 | 14, 15 | fmpti 5670 |
. . . . . . 7
β’ π:ΟβΆΟ |
17 | 16 | a1i 9 |
. . . . . 6
β’ (β€
β π:ΟβΆΟ) |
18 | | f1oi 5501 |
. . . . . . . . 9
β’ ( I
βΎ 1o):1oβ1-1-ontoβ1o |
19 | | f1of 5463 |
. . . . . . . . 9
β’ (( I
βΎ 1o):1oβ1-1-ontoβ1o β ( I βΎ
1o):1oβΆ1o) |
20 | 18, 19 | ax-mp 5 |
. . . . . . . 8
β’ ( I
βΎ 1o):1oβΆ1o |
21 | | 1onn 6523 |
. . . . . . . . 9
β’
1o β Ο |
22 | | omelon 4610 |
. . . . . . . . . 10
β’ Ο
β On |
23 | 22 | onelssi 4431 |
. . . . . . . . 9
β’
(1o β Ο β 1o β
Ο) |
24 | 21, 23 | ax-mp 5 |
. . . . . . . 8
β’
1o β Ο |
25 | | fss 5379 |
. . . . . . . 8
β’ ((( I
βΎ 1o):1oβΆ1o β§ 1o
β Ο) β ( I βΎ
1o):1oβΆΟ) |
26 | 20, 24, 25 | mp2an 426 |
. . . . . . 7
β’ ( I
βΎ 1o):1oβΆΟ |
27 | 26 | a1i 9 |
. . . . . 6
β’ (β€
β ( I βΎ
1o):1oβΆΟ) |
28 | 17, 27 | casef 7089 |
. . . . 5
β’ (β€
β case(π, ( I βΎ
1o)):(Ο β
1o)βΆΟ) |
29 | | omp1eom.g |
. . . . . 6
β’ πΊ = case(π, ( I βΎ
1o)) |
30 | 29 | feq1i 5360 |
. . . . 5
β’ (πΊ:(Ο β
1o)βΆΟ β case(π, ( I βΎ 1o)):(Ο
β 1o)βΆΟ) |
31 | 28, 30 | sylibr 134 |
. . . 4
β’ (β€
β πΊ:(Ο β
1o)βΆΟ) |
32 | 31 | ffvelcdmda 5653 |
. . 3
β’
((β€ β§ π¦
β (Ο β 1o)) β (πΊβπ¦) β Ο) |
33 | | ffn 5367 |
. . . . . . . . . . . . . . . 16
β’ (π:ΟβΆΟ β
π Fn
Ο) |
34 | 16, 33 | mp1i 10 |
. . . . . . . . . . . . . . 15
β’ ((π§ β Ο β§ π¦ = (inlβπ§)) β π Fn Ο) |
35 | | ffun 5370 |
. . . . . . . . . . . . . . . 16
β’ (( I
βΎ 1o):1oβΆ1o β Fun ( I
βΎ 1o)) |
36 | 20, 35 | mp1i 10 |
. . . . . . . . . . . . . . 15
β’ ((π§ β Ο β§ π¦ = (inlβπ§)) β Fun ( I βΎ
1o)) |
37 | | simpl 109 |
. . . . . . . . . . . . . . 15
β’ ((π§ β Ο β§ π¦ = (inlβπ§)) β π§ β Ο) |
38 | 34, 36, 37 | caseinl 7092 |
. . . . . . . . . . . . . 14
β’ ((π§ β Ο β§ π¦ = (inlβπ§)) β (case(π, ( I βΎ
1o))β(inlβπ§)) = (πβπ§)) |
39 | 29 | eqcomi 2181 |
. . . . . . . . . . . . . . . 16
β’
case(π, ( I βΎ
1o)) = πΊ |
40 | 39 | a1i 9 |
. . . . . . . . . . . . . . 15
β’ ((π§ β Ο β§ π¦ = (inlβπ§)) β case(π, ( I βΎ 1o)) = πΊ) |
41 | | simpr 110 |
. . . . . . . . . . . . . . . 16
β’ ((π§ β Ο β§ π¦ = (inlβπ§)) β π¦ = (inlβπ§)) |
42 | 41 | eqcomd 2183 |
. . . . . . . . . . . . . . 15
β’ ((π§ β Ο β§ π¦ = (inlβπ§)) β (inlβπ§) = π¦) |
43 | 40, 42 | fveq12d 5524 |
. . . . . . . . . . . . . 14
β’ ((π§ β Ο β§ π¦ = (inlβπ§)) β (case(π, ( I βΎ
1o))β(inlβπ§)) = (πΊβπ¦)) |
44 | | peano2 4596 |
. . . . . . . . . . . . . . . 16
β’ (π§ β Ο β suc π§ β
Ο) |
45 | | suceq 4404 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π§ β suc π₯ = suc π§) |
46 | 45, 14 | fvmptg 5594 |
. . . . . . . . . . . . . . . 16
β’ ((π§ β Ο β§ suc π§ β Ο) β (πβπ§) = suc π§) |
47 | 44, 46 | mpdan 421 |
. . . . . . . . . . . . . . 15
β’ (π§ β Ο β (πβπ§) = suc π§) |
48 | 47 | adantr 276 |
. . . . . . . . . . . . . 14
β’ ((π§ β Ο β§ π¦ = (inlβπ§)) β (πβπ§) = suc π§) |
49 | 38, 43, 48 | 3eqtr3d 2218 |
. . . . . . . . . . . . 13
β’ ((π§ β Ο β§ π¦ = (inlβπ§)) β (πΊβπ¦) = suc π§) |
50 | | peano3 4597 |
. . . . . . . . . . . . . 14
β’ (π§ β Ο β suc π§ β β
) |
51 | 50 | adantr 276 |
. . . . . . . . . . . . 13
β’ ((π§ β Ο β§ π¦ = (inlβπ§)) β suc π§ β β
) |
52 | 49, 51 | eqnetrd 2371 |
. . . . . . . . . . . 12
β’ ((π§ β Ο β§ π¦ = (inlβπ§)) β (πΊβπ¦) β β
) |
53 | 52 | adantl 277 |
. . . . . . . . . . 11
β’ ((((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ π₯ =
β
) β§ (π§ β
Ο β§ π¦ =
(inlβπ§))) β
(πΊβπ¦) β β
) |
54 | 53 | necomd 2433 |
. . . . . . . . . 10
β’ ((((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ π₯ =
β
) β§ (π§ β
Ο β§ π¦ =
(inlβπ§))) β
β
β (πΊβπ¦)) |
55 | 54 | neneqd 2368 |
. . . . . . . . 9
β’ ((((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ π₯ =
β
) β§ (π§ β
Ο β§ π¦ =
(inlβπ§))) β
Β¬ β
= (πΊβπ¦)) |
56 | | simplr 528 |
. . . . . . . . . 10
β’ ((((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ π₯ =
β
) β§ (π§ β
Ο β§ π¦ =
(inlβπ§))) β
π₯ =
β
) |
57 | 56 | eqeq1d 2186 |
. . . . . . . . 9
β’ ((((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ π₯ =
β
) β§ (π§ β
Ο β§ π¦ =
(inlβπ§))) β
(π₯ = (πΊβπ¦) β β
= (πΊβπ¦))) |
58 | 55, 57 | mtbird 673 |
. . . . . . . 8
β’ ((((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ π₯ =
β
) β§ (π§ β
Ο β§ π¦ =
(inlβπ§))) β
Β¬ π₯ = (πΊβπ¦)) |
59 | | djune 7079 |
. . . . . . . . . . . 12
β’ ((π§ β V β§ π₯ β V) β
(inlβπ§) β
(inrβπ₯)) |
60 | 59 | elvd 2744 |
. . . . . . . . . . 11
β’ (π§ β V β
(inlβπ§) β
(inrβπ₯)) |
61 | 60 | elv 2743 |
. . . . . . . . . 10
β’
(inlβπ§) β
(inrβπ₯) |
62 | 61 | neii 2349 |
. . . . . . . . 9
β’ Β¬
(inlβπ§) =
(inrβπ₯) |
63 | | simprr 531 |
. . . . . . . . . 10
β’ ((((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ π₯ =
β
) β§ (π§ β
Ο β§ π¦ =
(inlβπ§))) β
π¦ = (inlβπ§)) |
64 | | simpr 110 |
. . . . . . . . . . . 12
β’ (((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ π₯ =
β
) β π₯ =
β
) |
65 | 64 | iftrued 3543 |
. . . . . . . . . . 11
β’ (((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ π₯ =
β
) β if(π₯ =
β
, (inrβπ₯),
(inlββͺ π₯)) = (inrβπ₯)) |
66 | 65 | adantr 276 |
. . . . . . . . . 10
β’ ((((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ π₯ =
β
) β§ (π§ β
Ο β§ π¦ =
(inlβπ§))) β
if(π₯ = β
,
(inrβπ₯),
(inlββͺ π₯)) = (inrβπ₯)) |
67 | 63, 66 | eqeq12d 2192 |
. . . . . . . . 9
β’ ((((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ π₯ =
β
) β§ (π§ β
Ο β§ π¦ =
(inlβπ§))) β
(π¦ = if(π₯ = β
, (inrβπ₯), (inlββͺ
π₯)) β (inlβπ§) = (inrβπ₯))) |
68 | 62, 67 | mtbiri 675 |
. . . . . . . 8
β’ ((((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ π₯ =
β
) β§ (π§ β
Ο β§ π¦ =
(inlβπ§))) β
Β¬ π¦ = if(π₯ = β
, (inrβπ₯), (inlββͺ π₯))) |
69 | 58, 68 | 2falsed 702 |
. . . . . . 7
β’ ((((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ π₯ =
β
) β§ (π§ β
Ο β§ π¦ =
(inlβπ§))) β
(π₯ = (πΊβπ¦) β π¦ = if(π₯ = β
, (inrβπ₯), (inlββͺ
π₯)))) |
70 | 69 | rexlimdvaa 2595 |
. . . . . 6
β’ (((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ π₯ =
β
) β (βπ§
β Ο π¦ =
(inlβπ§) β (π₯ = (πΊβπ¦) β π¦ = if(π₯ = β
, (inrβπ₯), (inlββͺ
π₯))))) |
71 | | simplr 528 |
. . . . . . . . 9
β’ ((((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ π₯ =
β
) β§ (π§ β
1o β§ π¦ =
(inrβπ§))) β
π₯ =
β
) |
72 | 29 | a1i 9 |
. . . . . . . . . . . 12
β’ ((π§ β 1o β§
π¦ = (inrβπ§)) β πΊ = case(π, ( I βΎ
1o))) |
73 | | simpr 110 |
. . . . . . . . . . . 12
β’ ((π§ β 1o β§
π¦ = (inrβπ§)) β π¦ = (inrβπ§)) |
74 | 72, 73 | fveq12d 5524 |
. . . . . . . . . . 11
β’ ((π§ β 1o β§
π¦ = (inrβπ§)) β (πΊβπ¦) = (case(π, ( I βΎ
1o))β(inrβπ§))) |
75 | 14 | funmpt2 5257 |
. . . . . . . . . . . . . 14
β’ Fun π |
76 | 75 | a1i 9 |
. . . . . . . . . . . . 13
β’ ((π§ β 1o β§
π¦ = (inrβπ§)) β Fun π) |
77 | | fnresi 5335 |
. . . . . . . . . . . . . 14
β’ ( I
βΎ 1o) Fn 1o |
78 | 77 | a1i 9 |
. . . . . . . . . . . . 13
β’ ((π§ β 1o β§
π¦ = (inrβπ§)) β ( I βΎ
1o) Fn 1o) |
79 | | simpl 109 |
. . . . . . . . . . . . 13
β’ ((π§ β 1o β§
π¦ = (inrβπ§)) β π§ β 1o) |
80 | 76, 78, 79 | caseinr 7093 |
. . . . . . . . . . . 12
β’ ((π§ β 1o β§
π¦ = (inrβπ§)) β (case(π, ( I βΎ
1o))β(inrβπ§)) = (( I βΎ 1o)βπ§)) |
81 | | fvresi 5711 |
. . . . . . . . . . . . 13
β’ (π§ β 1o β ((
I βΎ 1o)βπ§) = π§) |
82 | 81 | adantr 276 |
. . . . . . . . . . . 12
β’ ((π§ β 1o β§
π¦ = (inrβπ§)) β (( I βΎ
1o)βπ§) =
π§) |
83 | 80, 82 | eqtrd 2210 |
. . . . . . . . . . 11
β’ ((π§ β 1o β§
π¦ = (inrβπ§)) β (case(π, ( I βΎ
1o))β(inrβπ§)) = π§) |
84 | | el1o 6440 |
. . . . . . . . . . . 12
β’ (π§ β 1o β
π§ =
β
) |
85 | 79, 84 | sylib 122 |
. . . . . . . . . . 11
β’ ((π§ β 1o β§
π¦ = (inrβπ§)) β π§ = β
) |
86 | 74, 83, 85 | 3eqtrd 2214 |
. . . . . . . . . 10
β’ ((π§ β 1o β§
π¦ = (inrβπ§)) β (πΊβπ¦) = β
) |
87 | 86 | adantl 277 |
. . . . . . . . 9
β’ ((((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ π₯ =
β
) β§ (π§ β
1o β§ π¦ =
(inrβπ§))) β
(πΊβπ¦) = β
) |
88 | 71, 87 | eqtr4d 2213 |
. . . . . . . 8
β’ ((((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ π₯ =
β
) β§ (π§ β
1o β§ π¦ =
(inrβπ§))) β
π₯ = (πΊβπ¦)) |
89 | 85 | adantl 277 |
. . . . . . . . . . 11
β’ ((((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ π₯ =
β
) β§ (π§ β
1o β§ π¦ =
(inrβπ§))) β
π§ =
β
) |
90 | 71, 89 | eqtr4d 2213 |
. . . . . . . . . 10
β’ ((((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ π₯ =
β
) β§ (π§ β
1o β§ π¦ =
(inrβπ§))) β
π₯ = π§) |
91 | 90 | fveq2d 5521 |
. . . . . . . . 9
β’ ((((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ π₯ =
β
) β§ (π§ β
1o β§ π¦ =
(inrβπ§))) β
(inrβπ₯) =
(inrβπ§)) |
92 | 65 | adantr 276 |
. . . . . . . . 9
β’ ((((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ π₯ =
β
) β§ (π§ β
1o β§ π¦ =
(inrβπ§))) β
if(π₯ = β
,
(inrβπ₯),
(inlββͺ π₯)) = (inrβπ₯)) |
93 | | simprr 531 |
. . . . . . . . 9
β’ ((((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ π₯ =
β
) β§ (π§ β
1o β§ π¦ =
(inrβπ§))) β
π¦ = (inrβπ§)) |
94 | 91, 92, 93 | 3eqtr4rd 2221 |
. . . . . . . 8
β’ ((((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ π₯ =
β
) β§ (π§ β
1o β§ π¦ =
(inrβπ§))) β
π¦ = if(π₯ = β
, (inrβπ₯), (inlββͺ
π₯))) |
95 | 88, 94 | 2thd 175 |
. . . . . . 7
β’ ((((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ π₯ =
β
) β§ (π§ β
1o β§ π¦ =
(inrβπ§))) β
(π₯ = (πΊβπ¦) β π¦ = if(π₯ = β
, (inrβπ₯), (inlββͺ
π₯)))) |
96 | 95 | rexlimdvaa 2595 |
. . . . . 6
β’ (((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ π₯ =
β
) β (βπ§
β 1o π¦ =
(inrβπ§) β (π₯ = (πΊβπ¦) β π¦ = if(π₯ = β
, (inrβπ₯), (inlββͺ
π₯))))) |
97 | | djur 7070 |
. . . . . . . 8
β’ (π¦ β (Ο β
1o) β (βπ§ β Ο π¦ = (inlβπ§) β¨ βπ§ β 1o π¦ = (inrβπ§))) |
98 | 97 | biimpi 120 |
. . . . . . 7
β’ (π¦ β (Ο β
1o) β (βπ§ β Ο π¦ = (inlβπ§) β¨ βπ§ β 1o π¦ = (inrβπ§))) |
99 | 98 | ad2antlr 489 |
. . . . . 6
β’ (((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ π₯ =
β
) β (βπ§
β Ο π¦ =
(inlβπ§) β¨
βπ§ β
1o π¦ =
(inrβπ§))) |
100 | 70, 96, 99 | mpjaod 718 |
. . . . 5
β’ (((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ π₯ =
β
) β (π₯ = (πΊβπ¦) β π¦ = if(π₯ = β
, (inrβπ₯), (inlββͺ
π₯)))) |
101 | | simplll 533 |
. . . . . . . . . . 11
β’ ((((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ Β¬ π₯ = β
) β§ (π§ β Ο β§ π¦ = (inlβπ§))) β π₯ β Ο) |
102 | | simplr 528 |
. . . . . . . . . . . 12
β’ ((((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ Β¬ π₯ = β
) β§ (π§ β Ο β§ π¦ = (inlβπ§))) β Β¬ π₯ = β
) |
103 | 102 | neqned 2354 |
. . . . . . . . . . 11
β’ ((((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ Β¬ π₯ = β
) β§ (π§ β Ο β§ π¦ = (inlβπ§))) β π₯ β β
) |
104 | | nnsucpred 4618 |
. . . . . . . . . . 11
β’ ((π₯ β Ο β§ π₯ β β
) β suc βͺ π₯ =
π₯) |
105 | 101, 103,
104 | syl2anc 411 |
. . . . . . . . . 10
β’ ((((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ Β¬ π₯ = β
) β§ (π§ β Ο β§ π¦ = (inlβπ§))) β suc βͺ
π₯ = π₯) |
106 | 105 | eqeq2d 2189 |
. . . . . . . . 9
β’ ((((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ Β¬ π₯ = β
) β§ (π§ β Ο β§ π¦ = (inlβπ§))) β (suc π§ = suc βͺ π₯ β suc π§ = π₯)) |
107 | | eqcom 2179 |
. . . . . . . . 9
β’ (suc
π§ = π₯ β π₯ = suc π§) |
108 | 106, 107 | bitrdi 196 |
. . . . . . . 8
β’ ((((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ Β¬ π₯ = β
) β§ (π§ β Ο β§ π¦ = (inlβπ§))) β (suc π§ = suc βͺ π₯ β π₯ = suc π§)) |
109 | | simprr 531 |
. . . . . . . . . . 11
β’ ((((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ Β¬ π₯ = β
) β§ (π§ β Ο β§ π¦ = (inlβπ§))) β π¦ = (inlβπ§)) |
110 | | simpr 110 |
. . . . . . . . . . . . 13
β’ (((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ Β¬ π₯ = β
) β Β¬ π₯ = β
) |
111 | 110 | iffalsed 3546 |
. . . . . . . . . . . 12
β’ (((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ Β¬ π₯ = β
) β if(π₯ = β
, (inrβπ₯), (inlββͺ
π₯)) = (inlββͺ π₯)) |
112 | 111 | adantr 276 |
. . . . . . . . . . 11
β’ ((((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ Β¬ π₯ = β
) β§ (π§ β Ο β§ π¦ = (inlβπ§))) β if(π₯ = β
, (inrβπ₯), (inlββͺ
π₯)) = (inlββͺ π₯)) |
113 | 109, 112 | eqeq12d 2192 |
. . . . . . . . . 10
β’ ((((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ Β¬ π₯ = β
) β§ (π§ β Ο β§ π¦ = (inlβπ§))) β (π¦ = if(π₯ = β
, (inrβπ₯), (inlββͺ
π₯)) β (inlβπ§) = (inlββͺ π₯))) |
114 | | vuniex 4440 |
. . . . . . . . . . . 12
β’ βͺ π₯
β V |
115 | | inl11 7066 |
. . . . . . . . . . . 12
β’ ((π§ β V β§ βͺ π₯
β V) β ((inlβπ§) = (inlββͺ
π₯) β π§ = βͺ
π₯)) |
116 | 114, 115 | mpan2 425 |
. . . . . . . . . . 11
β’ (π§ β V β
((inlβπ§) =
(inlββͺ π₯) β π§ = βͺ π₯)) |
117 | 116 | elv 2743 |
. . . . . . . . . 10
β’
((inlβπ§) =
(inlββͺ π₯) β π§ = βͺ π₯) |
118 | 113, 117 | bitrdi 196 |
. . . . . . . . 9
β’ ((((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ Β¬ π₯ = β
) β§ (π§ β Ο β§ π¦ = (inlβπ§))) β (π¦ = if(π₯ = β
, (inrβπ₯), (inlββͺ
π₯)) β π§ = βͺ
π₯)) |
119 | | nnon 4611 |
. . . . . . . . . . 11
β’ (π§ β Ο β π§ β On) |
120 | 119 | ad2antrl 490 |
. . . . . . . . . 10
β’ ((((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ Β¬ π₯ = β
) β§ (π§ β Ο β§ π¦ = (inlβπ§))) β π§ β On) |
121 | 7 | ad3antrrr 492 |
. . . . . . . . . . 11
β’ ((((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ Β¬ π₯ = β
) β§ (π§ β Ο β§ π¦ = (inlβπ§))) β βͺ π₯ β
Ο) |
122 | | nnon 4611 |
. . . . . . . . . . 11
β’ (βͺ π₯
β Ο β βͺ π₯ β On) |
123 | 121, 122 | syl 14 |
. . . . . . . . . 10
β’ ((((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ Β¬ π₯ = β
) β§ (π§ β Ο β§ π¦ = (inlβπ§))) β βͺ π₯ β On) |
124 | | suc11 4559 |
. . . . . . . . . 10
β’ ((π§ β On β§ βͺ π₯
β On) β (suc π§ =
suc βͺ π₯ β π§ = βͺ π₯)) |
125 | 120, 123,
124 | syl2anc 411 |
. . . . . . . . 9
β’ ((((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ Β¬ π₯ = β
) β§ (π§ β Ο β§ π¦ = (inlβπ§))) β (suc π§ = suc βͺ π₯ β π§ = βͺ π₯)) |
126 | 118, 125 | bitr4d 191 |
. . . . . . . 8
β’ ((((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ Β¬ π₯ = β
) β§ (π§ β Ο β§ π¦ = (inlβπ§))) β (π¦ = if(π₯ = β
, (inrβπ₯), (inlββͺ
π₯)) β suc π§ = suc βͺ π₯)) |
127 | 49 | adantl 277 |
. . . . . . . . 9
β’ ((((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ Β¬ π₯ = β
) β§ (π§ β Ο β§ π¦ = (inlβπ§))) β (πΊβπ¦) = suc π§) |
128 | 127 | eqeq2d 2189 |
. . . . . . . 8
β’ ((((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ Β¬ π₯ = β
) β§ (π§ β Ο β§ π¦ = (inlβπ§))) β (π₯ = (πΊβπ¦) β π₯ = suc π§)) |
129 | 108, 126,
128 | 3bitr4rd 221 |
. . . . . . 7
β’ ((((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ Β¬ π₯ = β
) β§ (π§ β Ο β§ π¦ = (inlβπ§))) β (π₯ = (πΊβπ¦) β π¦ = if(π₯ = β
, (inrβπ₯), (inlββͺ
π₯)))) |
130 | 129 | rexlimdvaa 2595 |
. . . . . 6
β’ (((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ Β¬ π₯ = β
) β (βπ§ β Ο π¦ = (inlβπ§) β (π₯ = (πΊβπ¦) β π¦ = if(π₯ = β
, (inrβπ₯), (inlββͺ
π₯))))) |
131 | | simplr 528 |
. . . . . . . . 9
β’ ((((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ Β¬ π₯ = β
) β§ (π§ β 1o β§ π¦ = (inrβπ§))) β Β¬ π₯ = β
) |
132 | 86 | adantl 277 |
. . . . . . . . . 10
β’ ((((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ Β¬ π₯ = β
) β§ (π§ β 1o β§ π¦ = (inrβπ§))) β (πΊβπ¦) = β
) |
133 | 132 | eqeq2d 2189 |
. . . . . . . . 9
β’ ((((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ Β¬ π₯ = β
) β§ (π§ β 1o β§ π¦ = (inrβπ§))) β (π₯ = (πΊβπ¦) β π₯ = β
)) |
134 | 131, 133 | mtbird 673 |
. . . . . . . 8
β’ ((((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ Β¬ π₯ = β
) β§ (π§ β 1o β§ π¦ = (inrβπ§))) β Β¬ π₯ = (πΊβπ¦)) |
135 | | djune 7079 |
. . . . . . . . . . . 12
β’ ((βͺ π₯
β V β§ π§ β V)
β (inlββͺ π₯) β (inrβπ§)) |
136 | 135 | elvd 2744 |
. . . . . . . . . . 11
β’ (βͺ π₯
β V β (inlββͺ π₯) β (inrβπ§)) |
137 | 114, 136 | ax-mp 5 |
. . . . . . . . . 10
β’
(inlββͺ π₯) β (inrβπ§) |
138 | 137 | nesymi 2393 |
. . . . . . . . 9
β’ Β¬
(inrβπ§) =
(inlββͺ π₯) |
139 | 73, 111 | eqeqan12rd 2194 |
. . . . . . . . 9
β’ ((((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ Β¬ π₯ = β
) β§ (π§ β 1o β§ π¦ = (inrβπ§))) β (π¦ = if(π₯ = β
, (inrβπ₯), (inlββͺ
π₯)) β (inrβπ§) = (inlββͺ π₯))) |
140 | 138, 139 | mtbiri 675 |
. . . . . . . 8
β’ ((((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ Β¬ π₯ = β
) β§ (π§ β 1o β§ π¦ = (inrβπ§))) β Β¬ π¦ = if(π₯ = β
, (inrβπ₯), (inlββͺ
π₯))) |
141 | 134, 140 | 2falsed 702 |
. . . . . . 7
β’ ((((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ Β¬ π₯ = β
) β§ (π§ β 1o β§ π¦ = (inrβπ§))) β (π₯ = (πΊβπ¦) β π¦ = if(π₯ = β
, (inrβπ₯), (inlββͺ
π₯)))) |
142 | 141 | rexlimdvaa 2595 |
. . . . . 6
β’ (((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ Β¬ π₯ = β
) β (βπ§ β 1o π¦ = (inrβπ§) β (π₯ = (πΊβπ¦) β π¦ = if(π₯ = β
, (inrβπ₯), (inlββͺ
π₯))))) |
143 | 98 | ad2antlr 489 |
. . . . . 6
β’ (((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ Β¬ π₯ = β
) β (βπ§ β Ο π¦ = (inlβπ§) β¨ βπ§ β 1o π¦ = (inrβπ§))) |
144 | 130, 142,
143 | mpjaod 718 |
. . . . 5
β’ (((π₯ β Ο β§ π¦ β (Ο β
1o)) β§ Β¬ π₯ = β
) β (π₯ = (πΊβπ¦) β π¦ = if(π₯ = β
, (inrβπ₯), (inlββͺ
π₯)))) |
145 | | exmiddc 836 |
. . . . . . 7
β’
(DECID π₯ = β
β (π₯ = β
β¨ Β¬ π₯ = β
)) |
146 | 11, 145 | syl 14 |
. . . . . 6
β’ (π₯ β Ο β (π₯ = β
β¨ Β¬ π₯ = β
)) |
147 | 146 | adantr 276 |
. . . . 5
β’ ((π₯ β Ο β§ π¦ β (Ο β
1o)) β (π₯ =
β
β¨ Β¬ π₯ =
β
)) |
148 | 100, 144,
147 | mpjaodan 798 |
. . . 4
β’ ((π₯ β Ο β§ π¦ β (Ο β
1o)) β (π₯ =
(πΊβπ¦) β π¦ = if(π₯ = β
, (inrβπ₯), (inlββͺ
π₯)))) |
149 | 148 | adantl 277 |
. . 3
β’
((β€ β§ (π₯
β Ο β§ π¦
β (Ο β 1o))) β (π₯ = (πΊβπ¦) β π¦ = if(π₯ = β
, (inrβπ₯), (inlββͺ
π₯)))) |
150 | 1, 13, 32, 149 | f1o2d 6078 |
. 2
β’ (β€
β πΉ:Οβ1-1-ontoβ(Ο β
1o)) |
151 | 150 | mptru 1362 |
1
β’ πΉ:Οβ1-1-ontoβ(Ο β
1o) |