![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-inf | Unicode version |
Description: Define the infimum of
class ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
df-inf |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA |
. . 3
![]() ![]() | |
2 | cB |
. . 3
![]() ![]() | |
3 | cR |
. . 3
![]() ![]() | |
4 | 1, 2, 3 | cinf 6981 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 3 | ccnv 4625 |
. . 3
![]() ![]() ![]() |
6 | 1, 2, 5 | csup 6980 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 4, 6 | wceq 1353 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: infeq1 7009 infeq2 7012 infeq3 7013 infeq123d 7014 nfinf 7015 eqinfti 7018 infvalti 7020 infclti 7021 inflbti 7022 infglbti 7023 infsnti 7028 inf00 7029 infisoti 7030 infex2g 7032 dfinfre 8912 infrenegsupex 9593 infxrnegsupex 11270 |
Copyright terms: Public domain | W3C validator |