# Metamath Proof Explorer

## Theorem onint

Description: The intersection (infimum) of a nonempty class of ordinal numbers belongs to the class. Compare Exercise 4 of TakeutiZaring p. 45. (Contributed by NM, 31-Jan-1997)

Ref Expression
Assertion onint
`|- ( ( A C_ On /\ A =/= (/) ) -> |^| A e. A )`

### Proof

Step Hyp Ref Expression
1 ordon
` |-  Ord On`
2 tz7.5
` |-  ( ( Ord On /\ A C_ On /\ A =/= (/) ) -> E. x e. A ( A i^i x ) = (/) )`
3 1 2 mp3an1
` |-  ( ( A C_ On /\ A =/= (/) ) -> E. x e. A ( A i^i x ) = (/) )`
4 ssel
` |-  ( A C_ On -> ( x e. A -> x e. On ) )`
5 4 imdistani
` |-  ( ( A C_ On /\ x e. A ) -> ( A C_ On /\ x e. On ) )`
6 ssel
` |-  ( A C_ On -> ( z e. A -> z e. On ) )`
7 ontri1
` |-  ( ( x e. On /\ z e. On ) -> ( x C_ z <-> -. z e. x ) )`
8 ssel
` |-  ( x C_ z -> ( y e. x -> y e. z ) )`
9 7 8 syl6bir
` |-  ( ( x e. On /\ z e. On ) -> ( -. z e. x -> ( y e. x -> y e. z ) ) )`
10 9 ex
` |-  ( x e. On -> ( z e. On -> ( -. z e. x -> ( y e. x -> y e. z ) ) ) )`
11 6 10 sylan9
` |-  ( ( A C_ On /\ x e. On ) -> ( z e. A -> ( -. z e. x -> ( y e. x -> y e. z ) ) ) )`
12 11 com4r
` |-  ( y e. x -> ( ( A C_ On /\ x e. On ) -> ( z e. A -> ( -. z e. x -> y e. z ) ) ) )`
13 12 imp31
` |-  ( ( ( y e. x /\ ( A C_ On /\ x e. On ) ) /\ z e. A ) -> ( -. z e. x -> y e. z ) )`
14 13 ralimdva
` |-  ( ( y e. x /\ ( A C_ On /\ x e. On ) ) -> ( A. z e. A -. z e. x -> A. z e. A y e. z ) )`
15 disj
` |-  ( ( A i^i x ) = (/) <-> A. z e. A -. z e. x )`
16 vex
` |-  y e. _V`
17 16 elint2
` |-  ( y e. |^| A <-> A. z e. A y e. z )`
18 14 15 17 3imtr4g
` |-  ( ( y e. x /\ ( A C_ On /\ x e. On ) ) -> ( ( A i^i x ) = (/) -> y e. |^| A ) )`
19 5 18 sylan2
` |-  ( ( y e. x /\ ( A C_ On /\ x e. A ) ) -> ( ( A i^i x ) = (/) -> y e. |^| A ) )`
20 19 exp32
` |-  ( y e. x -> ( A C_ On -> ( x e. A -> ( ( A i^i x ) = (/) -> y e. |^| A ) ) ) )`
21 20 com4l
` |-  ( A C_ On -> ( x e. A -> ( ( A i^i x ) = (/) -> ( y e. x -> y e. |^| A ) ) ) )`
22 21 imp32
` |-  ( ( A C_ On /\ ( x e. A /\ ( A i^i x ) = (/) ) ) -> ( y e. x -> y e. |^| A ) )`
23 22 ssrdv
` |-  ( ( A C_ On /\ ( x e. A /\ ( A i^i x ) = (/) ) ) -> x C_ |^| A )`
24 intss1
` |-  ( x e. A -> |^| A C_ x )`
` |-  ( ( A C_ On /\ ( x e. A /\ ( A i^i x ) = (/) ) ) -> |^| A C_ x )`
26 23 25 eqssd
` |-  ( ( A C_ On /\ ( x e. A /\ ( A i^i x ) = (/) ) ) -> x = |^| A )`
27 26 eleq1d
` |-  ( ( A C_ On /\ ( x e. A /\ ( A i^i x ) = (/) ) ) -> ( x e. A <-> |^| A e. A ) )`
28 27 biimpd
` |-  ( ( A C_ On /\ ( x e. A /\ ( A i^i x ) = (/) ) ) -> ( x e. A -> |^| A e. A ) )`
29 28 exp32
` |-  ( A C_ On -> ( x e. A -> ( ( A i^i x ) = (/) -> ( x e. A -> |^| A e. A ) ) ) )`
30 29 com34
` |-  ( A C_ On -> ( x e. A -> ( x e. A -> ( ( A i^i x ) = (/) -> |^| A e. A ) ) ) )`
31 30 pm2.43d
` |-  ( A C_ On -> ( x e. A -> ( ( A i^i x ) = (/) -> |^| A e. A ) ) )`
32 31 rexlimdv
` |-  ( A C_ On -> ( E. x e. A ( A i^i x ) = (/) -> |^| A e. A ) )`
33 3 32 syl5
` |-  ( A C_ On -> ( ( A C_ On /\ A =/= (/) ) -> |^| A e. A ) )`
34 33 anabsi5
` |-  ( ( A C_ On /\ A =/= (/) ) -> |^| A e. A )`