![]() |
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 6979 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 3 | ccnv 4624 |
. . 3
![]() ![]() ![]() |
6 | 1, 2, 5 | csup 6978 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 4, 6 | wceq 1353 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: infeq1 7007 infeq2 7010 infeq3 7011 infeq123d 7012 nfinf 7013 eqinfti 7016 infvalti 7018 infclti 7019 inflbti 7020 infglbti 7021 infsnti 7026 inf00 7027 infisoti 7028 infex2g 7030 dfinfre 8909 infrenegsupex 9590 infxrnegsupex 11264 |
Copyright terms: Public domain | W3C validator |