Metamath Proof Explorer

Theorem safesnsupfilb

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, 3-Sep-2024)

Ref Expression
Hypotheses safesnsupfilb.small 
|- ( ph -> ( O = (/) \/ O = 1o ) )
safesnsupfilb.finite 
|- ( ph -> B e. Fin )
safesnsupfilb.subset 
|- ( ph -> B C_ A )
safesnsupfilb.ordered 
|- ( ph -> R Or A )
Assertion safesnsupfilb 
|- ( ph -> A. x e. ( B \ if ( O ~< B , { sup ( B , A , R ) } , B ) ) A. y e. if ( O ~< B , { sup ( B , A , R ) } , B ) x R y )

Proof

Step Hyp Ref Expression
1 safesnsupfilb.small 
 |-  ( ph -> ( O = (/) \/ O = 1o ) )
2 safesnsupfilb.finite 
 |-  ( ph -> B e. Fin )
3 safesnsupfilb.subset 
 |-  ( ph -> B C_ A )
4 safesnsupfilb.ordered 
 |-  ( ph -> R Or A )
5 4 ad2antrr 
 |-  ( ( ( ph /\ O ~< B ) /\ x e. B ) -> R Or A )
6 3 ad2antrr 
 |-  ( ( ( ph /\ O ~< B ) /\ x e. B ) -> B C_ A )
7 2 ad2antrr 
 |-  ( ( ( ph /\ O ~< B ) /\ x e. B ) -> B e. Fin )
8 simpr 
 |-  ( ( ( ph /\ O ~< B ) /\ x e. B ) -> x e. B )
9 eqidd 
 |-  ( ( ( ph /\ O ~< B ) /\ x e. B ) -> sup ( B , A , R ) = sup ( B , A , R ) )
10 5 6 7 8 9 supgtoreq 
 |-  ( ( ( ph /\ O ~< B ) /\ x e. B ) -> ( x R sup ( B , A , R ) \/ x = sup ( B , A , R ) ) )
11 df-or 
 |-  ( ( x = sup ( B , A , R ) \/ x R sup ( B , A , R ) ) <-> ( -. x = sup ( B , A , R ) -> x R sup ( B , A , R ) ) )
12 orcom 
 |-  ( ( x R sup ( B , A , R ) \/ x = sup ( B , A , R ) ) <-> ( x = sup ( B , A , R ) \/ x R sup ( B , A , R ) ) )
13 df-ne 
 |-  ( x =/= sup ( B , A , R ) <-> -. x = sup ( B , A , R ) )
14 13 imbi1i 
 |-  ( ( x =/= sup ( B , A , R ) -> x R sup ( B , A , R ) ) <-> ( -. x = sup ( B , A , R ) -> x R sup ( B , A , R ) ) )
15 11 12 14 3bitr4i 
 |-  ( ( x R sup ( B , A , R ) \/ x = sup ( B , A , R ) ) <-> ( x =/= sup ( B , A , R ) -> x R sup ( B , A , R ) ) )
16 10 15 sylib 
 |-  ( ( ( ph /\ O ~< B ) /\ x e. B ) -> ( x =/= sup ( B , A , R ) -> x R sup ( B , A , R ) ) )
17 16 ralrimiva 
 |-  ( ( ph /\ O ~< B ) -> A. x e. B ( x =/= sup ( B , A , R ) -> x R sup ( B , A , R ) ) )
18 iftrue 
 |-  ( O ~< B -> if ( O ~< B , { sup ( B , A , R ) } , B ) = { sup ( B , A , R ) } )
19 18 difeq2d 
 |-  ( O ~< B -> ( B \ if ( O ~< B , { sup ( B , A , R ) } , B ) ) = ( B \ { sup ( B , A , R ) } ) )
20 19 adantl 
 |-  ( ( ph /\ O ~< B ) -> ( B \ if ( O ~< B , { sup ( B , A , R ) } , B ) ) = ( B \ { sup ( B , A , R ) } ) )
21 20 raleqdv 
 |-  ( ( ph /\ O ~< B ) -> ( A. x e. ( B \ if ( O ~< B , { sup ( B , A , R ) } , B ) ) A. y e. if ( O ~< B , { sup ( B , A , R ) } , B ) x R y <-> A. x e. ( B \ { sup ( B , A , R ) } ) A. y e. if ( O ~< B , { sup ( B , A , R ) } , B ) x R y ) )
22 simpr 
 |-  ( ( ph /\ O ~< B ) -> O ~< B )
23 22 iftrued 
 |-  ( ( ph /\ O ~< B ) -> if ( O ~< B , { sup ( B , A , R ) } , B ) = { sup ( B , A , R ) } )
24 23 raleqdv 
 |-  ( ( ph /\ O ~< B ) -> ( A. y e. if ( O ~< B , { sup ( B , A , R ) } , B ) x R y <-> A. y e. { sup ( B , A , R ) } x R y ) )
25 2 adantr 
 |-  ( ( ph /\ O ~< B ) -> B e. Fin )
26 1 adantr 
 |-  ( ( ph /\ O ~< B ) -> ( O = (/) \/ O = 1o ) )
27 0elon 
 |-  (/) e. On
28 eleq1 
 |-  ( O = (/) -> ( O e. On <-> (/) e. On ) )
