Step | Hyp | Ref
| Expression |
1 | | foeq1 5434 |
. . 3
ā¢ (š = š ā (š:Ļāontoā(š“ ā 1o) ā š:Ļāontoā(š“ ā 1o))) |
2 | 1 | cbvexv 1918 |
. 2
ā¢
(āš š:Ļāontoā(š“ ā 1o) ā āš š:Ļāontoā(š“ ā 1o)) |
3 | | id 19 |
. . . . . 6
ā¢ (š:Ļāontoā(š“ ā 1o) ā š:Ļāontoā(š“ ā 1o)) |
4 | | eqid 2177 |
. . . . . 6
ā¢ {š” ā Ļ ā£ (šāš”) ā (inl ā š“)} = {š” ā Ļ ā£ (šāš”) ā (inl ā š“)} |
5 | | eqid 2177 |
. . . . . 6
ā¢ (ā”inl ā š) = (ā”inl ā š) |
6 | 3, 4, 5 | ctssdccl 7109 |
. . . . 5
ā¢ (š:Ļāontoā(š“ ā 1o) ā ({š” ā Ļ ā£ (šāš”) ā (inl ā š“)} ā Ļ ā§ (ā”inl ā š):{š” ā Ļ ā£ (šāš”) ā (inl ā š“)}āontoāš“ ā§ āš ā Ļ DECID š ā {š” ā Ļ ā£ (šāš”) ā (inl ā š“)})) |
7 | | djulf1o 7056 |
. . . . . . . . 9
ā¢
inl:Vā1-1-ontoā({ā
} Ć V) |
8 | | f1ocnv 5474 |
. . . . . . . . 9
ā¢
(inl:Vā1-1-ontoā({ā
} Ć V) ā ā”inl:({ā
} Ć V)ā1-1-ontoāV) |
9 | | f1ofun 5463 |
. . . . . . . . 9
ā¢ (ā”inl:({ā
} Ć V)ā1-1-ontoāV ā Fun ā”inl) |
10 | 7, 8, 9 | mp2b 8 |
. . . . . . . 8
ā¢ Fun ā”inl |
11 | | vex 2740 |
. . . . . . . 8
ā¢ š ā V |
12 | | cofunexg 6109 |
. . . . . . . 8
ā¢ ((Fun
ā”inl ā§ š ā V) ā (ā”inl ā š) ā V) |
13 | 10, 11, 12 | mp2an 426 |
. . . . . . 7
ā¢ (ā”inl ā š) ā V |
14 | | foeq1 5434 |
. . . . . . 7
ā¢ (š = (ā”inl ā š) ā (š:{š” ā Ļ ā£ (šāš”) ā (inl ā š“)}āontoāš“ ā (ā”inl ā š):{š” ā Ļ ā£ (šāš”) ā (inl ā š“)}āontoāš“)) |
15 | 13, 14 | spcev 2832 |
. . . . . 6
ā¢ ((ā”inl ā š):{š” ā Ļ ā£ (šāš”) ā (inl ā š“)}āontoāš“ ā āš š:{š” ā Ļ ā£ (šāš”) ā (inl ā š“)}āontoāš“) |
16 | 15 | 3anim2i 1186 |
. . . . 5
ā¢ (({š” ā Ļ ā£ (šāš”) ā (inl ā š“)} ā Ļ ā§ (ā”inl ā š):{š” ā Ļ ā£ (šāš”) ā (inl ā š“)}āontoāš“ ā§ āš ā Ļ DECID š ā {š” ā Ļ ā£ (šāš”) ā (inl ā š“)}) ā ({š” ā Ļ ā£ (šāš”) ā (inl ā š“)} ā Ļ ā§ āš š:{š” ā Ļ ā£ (šāš”) ā (inl ā š“)}āontoāš“ ā§ āš ā Ļ DECID š ā {š” ā Ļ ā£ (šāš”) ā (inl ā š“)})) |
17 | 6, 16 | syl 14 |
. . . 4
ā¢ (š:Ļāontoā(š“ ā 1o) ā ({š” ā Ļ ā£ (šāš”) ā (inl ā š“)} ā Ļ ā§ āš š:{š” ā Ļ ā£ (šāš”) ā (inl ā š“)}āontoāš“ ā§ āš ā Ļ DECID š ā {š” ā Ļ ā£ (šāš”) ā (inl ā š“)})) |
18 | | omex 4592 |
. . . . . 6
ā¢ Ļ
ā V |
19 | 18 | rabex 4147 |
. . . . 5
ā¢ {š” ā Ļ ā£ (šāš”) ā (inl ā š“)} ā V |
20 | | sseq1 3178 |
. . . . . 6
ā¢ (š = {š” ā Ļ ā£ (šāš”) ā (inl ā š“)} ā (š ā Ļ ā {š” ā Ļ ā£ (šāš”) ā (inl ā š“)} ā Ļ)) |
21 | | foeq2 5435 |
. . . . . . 7
ā¢ (š = {š” ā Ļ ā£ (šāš”) ā (inl ā š“)} ā (š:š āontoāš“ ā š:{š” ā Ļ ā£ (šāš”) ā (inl ā š“)}āontoāš“)) |
22 | 21 | exbidv 1825 |
. . . . . 6
ā¢ (š = {š” ā Ļ ā£ (šāš”) ā (inl ā š“)} ā (āš š:š āontoāš“ ā āš š:{š” ā Ļ ā£ (šāš”) ā (inl ā š“)}āontoāš“)) |
23 | | eleq2 2241 |
. . . . . . . 8
ā¢ (š = {š” ā Ļ ā£ (šāš”) ā (inl ā š“)} ā (š ā š ā š ā {š” ā Ļ ā£ (šāš”) ā (inl ā š“)})) |
24 | 23 | dcbid 838 |
. . . . . . 7
ā¢ (š = {š” ā Ļ ā£ (šāš”) ā (inl ā š“)} ā (DECID š ā š ā DECID š ā {š” ā Ļ ā£ (šāš”) ā (inl ā š“)})) |
25 | 24 | ralbidv 2477 |
. . . . . 6
ā¢ (š = {š” ā Ļ ā£ (šāš”) ā (inl ā š“)} ā (āš ā Ļ DECID š ā š ā āš ā Ļ DECID š ā {š” ā Ļ ā£ (šāš”) ā (inl ā š“)})) |
26 | 20, 22, 25 | 3anbi123d 1312 |
. . . . 5
ā¢ (š = {š” ā Ļ ā£ (šāš”) ā (inl ā š“)} ā ((š ā Ļ ā§ āš š:š āontoāš“ ā§ āš ā Ļ DECID š ā š ) ā ({š” ā Ļ ā£ (šāš”) ā (inl ā š“)} ā Ļ ā§ āš š:{š” ā Ļ ā£ (šāš”) ā (inl ā š“)}āontoāš“ ā§ āš ā Ļ DECID š ā {š” ā Ļ ā£ (šāš”) ā (inl ā š“)}))) |
27 | 19, 26 | spcev 2832 |
. . . 4
ā¢ (({š” ā Ļ ā£ (šāš”) ā (inl ā š“)} ā Ļ ā§ āš š:{š” ā Ļ ā£ (šāš”) ā (inl ā š“)}āontoāš“ ā§ āš ā Ļ DECID š ā {š” ā Ļ ā£ (šāš”) ā (inl ā š“)}) ā āš (š ā Ļ ā§ āš š:š āontoāš“ ā§ āš ā Ļ DECID š ā š )) |
28 | 17, 27 | syl 14 |
. . 3
ā¢ (š:Ļāontoā(š“ ā 1o) ā āš (š ā Ļ ā§ āš š:š āontoāš“ ā§ āš ā Ļ DECID š ā š )) |
29 | 28 | exlimiv 1598 |
. 2
ā¢
(āš š:Ļāontoā(š“ ā 1o) ā āš (š ā Ļ ā§ āš š:š āontoāš“ ā§ āš ā Ļ DECID š ā š )) |
30 | 2, 29 | sylbi 121 |
1
ā¢
(āš š:Ļāontoā(š“ ā 1o) ā āš (š ā Ļ ā§ āš š:š āontoāš“ ā§ āš ā Ļ DECID š ā š )) |