Step | Hyp | Ref
| Expression |
1 | | nfv 1528 |
. . . . . . . . 9
β’
β²π(βπ§ π§ β π¦ β§ π¦ βΌ π₯) |
2 | | nfe1 1496 |
. . . . . . . . 9
β’
β²πβπ π:π₯βontoβπ¦ |
3 | 1, 2 | nfim 1572 |
. . . . . . . 8
β’
β²π((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) |
4 | 3 | nfal 1576 |
. . . . . . 7
β’
β²πβπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) |
5 | 4 | nfal 1576 |
. . . . . 6
β’
β²πβπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) |
6 | | nfv 1528 |
. . . . . 6
β’
β²π π’ β
{β
} |
7 | 5, 6 | nfan 1565 |
. . . . 5
β’
β²π(βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) |
8 | | nfv 1528 |
. . . . 5
β’
β²πDECID β
β π’ |
9 | | simpl 109 |
. . . . . 6
β’
((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦)) |
10 | | p0ex 4189 |
. . . . . . . . . . . 12
β’ {β
}
β V |
11 | | ssdomg 6778 |
. . . . . . . . . . . 12
β’
({β
} β V β (π’ β {β
} β π’ βΌ {β
})) |
12 | 10, 11 | ax-mp 5 |
. . . . . . . . . . 11
β’ (π’ β {β
} β π’ βΌ
{β
}) |
13 | | df1o2 6430 |
. . . . . . . . . . 11
β’
1o = {β
} |
14 | 12, 13 | breqtrrdi 4046 |
. . . . . . . . . 10
β’ (π’ β {β
} β π’ βΌ
1o) |
15 | | 1onn 6521 |
. . . . . . . . . . 11
β’
1o β Ο |
16 | | domrefg 6767 |
. . . . . . . . . . 11
β’
(1o β Ο β 1o βΌ
1o) |
17 | 15, 16 | ax-mp 5 |
. . . . . . . . . 10
β’
1o βΌ 1o |
18 | | djudom 7092 |
. . . . . . . . . 10
β’ ((π’ βΌ 1o β§
1o βΌ 1o) β (π’ β 1o) βΌ
(1o β 1o)) |
19 | 14, 17, 18 | sylancl 413 |
. . . . . . . . 9
β’ (π’ β {β
} β (π’ β 1o) βΌ
(1o β 1o)) |
20 | | dju1p1e2 7196 |
. . . . . . . . 9
β’
(1o β 1o) β
2o |
21 | | domentr 6791 |
. . . . . . . . 9
β’ (((π’ β 1o) βΌ
(1o β 1o) β§ (1o β
1o) β 2o) β (π’ β 1o) βΌ
2o) |
22 | 19, 20, 21 | sylancl 413 |
. . . . . . . 8
β’ (π’ β {β
} β (π’ β 1o) βΌ
2o) |
23 | 22 | adantl 277 |
. . . . . . 7
β’
((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β (π’ β 1o) βΌ
2o) |
24 | | 0lt1o 6441 |
. . . . . . . . 9
β’ β
β 1o |
25 | | djurcl 7051 |
. . . . . . . . 9
β’ (β
β 1o β (inrββ
) β (π’ β 1o)) |
26 | 24, 25 | ax-mp 5 |
. . . . . . . 8
β’
(inrββ
) β (π’ β 1o) |
27 | | elex2 2754 |
. . . . . . . 8
β’
((inrββ
) β (π’ β 1o) β βπ§ π§ β (π’ β 1o)) |
28 | 26, 27 | ax-mp 5 |
. . . . . . 7
β’
βπ§ π§ β (π’ β 1o) |
29 | 23, 28 | jctil 312 |
. . . . . 6
β’
((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β (βπ§ π§ β (π’ β 1o) β§ (π’ β 1o) βΌ
2o)) |
30 | | vex 2741 |
. . . . . . . 8
β’ π’ β V |
31 | | djuex 7042 |
. . . . . . . 8
β’ ((π’ β V β§ 1o
β Ο) β (π’
β 1o) β V) |
32 | 30, 15, 31 | mp2an 426 |
. . . . . . 7
β’ (π’ β 1o) β
V |
33 | | 2onn 6522 |
. . . . . . . 8
β’
2o β Ο |
34 | | breq2 4008 |
. . . . . . . . . . . 12
β’ (π₯ = 2o β (π¦ βΌ π₯ β π¦ βΌ 2o)) |
35 | 34 | anbi2d 464 |
. . . . . . . . . . 11
β’ (π₯ = 2o β
((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β (βπ§ π§ β π¦ β§ π¦ βΌ 2o))) |
36 | | foeq2 5436 |
. . . . . . . . . . . 12
β’ (π₯ = 2o β (π:π₯βontoβπ¦ β π:2oβontoβπ¦)) |
37 | 36 | exbidv 1825 |
. . . . . . . . . . 11
β’ (π₯ = 2o β
(βπ π:π₯βontoβπ¦ β βπ π:2oβontoβπ¦)) |
38 | 35, 37 | imbi12d 234 |
. . . . . . . . . 10
β’ (π₯ = 2o β
(((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β ((βπ§ π§ β π¦ β§ π¦ βΌ 2o) β βπ π:2oβontoβπ¦))) |
39 | 38 | albidv 1824 |
. . . . . . . . 9
β’ (π₯ = 2o β
(βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ 2o) β βπ π:2oβontoβπ¦))) |
40 | 39 | spcgv 2825 |
. . . . . . . 8
β’
(2o β Ο β (βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ 2o) β βπ π:2oβontoβπ¦))) |
41 | 33, 40 | ax-mp 5 |
. . . . . . 7
β’
(βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ 2o) β βπ π:2oβontoβπ¦)) |
42 | | eleq2 2241 |
. . . . . . . . . . 11
β’ (π¦ = (π’ β 1o) β (π§ β π¦ β π§ β (π’ β 1o))) |
43 | 42 | exbidv 1825 |
. . . . . . . . . 10
β’ (π¦ = (π’ β 1o) β (βπ§ π§ β π¦ β βπ§ π§ β (π’ β 1o))) |
44 | | breq1 4007 |
. . . . . . . . . 10
β’ (π¦ = (π’ β 1o) β (π¦ βΌ 2o β
(π’ β 1o)
βΌ 2o)) |
45 | 43, 44 | anbi12d 473 |
. . . . . . . . 9
β’ (π¦ = (π’ β 1o) β
((βπ§ π§ β π¦ β§ π¦ βΌ 2o) β (βπ§ π§ β (π’ β 1o) β§ (π’ β 1o) βΌ
2o))) |
46 | | foeq3 5437 |
. . . . . . . . . 10
β’ (π¦ = (π’ β 1o) β (π:2oβontoβπ¦ β π:2oβontoβ(π’ β 1o))) |
47 | 46 | exbidv 1825 |
. . . . . . . . 9
β’ (π¦ = (π’ β 1o) β (βπ π:2oβontoβπ¦ β βπ π:2oβontoβ(π’ β 1o))) |
48 | 45, 47 | imbi12d 234 |
. . . . . . . 8
β’ (π¦ = (π’ β 1o) β
(((βπ§ π§ β π¦ β§ π¦ βΌ 2o) β βπ π:2oβontoβπ¦) β ((βπ§ π§ β (π’ β 1o) β§ (π’ β 1o) βΌ
2o) β βπ π:2oβontoβ(π’ β 1o)))) |
49 | 48 | spcgv 2825 |
. . . . . . 7
β’ ((π’ β 1o) β
V β (βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ 2o) β βπ π:2oβontoβπ¦) β ((βπ§ π§ β (π’ β 1o) β§ (π’ β 1o) βΌ
2o) β βπ π:2oβontoβ(π’ β 1o)))) |
50 | 32, 41, 49 | mpsyl 65 |
. . . . . 6
β’
(βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β ((βπ§ π§ β (π’ β 1o) β§ (π’ β 1o) βΌ
2o) β βπ π:2oβontoβ(π’ β 1o))) |
51 | 9, 29, 50 | sylc 62 |
. . . . 5
β’
((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β βπ π:2oβontoβ(π’ β 1o)) |
52 | | simpr 110 |
. . . . . . . . . 10
β’
((((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β§ π:2oβontoβ(π’ β 1o)) β§ (πββ
) =
(inlββ
)) β (πββ
) =
(inlββ
)) |
53 | | fof 5439 |
. . . . . . . . . . . . 13
β’ (π:2oβontoβ(π’ β 1o) β π:2oβΆ(π’ β
1o)) |
54 | 53 | adantl 277 |
. . . . . . . . . . . 12
β’
(((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β§ π:2oβontoβ(π’ β 1o)) β π:2oβΆ(π’ β
1o)) |
55 | | elelsuc 4410 |
. . . . . . . . . . . . . . 15
β’ (β
β 1o β β
β suc 1o) |
56 | 24, 55 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’ β
β suc 1o |
57 | | df-2o 6418 |
. . . . . . . . . . . . . 14
β’
2o = suc 1o |
58 | 56, 57 | eleqtrri 2253 |
. . . . . . . . . . . . 13
β’ β
β 2o |
59 | 58 | a1i 9 |
. . . . . . . . . . . 12
β’
(((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β§ π:2oβontoβ(π’ β 1o)) β β
β 2o) |
60 | 54, 59 | ffvelcdmd 5653 |
. . . . . . . . . . 11
β’
(((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β§ π:2oβontoβ(π’ β 1o)) β (πββ
) β (π’ β
1o)) |
61 | 60 | adantr 276 |
. . . . . . . . . 10
β’
((((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β§ π:2oβontoβ(π’ β 1o)) β§ (πββ
) =
(inlββ
)) β (πββ
) β (π’ β 1o)) |
62 | 52, 61 | eqeltrrd 2255 |
. . . . . . . . 9
β’
((((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β§ π:2oβontoβ(π’ β 1o)) β§ (πββ
) =
(inlββ
)) β (inlββ
) β (π’ β 1o)) |
63 | | 0ex 4131 |
. . . . . . . . . 10
β’ β
β V |
64 | | djulclb 7054 |
. . . . . . . . . 10
β’ (β
β V β (β
β π’ β (inlββ
) β (π’ β
1o))) |
65 | 63, 64 | ax-mp 5 |
. . . . . . . . 9
β’ (β
β π’ β
(inlββ
) β (π’ β 1o)) |
66 | 62, 65 | sylibr 134 |
. . . . . . . 8
β’
((((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β§ π:2oβontoβ(π’ β 1o)) β§ (πββ
) =
(inlββ
)) β β
β π’) |
67 | 66 | orcd 733 |
. . . . . . 7
β’
((((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β§ π:2oβontoβ(π’ β 1o)) β§ (πββ
) =
(inlββ
)) β (β
β π’ β¨ Β¬ β
β π’)) |
68 | | df-dc 835 |
. . . . . . 7
β’
(DECID β
β π’ β (β
β π’ β¨ Β¬ β
β π’)) |
69 | 67, 68 | sylibr 134 |
. . . . . 6
β’
((((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β§ π:2oβontoβ(π’ β 1o)) β§ (πββ
) =
(inlββ
)) β DECID β
β π’) |
70 | | simpr 110 |
. . . . . . . . . . 11
β’
(((((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β§ π:2oβontoβ(π’ β 1o)) β§ (πββ
) =
(inrββ
)) β§ (πβ1o) = (inlββ
))
β (πβ1o) =
(inlββ
)) |
71 | 54 | adantr 276 |
. . . . . . . . . . . . 13
β’
((((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β§ π:2oβontoβ(π’ β 1o)) β§ (πββ
) =
(inrββ
)) β π:2oβΆ(π’ β 1o)) |
72 | | 1oex 6425 |
. . . . . . . . . . . . . . . 16
β’
1o β V |
73 | 72 | prid2 3700 |
. . . . . . . . . . . . . . 15
β’
1o β {β
, 1o} |
74 | | df2o3 6431 |
. . . . . . . . . . . . . . 15
β’
2o = {β
, 1o} |
75 | 73, 74 | eleqtrri 2253 |
. . . . . . . . . . . . . 14
β’
1o β 2o |
76 | 75 | a1i 9 |
. . . . . . . . . . . . 13
β’
((((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β§ π:2oβontoβ(π’ β 1o)) β§ (πββ
) =
(inrββ
)) β 1o β
2o) |
77 | 71, 76 | ffvelcdmd 5653 |
. . . . . . . . . . . 12
β’
((((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β§ π:2oβontoβ(π’ β 1o)) β§ (πββ
) =
(inrββ
)) β (πβ1o) β (π’ β
1o)) |
78 | 77 | adantr 276 |
. . . . . . . . . . 11
β’
(((((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β§ π:2oβontoβ(π’ β 1o)) β§ (πββ
) =
(inrββ
)) β§ (πβ1o) = (inlββ
))
β (πβ1o) β (π’ β
1o)) |
79 | 70, 78 | eqeltrrd 2255 |
. . . . . . . . . 10
β’
(((((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β§ π:2oβontoβ(π’ β 1o)) β§ (πββ
) =
(inrββ
)) β§ (πβ1o) = (inlββ
))
β (inlββ
) β (π’ β 1o)) |
80 | 79, 65 | sylibr 134 |
. . . . . . . . 9
β’
(((((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β§ π:2oβontoβ(π’ β 1o)) β§ (πββ
) =
(inrββ
)) β§ (πβ1o) = (inlββ
))
β β
β π’) |
81 | 80 | orcd 733 |
. . . . . . . 8
β’
(((((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β§ π:2oβontoβ(π’ β 1o)) β§ (πββ
) =
(inrββ
)) β§ (πβ1o) = (inlββ
))
β (β
β π’
β¨ Β¬ β
β π’)) |
82 | 81, 68 | sylibr 134 |
. . . . . . 7
β’
(((((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β§ π:2oβontoβ(π’ β 1o)) β§ (πββ
) =
(inrββ
)) β§ (πβ1o) = (inlββ
))
β DECID β
β π’) |
83 | | simp-4r 542 |
. . . . . . . . . . . 12
β’
((((((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β§ π:2oβontoβ(π’ β 1o)) β§ (πββ
) =
(inrββ
)) β§ (πβ1o) = (inrββ
))
β§ β
β π’)
β π:2oβontoβ(π’ β 1o)) |
84 | | djulcl 7050 |
. . . . . . . . . . . . 13
β’ (β
β π’ β
(inlββ
) β (π’ β 1o)) |
85 | 84 | adantl 277 |
. . . . . . . . . . . 12
β’
((((((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β§ π:2oβontoβ(π’ β 1o)) β§ (πββ
) =
(inrββ
)) β§ (πβ1o) = (inrββ
))
β§ β
β π’)
β (inlββ
) β (π’ β 1o)) |
86 | | foelrn 5754 |
. . . . . . . . . . . 12
β’ ((π:2oβontoβ(π’ β 1o) β§
(inlββ
) β (π’ β 1o)) β βπ€ β 2o
(inlββ
) = (πβπ€)) |
87 | 83, 85, 86 | syl2anc 411 |
. . . . . . . . . . 11
β’
((((((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β§ π:2oβontoβ(π’ β 1o)) β§ (πββ
) =
(inrββ
)) β§ (πβ1o) = (inrββ
))
β§ β
β π’)
β βπ€ β
2o (inlββ
) = (πβπ€)) |
88 | | simplrr 536 |
. . . . . . . . . . . . 13
β’
((((((((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β§ π:2oβontoβ(π’ β 1o)) β§ (πββ
) =
(inrββ
)) β§ (πβ1o) = (inrββ
))
β§ β
β π’)
β§ (π€ β
2o β§ (inlββ
) = (πβπ€))) β§ π€ = β
) β (inlββ
) =
(πβπ€)) |
89 | | simpr 110 |
. . . . . . . . . . . . . 14
β’
((((((((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β§ π:2oβontoβ(π’ β 1o)) β§ (πββ
) =
(inrββ
)) β§ (πβ1o) = (inrββ
))
β§ β
β π’)
β§ (π€ β
2o β§ (inlββ
) = (πβπ€))) β§ π€ = β
) β π€ = β
) |
90 | 89 | fveq2d 5520 |
. . . . . . . . . . . . 13
β’
((((((((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β§ π:2oβontoβ(π’ β 1o)) β§ (πββ
) =
(inrββ
)) β§ (πβ1o) = (inrββ
))
β§ β
β π’)
β§ (π€ β
2o β§ (inlββ
) = (πβπ€))) β§ π€ = β
) β (πβπ€) = (πββ
)) |
91 | | simp-5r 544 |
. . . . . . . . . . . . 13
β’
((((((((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β§ π:2oβontoβ(π’ β 1o)) β§ (πββ
) =
(inrββ
)) β§ (πβ1o) = (inrββ
))
β§ β
β π’)
β§ (π€ β
2o β§ (inlββ
) = (πβπ€))) β§ π€ = β
) β (πββ
) =
(inrββ
)) |
92 | 88, 90, 91 | 3eqtrd 2214 |
. . . . . . . . . . . 12
β’
((((((((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β§ π:2oβontoβ(π’ β 1o)) β§ (πββ
) =
(inrββ
)) β§ (πβ1o) = (inrββ
))
β§ β
β π’)
β§ (π€ β
2o β§ (inlββ
) = (πβπ€))) β§ π€ = β
) β (inlββ
) =
(inrββ
)) |
93 | | simplrr 536 |
. . . . . . . . . . . . 13
β’
((((((((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β§ π:2oβontoβ(π’ β 1o)) β§ (πββ
) =
(inrββ
)) β§ (πβ1o) = (inrββ
))
β§ β
β π’)
β§ (π€ β
2o β§ (inlββ
) = (πβπ€))) β§ π€ = 1o) β (inlββ
)
= (πβπ€)) |
94 | | simpr 110 |
. . . . . . . . . . . . . 14
β’
((((((((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β§ π:2oβontoβ(π’ β 1o)) β§ (πββ
) =
(inrββ
)) β§ (πβ1o) = (inrββ
))
β§ β
β π’)
β§ (π€ β
2o β§ (inlββ
) = (πβπ€))) β§ π€ = 1o) β π€ = 1o) |
95 | 94 | fveq2d 5520 |
. . . . . . . . . . . . 13
β’
((((((((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β§ π:2oβontoβ(π’ β 1o)) β§ (πββ
) =
(inrββ
)) β§ (πβ1o) = (inrββ
))
β§ β
β π’)
β§ (π€ β
2o β§ (inlββ
) = (πβπ€))) β§ π€ = 1o) β (πβπ€) = (πβ1o)) |
96 | | simp-4r 542 |
. . . . . . . . . . . . 13
β’
((((((((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β§ π:2oβontoβ(π’ β 1o)) β§ (πββ
) =
(inrββ
)) β§ (πβ1o) = (inrββ
))
β§ β
β π’)
β§ (π€ β
2o β§ (inlββ
) = (πβπ€))) β§ π€ = 1o) β (πβ1o) =
(inrββ
)) |
97 | 93, 95, 96 | 3eqtrd 2214 |
. . . . . . . . . . . 12
β’
((((((((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β§ π:2oβontoβ(π’ β 1o)) β§ (πββ
) =
(inrββ
)) β§ (πβ1o) = (inrββ
))
β§ β
β π’)
β§ (π€ β
2o β§ (inlββ
) = (πβπ€))) β§ π€ = 1o) β (inlββ
)
= (inrββ
)) |
98 | | elpri 3616 |
. . . . . . . . . . . . . 14
β’ (π€ β {β
, 1o}
β (π€ = β
β¨
π€ =
1o)) |
99 | 98, 74 | eleq2s 2272 |
. . . . . . . . . . . . 13
β’ (π€ β 2o β
(π€ = β
β¨ π€ =
1o)) |
100 | 99 | ad2antrl 490 |
. . . . . . . . . . . 12
β’
(((((((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β§ π:2oβontoβ(π’ β 1o)) β§ (πββ
) =
(inrββ
)) β§ (πβ1o) = (inrββ
))
β§ β
β π’)
β§ (π€ β
2o β§ (inlββ
) = (πβπ€))) β (π€ = β
β¨ π€ = 1o)) |
101 | 92, 97, 100 | mpjaodan 798 |
. . . . . . . . . . 11
β’
(((((((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β§ π:2oβontoβ(π’ β 1o)) β§ (πββ
) =
(inrββ
)) β§ (πβ1o) = (inrββ
))
β§ β
β π’)
β§ (π€ β
2o β§ (inlββ
) = (πβπ€))) β (inlββ
) =
(inrββ
)) |
102 | 87, 101 | rexlimddv 2599 |
. . . . . . . . . 10
β’
((((((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β§ π:2oβontoβ(π’ β 1o)) β§ (πββ
) =
(inrββ
)) β§ (πβ1o) = (inrββ
))
β§ β
β π’)
β (inlββ
) = (inrββ
)) |
103 | | djune 7077 |
. . . . . . . . . . . . 13
β’ ((β
β V β§ β
β V) β (inlββ
) β
(inrββ
)) |
104 | 63, 63, 103 | mp2an 426 |
. . . . . . . . . . . 12
β’
(inlββ
) β (inrββ
) |
105 | 104 | neii 2349 |
. . . . . . . . . . 11
β’ Β¬
(inlββ
) = (inrββ
) |
106 | 105 | a1i 9 |
. . . . . . . . . 10
β’
((((((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β§ π:2oβontoβ(π’ β 1o)) β§ (πββ
) =
(inrββ
)) β§ (πβ1o) = (inrββ
))
β§ β
β π’)
β Β¬ (inlββ
) = (inrββ
)) |
107 | 102, 106 | pm2.65da 661 |
. . . . . . . . 9
β’
(((((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β§ π:2oβontoβ(π’ β 1o)) β§ (πββ
) =
(inrββ
)) β§ (πβ1o) = (inrββ
))
β Β¬ β
β π’) |
108 | 107 | olcd 734 |
. . . . . . . 8
β’
(((((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β§ π:2oβontoβ(π’ β 1o)) β§ (πββ
) =
(inrββ
)) β§ (πβ1o) = (inrββ
))
β (β
β π’
β¨ Β¬ β
β π’)) |
109 | 108, 68 | sylibr 134 |
. . . . . . 7
β’
(((((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β§ π:2oβontoβ(π’ β 1o)) β§ (πββ
) =
(inrββ
)) β§ (πβ1o) = (inrββ
))
β DECID β
β π’) |
110 | | simplr 528 |
. . . . . . . . . 10
β’
(((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β§ π:2oβontoβ(π’ β 1o)) β π’ β
{β
}) |
111 | 110, 13 | sseqtrrdi 3205 |
. . . . . . . . 9
β’
(((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β§ π:2oβontoβ(π’ β 1o)) β π’ β
1o) |
112 | 111 | adantr 276 |
. . . . . . . 8
β’
((((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β§ π:2oβontoβ(π’ β 1o)) β§ (πββ
) =
(inrββ
)) β π’ β 1o) |
113 | 112, 77 | exmidfodomrlemeldju 7198 |
. . . . . . 7
β’
((((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β§ π:2oβontoβ(π’ β 1o)) β§ (πββ
) =
(inrββ
)) β ((πβ1o) = (inlββ
)
β¨ (πβ1o) =
(inrββ
))) |
114 | 82, 109, 113 | mpjaodan 798 |
. . . . . 6
β’
((((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β§ π:2oβontoβ(π’ β 1o)) β§ (πββ
) =
(inrββ
)) β DECID β
β π’) |
115 | 111, 60 | exmidfodomrlemeldju 7198 |
. . . . . 6
β’
(((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β§ π:2oβontoβ(π’ β 1o)) β ((πββ
) =
(inlββ
) β¨ (πββ
) =
(inrββ
))) |
116 | 69, 114, 115 | mpjaodan 798 |
. . . . 5
β’
(((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β§ π:2oβontoβ(π’ β 1o)) β
DECID β
β π’) |
117 | 7, 8, 51, 116 | exlimdd 1872 |
. . . 4
β’
((βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β§ π’ β {β
}) β
DECID β
β π’) |
118 | 117 | ex 115 |
. . 3
β’
(βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β (π’ β {β
} β
DECID β
β π’)) |
119 | 118 | alrimiv 1874 |
. 2
β’
(βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β βπ’(π’ β {β
} β
DECID β
β π’)) |
120 | | df-exmid 4196 |
. 2
β’
(EXMID β βπ’(π’ β {β
} β
DECID β
β π’)) |
121 | 119, 120 | sylibr 134 |
1
β’
(βπ₯βπ¦((βπ§ π§ β π¦ β§ π¦ βΌ π₯) β βπ π:π₯βontoβπ¦) β
EXMID) |