Description: A nonempty subclass of an ordinal class has a minimal element. Proposition 7.5 of TakeutiZaring p. 36. (Contributed by NM, 18-Feb-2004) (Revised by David Abernethy, 16-Mar-2011)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | tz7.5 | |- ( ( Ord A /\ B C_ A /\ B =/= (/) ) -> E. x e. B ( B i^i x ) = (/) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ordwe | |- ( Ord A -> _E We A ) |
|
| 2 | wefrc | |- ( ( _E We A /\ B C_ A /\ B =/= (/) ) -> E. x e. B ( B i^i x ) = (/) ) |
|
| 3 | 1 2 | syl3an1 | |- ( ( Ord A /\ B C_ A /\ B =/= (/) ) -> E. x e. B ( B i^i x ) = (/) ) |