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

Proof

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