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 ⊢ ( 𝜑 → ( 𝑂 = ∅ ∨ 𝑂 = 1o ) )
safesnsupfilb.finite ⊢ ( 𝜑 → 𝐵 ∈ Fin )
safesnsupfilb.subset ⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
safesnsupfilb.ordered ⊢ ( 𝜑 → 𝑅 Or 𝐴 )
Assertion safesnsupfilb ( 𝜑 → ∀ 𝑥 ∈ ( 𝐵 ∖ if ( 𝑂 ≺ 𝐵 , { sup ( 𝐵 , 𝐴 , 𝑅 ) } , 𝐵 ) ) ∀ 𝑦 ∈ if ( 𝑂 ≺ 𝐵 , { sup ( 𝐵 , 𝐴 , 𝑅 ) } , 𝐵 ) 𝑥 𝑅 𝑦 )

Proof

Step Hyp Ref Expression
1 safesnsupfilb.small ⊢ ( 𝜑 → ( 𝑂 = ∅ ∨ 𝑂 = 1o ) )
2 safesnsupfilb.finite ⊢ ( 𝜑 → 𝐵 ∈ Fin )
3 safesnsupfilb.subset ⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
4 safesnsupfilb.ordered ⊢ ( 𝜑 → 𝑅 Or 𝐴 )
5 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑂 ≺ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑅 Or 𝐴 )
6 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑂 ≺ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝐵 ⊆ 𝐴 )
7 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑂 ≺ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝐵 ∈ Fin )
8 simpr ⊢ ( ( ( 𝜑 ∧ 𝑂 ≺ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
9 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑂 ≺ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → sup ( 𝐵 , 𝐴 , 𝑅 ) = sup ( 𝐵 , 𝐴 , 𝑅 ) )
10 5 6 7 8 9 supgtoreq ⊢ ( ( ( 𝜑 ∧ 𝑂 ≺ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ∨ 𝑥 = sup ( 𝐵 , 𝐴 , 𝑅 ) ) )
11 df-or ⊢ ( ( 𝑥 = sup ( 𝐵 , 𝐴 , 𝑅 ) ∨ 𝑥 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) ↔ ( ¬ 𝑥 = sup ( 𝐵 , 𝐴 , 𝑅 ) → 𝑥 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) )
12 orcom ⊢ ( ( 𝑥 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ∨ 𝑥 = sup ( 𝐵 , 𝐴 , 𝑅 ) ) ↔ ( 𝑥 = sup ( 𝐵 , 𝐴 , 𝑅 ) ∨ 𝑥 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) )
13 df-ne ⊢ ( 𝑥 ≠ sup ( 𝐵 , 𝐴 , 𝑅 ) ↔ ¬ 𝑥 = sup ( 𝐵 , 𝐴 , 𝑅 ) )
14 13 imbi1i ⊢ ( ( 𝑥 ≠ sup ( 𝐵 , 𝐴 , 𝑅 ) → 𝑥 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) ↔ ( ¬ 𝑥 = sup ( 𝐵 , 𝐴 , 𝑅 ) → 𝑥 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) )
15 11 12 14 3bitr4i ⊢ ( ( 𝑥 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ∨ 𝑥 = sup ( 𝐵 , 𝐴 , 𝑅 ) ) ↔ ( 𝑥 ≠ sup ( 𝐵 , 𝐴 , 𝑅 ) → 𝑥 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) )
16 10 15 sylib ⊢ ( ( ( 𝜑 ∧ 𝑂 ≺ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ≠ sup ( 𝐵 , 𝐴 , 𝑅 ) → 𝑥 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) )
17 16 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑂 ≺ 𝐵 ) → ∀ 𝑥 ∈ 𝐵 ( 𝑥 ≠ sup ( 𝐵 , 𝐴 , 𝑅 ) → 𝑥 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) )
18 iftrue ⊢ ( 𝑂 ≺ 𝐵 → if ( 𝑂 ≺ 𝐵 , { sup ( 𝐵 , 𝐴 , 𝑅 ) } , 𝐵 ) = { sup ( 𝐵 , 𝐴 , 𝑅 ) } )
19 18 difeq2d ⊢ ( 𝑂 ≺ 𝐵 → ( 𝐵 ∖ if ( 𝑂 ≺ 𝐵 , { sup ( 𝐵 , 𝐴 , 𝑅 ) } , 𝐵 ) ) = ( 𝐵 ∖ { sup ( 𝐵 , 𝐴 , 𝑅 ) } ) )
20 19 adantl ⊢ ( ( 𝜑 ∧ 𝑂 ≺ 𝐵 ) → ( 𝐵 ∖ if ( 𝑂 ≺ 𝐵 , { sup ( 𝐵 , 𝐴 , 𝑅 ) } , 𝐵 ) ) = ( 𝐵 ∖ { sup ( 𝐵 , 𝐴 , 𝑅 ) } ) )
21 20 raleqdv ⊢ ( ( 𝜑 ∧ 𝑂 ≺ 𝐵 ) → ( ∀ 𝑥 ∈ ( 𝐵 ∖ if ( 𝑂 ≺ 𝐵 , { sup ( 𝐵 , 𝐴 , 𝑅 ) } , 𝐵 ) ) ∀ 𝑦 ∈ if ( 𝑂 ≺ 𝐵 , { sup ( 𝐵 , 𝐴 , 𝑅 ) } , 𝐵 ) 𝑥 𝑅 𝑦 ↔ ∀ 𝑥 ∈ ( 𝐵 ∖ { sup ( 𝐵 , 𝐴 , 𝑅 ) } ) ∀ 𝑦 ∈ if ( 𝑂 ≺ 𝐵 , { sup ( 𝐵 , 𝐴 , 𝑅 ) } , 𝐵 ) 𝑥 𝑅 𝑦 ) )
22 simpr ⊢ ( ( 𝜑 ∧ 𝑂 ≺ 𝐵 ) → 𝑂 ≺ 𝐵 )
23 22 iftrued ⊢ ( ( 𝜑 ∧ 𝑂 ≺ 𝐵 ) → if ( 𝑂 ≺ 𝐵 , { sup ( 𝐵 , 𝐴 , 𝑅 ) } , 𝐵 ) = { sup ( 𝐵 , 𝐴 , 𝑅 ) } )
24 23 raleqdv ⊢ ( ( 𝜑 ∧ 𝑂 ≺ 𝐵 ) → ( ∀ 𝑦 ∈ if ( 𝑂 ≺ 𝐵 , { sup ( 𝐵 , 𝐴 , 𝑅 ) } , 𝐵 ) 𝑥 𝑅 𝑦 ↔ ∀ 𝑦 ∈ { sup ( 𝐵 , 𝐴 , 𝑅 ) } 𝑥 𝑅 𝑦 ) )
25 2 adantr ⊢ ( ( 𝜑 ∧ 𝑂 ≺ 𝐵 ) → 𝐵 ∈ Fin )
26 1 adantr ⊢ ( ( 𝜑 ∧ 𝑂 ≺ 𝐵 ) → ( 𝑂 = ∅ ∨ 𝑂 = 1o ) )
27 0elon ⊢ ∅ ∈ On
28 eleq1 ⊢ ( 𝑂 = ∅ → ( 𝑂 ∈ On ↔ ∅ ∈ On ) )
29 27 28 mpbiri ⊢ ( 𝑂 = ∅ → 𝑂 ∈ On )
30 1on ⊢ 1o ∈ On
31 eleq1 ⊢ ( 𝑂 = 1o → ( 𝑂 ∈ On ↔ 1o ∈ On ) )
32 30 31 mpbiri ⊢ ( 𝑂 = 1o → 𝑂 ∈ On )
33 29 32 jaoi ⊢ ( ( 𝑂 = ∅ ∨ 𝑂 = 1o ) → 𝑂 ∈ On )
34 26 33 syl ⊢ ( ( 𝜑 ∧ 𝑂 ≺ 𝐵 ) → 𝑂 ∈ On )
35 22 34 sdomne0d ⊢ ( ( 𝜑 ∧ 𝑂 ≺ 𝐵 ) → 𝐵 ≠ ∅ )
36 3 adantr ⊢ ( ( 𝜑 ∧ 𝑂 ≺ 𝐵 ) → 𝐵 ⊆ 𝐴 )
37 25 35 36 3jca ⊢ ( ( 𝜑 ∧ 𝑂 ≺ 𝐵 ) → ( 𝐵 ∈ Fin ∧ 𝐵 ≠ ∅ ∧ 𝐵 ⊆ 𝐴 ) )
38 fisupcl ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ Fin ∧ 𝐵 ≠ ∅ ∧ 𝐵 ⊆ 𝐴 ) ) → sup ( 𝐵 , 𝐴 , 𝑅 ) ∈ 𝐵 )
39 4 37 38 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑂 ≺ 𝐵 ) → sup ( 𝐵 , 𝐴 , 𝑅 ) ∈ 𝐵 )
40 breq2 ⊢ ( 𝑦 = sup ( 𝐵 , 𝐴 , 𝑅 ) → ( 𝑥 𝑅 𝑦 ↔ 𝑥 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) )
41 40 ralsng ⊢ ( sup ( 𝐵 , 𝐴 , 𝑅 ) ∈ 𝐵 → ( ∀ 𝑦 ∈ { sup ( 𝐵 , 𝐴 , 𝑅 ) } 𝑥 𝑅 𝑦 ↔ 𝑥 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) )
42 39 41 syl ⊢ ( ( 𝜑 ∧ 𝑂 ≺ 𝐵 ) → ( ∀ 𝑦 ∈ { sup ( 𝐵 , 𝐴 , 𝑅 ) } 𝑥 𝑅 𝑦 ↔ 𝑥 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) )
43 24 42 bitrd ⊢ ( ( 𝜑 ∧ 𝑂 ≺ 𝐵 ) → ( ∀ 𝑦 ∈ if ( 𝑂 ≺ 𝐵 , { sup ( 𝐵 , 𝐴 , 𝑅 ) } , 𝐵 ) 𝑥 𝑅 𝑦 ↔ 𝑥 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) )
44 43 ralbidv ⊢ ( ( 𝜑 ∧ 𝑂 ≺ 𝐵 ) → ( ∀ 𝑥 ∈ ( 𝐵 ∖ { sup ( 𝐵 , 𝐴 , 𝑅 ) } ) ∀ 𝑦 ∈ if ( 𝑂 ≺ 𝐵 , { sup ( 𝐵 , 𝐴 , 𝑅 ) } , 𝐵 ) 𝑥 𝑅 𝑦 ↔ ∀ 𝑥 ∈ ( 𝐵 ∖ { sup ( 𝐵 , 𝐴 , 𝑅 ) } ) 𝑥 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) )
45 raldifsnb ⊢ ( ∀ 𝑥 ∈ 𝐵 ( 𝑥 ≠ sup ( 𝐵 , 𝐴 , 𝑅 ) → 𝑥 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) ↔ ∀ 𝑥 ∈ ( 𝐵 ∖ { sup ( 𝐵 , 𝐴 , 𝑅 ) } ) 𝑥 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) )
46 44 45 bitr4di ⊢ ( ( 𝜑 ∧ 𝑂 ≺ 𝐵 ) → ( ∀ 𝑥 ∈ ( 𝐵 ∖ { sup ( 𝐵 , 𝐴 , 𝑅 ) } ) ∀ 𝑦 ∈ if ( 𝑂 ≺ 𝐵 , { sup ( 𝐵 , 𝐴 , 𝑅 ) } , 𝐵 ) 𝑥 𝑅 𝑦 ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ≠ sup ( 𝐵 , 𝐴 , 𝑅 ) → 𝑥 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) ) )
47 21 46 bitrd ⊢ ( ( 𝜑 ∧ 𝑂 ≺ 𝐵 ) → ( ∀ 𝑥 ∈ ( 𝐵 ∖ if ( 𝑂 ≺ 𝐵 , { sup ( 𝐵 , 𝐴 , 𝑅 ) } , 𝐵 ) ) ∀ 𝑦 ∈ if ( 𝑂 ≺ 𝐵 , { sup ( 𝐵 , 𝐴 , 𝑅 ) } , 𝐵 ) 𝑥 𝑅 𝑦 ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ≠ sup ( 𝐵 , 𝐴 , 𝑅 ) → 𝑥 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) ) )
48 17 47 mpbird ⊢ ( ( 𝜑 ∧ 𝑂 ≺ 𝐵 ) → ∀ 𝑥 ∈ ( 𝐵 ∖ if ( 𝑂 ≺ 𝐵 , { sup ( 𝐵 , 𝐴 , 𝑅 ) } , 𝐵 ) ) ∀ 𝑦 ∈ if ( 𝑂 ≺ 𝐵 , { sup ( 𝐵 , 𝐴 , 𝑅 ) } , 𝐵 ) 𝑥 𝑅 𝑦 )
49 ral0 ⊢ ∀ 𝑥 ∈ ∅ ∀ 𝑦 ∈ if ( 𝑂 ≺ 𝐵 , { sup ( 𝐵 , 𝐴 , 𝑅 ) } , 𝐵 ) 𝑥 𝑅 𝑦
50 iffalse ⊢ ( ¬ 𝑂 ≺ 𝐵 → if ( 𝑂 ≺ 𝐵 , { sup ( 𝐵 , 𝐴 , 𝑅 ) } , 𝐵 ) = 𝐵 )
51 50 adantl ⊢ ( ( 𝜑 ∧ ¬ 𝑂 ≺ 𝐵 ) → if ( 𝑂 ≺ 𝐵 , { sup ( 𝐵 , 𝐴 , 𝑅 ) } , 𝐵 ) = 𝐵 )
52 51 difeq2d ⊢ ( ( 𝜑 ∧ ¬ 𝑂 ≺ 𝐵 ) → ( 𝐵 ∖ if ( 𝑂 ≺ 𝐵 , { sup ( 𝐵 , 𝐴 , 𝑅 ) } , 𝐵 ) ) = ( 𝐵 ∖ 𝐵 ) )
53 difid ⊢ ( 𝐵 ∖ 𝐵 ) = ∅
54 52 53 eqtrdi ⊢ ( ( 𝜑 ∧ ¬ 𝑂 ≺ 𝐵 ) → ( 𝐵 ∖ if ( 𝑂 ≺ 𝐵 , { sup ( 𝐵 , 𝐴 , 𝑅 ) } , 𝐵 ) ) = ∅ )
55 54 raleqdv ⊢ ( ( 𝜑 ∧ ¬ 𝑂 ≺ 𝐵 ) → ( ∀ 𝑥 ∈ ( 𝐵 ∖ if ( 𝑂 ≺ 𝐵 , { sup ( 𝐵 , 𝐴 , 𝑅 ) } , 𝐵 ) ) ∀ 𝑦 ∈ if ( 𝑂 ≺ 𝐵 , { sup ( 𝐵 , 𝐴 , 𝑅 ) } , 𝐵 ) 𝑥 𝑅 𝑦 ↔ ∀ 𝑥 ∈ ∅ ∀ 𝑦 ∈ if ( 𝑂 ≺ 𝐵 , { sup ( 𝐵 , 𝐴 , 𝑅 ) } , 𝐵 ) 𝑥 𝑅 𝑦 ) )
56 49 55 mpbiri ⊢ ( ( 𝜑 ∧ ¬ 𝑂 ≺ 𝐵 ) → ∀ 𝑥 ∈ ( 𝐵 ∖ if ( 𝑂 ≺ 𝐵 , { sup ( 𝐵 , 𝐴 , 𝑅 ) } , 𝐵 ) ) ∀ 𝑦 ∈ if ( 𝑂 ≺ 𝐵 , { sup ( 𝐵 , 𝐴 , 𝑅 ) } , 𝐵 ) 𝑥 𝑅 𝑦 )
57 48 56 pm2.61dan ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐵 ∖ if ( 𝑂 ≺ 𝐵 , { sup ( 𝐵 , 𝐴 , 𝑅 ) } , 𝐵 ) ) ∀ 𝑦 ∈ if ( 𝑂 ≺ 𝐵 , { sup ( 𝐵 , 𝐴 , 𝑅 ) } , 𝐵 ) 𝑥 𝑅 𝑦 )