Step | Hyp | Ref
| Expression |
1 | | ctssdccl.s |
. . . 4
β’ π = {π₯ β Ο β£ (πΉβπ₯) β (inl β π΄)} |
2 | | ssrab2 3240 |
. . . 4
β’ {π₯ β Ο β£ (πΉβπ₯) β (inl β π΄)} β Ο |
3 | 1, 2 | eqsstri 3187 |
. . 3
β’ π β
Ο |
4 | 3 | a1i 9 |
. 2
β’ (π β π β Ο) |
5 | | djulf1o 7056 |
. . . . . . 7
β’
inl:Vβ1-1-ontoβ({β
} Γ V) |
6 | | f1ocnv 5474 |
. . . . . . 7
β’
(inl:Vβ1-1-ontoβ({β
} Γ V) β β‘inl:({β
} Γ V)β1-1-ontoβV) |
7 | | f1ofun 5463 |
. . . . . . 7
β’ (β‘inl:({β
} Γ V)β1-1-ontoβV β Fun β‘inl) |
8 | 5, 6, 7 | mp2b 8 |
. . . . . 6
β’ Fun β‘inl |
9 | | ctssdccl.f |
. . . . . . 7
β’ (π β πΉ:Οβontoβ(π΄ β 1o)) |
10 | | fofun 5439 |
. . . . . . 7
β’ (πΉ:Οβontoβ(π΄ β 1o) β Fun πΉ) |
11 | 9, 10 | syl 14 |
. . . . . 6
β’ (π β Fun πΉ) |
12 | | funco 5256 |
. . . . . . 7
β’ ((Fun
β‘inl β§ Fun πΉ) β Fun (β‘inl β πΉ)) |
13 | | ctssdccl.g |
. . . . . . . 8
β’ πΊ = (β‘inl β πΉ) |
14 | 13 | funeqi 5237 |
. . . . . . 7
β’ (Fun
πΊ β Fun (β‘inl β πΉ)) |
15 | 12, 14 | sylibr 134 |
. . . . . 6
β’ ((Fun
β‘inl β§ Fun πΉ) β Fun πΊ) |
16 | 8, 11, 15 | sylancr 414 |
. . . . 5
β’ (π β Fun πΊ) |
17 | | fof 5438 |
. . . . . . . . . . . 12
β’ (πΉ:Οβontoβ(π΄ β 1o) β πΉ:ΟβΆ(π΄ β
1o)) |
18 | 9, 17 | syl 14 |
. . . . . . . . . . 11
β’ (π β πΉ:ΟβΆ(π΄ β 1o)) |
19 | 18 | fdmd 5372 |
. . . . . . . . . 10
β’ (π β dom πΉ = Ο) |
20 | 19 | eleq2d 2247 |
. . . . . . . . 9
β’ (π β (π β dom πΉ β π β Ο)) |
21 | 20 | anbi1d 465 |
. . . . . . . 8
β’ (π β ((π β dom πΉ β§ (πΉβπ) β dom β‘inl) β (π β Ο β§ (πΉβπ) β dom β‘inl))) |
22 | | dmcoss 4896 |
. . . . . . . . . . . 12
β’ dom
(β‘inl β πΉ) β dom πΉ |
23 | 22 | sseli 3151 |
. . . . . . . . . . 11
β’ (π β dom (β‘inl β πΉ) β π β dom πΉ) |
24 | 23 | pm4.71ri 392 |
. . . . . . . . . 10
β’ (π β dom (β‘inl β πΉ) β (π β dom πΉ β§ π β dom (β‘inl β πΉ))) |
25 | | dmfco 5584 |
. . . . . . . . . . 11
β’ ((Fun
πΉ β§ π β dom πΉ) β (π β dom (β‘inl β πΉ) β (πΉβπ) β dom β‘inl)) |
26 | 25 | pm5.32da 452 |
. . . . . . . . . 10
β’ (Fun
πΉ β ((π β dom πΉ β§ π β dom (β‘inl β πΉ)) β (π β dom πΉ β§ (πΉβπ) β dom β‘inl))) |
27 | 24, 26 | bitrid 192 |
. . . . . . . . 9
β’ (Fun
πΉ β (π β dom (β‘inl β πΉ) β (π β dom πΉ β§ (πΉβπ) β dom β‘inl))) |
28 | 11, 27 | syl 14 |
. . . . . . . 8
β’ (π β (π β dom (β‘inl β πΉ) β (π β dom πΉ β§ (πΉβπ) β dom β‘inl))) |
29 | | simpr 110 |
. . . . . . . . . . 11
β’ (((π β§ π β Ο) β§ (πΉβπ) β (inl β π΄)) β (πΉβπ) β (inl β π΄)) |
30 | | imassrn 4981 |
. . . . . . . . . . . . . 14
β’ (inl
β π΄) β ran
inl |
31 | 30 | sseli 3151 |
. . . . . . . . . . . . 13
β’ ((πΉβπ) β (inl β π΄) β (πΉβπ) β ran inl) |
32 | 31 | adantl 277 |
. . . . . . . . . . . 12
β’ (((π β§ π β Ο) β§ (πΉβπ) β (inl β π΄)) β (πΉβπ) β ran inl) |
33 | | df-rn 4637 |
. . . . . . . . . . . . 13
β’ ran inl =
dom β‘inl |
34 | 33 | eleq2i 2244 |
. . . . . . . . . . . 12
β’ ((πΉβπ) β ran inl β (πΉβπ) β dom β‘inl) |
35 | 32, 34 | sylib 122 |
. . . . . . . . . . 11
β’ (((π β§ π β Ο) β§ (πΉβπ) β (inl β π΄)) β (πΉβπ) β dom β‘inl) |
36 | 29, 35 | 2thd 175 |
. . . . . . . . . 10
β’ (((π β§ π β Ο) β§ (πΉβπ) β (inl β π΄)) β ((πΉβπ) β (inl β π΄) β (πΉβπ) β dom β‘inl)) |
37 | | djuin 7062 |
. . . . . . . . . . . . . 14
β’ ((inl
β π΄) β© (inr
β 1o)) = β
|
38 | | disjel 3477 |
. . . . . . . . . . . . . 14
β’ ((((inl
β π΄) β© (inr
β 1o)) = β
β§ (πΉβπ) β (inl β π΄)) β Β¬ (πΉβπ) β (inr β
1o)) |
39 | 37, 38 | mpan 424 |
. . . . . . . . . . . . 13
β’ ((πΉβπ) β (inl β π΄) β Β¬ (πΉβπ) β (inr β
1o)) |
40 | 39 | con2i 627 |
. . . . . . . . . . . 12
β’ ((πΉβπ) β (inr β 1o) β
Β¬ (πΉβπ) β (inl β π΄)) |
41 | 40 | adantl 277 |
. . . . . . . . . . 11
β’ (((π β§ π β Ο) β§ (πΉβπ) β (inr β 1o)) β
Β¬ (πΉβπ) β (inl β π΄)) |
42 | | djuin 7062 |
. . . . . . . . . . . . . . . 16
β’ ((inl
β V) β© (inr β 1o)) = β
|
43 | | disjel 3477 |
. . . . . . . . . . . . . . . 16
β’ ((((inl
β V) β© (inr β 1o)) = β
β§ (πΉβπ) β (inl β V)) β Β¬ (πΉβπ) β (inr β
1o)) |
44 | 42, 43 | mpan 424 |
. . . . . . . . . . . . . . 15
β’ ((πΉβπ) β (inl β V) β Β¬ (πΉβπ) β (inr β
1o)) |
45 | | dfrn4 5089 |
. . . . . . . . . . . . . . 15
β’ ran inl =
(inl β V) |
46 | 44, 45 | eleq2s 2272 |
. . . . . . . . . . . . . 14
β’ ((πΉβπ) β ran inl β Β¬ (πΉβπ) β (inr β
1o)) |
47 | 46 | con2i 627 |
. . . . . . . . . . . . 13
β’ ((πΉβπ) β (inr β 1o) β
Β¬ (πΉβπ) β ran
inl) |
48 | 47 | adantl 277 |
. . . . . . . . . . . 12
β’ (((π β§ π β Ο) β§ (πΉβπ) β (inr β 1o)) β
Β¬ (πΉβπ) β ran
inl) |
49 | 48, 34 | sylnib 676 |
. . . . . . . . . . 11
β’ (((π β§ π β Ο) β§ (πΉβπ) β (inr β 1o)) β
Β¬ (πΉβπ) β dom β‘inl) |
50 | 41, 49 | 2falsed 702 |
. . . . . . . . . 10
β’ (((π β§ π β Ο) β§ (πΉβπ) β (inr β 1o)) β
((πΉβπ) β (inl β π΄) β (πΉβπ) β dom β‘inl)) |
51 | 18 | ffvelcdmda 5651 |
. . . . . . . . . . . 12
β’ ((π β§ π β Ο) β (πΉβπ) β (π΄ β 1o)) |
52 | | djuun 7065 |
. . . . . . . . . . . . 13
β’ ((inl
β π΄) βͺ (inr
β 1o)) = (π΄ β 1o) |
53 | 52 | eleq2i 2244 |
. . . . . . . . . . . 12
β’ ((πΉβπ) β ((inl β π΄) βͺ (inr β 1o)) β
(πΉβπ) β (π΄ β 1o)) |
54 | 51, 53 | sylibr 134 |
. . . . . . . . . . 11
β’ ((π β§ π β Ο) β (πΉβπ) β ((inl β π΄) βͺ (inr β
1o))) |
55 | | elun 3276 |
. . . . . . . . . . 11
β’ ((πΉβπ) β ((inl β π΄) βͺ (inr β 1o)) β
((πΉβπ) β (inl β π΄) β¨ (πΉβπ) β (inr β
1o))) |
56 | 54, 55 | sylib 122 |
. . . . . . . . . 10
β’ ((π β§ π β Ο) β ((πΉβπ) β (inl β π΄) β¨ (πΉβπ) β (inr β
1o))) |
57 | 36, 50, 56 | mpjaodan 798 |
. . . . . . . . 9
β’ ((π β§ π β Ο) β ((πΉβπ) β (inl β π΄) β (πΉβπ) β dom β‘inl)) |
58 | 57 | pm5.32da 452 |
. . . . . . . 8
β’ (π β ((π β Ο β§ (πΉβπ) β (inl β π΄)) β (π β Ο β§ (πΉβπ) β dom β‘inl))) |
59 | 21, 28, 58 | 3bitr4d 220 |
. . . . . . 7
β’ (π β (π β dom (β‘inl β πΉ) β (π β Ο β§ (πΉβπ) β (inl β π΄)))) |
60 | 13 | dmeqi 4828 |
. . . . . . . 8
β’ dom πΊ = dom (β‘inl β πΉ) |
61 | 60 | eleq2i 2244 |
. . . . . . 7
β’ (π β dom πΊ β π β dom (β‘inl β πΉ)) |
62 | | fveq2 5515 |
. . . . . . . . 9
β’ (π₯ = π β (πΉβπ₯) = (πΉβπ)) |
63 | 62 | eleq1d 2246 |
. . . . . . . 8
β’ (π₯ = π β ((πΉβπ₯) β (inl β π΄) β (πΉβπ) β (inl β π΄))) |
64 | 63, 1 | elrab2 2896 |
. . . . . . 7
β’ (π β π β (π β Ο β§ (πΉβπ) β (inl β π΄))) |
65 | 59, 61, 64 | 3bitr4g 223 |
. . . . . 6
β’ (π β (π β dom πΊ β π β π)) |
66 | 65 | eqrdv 2175 |
. . . . 5
β’ (π β dom πΊ = π) |
67 | | df-fn 5219 |
. . . . 5
β’ (πΊ Fn π β (Fun πΊ β§ dom πΊ = π)) |
68 | 16, 66, 67 | sylanbrc 417 |
. . . 4
β’ (π β πΊ Fn π) |
69 | 13 | fveq1i 5516 |
. . . . . . 7
β’ (πΊβπ) = ((β‘inl β πΉ)βπ) |
70 | 18 | adantr 276 |
. . . . . . . 8
β’ ((π β§ π β π) β πΉ:ΟβΆ(π΄ β 1o)) |
71 | | fveq2 5515 |
. . . . . . . . . . . . 13
β’ (π₯ = π β (πΉβπ₯) = (πΉβπ)) |
72 | 71 | eleq1d 2246 |
. . . . . . . . . . . 12
β’ (π₯ = π β ((πΉβπ₯) β (inl β π΄) β (πΉβπ) β (inl β π΄))) |
73 | 72, 1 | elrab2 2896 |
. . . . . . . . . . 11
β’ (π β π β (π β Ο β§ (πΉβπ) β (inl β π΄))) |
74 | 73 | biimpi 120 |
. . . . . . . . . 10
β’ (π β π β (π β Ο β§ (πΉβπ) β (inl β π΄))) |
75 | 74 | adantl 277 |
. . . . . . . . 9
β’ ((π β§ π β π) β (π β Ο β§ (πΉβπ) β (inl β π΄))) |
76 | 75 | simpld 112 |
. . . . . . . 8
β’ ((π β§ π β π) β π β Ο) |
77 | | fvco3 5587 |
. . . . . . . 8
β’ ((πΉ:ΟβΆ(π΄ β 1o) β§
π β Ο) β
((β‘inl β πΉ)βπ) = (β‘inlβ(πΉβπ))) |
78 | 70, 76, 77 | syl2anc 411 |
. . . . . . 7
β’ ((π β§ π β π) β ((β‘inl β πΉ)βπ) = (β‘inlβ(πΉβπ))) |
79 | 69, 78 | eqtrid 2222 |
. . . . . 6
β’ ((π β§ π β π) β (πΊβπ) = (β‘inlβ(πΉβπ))) |
80 | | f1ofun 5463 |
. . . . . . . . . 10
β’
(inl:Vβ1-1-ontoβ({β
} Γ V) β Fun
inl) |
81 | 5, 80 | ax-mp 5 |
. . . . . . . . 9
β’ Fun
inl |
82 | | fvelima 5567 |
. . . . . . . . 9
β’ ((Fun inl
β§ (πΉβπ) β (inl β π΄)) β βπ§ β π΄ (inlβπ§) = (πΉβπ)) |
83 | 81, 82 | mpan 424 |
. . . . . . . 8
β’ ((πΉβπ) β (inl β π΄) β βπ§ β π΄ (inlβπ§) = (πΉβπ)) |
84 | 75, 83 | simpl2im 386 |
. . . . . . 7
β’ ((π β§ π β π) β βπ§ β π΄ (inlβπ§) = (πΉβπ)) |
85 | | simprr 531 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ (π§ β π΄ β§ (inlβπ§) = (πΉβπ))) β (inlβπ§) = (πΉβπ)) |
86 | 85 | fveq2d 5519 |
. . . . . . . 8
β’ (((π β§ π β π) β§ (π§ β π΄ β§ (inlβπ§) = (πΉβπ))) β (β‘inlβ(inlβπ§)) = (β‘inlβ(πΉβπ))) |
87 | | vex 2740 |
. . . . . . . . . 10
β’ π§ β V |
88 | | f1ocnvfv1 5777 |
. . . . . . . . . 10
β’
((inl:Vβ1-1-ontoβ({β
} Γ V) β§ π§ β V) β (β‘inlβ(inlβπ§)) = π§) |
89 | 5, 87, 88 | mp2an 426 |
. . . . . . . . 9
β’ (β‘inlβ(inlβπ§)) = π§ |
90 | | simprl 529 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ (π§ β π΄ β§ (inlβπ§) = (πΉβπ))) β π§ β π΄) |
91 | 89, 90 | eqeltrid 2264 |
. . . . . . . 8
β’ (((π β§ π β π) β§ (π§ β π΄ β§ (inlβπ§) = (πΉβπ))) β (β‘inlβ(inlβπ§)) β π΄) |
92 | 86, 91 | eqeltrrd 2255 |
. . . . . . 7
β’ (((π β§ π β π) β§ (π§ β π΄ β§ (inlβπ§) = (πΉβπ))) β (β‘inlβ(πΉβπ)) β π΄) |
93 | 84, 92 | rexlimddv 2599 |
. . . . . 6
β’ ((π β§ π β π) β (β‘inlβ(πΉβπ)) β π΄) |
94 | 79, 93 | eqeltrd 2254 |
. . . . 5
β’ ((π β§ π β π) β (πΊβπ) β π΄) |
95 | 94 | ralrimiva 2550 |
. . . 4
β’ (π β βπ β π (πΊβπ) β π΄) |
96 | | ffnfv 5674 |
. . . 4
β’ (πΊ:πβΆπ΄ β (πΊ Fn π β§ βπ β π (πΊβπ) β π΄)) |
97 | 68, 95, 96 | sylanbrc 417 |
. . 3
β’ (π β πΊ:πβΆπ΄) |
98 | | djulcl 7049 |
. . . . . . . 8
β’ (π β π΄ β (inlβπ) β (π΄ β 1o)) |
99 | | foelrn 5753 |
. . . . . . . . . 10
β’ ((πΉ:Οβontoβ(π΄ β 1o) β§
(inlβπ) β (π΄ β 1o)) β
βπ¦ β Ο
(inlβπ) = (πΉβπ¦)) |
100 | 9, 99 | sylan 283 |
. . . . . . . . 9
β’ ((π β§ (inlβπ) β (π΄ β 1o)) β
βπ¦ β Ο
(inlβπ) = (πΉβπ¦)) |
101 | | df-rex 2461 |
. . . . . . . . 9
β’
(βπ¦ β
Ο (inlβπ) =
(πΉβπ¦) β βπ¦(π¦ β Ο β§ (inlβπ) = (πΉβπ¦))) |
102 | 100, 101 | sylib 122 |
. . . . . . . 8
β’ ((π β§ (inlβπ) β (π΄ β 1o)) β
βπ¦(π¦ β Ο β§ (inlβπ) = (πΉβπ¦))) |
103 | 98, 102 | sylan2 286 |
. . . . . . 7
β’ ((π β§ π β π΄) β βπ¦(π¦ β Ο β§ (inlβπ) = (πΉβπ¦))) |
104 | | fveq2 5515 |
. . . . . . . . . . . . 13
β’ (π₯ = π¦ β (πΉβπ₯) = (πΉβπ¦)) |
105 | 104 | eleq1d 2246 |
. . . . . . . . . . . 12
β’ (π₯ = π¦ β ((πΉβπ₯) β (inl β π΄) β (πΉβπ¦) β (inl β π΄))) |
106 | | simprl 529 |
. . . . . . . . . . . 12
β’ (((π β§ π β π΄) β§ (π¦ β Ο β§ (inlβπ) = (πΉβπ¦))) β π¦ β Ο) |
107 | | simprr 531 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π΄) β§ (π¦ β Ο β§ (inlβπ) = (πΉβπ¦))) β (inlβπ) = (πΉβπ¦)) |
108 | | vex 2740 |
. . . . . . . . . . . . . . . 16
β’ π β V |
109 | | f1odm 5465 |
. . . . . . . . . . . . . . . . 17
β’
(inl:Vβ1-1-ontoβ({β
} Γ V) β dom inl =
V) |
110 | 5, 109 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
β’ dom inl =
V |
111 | 108, 110 | eleqtrri 2253 |
. . . . . . . . . . . . . . 15
β’ π β dom inl |
112 | | funfvima 5748 |
. . . . . . . . . . . . . . 15
β’ ((Fun inl
β§ π β dom inl)
β (π β π΄ β (inlβπ) β (inl β π΄))) |
113 | 81, 111, 112 | mp2an 426 |
. . . . . . . . . . . . . 14
β’ (π β π΄ β (inlβπ) β (inl β π΄)) |
114 | 113 | ad2antlr 489 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π΄) β§ (π¦ β Ο β§ (inlβπ) = (πΉβπ¦))) β (inlβπ) β (inl β π΄)) |
115 | 107, 114 | eqeltrrd 2255 |
. . . . . . . . . . . 12
β’ (((π β§ π β π΄) β§ (π¦ β Ο β§ (inlβπ) = (πΉβπ¦))) β (πΉβπ¦) β (inl β π΄)) |
116 | 105, 106,
115 | elrabd 2895 |
. . . . . . . . . . 11
β’ (((π β§ π β π΄) β§ (π¦ β Ο β§ (inlβπ) = (πΉβπ¦))) β π¦ β {π₯ β Ο β£ (πΉβπ₯) β (inl β π΄)}) |
117 | 116, 1 | eleqtrrdi 2271 |
. . . . . . . . . 10
β’ (((π β§ π β π΄) β§ (π¦ β Ο β§ (inlβπ) = (πΉβπ¦))) β π¦ β π) |
118 | 117, 107 | jca 306 |
. . . . . . . . 9
β’ (((π β§ π β π΄) β§ (π¦ β Ο β§ (inlβπ) = (πΉβπ¦))) β (π¦ β π β§ (inlβπ) = (πΉβπ¦))) |
119 | 118 | ex 115 |
. . . . . . . 8
β’ ((π β§ π β π΄) β ((π¦ β Ο β§ (inlβπ) = (πΉβπ¦)) β (π¦ β π β§ (inlβπ) = (πΉβπ¦)))) |
120 | 119 | eximdv 1880 |
. . . . . . 7
β’ ((π β§ π β π΄) β (βπ¦(π¦ β Ο β§ (inlβπ) = (πΉβπ¦)) β βπ¦(π¦ β π β§ (inlβπ) = (πΉβπ¦)))) |
121 | 103, 120 | mpd 13 |
. . . . . 6
β’ ((π β§ π β π΄) β βπ¦(π¦ β π β§ (inlβπ) = (πΉβπ¦))) |
122 | | df-rex 2461 |
. . . . . 6
β’
(βπ¦ β
π (inlβπ) = (πΉβπ¦) β βπ¦(π¦ β π β§ (inlβπ) = (πΉβπ¦))) |
123 | 121, 122 | sylibr 134 |
. . . . 5
β’ ((π β§ π β π΄) β βπ¦ β π (inlβπ) = (πΉβπ¦)) |
124 | | f1ocnvfv1 5777 |
. . . . . . . . . 10
β’
((inl:Vβ1-1-ontoβ({β
} Γ V) β§ π β V) β (β‘inlβ(inlβπ)) = π) |
125 | 5, 108, 124 | mp2an 426 |
. . . . . . . . 9
β’ (β‘inlβ(inlβπ)) = π |
126 | | simpr 110 |
. . . . . . . . . 10
β’ ((((π β§ π β π΄) β§ π¦ β π) β§ (inlβπ) = (πΉβπ¦)) β (inlβπ) = (πΉβπ¦)) |
127 | 126 | fveq2d 5519 |
. . . . . . . . 9
β’ ((((π β§ π β π΄) β§ π¦ β π) β§ (inlβπ) = (πΉβπ¦)) β (β‘inlβ(inlβπ)) = (β‘inlβ(πΉβπ¦))) |
128 | 125, 127 | eqtr3id 2224 |
. . . . . . . 8
β’ ((((π β§ π β π΄) β§ π¦ β π) β§ (inlβπ) = (πΉβπ¦)) β π = (β‘inlβ(πΉβπ¦))) |
129 | 13 | fveq1i 5516 |
. . . . . . . . . 10
β’ (πΊβπ¦) = ((β‘inl β πΉ)βπ¦) |
130 | 18 | ad2antrr 488 |
. . . . . . . . . . 11
β’ (((π β§ π β π΄) β§ π¦ β π) β πΉ:ΟβΆ(π΄ β 1o)) |
131 | 3 | sseli 3151 |
. . . . . . . . . . . 12
β’ (π¦ β π β π¦ β Ο) |
132 | 131 | adantl 277 |
. . . . . . . . . . 11
β’ (((π β§ π β π΄) β§ π¦ β π) β π¦ β Ο) |
133 | | fvco3 5587 |
. . . . . . . . . . 11
β’ ((πΉ:ΟβΆ(π΄ β 1o) β§
π¦ β Ο) β
((β‘inl β πΉ)βπ¦) = (β‘inlβ(πΉβπ¦))) |
134 | 130, 132,
133 | syl2anc 411 |
. . . . . . . . . 10
β’ (((π β§ π β π΄) β§ π¦ β π) β ((β‘inl β πΉ)βπ¦) = (β‘inlβ(πΉβπ¦))) |
135 | 129, 134 | eqtrid 2222 |
. . . . . . . . 9
β’ (((π β§ π β π΄) β§ π¦ β π) β (πΊβπ¦) = (β‘inlβ(πΉβπ¦))) |
136 | 135 | adantr 276 |
. . . . . . . 8
β’ ((((π β§ π β π΄) β§ π¦ β π) β§ (inlβπ) = (πΉβπ¦)) β (πΊβπ¦) = (β‘inlβ(πΉβπ¦))) |
137 | 128, 136 | eqtr4d 2213 |
. . . . . . 7
β’ ((((π β§ π β π΄) β§ π¦ β π) β§ (inlβπ) = (πΉβπ¦)) β π = (πΊβπ¦)) |
138 | 137 | ex 115 |
. . . . . 6
β’ (((π β§ π β π΄) β§ π¦ β π) β ((inlβπ) = (πΉβπ¦) β π = (πΊβπ¦))) |
139 | 138 | reximdva 2579 |
. . . . 5
β’ ((π β§ π β π΄) β (βπ¦ β π (inlβπ) = (πΉβπ¦) β βπ¦ β π π = (πΊβπ¦))) |
140 | 123, 139 | mpd 13 |
. . . 4
β’ ((π β§ π β π΄) β βπ¦ β π π = (πΊβπ¦)) |
141 | 140 | ralrimiva 2550 |
. . 3
β’ (π β βπ β π΄ βπ¦ β π π = (πΊβπ¦)) |
142 | | dffo3 5663 |
. . 3
β’ (πΊ:πβontoβπ΄ β (πΊ:πβΆπ΄ β§ βπ β π΄ βπ¦ β π π = (πΊβπ¦))) |
143 | 97, 141, 142 | sylanbrc 417 |
. 2
β’ (π β πΊ:πβontoβπ΄) |
144 | 53, 55 | bitr3i 186 |
. . . . . . 7
β’ ((πΉβπ) β (π΄ β 1o) β ((πΉβπ) β (inl β π΄) β¨ (πΉβπ) β (inr β
1o))) |
145 | 51, 144 | sylib 122 |
. . . . . 6
β’ ((π β§ π β Ο) β ((πΉβπ) β (inl β π΄) β¨ (πΉβπ) β (inr β
1o))) |
146 | 40 | orim2i 761 |
. . . . . 6
β’ (((πΉβπ) β (inl β π΄) β¨ (πΉβπ) β (inr β 1o)) β
((πΉβπ) β (inl β π΄) β¨ Β¬ (πΉβπ) β (inl β π΄))) |
147 | 145, 146 | syl 14 |
. . . . 5
β’ ((π β§ π β Ο) β ((πΉβπ) β (inl β π΄) β¨ Β¬ (πΉβπ) β (inl β π΄))) |
148 | | df-dc 835 |
. . . . 5
β’
(DECID (πΉβπ) β (inl β π΄) β ((πΉβπ) β (inl β π΄) β¨ Β¬ (πΉβπ) β (inl β π΄))) |
149 | 147, 148 | sylibr 134 |
. . . 4
β’ ((π β§ π β Ο) β DECID
(πΉβπ) β (inl β π΄)) |
150 | | ibar 301 |
. . . . . . 7
β’ (π β Ο β ((πΉβπ) β (inl β π΄) β (π β Ο β§ (πΉβπ) β (inl β π΄)))) |
151 | 150 | adantl 277 |
. . . . . 6
β’ ((π β§ π β Ο) β ((πΉβπ) β (inl β π΄) β (π β Ο β§ (πΉβπ) β (inl β π΄)))) |
152 | 151, 64 | bitr4di 198 |
. . . . 5
β’ ((π β§ π β Ο) β ((πΉβπ) β (inl β π΄) β π β π)) |
153 | 152 | dcbid 838 |
. . . 4
β’ ((π β§ π β Ο) β (DECID
(πΉβπ) β (inl β π΄) β DECID π β π)) |
154 | 149, 153 | mpbid 147 |
. . 3
β’ ((π β§ π β Ο) β DECID
π β π) |
155 | 154 | ralrimiva 2550 |
. 2
β’ (π β βπ β Ο DECID π β π) |
156 | 4, 143, 155 | 3jca 1177 |
1
β’ (π β (π β Ο β§ πΊ:πβontoβπ΄ β§ βπ β Ο DECID π β π)) |