Metamath Proof Explorer

Theorem safesnsupfiss

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

Proof

Step Hyp Ref Expression
1 safesnsupfiss.small ⊢ φ → O = ∅ ∨ O = 1 𝑜
2 safesnsupfiss.finite ⊢ φ → B ∈ Fin
3 safesnsupfiss.subset ⊢ φ → B ⊆ A
4 safesnsupfiss.ordered ⊢ φ → R Or A
5 elif ⊢ x ∈ if O ≺ B sup B A R B ↔ O ≺ B ∧ x ∈ sup B A R ∨ ¬ O ≺ B ∧ x ∈ B
6 elsni ⊢ x ∈ sup B A R → x = sup B A R
7 simpr ⊢ φ ∧ O ≺ B ∧ x = sup B A R → x = sup B A R
8 4 adantr ⊢ φ ∧ O ≺ B → R Or A
9 2 adantr ⊢ φ ∧ O ≺ B → B ∈ Fin
10 simpr ⊢ φ ∧ O ≺ B → O ≺ B
11 0elon ⊢ ∅ ∈ On
12 eleq1 ⊢ O = ∅ → O ∈ On ↔ ∅ ∈ On
13 11 12 mpbiri ⊢ O = ∅ → O ∈ On
14 1on ⊢ 1 𝑜 ∈ On
15 eleq1 ⊢ O = 1 𝑜 → O ∈ On ↔ 1 𝑜 ∈ On
16 14 15 mpbiri ⊢ O = 1 𝑜 → O ∈ On
17 13 16 jaoi ⊢ O = ∅ ∨ O = 1 𝑜 → O ∈ On
18 1 17 syl ⊢ φ → O ∈ On
19 18 adantr ⊢ φ ∧ O ≺ B → O ∈ On
20 10 19 sdomne0d ⊢ φ ∧ O ≺ B → B ≠ ∅
21 3 adantr ⊢ φ ∧ O ≺ B → B ⊆ A
22 fisupcl ⊢ R Or A ∧ B ∈ Fin ∧ B ≠ ∅ ∧ B ⊆ A → sup B A R ∈ B
23 8 9 20 21 22 syl13anc ⊢ φ ∧ O ≺ B → sup B A R ∈ B
24 23 adantr ⊢ φ ∧ O ≺ B ∧ x = sup B A R → sup B A R ∈ B
25 7 24 eqeltrd ⊢ φ ∧ O ≺ B ∧ x = sup B A R → x ∈ B
26 25 ex ⊢ φ ∧ O ≺ B → x = sup B A R → x ∈ B
27 6 26 syl5 ⊢ φ ∧ O ≺ B → x ∈ sup B A R → x ∈ B
28 27 expimpd ⊢ φ → O ≺ B ∧ x ∈ sup B A R → x ∈ B
29 simpr ⊢ ¬ O ≺ B ∧ x ∈ B → x ∈ B
30 29 a1i ⊢ φ → ¬ O ≺ B ∧ x ∈ B → x ∈ B
31 28 30 jaod ⊢ φ → O ≺ B ∧ x ∈ sup B A R ∨ ¬ O ≺ B ∧ x ∈ B → x ∈ B
32 5 31 biimtrid ⊢ φ → x ∈ if O ≺ B sup B A R B → x ∈ B
33 32 ssrdv ⊢ φ → if O ≺ B sup B A R B ⊆ B