| Parents |
| hol |
| Constants |
|
∅i
|
IND |
|
$∈i
|
IND → IND → BOOL |
|
suci
|
IND → IND |
| Aliases |
|
∅
|
∅i : IND |
|
∈
|
$∈i : IND → IND → BOOL |
|
suc
|
suci : IND → IND |
| Fixity |
| Right Infix 240: |
∈i |
| Axioms |
|
strong_infinity_axiom
|
⊢ ∃  mk_var("∈i",  (IND → IND → BOOL)⌝)⌝
 • ∀ p • ∃ q • p ∈i q ∧ (∀ x • x ∈i q ⇒ (∃ y • y ∈i q ∧ (∀ Z • ∃ z • z ∈i y ∧ (∀ v • v ∈i z ⇔ v ∈i x ∧ Z v))) ∧ (∀ f • (∀ u• u ∈i x ⇒ f u ∈i q) ⇒ (∃ y • y ∈i q ∧ (∀ u• u ∈i x ⇒ f u ∈i y))))
|
| Definitions |
|
∅i
|
⊢ T |
|
∈i
|
⊢ ∀ p • ∃ q • p ∈ q ∧ (∀ x • x ∈ q ⇒ (∃ y • y ∈ q ∧ (∀ Z • ∃ z • z ∈ y ∧ (∀ v• v ∈ z ⇔ v ∈ x ∧ Z v))) ∧ (∀ f • (∀ u• u ∈ x ⇒ f u ∈ q) ⇒ (∃ y • y ∈ q ∧ (∀ u• u ∈ x ⇒ f u ∈ y))))
|
|
suci
|
⊢ ∀ or • suc or = (ε or'• ∀ x• x ∈ or ∨ x = or ⇔ x ∈ or')
|
