Step | Hyp | Ref
| Expression |
1 | | subctctexmid.x |
. . . . 5
β’ (π β βπ₯(βπ (π β Ο β§ βπ π:π βontoβπ₯) β βπ π:Οβontoβ(π₯ β 1o))) |
2 | | omex 4586 |
. . . . . . . 8
β’ Ο
β V |
3 | 2 | rabex 4142 |
. . . . . . 7
β’ {π§ β Ο β£ π¦ = {β
}} β
V |
4 | 3 | a1i 9 |
. . . . . 6
β’ (π β {π§ β Ο β£ π¦ = {β
}} β V) |
5 | | ssrab2 3238 |
. . . . . . 7
β’ {π§ β Ο β£ π¦ = {β
}} β
Ο |
6 | | f1oi 5491 |
. . . . . . . . 9
β’ ( I
βΎ {π§ β Ο
β£ π¦ =
{β
}}):{π§ β
Ο β£ π¦ =
{β
}}β1-1-ontoβ{π§ β Ο β£ π¦ = {β
}} |
7 | | f1ofo 5460 |
. . . . . . . . 9
β’ (( I
βΎ {π§ β Ο
β£ π¦ =
{β
}}):{π§ β
Ο β£ π¦ =
{β
}}β1-1-ontoβ{π§ β Ο β£ π¦ = {β
}} β ( I βΎ {π§ β Ο β£ π¦ = {β
}}):{π§ β Ο β£ π¦ = {β
}}βontoβ{π§ β Ο β£ π¦ = {β
}}) |
8 | 6, 7 | ax-mp 5 |
. . . . . . . 8
β’ ( I
βΎ {π§ β Ο
β£ π¦ =
{β
}}):{π§ β
Ο β£ π¦ =
{β
}}βontoβ{π§ β Ο β£ π¦ = {β
}} |
9 | | resiexg 4945 |
. . . . . . . . . 10
β’ ({π§ β Ο β£ π¦ = {β
}} β V β (
I βΎ {π§ β Ο
β£ π¦ = {β
}})
β V) |
10 | 3, 9 | ax-mp 5 |
. . . . . . . . 9
β’ ( I
βΎ {π§ β Ο
β£ π¦ = {β
}})
β V |
11 | | foeq1 5426 |
. . . . . . . . 9
β’ (π = ( I βΎ {π§ β Ο β£ π¦ = {β
}}) β (π:{π§ β Ο β£ π¦ = {β
}}βontoβ{π§ β Ο β£ π¦ = {β
}} β ( I βΎ {π§ β Ο β£ π¦ = {β
}}):{π§ β Ο β£ π¦ = {β
}}βontoβ{π§ β Ο β£ π¦ = {β
}})) |
12 | 10, 11 | spcev 2830 |
. . . . . . . 8
β’ (( I
βΎ {π§ β Ο
β£ π¦ =
{β
}}):{π§ β
Ο β£ π¦ =
{β
}}βontoβ{π§ β Ο β£ π¦ = {β
}} β
βπ π:{π§ β Ο β£ π¦ = {β
}}βontoβ{π§ β Ο β£ π¦ = {β
}}) |
13 | 8, 12 | ax-mp 5 |
. . . . . . 7
β’
βπ π:{π§ β Ο β£ π¦ = {β
}}βontoβ{π§ β Ο β£ π¦ = {β
}} |
14 | 5, 13 | pm3.2i 272 |
. . . . . 6
β’ ({π§ β Ο β£ π¦ = {β
}} β Ο
β§ βπ π:{π§ β Ο β£ π¦ = {β
}}βontoβ{π§ β Ο β£ π¦ = {β
}}) |
15 | | sseq1 3176 |
. . . . . . . 8
β’ (π = {π§ β Ο β£ π¦ = {β
}} β (π β Ο β {π§ β Ο β£ π¦ = {β
}} β
Ο)) |
16 | | foeq2 5427 |
. . . . . . . . 9
β’ (π = {π§ β Ο β£ π¦ = {β
}} β (π:π βontoβ{π§ β Ο β£ π¦ = {β
}} β π:{π§ β Ο β£ π¦ = {β
}}βontoβ{π§ β Ο β£ π¦ = {β
}})) |
17 | 16 | exbidv 1823 |
. . . . . . . 8
β’ (π = {π§ β Ο β£ π¦ = {β
}} β (βπ π:π βontoβ{π§ β Ο β£ π¦ = {β
}} β βπ π:{π§ β Ο β£ π¦ = {β
}}βontoβ{π§ β Ο β£ π¦ = {β
}})) |
18 | 15, 17 | anbi12d 473 |
. . . . . . 7
β’ (π = {π§ β Ο β£ π¦ = {β
}} β ((π β Ο β§ βπ π:π βontoβ{π§ β Ο β£ π¦ = {β
}}) β ({π§ β Ο β£ π¦ = {β
}} β Ο β§
βπ π:{π§ β Ο β£ π¦ = {β
}}βontoβ{π§ β Ο β£ π¦ = {β
}}))) |
19 | 18 | spcegv 2823 |
. . . . . 6
β’ ({π§ β Ο β£ π¦ = {β
}} β V β
(({π§ β Ο β£
π¦ = {β
}} β
Ο β§ βπ
π:{π§ β Ο β£ π¦ = {β
}}βontoβ{π§ β Ο β£ π¦ = {β
}}) β βπ (π β Ο β§ βπ π:π βontoβ{π§ β Ο β£ π¦ = {β
}}))) |
20 | 4, 14, 19 | mpisyl 1444 |
. . . . 5
β’ (π β βπ (π β Ο β§ βπ π:π βontoβ{π§ β Ο β£ π¦ = {β
}})) |
21 | | foeq3 5428 |
. . . . . . . . . 10
β’ (π₯ = {π§ β Ο β£ π¦ = {β
}} β (π:π βontoβπ₯ β π:π βontoβ{π§ β Ο β£ π¦ = {β
}})) |
22 | 21 | exbidv 1823 |
. . . . . . . . 9
β’ (π₯ = {π§ β Ο β£ π¦ = {β
}} β (βπ π:π βontoβπ₯ β βπ π:π βontoβ{π§ β Ο β£ π¦ = {β
}})) |
23 | 22 | anbi2d 464 |
. . . . . . . 8
β’ (π₯ = {π§ β Ο β£ π¦ = {β
}} β ((π β Ο β§ βπ π:π βontoβπ₯) β (π β Ο β§ βπ π:π βontoβ{π§ β Ο β£ π¦ = {β
}}))) |
24 | 23 | exbidv 1823 |
. . . . . . 7
β’ (π₯ = {π§ β Ο β£ π¦ = {β
}} β (βπ (π β Ο β§ βπ π:π βontoβπ₯) β βπ (π β Ο β§ βπ π:π βontoβ{π§ β Ο β£ π¦ = {β
}}))) |
25 | | djueq1 7029 |
. . . . . . . . 9
β’ (π₯ = {π§ β Ο β£ π¦ = {β
}} β (π₯ β 1o) = ({π§ β Ο β£ π¦ = {β
}} β
1o)) |
26 | | foeq3 5428 |
. . . . . . . . 9
β’ ((π₯ β 1o) =
({π§ β Ο β£
π¦ = {β
}} β
1o) β (π:Οβontoβ(π₯ β 1o) β π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β
1o))) |
27 | 25, 26 | syl 14 |
. . . . . . . 8
β’ (π₯ = {π§ β Ο β£ π¦ = {β
}} β (π:Οβontoβ(π₯ β 1o) β π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β
1o))) |
28 | 27 | exbidv 1823 |
. . . . . . 7
β’ (π₯ = {π§ β Ο β£ π¦ = {β
}} β (βπ π:Οβontoβ(π₯ β 1o) β βπ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β
1o))) |
29 | 24, 28 | imbi12d 235 |
. . . . . 6
β’ (π₯ = {π§ β Ο β£ π¦ = {β
}} β ((βπ (π β Ο β§ βπ π:π βontoβπ₯) β βπ π:Οβontoβ(π₯ β 1o)) β
(βπ (π β Ο β§
βπ π:π βontoβ{π§ β Ο β£ π¦ = {β
}}) β βπ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β
1o)))) |
30 | 3, 29 | spcv 2829 |
. . . . 5
β’
(βπ₯(βπ (π β Ο β§ βπ π:π βontoβπ₯) β βπ π:Οβontoβ(π₯ β 1o)) β
(βπ (π β Ο β§
βπ π:π βontoβ{π§ β Ο β£ π¦ = {β
}}) β βπ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β
1o))) |
31 | 1, 20, 30 | sylc 62 |
. . . 4
β’ (π β βπ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β
1o)) |
32 | | fveq1 5506 |
. . . . . . . . . . . 12
β’ (β = (π€ β Ο β¦ if((1st
β(πβπ€)) = β
, 1o,
β
)) β (ββπ) = ((π€ β Ο β¦ if((1st
β(πβπ€)) = β
, 1o,
β
))βπ)) |
33 | 32 | eqeq1d 2184 |
. . . . . . . . . . 11
β’ (β = (π€ β Ο β¦ if((1st
β(πβπ€)) = β
, 1o,
β
)) β ((ββπ) = 1o β ((π€ β Ο β¦ if((1st
β(πβπ€)) = β
, 1o,
β
))βπ) =
1o)) |
34 | 33 | rexbidv 2476 |
. . . . . . . . . 10
β’ (β = (π€ β Ο β¦ if((1st
β(πβπ€)) = β
, 1o,
β
)) β (βπ
β Ο (ββπ) = 1o β βπ β Ο ((π€ β Ο β¦
if((1st β(πβπ€)) = β
, 1o,
β
))βπ) =
1o)) |
35 | 34 | notbid 667 |
. . . . . . . . 9
β’ (β = (π€ β Ο β¦ if((1st
β(πβπ€)) = β
, 1o,
β
)) β (Β¬ βπ β Ο (ββπ) = 1o β Β¬ βπ β Ο ((π€ β Ο β¦
if((1st β(πβπ€)) = β
, 1o,
β
))βπ) =
1o)) |
36 | 35 | notbid 667 |
. . . . . . . 8
β’ (β = (π€ β Ο β¦ if((1st
β(πβπ€)) = β
, 1o,
β
)) β (Β¬ Β¬ βπ β Ο (ββπ) = 1o β Β¬ Β¬
βπ β Ο
((π€ β Ο β¦
if((1st β(πβπ€)) = β
, 1o,
β
))βπ) =
1o)) |
37 | 36, 34 | imbi12d 235 |
. . . . . . 7
β’ (β = (π€ β Ο β¦ if((1st
β(πβπ€)) = β
, 1o,
β
)) β ((Β¬ Β¬ βπ β Ο (ββπ) = 1o β βπ β Ο (ββπ) = 1o) β (Β¬ Β¬
βπ β Ο
((π€ β Ο β¦
if((1st β(πβπ€)) = β
, 1o,
β
))βπ) =
1o β βπ β Ο ((π€ β Ο β¦ if((1st
β(πβπ€)) = β
, 1o,
β
))βπ) =
1o))) |
38 | | subctctexmid.mk |
. . . . . . . . 9
β’ (π β Ο β
Markov) |
39 | | ismkvnex 7143 |
. . . . . . . . . 10
β’ (Ο
β Markov β (Ο β Markov β ββ β (2o
βπ Ο)(Β¬ Β¬ βπ β Ο (ββπ) = 1o β βπ β Ο (ββπ) = 1o))) |
40 | 38, 39 | syl 14 |
. . . . . . . . 9
β’ (π β (Ο β Markov
β ββ β
(2o βπ Ο)(Β¬ Β¬ βπ β Ο (ββπ) = 1o β βπ β Ο (ββπ) = 1o))) |
41 | 38, 40 | mpbid 148 |
. . . . . . . 8
β’ (π β ββ β (2o
βπ Ο)(Β¬ Β¬ βπ β Ο (ββπ) = 1o β βπ β Ο (ββπ) = 1o)) |
42 | 41 | adantr 276 |
. . . . . . 7
β’ ((π β§ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β 1o)) β
ββ β
(2o βπ Ο)(Β¬ Β¬ βπ β Ο (ββπ) = 1o β βπ β Ο (ββπ) = 1o)) |
43 | | 1lt2o 6433 |
. . . . . . . . . . . 12
β’
1o β 2o |
44 | 43 | a1i 9 |
. . . . . . . . . . 11
β’ ((((π β§ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β 1o)) β§
π β Ο) β§
(1st β(πβπ)) = β
) β 1o β
2o) |
45 | | 0lt2o 6432 |
. . . . . . . . . . . 12
β’ β
β 2o |
46 | 45 | a1i 9 |
. . . . . . . . . . 11
β’ ((((π β§ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β 1o)) β§
π β Ο) β§
Β¬ (1st β(πβπ)) = β
) β β
β
2o) |
47 | | simplr 528 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β 1o)) β§
π β Ο) β
π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β
1o)) |
48 | | fof 5430 |
. . . . . . . . . . . . . . 15
β’ (π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β 1o) β
π:ΟβΆ({π§ β Ο β£ π¦ = {β
}} β
1o)) |
49 | 47, 48 | syl 14 |
. . . . . . . . . . . . . 14
β’ (((π β§ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β 1o)) β§
π β Ο) β
π:ΟβΆ({π§ β Ο β£ π¦ = {β
}} β
1o)) |
50 | | simpr 110 |
. . . . . . . . . . . . . 14
β’ (((π β§ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β 1o)) β§
π β Ο) β
π β
Ο) |
51 | 49, 50 | ffvelrnd 5644 |
. . . . . . . . . . . . 13
β’ (((π β§ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β 1o)) β§
π β Ο) β
(πβπ) β ({π§ β Ο β£ π¦ = {β
}} β
1o)) |
52 | | eldju1st 7060 |
. . . . . . . . . . . . 13
β’ ((πβπ) β ({π§ β Ο β£ π¦ = {β
}} β 1o) β
((1st β(πβπ)) = β
β¨ (1st
β(πβπ)) =
1o)) |
53 | 51, 52 | syl 14 |
. . . . . . . . . . . 12
β’ (((π β§ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β 1o)) β§
π β Ο) β
((1st β(πβπ)) = β
β¨ (1st
β(πβπ)) =
1o)) |
54 | | 1n0 6423 |
. . . . . . . . . . . . . . . 16
β’
1o β β
|
55 | 54 | neii 2347 |
. . . . . . . . . . . . . . 15
β’ Β¬
1o = β
|
56 | | eqeq1 2182 |
. . . . . . . . . . . . . . 15
β’
((1st β(πβπ)) = 1o β ((1st
β(πβπ)) = β
β
1o = β
)) |
57 | 55, 56 | mtbiri 675 |
. . . . . . . . . . . . . 14
β’
((1st β(πβπ)) = 1o β Β¬
(1st β(πβπ)) = β
) |
58 | 57 | orim2i 761 |
. . . . . . . . . . . . 13
β’
(((1st β(πβπ)) = β
β¨ (1st
β(πβπ)) = 1o) β
((1st β(πβπ)) = β
β¨ Β¬ (1st
β(πβπ)) = β
)) |
59 | | df-dc 835 |
. . . . . . . . . . . . 13
β’
(DECID (1st β(πβπ)) = β
β ((1st
β(πβπ)) = β
β¨ Β¬
(1st β(πβπ)) = β
)) |
60 | 58, 59 | sylibr 134 |
. . . . . . . . . . . 12
β’
(((1st β(πβπ)) = β
β¨ (1st
β(πβπ)) = 1o) β
DECID (1st β(πβπ)) = β
) |
61 | 53, 60 | syl 14 |
. . . . . . . . . . 11
β’ (((π β§ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β 1o)) β§
π β Ο) β
DECID (1st β(πβπ)) = β
) |
62 | 44, 46, 61 | ifcldadc 3561 |
. . . . . . . . . 10
β’ (((π β§ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β 1o)) β§
π β Ο) β
if((1st β(πβπ)) = β
, 1o, β
) β
2o) |
63 | 62 | fmpttd 5663 |
. . . . . . . . 9
β’ ((π β§ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β 1o)) β
(π β Ο β¦
if((1st β(πβπ)) = β
, 1o,
β
)):ΟβΆ2o) |
64 | | 2fveq3 5512 |
. . . . . . . . . . . . . 14
β’ (π€ = π β (1st β(πβπ€)) = (1st β(πβπ))) |
65 | 64 | eqeq1d 2184 |
. . . . . . . . . . . . 13
β’ (π€ = π β ((1st β(πβπ€)) = β
β (1st
β(πβπ)) = β
)) |
66 | 65 | ifbid 3553 |
. . . . . . . . . . . 12
β’ (π€ = π β if((1st β(πβπ€)) = β
, 1o, β
) =
if((1st β(πβπ)) = β
, 1o,
β
)) |
67 | | eqcom 2177 |
. . . . . . . . . . . 12
β’ (π€ = π β π = π€) |
68 | | eqcom 2177 |
. . . . . . . . . . . 12
β’
(if((1st β(πβπ€)) = β
, 1o, β
) =
if((1st β(πβπ)) = β
, 1o, β
) β
if((1st β(πβπ)) = β
, 1o, β
) =
if((1st β(πβπ€)) = β
, 1o,
β
)) |
69 | 66, 67, 68 | 3imtr3i 201 |
. . . . . . . . . . 11
β’ (π = π€ β if((1st β(πβπ)) = β
, 1o, β
) =
if((1st β(πβπ€)) = β
, 1o,
β
)) |
70 | 69 | cbvmptv 4094 |
. . . . . . . . . 10
β’ (π β Ο β¦
if((1st β(πβπ)) = β
, 1o, β
)) =
(π€ β Ο β¦
if((1st β(πβπ€)) = β
, 1o,
β
)) |
71 | 70 | feq1i 5350 |
. . . . . . . . 9
β’ ((π β Ο β¦
if((1st β(πβπ)) = β
, 1o,
β
)):ΟβΆ2o β (π€ β Ο β¦ if((1st
β(πβπ€)) = β
, 1o,
β
)):ΟβΆ2o) |
72 | 63, 71 | sylib 122 |
. . . . . . . 8
β’ ((π β§ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β 1o)) β
(π€ β Ο β¦
if((1st β(πβπ€)) = β
, 1o,
β
)):ΟβΆ2o) |
73 | | 2onn 6512 |
. . . . . . . . . 10
β’
2o β Ο |
74 | 73 | elexi 2747 |
. . . . . . . . 9
β’
2o β V |
75 | 74, 2 | elmap 6667 |
. . . . . . . 8
β’ ((π€ β Ο β¦
if((1st β(πβπ€)) = β
, 1o, β
)) β
(2o βπ Ο) β (π€ β Ο β¦ if((1st
β(πβπ€)) = β
, 1o,
β
)):ΟβΆ2o) |
76 | 72, 75 | sylibr 134 |
. . . . . . 7
β’ ((π β§ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β 1o)) β
(π€ β Ο β¦
if((1st β(πβπ€)) = β
, 1o, β
)) β
(2o βπ Ο)) |
77 | 37, 42, 76 | rspcdva 2844 |
. . . . . 6
β’ ((π β§ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β 1o)) β
(Β¬ Β¬ βπ
β Ο ((π€ β
Ο β¦ if((1st β(πβπ€)) = β
, 1o,
β
))βπ) =
1o β βπ β Ο ((π€ β Ο β¦ if((1st
β(πβπ€)) = β
, 1o,
β
))βπ) =
1o)) |
78 | | eqid 2175 |
. . . . . . . . . . . . 13
β’ (π€ β Ο β¦
if((1st β(πβπ€)) = β
, 1o, β
)) =
(π€ β Ο β¦
if((1st β(πβπ€)) = β
, 1o,
β
)) |
79 | 78, 66, 50, 62 | fvmptd3 5601 |
. . . . . . . . . . . 12
β’ (((π β§ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β 1o)) β§
π β Ο) β
((π€ β Ο β¦
if((1st β(πβπ€)) = β
, 1o,
β
))βπ) =
if((1st β(πβπ)) = β
, 1o,
β
)) |
80 | 79 | eqeq1d 2184 |
. . . . . . . . . . 11
β’ (((π β§ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β 1o)) β§
π β Ο) β
(((π€ β Ο β¦
if((1st β(πβπ€)) = β
, 1o,
β
))βπ) =
1o β if((1st β(πβπ)) = β
, 1o, β
) =
1o)) |
81 | 51 | adantr 276 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β 1o)) β§
π β Ο) β§
if((1st β(πβπ)) = β
, 1o, β
) =
1o) β (πβπ) β ({π§ β Ο β£ π¦ = {β
}} β
1o)) |
82 | | simpr 110 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β 1o)) β§
π β Ο) β§
if((1st β(πβπ)) = β
, 1o, β
) =
1o) β if((1st β(πβπ)) = β
, 1o, β
) =
1o) |
83 | 82 | eqcomd 2181 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β 1o)) β§
π β Ο) β§
if((1st β(πβπ)) = β
, 1o, β
) =
1o) β 1o = if((1st β(πβπ)) = β
, 1o,
β
)) |
84 | | eqifdc 3566 |
. . . . . . . . . . . . . . . . . . 19
β’
(DECID (1st β(πβπ)) = β
β (1o =
if((1st β(πβπ)) = β
, 1o, β
) β
(((1st β(πβπ)) = β
β§ 1o =
1o) β¨ (Β¬ (1st β(πβπ)) = β
β§ 1o =
β
)))) |
85 | 61, 84 | syl 14 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β 1o)) β§
π β Ο) β
(1o = if((1st β(πβπ)) = β
, 1o, β
) β
(((1st β(πβπ)) = β
β§ 1o =
1o) β¨ (Β¬ (1st β(πβπ)) = β
β§ 1o =
β
)))) |
86 | | eqid 2175 |
. . . . . . . . . . . . . . . . . . 19
β’
1o = 1o |
87 | | orcom 728 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((1st β(πβπ)) = β
β§ 1o =
1o) β¨ (Β¬ (1st β(πβπ)) = β
β§ 1o = β
))
β ((Β¬ (1st β(πβπ)) = β
β§ 1o = β
)
β¨ ((1st β(πβπ)) = β
β§ 1o =
1o))) |
88 | 55 | intnan 929 |
. . . . . . . . . . . . . . . . . . . . 21
β’ Β¬
(Β¬ (1st β(πβπ)) = β
β§ 1o =
β
) |
89 | | biorf 744 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (Β¬
(Β¬ (1st β(πβπ)) = β
β§ 1o = β
)
β (((1st β(πβπ)) = β
β§ 1o =
1o) β ((Β¬ (1st β(πβπ)) = β
β§ 1o = β
)
β¨ ((1st β(πβπ)) = β
β§ 1o =
1o)))) |
90 | 88, 89 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((1st β(πβπ)) = β
β§ 1o =
1o) β ((Β¬ (1st β(πβπ)) = β
β§ 1o = β
)
β¨ ((1st β(πβπ)) = β
β§ 1o =
1o))) |
91 | 87, 90 | bitr4i 188 |
. . . . . . . . . . . . . . . . . . 19
β’
((((1st β(πβπ)) = β
β§ 1o =
1o) β¨ (Β¬ (1st β(πβπ)) = β
β§ 1o = β
))
β ((1st β(πβπ)) = β
β§ 1o =
1o)) |
92 | 86, 91 | mpbiran2 941 |
. . . . . . . . . . . . . . . . . 18
β’
((((1st β(πβπ)) = β
β§ 1o =
1o) β¨ (Β¬ (1st β(πβπ)) = β
β§ 1o = β
))
β (1st β(πβπ)) = β
) |
93 | 85, 92 | bitrdi 197 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β 1o)) β§
π β Ο) β
(1o = if((1st β(πβπ)) = β
, 1o, β
) β
(1st β(πβπ)) = β
)) |
94 | 93 | adantr 276 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β 1o)) β§
π β Ο) β§
if((1st β(πβπ)) = β
, 1o, β
) =
1o) β (1o = if((1st β(πβπ)) = β
, 1o, β
) β
(1st β(πβπ)) = β
)) |
95 | 83, 94 | mpbid 148 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β 1o)) β§
π β Ο) β§
if((1st β(πβπ)) = β
, 1o, β
) =
1o) β (1st β(πβπ)) = β
) |
96 | | eldju2ndl 7061 |
. . . . . . . . . . . . . . 15
β’ (((πβπ) β ({π§ β Ο β£ π¦ = {β
}} β 1o) β§
(1st β(πβπ)) = β
) β (2nd
β(πβπ)) β {π§ β Ο β£ π¦ = {β
}}) |
97 | 81, 95, 96 | syl2anc 411 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β 1o)) β§
π β Ο) β§
if((1st β(πβπ)) = β
, 1o, β
) =
1o) β (2nd β(πβπ)) β {π§ β Ο β£ π¦ = {β
}}) |
98 | | biidd 173 |
. . . . . . . . . . . . . . 15
β’ (π§ = (2nd β(πβπ)) β (π¦ = {β
} β π¦ = {β
})) |
99 | 98 | elrab 2891 |
. . . . . . . . . . . . . 14
β’
((2nd β(πβπ)) β {π§ β Ο β£ π¦ = {β
}} β ((2nd
β(πβπ)) β Ο β§ π¦ = {β
})) |
100 | 97, 99 | sylib 122 |
. . . . . . . . . . . . 13
β’ ((((π β§ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β 1o)) β§
π β Ο) β§
if((1st β(πβπ)) = β
, 1o, β
) =
1o) β ((2nd β(πβπ)) β Ο β§ π¦ = {β
})) |
101 | 100 | simprd 114 |
. . . . . . . . . . . 12
β’ ((((π β§ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β 1o)) β§
π β Ο) β§
if((1st β(πβπ)) = β
, 1o, β
) =
1o) β π¦ =
{β
}) |
102 | 101 | ex 115 |
. . . . . . . . . . 11
β’ (((π β§ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β 1o)) β§
π β Ο) β
(if((1st β(πβπ)) = β
, 1o, β
) =
1o β π¦ =
{β
})) |
103 | 80, 102 | sylbid 151 |
. . . . . . . . . 10
β’ (((π β§ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β 1o)) β§
π β Ο) β
(((π€ β Ο β¦
if((1st β(πβπ€)) = β
, 1o,
β
))βπ) =
1o β π¦ =
{β
})) |
104 | 103 | rexlimdva 2592 |
. . . . . . . . 9
β’ ((π β§ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β 1o)) β
(βπ β Ο
((π€ β Ο β¦
if((1st β(πβπ€)) = β
, 1o,
β
))βπ) =
1o β π¦ =
{β
})) |
105 | | simplr 528 |
. . . . . . . . . . . 12
β’ (((π β§ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β 1o)) β§
π¦ = {β
}) β π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β
1o)) |
106 | | biidd 173 |
. . . . . . . . . . . . . 14
β’ (π§ = β
β (π¦ = {β
} β π¦ = {β
})) |
107 | | peano1 4587 |
. . . . . . . . . . . . . . 15
β’ β
β Ο |
108 | 107 | a1i 9 |
. . . . . . . . . . . . . 14
β’ (((π β§ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β 1o)) β§
π¦ = {β
}) β
β
β Ο) |
109 | | simpr 110 |
. . . . . . . . . . . . . 14
β’ (((π β§ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β 1o)) β§
π¦ = {β
}) β π¦ = {β
}) |
110 | 106, 108,
109 | elrabd 2893 |
. . . . . . . . . . . . 13
β’ (((π β§ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β 1o)) β§
π¦ = {β
}) β
β
β {π§ β
Ο β£ π¦ =
{β
}}) |
111 | | djulcl 7040 |
. . . . . . . . . . . . 13
β’ (β
β {π§ β Ο
β£ π¦ = {β
}}
β (inlββ
) β ({π§ β Ο β£ π¦ = {β
}} β
1o)) |
112 | 110, 111 | syl 14 |
. . . . . . . . . . . 12
β’ (((π β§ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β 1o)) β§
π¦ = {β
}) β
(inlββ
) β ({π§ β Ο β£ π¦ = {β
}} β
1o)) |
113 | | foelrn 5744 |
. . . . . . . . . . . 12
β’ ((π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β 1o) β§
(inlββ
) β ({π§ β Ο β£ π¦ = {β
}} β 1o)) β
βπ β Ο
(inlββ
) = (πβπ)) |
114 | 105, 112,
113 | syl2anc 411 |
. . . . . . . . . . 11
β’ (((π β§ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β 1o)) β§
π¦ = {β
}) β
βπ β Ο
(inlββ
) = (πβπ)) |
115 | 79 | adantlr 477 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β 1o)) β§
π¦ = {β
}) β§ π β Ο) β ((π€ β Ο β¦
if((1st β(πβπ€)) = β
, 1o,
β
))βπ) =
if((1st β(πβπ)) = β
, 1o,
β
)) |
116 | | fveq2 5507 |
. . . . . . . . . . . . . . . 16
β’
((inlββ
) = (πβπ) β (1st
β(inlββ
)) = (1st β(πβπ))) |
117 | | 1stinl 7063 |
. . . . . . . . . . . . . . . . 17
β’ (β
β Ο β (1st β(inlββ
)) =
β
) |
118 | 107, 117 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
β’
(1st β(inlββ
)) = β
|
119 | 116, 118 | eqtr3di 2223 |
. . . . . . . . . . . . . . 15
β’
((inlββ
) = (πβπ) β (1st β(πβπ)) = β
) |
120 | 119 | iftrued 3539 |
. . . . . . . . . . . . . 14
β’
((inlββ
) = (πβπ) β if((1st β(πβπ)) = β
, 1o, β
) =
1o) |
121 | 115, 120 | sylan9eq 2228 |
. . . . . . . . . . . . 13
β’
(((((π β§ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β 1o)) β§
π¦ = {β
}) β§ π β Ο) β§
(inlββ
) = (πβπ)) β ((π€ β Ο β¦ if((1st
β(πβπ€)) = β
, 1o,
β
))βπ) =
1o) |
122 | 121 | ex 115 |
. . . . . . . . . . . 12
β’ ((((π β§ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β 1o)) β§
π¦ = {β
}) β§ π β Ο) β
((inlββ
) = (πβπ) β ((π€ β Ο β¦ if((1st
β(πβπ€)) = β
, 1o,
β
))βπ) =
1o)) |
123 | 122 | reximdva 2577 |
. . . . . . . . . . 11
β’ (((π β§ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β 1o)) β§
π¦ = {β
}) β
(βπ β Ο
(inlββ
) = (πβπ) β βπ β Ο ((π€ β Ο β¦ if((1st
β(πβπ€)) = β
, 1o,
β
))βπ) =
1o)) |
124 | 114, 123 | mpd 13 |
. . . . . . . . . 10
β’ (((π β§ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β 1o)) β§
π¦ = {β
}) β
βπ β Ο
((π€ β Ο β¦
if((1st β(πβπ€)) = β
, 1o,
β
))βπ) =
1o) |
125 | 124 | ex 115 |
. . . . . . . . 9
β’ ((π β§ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β 1o)) β
(π¦ = {β
} β
βπ β Ο
((π€ β Ο β¦
if((1st β(πβπ€)) = β
, 1o,
β
))βπ) =
1o)) |
126 | 104, 125 | impbid 129 |
. . . . . . . 8
β’ ((π β§ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β 1o)) β
(βπ β Ο
((π€ β Ο β¦
if((1st β(πβπ€)) = β
, 1o,
β
))βπ) =
1o β π¦ =
{β
})) |
127 | 126 | notbid 667 |
. . . . . . 7
β’ ((π β§ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β 1o)) β
(Β¬ βπ β
Ο ((π€ β Ο
β¦ if((1st β(πβπ€)) = β
, 1o,
β
))βπ) =
1o β Β¬ π¦ = {β
})) |
128 | 127 | notbid 667 |
. . . . . 6
β’ ((π β§ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β 1o)) β
(Β¬ Β¬ βπ
β Ο ((π€ β
Ο β¦ if((1st β(πβπ€)) = β
, 1o,
β
))βπ) =
1o β Β¬ Β¬ π¦ = {β
})) |
129 | 77, 128, 126 | 3imtr3d 203 |
. . . . 5
β’ ((π β§ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β 1o)) β
(Β¬ Β¬ π¦ = {β
}
β π¦ =
{β
})) |
130 | | df-stab 831 |
. . . . 5
β’
(STAB π¦ = {β
} β (Β¬ Β¬ π¦ = {β
} β π¦ = {β
})) |
131 | 129, 130 | sylibr 134 |
. . . 4
β’ ((π β§ π:Οβontoβ({π§ β Ο β£ π¦ = {β
}} β 1o)) β
STAB π¦ =
{β
}) |
132 | 31, 131 | exlimddv 1896 |
. . 3
β’ (π β STAB π¦ = {β
}) |
133 | 132 | adantr 276 |
. 2
β’ ((π β§ π¦ β {β
}) β
STAB π¦ =
{β
}) |
134 | 133 | exmid1stab 14232 |
1
β’ (π β
EXMID) |