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 ⊢ φ → O = ∅ ∨ O = 1 𝑜
safesnsupfilb.finite ⊢ φ → B ∈ Fin
safesnsupfilb.subset ⊢ φ → B ⊆ A
safesnsupfilb.ordered ⊢ φ → R Or A
Assertion safesnsupfilb ⊢ φ → ∀ x ∈ B ∖ if O ≺ B sup B A R B ∀ y ∈ if O ≺ B sup B A R B x R y

Proof

Step Hyp Ref Expression
1 safesnsupfilb.small ⊢ φ → O = ∅ ∨ O = 1 𝑜
2 safesnsupfilb.finite ⊢ φ → B ∈ Fin
3 safesnsupfilb.subset ⊢ φ → B ⊆ A
4 safesnsupfilb.ordered ⊢ φ → R Or A
5 4 ad2antrr ⊢ φ ∧ O ≺ B ∧ x ∈ B → R Or A
6 3 ad2antrr ⊢ φ ∧ O ≺ B ∧ x ∈ B → B ⊆ A
7 2 ad2antrr ⊢ φ ∧ O ≺ B ∧ x ∈ B → B ∈ Fin
8 simpr ⊢ φ ∧ O ≺ B ∧ x ∈ B → x ∈ B
9 eqidd ⊢ φ ∧ O ≺ B ∧ x ∈ B → sup B A R = sup B A R
10 5 6 7 8 9 supgtoreq ⊢ φ ∧ O ≺ B ∧ x ∈ 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 ⊢ φ ∧ O ≺ B ∧ x ∈ B → x ≠ sup B A R → x R sup B A R
17 16 ralrimiva ⊢ φ ∧ O ≺ B → ∀ x ∈ 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 ⊢ φ ∧ O ≺ B → B ∖ if O ≺ B sup B A R B = B ∖ sup B A R
21 20 raleqdv ⊢ φ ∧ O ≺ B → ∀ x ∈ B ∖ if O ≺ B sup B A R B ∀ y ∈ if O ≺ B sup B A R B x R y ↔ ∀ x ∈ B ∖ sup B A R ∀ y ∈ if O ≺ B sup B A R B x R y
22 simpr ⊢ φ ∧ O ≺ B → O ≺ B
23 22 iftrued ⊢ φ ∧ O ≺ B → if O ≺ B sup B A R B = sup B A R
24 23 raleqdv ⊢ φ ∧ O ≺ B → ∀ y ∈ if O ≺ B sup B A R B x R y ↔ ∀ y ∈ sup B A R x R y
25 2 adantr ⊢ φ ∧ O ≺ B → B ∈ Fin
26 1 adantr ⊢ φ ∧ O ≺ B → O = ∅ ∨ O = 1 𝑜
27 0elon ⊢ ∅ ∈ On
28 eleq1 ⊢ O = ∅ → O ∈ On ↔ ∅ ∈ On
29 27 28 mpbiri ⊢ O = ∅ → O ∈ On
30 1on ⊢ 1 𝑜 ∈ On
31 eleq1 ⊢ O = 1 𝑜 → O ∈ On ↔ 1 𝑜 ∈ On
32 30 31 mpbiri ⊢ O = 1 𝑜 → O ∈ On
33 29 32 jaoi ⊢ O = ∅ ∨ O = 1 𝑜 → O ∈ On
34 26 33 syl ⊢ φ ∧ O ≺ B → O ∈ On
35 22 34 sdomne0d ⊢ φ ∧ O ≺ B → B ≠ ∅
36 3 adantr ⊢ φ ∧ O ≺ B → B ⊆ A
37 25 35 36 3jca ⊢ φ ∧ O ≺ B → B ∈ Fin ∧ B ≠ ∅ ∧ B ⊆ A
38 fisupcl ⊢ R Or A ∧ B ∈ Fin ∧ B ≠ ∅ ∧ B ⊆ A → sup B A R ∈ B
39 4 37 38 syl2an2r ⊢ φ ∧ O ≺ B → sup B A R ∈ B
40 breq2 ⊢ y = sup B A R → x R y ↔ x R sup B A R
41 40 ralsng ⊢ sup B A R ∈ B → ∀ y ∈ sup B A R x R y ↔ x R sup B A R
42 39 41 syl ⊢ φ ∧ O ≺ B → ∀ y ∈ sup B A R x R y ↔ x R sup B A R
43 24 42 bitrd ⊢ φ ∧ O ≺ B → ∀ y ∈ if O ≺ B sup B A R B x R y ↔ x R sup B A R
44 43 ralbidv ⊢ φ ∧ O ≺ B → ∀ x ∈ B ∖ sup B A R ∀ y ∈ if O ≺ B sup B A R B x R y ↔ ∀ x ∈ B ∖ sup B A R x R sup B A R
45 raldifsnb ⊢ ∀ x ∈ B x ≠ sup B A R → x R sup B A R ↔ ∀ x ∈ B ∖ sup B A R x R sup B A R
46 44 45 bitr4di ⊢ φ ∧ O ≺ B → ∀ x ∈ B ∖ sup B A R ∀ y ∈ if O ≺ B sup B A R B x R y ↔ ∀ x ∈ B x ≠ sup B A R → x R sup B A R
47 21 46 bitrd ⊢ φ ∧ O ≺ B → ∀ x ∈ B ∖ if O ≺ B sup B A R B ∀ y ∈ if O ≺ B sup B A R B x R y ↔ ∀ x ∈ B x ≠ sup B A R → x R sup B A R
48 17 47 mpbird ⊢ φ ∧ O ≺ B → ∀ x ∈ B ∖ if O ≺ B sup B A R B ∀ y ∈ if O ≺ B sup B A R B x R y
49 ral0 ⊢ ∀ x ∈ ∅ ∀ y ∈ 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 ⊢ φ ∧ ¬ O ≺ B → if O ≺ B sup B A R B = B
52 51 difeq2d ⊢ φ ∧ ¬ O ≺ B → B ∖ if O ≺ B sup B A R B = B ∖ B
53 difid ⊢ B ∖ B = ∅
54 52 53 eqtrdi ⊢ φ ∧ ¬ O ≺ B → B ∖ if O ≺ B sup B A R B = ∅
55 54 raleqdv ⊢ φ ∧ ¬ O ≺ B → ∀ x ∈ B ∖ if O ≺ B sup B A R B ∀ y ∈ if O ≺ B sup B A R B x R y ↔ ∀ x ∈ ∅ ∀ y ∈ if O ≺ B sup B A R B x R y
56 49 55 mpbiri ⊢ φ ∧ ¬ O ≺ B → ∀ x ∈ B ∖ if O ≺ B sup B A R B ∀ y ∈ if O ≺ B sup B A R B x R y
57 48 56 pm2.61dan ⊢ φ → ∀ x ∈ B ∖ if O ≺ B sup B A R B ∀ y ∈ if O ≺ B sup B A R B x R y