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	$⊢ φ \to (O = \emptyset \lor O = 1_{𝑜})$
	safesnsupfiss.finite	$⊢ φ \to B \in Fin$
	safesnsupfiss.subset	$⊢ φ \to B \subseteq A$
	safesnsupfiss.ordered	$⊢ φ \to R Or A$
Assertion	safesnsupfiss	$⊢ φ \to if (O ≺ B, \{sup (B, A, R)\}, B) \subseteq B$

Proof

Step	Hyp	Ref	Expression
1		safesnsupfiss.small	$⊢ φ \to (O = \emptyset \lor O = 1_{𝑜})$
2		safesnsupfiss.finite	$⊢ φ \to B \in Fin$
3		safesnsupfiss.subset	$⊢ φ \to B \subseteq A$
4		safesnsupfiss.ordered	$⊢ φ \to R Or A$
5		elif	$⊢ x \in if (O ≺ B, \{sup (B, A, R)\}, B) \leftrightarrow ((O ≺ B \land x \in \{sup (B, A, R)\}) \lor (\neg O ≺ B \land x \in B))$
6		elsni	$⊢ x \in \{sup (B, A, R)\} \to x = sup (B, A, R)$
7		simpr	$⊢ ((φ \land O ≺ B) \land x = sup (B, A, R)) \to x = sup (B, A, R)$
8	4	adantr	$⊢ (φ \land O ≺ B) \to R Or A$
9	2	adantr	$⊢ (φ \land O ≺ B) \to B \in Fin$
10		simpr	$⊢ (φ \land O ≺ B) \to O ≺ B$
11		0elon	$⊢ \emptyset \in On$
12		eleq1	$⊢ O = \emptyset \to (O \in On \leftrightarrow \emptyset \in On)$
13	11 12	mpbiri	$⊢ O = \emptyset \to O \in On$
14		1on	$⊢ 1_{𝑜} \in On$
15		eleq1	$⊢ O = 1_{𝑜} \to (O \in On \leftrightarrow 1_{𝑜} \in On)$
16	14 15	mpbiri	$⊢ O = 1_{𝑜} \to O \in On$
17	13 16	jaoi	$⊢ (O = \emptyset \lor O = 1_{𝑜}) \to O \in On$
18	1 17	syl	$⊢ φ \to O \in On$
19	18	adantr	$⊢ (φ \land O ≺ B) \to O \in On$
20	10 19	sdomne0d	$⊢ (φ \land O ≺ B) \to B \neq \emptyset$
21	3	adantr	$⊢ (φ \land O ≺ B) \to B \subseteq A$
22		fisupcl	$⊢ (R Or A \land (B \in Fin \land B \neq \emptyset \land B \subseteq A)) \to sup (B, A, R) \in B$
23	8 9 20 21 22	syl13anc	$⊢ (φ \land O ≺ B) \to sup (B, A, R) \in B$
24	23	adantr	$⊢ ((φ \land O ≺ B) \land x = sup (B, A, R)) \to sup (B, A, R) \in B$
25	7 24	eqeltrd	$⊢ ((φ \land O ≺ B) \land x = sup (B, A, R)) \to x \in B$
26	25	ex	$⊢ (φ \land O ≺ B) \to (x = sup (B, A, R) \to x \in B)$
27	6 26	syl5	$⊢ (φ \land O ≺ B) \to (x \in \{sup (B, A, R)\} \to x \in B)$
28	27	expimpd	$⊢ φ \to ((O ≺ B \land x \in \{sup (B, A, R)\}) \to x \in B)$
29		simpr	$⊢ (\neg O ≺ B \land x \in B) \to x \in B$
30	29	a1i	$⊢ φ \to ((\neg O ≺ B \land x \in B) \to x \in B)$
31	28 30	jaod	$⊢ φ \to (((O ≺ B \land x \in \{sup (B, A, R)\}) \lor (\neg O ≺ B \land x \in B)) \to x \in B)$
32	5 31	biimtrid	$⊢ φ \to (x \in if (O ≺ B, \{sup (B, A, R)\}, B) \to x \in B)$
33	32	ssrdv	$⊢ φ \to if (O ≺ B, \{sup (B, A, R)\}, B) \subseteq B$

Metamath Proof Explorer

Theorem safesnsupfiss

Proof