![]() |
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 6982 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 3 | ccnv 4626 |
. . 3
![]() ![]() ![]() |
6 | 1, 2, 5 | csup 6981 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 4, 6 | wceq 1353 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: infeq1 7010 infeq2 7013 infeq3 7014 infeq123d 7015 nfinf 7016 eqinfti 7019 infvalti 7021 infclti 7022 inflbti 7023 infglbti 7024 infsnti 7029 inf00 7030 infisoti 7031 infex2g 7033 dfinfre 8913 infrenegsupex 9594 infxrnegsupex 11271 |
Copyright terms: Public domain | W3C validator |