29 27 28 mpbiri 
 |-  ( O = (/) -> O e. On )
30 1on 
 |-  1o e. On
31 eleq1 
 |-  ( O = 1o -> ( O e. On <-> 1o e. On ) )
32 30 31 mpbiri 
 |-  ( O = 1o -> O e. On )
33 29 32 jaoi 
 |-  ( ( O = (/) \/ O = 1o ) -> O e. On )
34 26 33 syl 
 |-  ( ( ph /\ O ~< B ) -> O e. On )
35 22 34 sdomne0d 
 |-  ( ( ph /\ O ~< B ) -> B =/= (/) )
36 3 adantr 
 |-  ( ( ph /\ O ~< B ) -> B C_ A )
37 25 35 36 3jca 
 |-  ( ( ph /\ O ~< B ) -> ( B e. Fin /\ B =/= (/) /\ B C_ A ) )
38 fisupcl 
 |-  ( ( R Or A /\ ( B e. Fin /\ B =/= (/) /\ B C_ A ) ) -> sup ( B , A , R ) e. B )
39 4 37 38 syl2an2r 
 |-  ( ( ph /\ O ~< B ) -> sup ( B , A , R ) e. B )
40 breq2 
 |-  ( y = sup ( B , A , R ) -> ( x R y <-> x R sup ( B , A , R ) ) )
41 40 ralsng 
 |-  ( sup ( B , A , R ) e. B -> ( A. y e. { sup ( B , A , R ) } x R y <-> x R sup ( B , A , R ) ) )
42 39 41 syl 
 |-  ( ( ph /\ O ~< B ) -> ( A. y e. { sup ( B , A , R ) } x R y <-> x R sup ( B , A , R ) ) )
43 24 42 bitrd 
 |-  ( ( ph /\ O ~< B ) -> ( A. y e. if ( O ~< B , { sup ( B , A , R ) } , B ) x R y <-> x R sup ( B , A , R ) ) )
44 43 ralbidv 
 |-  ( ( ph /\ O ~< B ) -> ( A. x e. ( B \ { sup ( B , A , R ) } ) A. y e. if ( O ~< B , { sup ( B , A , R ) } , B ) x R y <-> A. x e. ( B \ { sup ( B , A , R ) } ) x R sup ( B , A , R ) ) )
45 raldifsnb 
 |-  ( A. x e. B ( x =/= sup ( B , A , R ) -> x R sup ( B , A , R ) ) <-> A. x e. ( B \ { sup ( B , A , R ) } ) x R sup ( B , A , R ) )
46 44 45 bitr4di 
 |-  ( ( ph /\ O ~< B ) -> ( A. x e. ( B \ { sup ( B , A , R ) } ) A. y e. if ( O ~< B , { sup ( B , A , R ) } , B ) x R y <-> A. x e. B ( x =/= sup ( B , A , R ) -> x R sup ( B , A , R ) ) ) )
47 21 46 bitrd 
 |-  ( ( ph /\ O ~< B ) -> ( A. x e. ( B \ if ( O ~< B , { sup ( B , A , R ) } , B ) ) A. y e. if ( O ~< B , { sup ( B , A , R ) } , B ) x R y <-> A. x e. B ( x =/= sup ( B , A , R ) -> x R sup ( B , A , R ) ) ) )
48 17 47 mpbird 
 |-  ( ( ph /\ O ~< B ) -> A. x e. ( B \ if ( O ~< B , { sup ( B , A , R ) } , B ) ) A. y e. if ( O ~< B , { sup ( B , A , R ) } , B ) x R y )
49 ral0 
 |-  A. x e. (/) A. y e. if ( O ~< B , { sup ( B , A , R ) } , B ) x R y
50 iffalse 
 |-  ( -. O ~< B -> if ( O ~< B , { sup ( B , A , R ) } , B ) = B )
51 50 adantl 
 |-  ( ( ph /\ -. O ~< B ) -> if ( O ~< B , { sup ( B , A , R ) } , B ) = B )
52 51 difeq2d 
 |-  ( ( ph /\ -. O ~< B ) -> ( B \ if ( O ~< B , { sup ( B , A , R ) } , B ) ) = ( B \ B ) )
53 difid 
 |-  ( B \ B ) = (/)
54 52 53 eqtrdi 
 |-  ( ( ph /\ -. O ~< B ) -> ( B \ if ( O ~< B , { sup ( B , A , R ) } , B ) ) = (/) )
55 54 raleqdv 
 |-  ( ( ph /\ -. O ~< B ) -> ( A. x e. ( B \ if ( O ~< B , { sup ( B , A , R ) } , B ) ) A. y e. if ( O ~< B , { sup ( B , A , R ) } , B ) x R y <-> A. x e. (/) A. y e. if ( O ~< B , { sup ( B , A , R ) } , B ) x R y ) )
56 49 55 mpbiri 
 |-  ( ( ph /\ -. O ~< B ) -> A. x e. ( B \ if ( O ~< B , { sup ( B , A , R ) } , B ) ) A. y e. if ( O ~< B , { sup ( B , A , R ) } , B ) x R y )
57 48 56 pm2.61dan 
 |-  ( ph -> A. x e. ( B \ if ( O ~< B , { sup ( B , A , R ) } , B ) ) A. y e. if ( O ~< B , { sup ( B , A , R ) } , B ) x R y )