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 )
25 24 ad2antrl 
 |-  ( ( 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 )