Metamath Proof Explorer

Theorem safesnsupfidom1o

Description: If B is a finite subset of ordered class A , we can safely create a small subset with the same largest element and upper bound, if any. (Contributed by RP, 1-Sep-2024)

Ref Expression
Hypotheses safesnsupfidom1o.small 
|- ( ph -> ( O = (/) \/ O = 1o ) )
safesnsupfidom1o.finite 
|- ( ph -> B e. Fin )
Assertion safesnsupfidom1o 
|- ( ph -> if ( O ~< B , { sup ( B , A , R ) } , B ) ~<_ 1o )

Proof

Step Hyp Ref Expression
1 safesnsupfidom1o.small 
 |-  ( ph -> ( O = (/) \/ O = 1o ) )
2 safesnsupfidom1o.finite 
 |-  ( ph -> B e. Fin )
3 iftrue 
 |-  ( O ~< B -> if ( O ~< B , { sup ( B , A , R ) } , B ) = { sup ( B , A , R ) } )
4 3 adantl 
 |-  ( ( ph /\ O ~< B ) -> if ( O ~< B , { sup ( B , A , R ) } , B ) = { sup ( B , A , R ) } )
5 ensn1g 
 |-  ( sup ( B , A , R ) e. _V -> { sup ( B , A , R ) } ~~ 1o )
6 1on 
 |-  1o e. On
7 domrefg 
 |-  ( 1o e. On -> 1o ~<_ 1o )
8 6 7 ax-mp 
 |-  1o ~<_ 1o
9 endomtr 
 |-  ( ( { sup ( B , A , R ) } ~~ 1o /\ 1o ~<_ 1o ) -> { sup ( B , A , R ) } ~<_ 1o )
10 5 8 9 sylancl 
 |-  ( sup ( B , A , R ) e. _V -> { sup ( B , A , R ) } ~<_ 1o )
11 snprc 
 |-  ( -. sup ( B , A , R ) e. _V <-> { sup ( B , A , R ) } = (/) )
12 snex 
 |-  { sup ( B , A , R ) } e. _V
13 eqeng 
 |-  ( { sup ( B , A , R ) } e. _V -> ( { sup ( B , A , R ) } = (/) -> { sup ( B , A , R ) } ~~ (/) ) )
14 12 13 ax-mp 
 |-  ( { sup ( B , A , R ) } = (/) -> { sup ( B , A , R ) } ~~ (/) )
15 11 14 sylbi 
 |-  ( -. sup ( B , A , R ) e. _V -> { sup ( B , A , R ) } ~~ (/) )
16 0domg 
 |-  ( 1o e. On -> (/) ~<_ 1o )
17 6 16 ax-mp 
 |-  (/) ~<_ 1o
18 endomtr 
 |-  ( ( { sup ( B , A , R ) } ~~ (/) /\ (/) ~<_ 1o ) -> { sup ( B , A , R ) } ~<_ 1o )
19 15 17 18 sylancl 
 |-  ( -. sup ( B , A , R ) e. _V -> { sup ( B , A , R ) } ~<_ 1o )
20 10 19 pm2.61i 
 |-  { sup ( B , A , R ) } ~<_ 1o
21 4 20 eqbrtrdi 
 |-  ( ( ph /\ O ~< B ) -> if ( O ~< B , { sup ( B , A , R ) } , B ) ~<_ 1o )
22 iffalse 
 |-  ( -. O ~< B -> if ( O ~< B , { sup ( B , A , R ) } , B ) = B )
23 22 adantl 
 |-  ( ( ph /\ -. O ~< B ) -> if ( O ~< B , { sup ( B , A , R ) } , B ) = B )
24 0elon 
 |-  (/) e. On
25 eleq1 
 |-  ( O = (/) -> ( O e. On <-> (/) e. On ) )
26 24 25 mpbiri 
 |-  ( O = (/) -> O e. On )
27 eleq1 
 |-  ( O = 1o -> ( O e. On <-> 1o e. On ) )
28 6 27 mpbiri 
 |-  ( O = 1o -> O e. On )
29 26 28 jaoi 
 |-  ( ( O = (/) \/ O = 1o ) -> O e. On )
30 fidomtri 
 |-  ( ( B e. Fin /\ O e. On ) -> ( B ~<_ O <-> -. O ~< B ) )
31 29 30 sylan2 
 |-  ( ( B e. Fin /\ ( O = (/) \/ O = 1o ) ) -> ( B ~<_ O <-> -. O ~< B ) )
32 breq2 
 |-  ( O = (/) -> ( B ~<_ O <-> B ~<_ (/) ) )
33 domtr 
 |-  ( ( B ~<_ (/) /\ (/) ~<_ 1o ) -> B ~<_ 1o )
34 17 33 mpan2 
 |-  ( B ~<_ (/) -> B ~<_ 1o )
35 32 34 syl6bi 
 |-  ( O = (/) -> ( B ~<_ O -> B ~<_ 1o ) )
36 breq2 
 |-  ( O = 1o -> ( B ~<_ O <-> B ~<_ 1o ) )
37 36 biimpd 
 |-  ( O = 1o -> ( B ~<_ O -> B ~<_ 1o ) )
38 35 37 jaoi 
 |-  ( ( O = (/) \/ O = 1o ) -> ( B ~<_ O -> B ~<_ 1o ) )
39 38 adantl 
 |-  ( ( B e. Fin /\ ( O = (/) \/ O = 1o ) ) -> ( B ~<_ O -> B ~<_ 1o ) )
40 31 39 sylbird 
 |-  ( ( B e. Fin /\ ( O = (/) \/ O = 1o ) ) -> ( -. O ~< B -> B ~<_ 1o ) )
41 2 1 40 syl2anc 
 |-  ( ph -> ( -. O ~< B -> B ~<_ 1o ) )
42 41 imp 
 |-  ( ( ph /\ -. O ~< B ) -> B ~<_ 1o )
43 23 42 eqbrtrd 
 |-  ( ( ph /\ -. O ~< B ) -> if ( O ~< B , { sup ( B , A , R ) } , B ) ~<_ 1o )
44 21 43 pm2.61dan 
 |-  ( ph -> if ( O ~< B , { sup ( B , A , R ) } , B ) ~<_ 1o )