Step | Hyp | Ref
| Expression |
1 | | simp11 1204 |
. 2
âĒ (((ðī <<s ðĩ ⧠ðķ â ðŦ No
⧠ð· â
ðŦ No ) ⧠(âðĨ â ðī âðĶ â ðķ ðĨ âĪs ðĶ ⧠âð§ â ðĩ âðĪ â ð· ðĪ âĪs ð§) ⧠(âðĄ â ðķ âðĒ â ðī ðĄ âĪs ðĒ ⧠âð â ð· âð â ðĩ ð âĪs ð)) â ðī <<s ðĩ) |
2 | | simp2 1138 |
. 2
âĒ (((ðī <<s ðĩ ⧠ðķ â ðŦ No
⧠ð· â
ðŦ No ) ⧠(âðĨ â ðī âðĶ â ðķ ðĨ âĪs ðĶ ⧠âð§ â ðĩ âðĪ â ð· ðĪ âĪs ð§) ⧠(âðĄ â ðķ âðĒ â ðī ðĄ âĪs ðĒ ⧠âð â ð· âð â ðĩ ð âĪs ð)) â (âðĨ â ðī âðĶ â ðķ ðĨ âĪs ðĶ ⧠âð§ â ðĩ âðĪ â ð· ðĪ âĪs ð§)) |
3 | | simp12 1205 |
. . 3
âĒ (((ðī <<s ðĩ ⧠ðķ â ðŦ No
⧠ð· â
ðŦ No ) ⧠(âðĨ â ðī âðĶ â ðķ ðĨ âĪs ðĶ ⧠âð§ â ðĩ âðĪ â ð· ðĪ âĪs ð§) ⧠(âðĄ â ðķ âðĒ â ðī ðĄ âĪs ðĒ ⧠âð â ð· âð â ðĩ ð âĪs ð)) â ðķ â ðŦ No
) |
4 | | simp3l 1202 |
. . 3
âĒ (((ðī <<s ðĩ ⧠ðķ â ðŦ No
⧠ð· â
ðŦ No ) ⧠(âðĨ â ðī âðĶ â ðķ ðĨ âĪs ðĶ ⧠âð§ â ðĩ âðĪ â ð· ðĪ âĪs ð§) ⧠(âðĄ â ðķ âðĒ â ðī ðĄ âĪs ðĒ ⧠âð â ð· âð â ðĩ ð âĪs ð)) â âðĄ â ðķ âðĒ â ðī ðĄ âĪs ðĒ) |
5 | | scutcut 27143 |
. . . . 5
âĒ (ðī <<s ðĩ â ((ðī |s ðĩ) â No
⧠ðī <<s {(ðī |s ðĩ)} ⧠{(ðī |s ðĩ)} <<s ðĩ)) |
6 | 1, 5 | syl 17 |
. . . 4
âĒ (((ðī <<s ðĩ ⧠ðķ â ðŦ No
⧠ð· â
ðŦ No ) ⧠(âðĨ â ðī âðĶ â ðķ ðĨ âĪs ðĶ ⧠âð§ â ðĩ âðĪ â ð· ðĪ âĪs ð§) ⧠(âðĄ â ðķ âðĒ â ðī ðĄ âĪs ðĒ ⧠âð â ð· âð â ðĩ ð âĪs ð)) â ((ðī |s ðĩ) â No
⧠ðī <<s {(ðī |s ðĩ)} ⧠{(ðī |s ðĩ)} <<s ðĩ)) |
7 | 6 | simp2d 1144 |
. . 3
âĒ (((ðī <<s ðĩ ⧠ðķ â ðŦ No
⧠ð· â
ðŦ No ) ⧠(âðĨ â ðī âðĶ â ðķ ðĨ âĪs ðĶ ⧠âð§ â ðĩ âðĪ â ð· ðĪ âĪs ð§) ⧠(âðĄ â ðķ âðĒ â ðī ðĄ âĪs ðĒ ⧠âð â ð· âð â ðĩ ð âĪs ð)) â ðī <<s {(ðī |s ðĩ)}) |
8 | | cofsslt 27240 |
. . 3
âĒ ((ðķ â ðŦ No ⧠âðĄ â ðķ âðĒ â ðī ðĄ âĪs ðĒ ⧠ðī <<s {(ðī |s ðĩ)}) â ðķ <<s {(ðī |s ðĩ)}) |
9 | 3, 4, 7, 8 | syl3anc 1372 |
. 2
âĒ (((ðī <<s ðĩ ⧠ðķ â ðŦ No
⧠ð· â
ðŦ No ) ⧠(âðĨ â ðī âðĶ â ðķ ðĨ âĪs ðĶ ⧠âð§ â ðĩ âðĪ â ð· ðĪ âĪs ð§) ⧠(âðĄ â ðķ âðĒ â ðī ðĄ âĪs ðĒ ⧠âð â ð· âð â ðĩ ð âĪs ð)) â ðķ <<s {(ðī |s ðĩ)}) |
10 | | simp13 1206 |
. . 3
âĒ (((ðī <<s ðĩ ⧠ðķ â ðŦ No
⧠ð· â
ðŦ No ) ⧠(âðĨ â ðī âðĶ â ðķ ðĨ âĪs ðĶ ⧠âð§ â ðĩ âðĪ â ð· ðĪ âĪs ð§) ⧠(âðĄ â ðķ âðĒ â ðī ðĄ âĪs ðĒ ⧠âð â ð· âð â ðĩ ð âĪs ð)) â ð· â ðŦ No
) |
11 | | simp3r 1203 |
. . 3
âĒ (((ðī <<s ðĩ ⧠ðķ â ðŦ No
⧠ð· â
ðŦ No ) ⧠(âðĨ â ðī âðĶ â ðķ ðĨ âĪs ðĶ ⧠âð§ â ðĩ âðĪ â ð· ðĪ âĪs ð§) ⧠(âðĄ â ðķ âðĒ â ðī ðĄ âĪs ðĒ ⧠âð â ð· âð â ðĩ ð âĪs ð)) â âð â ð· âð â ðĩ ð âĪs ð) |
12 | 6 | simp3d 1145 |
. . 3
âĒ (((ðī <<s ðĩ ⧠ðķ â ðŦ No
⧠ð· â
ðŦ No ) ⧠(âðĨ â ðī âðĶ â ðķ ðĨ âĪs ðĶ ⧠âð§ â ðĩ âðĪ â ð· ðĪ âĪs ð§) ⧠(âðĄ â ðķ âðĒ â ðī ðĄ âĪs ðĒ ⧠âð â ð· âð â ðĩ ð âĪs ð)) â {(ðī |s ðĩ)} <<s ðĩ) |
13 | | coinitsslt 27241 |
. . 3
âĒ ((ð· â ðŦ No ⧠âð â ð· âð â ðĩ ð âĪs ð ⧠{(ðī |s ðĩ)} <<s ðĩ) â {(ðī |s ðĩ)} <<s ð·) |
14 | 10, 11, 12, 13 | syl3anc 1372 |
. 2
âĒ (((ðī <<s ðĩ ⧠ðķ â ðŦ No
⧠ð· â
ðŦ No ) ⧠(âðĨ â ðī âðĶ â ðķ ðĨ âĪs ðĶ ⧠âð§ â ðĩ âðĪ â ð· ðĪ âĪs ð§) ⧠(âðĄ â ðķ âðĒ â ðī ðĄ âĪs ðĒ ⧠âð â ð· âð â ðĩ ð âĪs ð)) â {(ðī |s ðĩ)} <<s ð·) |
15 | | cofcut1 27242 |
. 2
âĒ ((ðī <<s ðĩ ⧠(âðĨ â ðī âðĶ â ðķ ðĨ âĪs ðĶ ⧠âð§ â ðĩ âðĪ â ð· ðĪ âĪs ð§) ⧠(ðķ <<s {(ðī |s ðĩ)} ⧠{(ðī |s ðĩ)} <<s ð·)) â (ðī |s ðĩ) = (ðķ |s ð·)) |
16 | 1, 2, 9, 14, 15 | syl112anc 1375 |
1
âĒ (((ðī <<s ðĩ ⧠ðķ â ðŦ No
⧠ð· â
ðŦ No ) ⧠(âðĨ â ðī âðĶ â ðķ ðĨ âĪs ðĶ ⧠âð§ â ðĩ âðĪ â ð· ðĪ âĪs ð§) ⧠(âðĄ â ðķ âðĒ â ðī ðĄ âĪs ðĒ ⧠âð â ð· âð â ðĩ ð âĪs ð)) â (ðī |s ðĩ) = (ðķ |s ð·)) |