Detailed syntax breakdown of Definition df-si3
| Step | Hyp | Ref
| Expression |
|---|
| 1 | | cA |
. . 3
class A |
| 2 | 1 | csi3 5757 |
. 2
class SI3 A |
| 3 | | c1st 4717 |
. . . . 5
class 1st |
| 4 | 3 | csi 4720 |
. . . 4
class SI
1st |
| 5 | | c2nd 4783 |
. . . . . . 7
class 2nd |
| 6 | 3, 5 | ccom 4721 |
. . . . . 6
class (1st ∘ 2nd ) |
| 7 | 6 | csi 4720 |
. . . . 5
class SI
(1st ∘ 2nd
) |
| 8 | 5, 5 | ccom 4721 |
. . . . . 6
class (2nd ∘ 2nd ) |
| 9 | 8 | csi 4720 |
. . . . 5
class SI
(2nd ∘ 2nd
) |
| 10 | 7, 9 | ctxp 5735 |
. . . 4
class ( SI
(1st ∘ 2nd )
⊗ SI (2nd ∘ 2nd )) |
| 11 | 4, 10 | ctxp 5735 |
. . 3
class ( SI
1st ⊗ ( SI
(1st ∘ 2nd )
⊗ SI (2nd ∘ 2nd ))) |
| 12 | 1 | cpw1 4135 |
. . 3
class ℘1A |
| 13 | 11, 12 | cima 4722 |
. 2
class (( SI
1st ⊗ ( SI
(1st ∘ 2nd )
⊗ SI (2nd ∘ 2nd ))) “ ℘1A) |
| 14 | 2, 13 | wceq 1642 |
1
wff SI3 A = (( SI
1st ⊗ ( SI
(1st ∘ 2nd )
⊗ SI (2nd ∘ 2nd ))) “ ℘1A) |
