safesnsupfidom1o

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

Proof

Step	Hyp	Ref	Expression
1		safesnsupfidom1o.small	$⊢ φ \to (O = \emptyset \lor O = 1_{𝑜})$
2		safesnsupfidom1o.finite	$⊢ φ \to B \in Fin$
3		iftrue	$⊢ O ≺ B \to if (O ≺ B, \{sup (B, A, R)\}, B) = \{sup (B, A, R)\}$
4	3	adantl	$⊢ (φ \land O ≺ B) \to if (O ≺ B, \{sup (B, A, R)\}, B) = \{sup (B, A, R)\}$
5		ensn1g	$⊢ sup (B, A, R) \in V \to \{sup (B, A, R)\} \approx 1_{𝑜}$
6		1on	$⊢ 1_{𝑜} \in On$
7		domrefg	$⊢ 1_{𝑜} \in On \to 1_{𝑜} ≼ 1_{𝑜}$
8	6 7	ax-mp	$⊢ 1_{𝑜} ≼ 1_{𝑜}$
9		endomtr	$⊢ (\{sup (B, A, R)\} \approx 1_{𝑜} \land 1_{𝑜} ≼ 1_{𝑜}) \to \{sup (B, A, R)\} ≼ 1_{𝑜}$
10	5 8 9	sylancl	$⊢ sup (B, A, R) \in V \to \{sup (B, A, R)\} ≼ 1_{𝑜}$
11		snprc	$⊢ \neg sup (B, A, R) \in V \leftrightarrow \{sup (B, A, R)\} = \emptyset$
12		snex	$⊢ \{sup (B, A, R)\} \in V$
13		eqeng	$⊢ \{sup (B, A, R)\} \in V \to (\{sup (B, A, R)\} = \emptyset \to \{sup (B, A, R)\} \approx \emptyset)$
14	12 13	ax-mp	$⊢ \{sup (B, A, R)\} = \emptyset \to \{sup (B, A, R)\} \approx \emptyset$
15	11 14	sylbi	$⊢ \neg sup (B, A, R) \in V \to \{sup (B, A, R)\} \approx \emptyset$
16		0domg	$⊢ 1_{𝑜} \in On \to \emptyset ≼ 1_{𝑜}$
17	6 16	ax-mp	$⊢ \emptyset ≼ 1_{𝑜}$
18		endomtr	$⊢ (\{sup (B, A, R)\} \approx \emptyset \land \emptyset ≼ 1_{𝑜}) \to \{sup (B, A, R)\} ≼ 1_{𝑜}$
19	15 17 18	sylancl	$⊢ \neg sup (B, A, R) \in V \to \{sup (B, A, R)\} ≼ 1_{𝑜}$
20	10 19	pm2.61i	$⊢ \{sup (B, A, R)\} ≼ 1_{𝑜}$
21	4 20	eqbrtrdi	$⊢ (φ \land O ≺ B) \to if (O ≺ B, \{sup (B, A, R)\}, B) ≼ 1_{𝑜}$
22		iffalse	$⊢ \neg O ≺ B \to if (O ≺ B, \{sup (B, A, R)\}, B) = B$
23	22	adantl	$⊢ (φ \land \neg O ≺ B) \to if (O ≺ B, \{sup (B, A, R)\}, B) = B$
24		0elon	$⊢ \emptyset \in On$
25		eleq1	$⊢ O = \emptyset \to (O \in On \leftrightarrow \emptyset \in On)$
26	24 25	mpbiri	$⊢ O = \emptyset \to O \in On$
27		eleq1	$⊢ O = 1_{𝑜} \to (O \in On \leftrightarrow 1_{𝑜} \in On)$
28	6 27	mpbiri	$⊢ O = 1_{𝑜} \to O \in On$
29	26 28	jaoi	$⊢ (O = \emptyset \lor O = 1_{𝑜}) \to O \in On$
30		fidomtri	$⊢ (B \in Fin \land O \in On) \to (B ≼ O \leftrightarrow \neg O ≺ B)$
31	29 30	sylan2	$⊢ (B \in Fin \land (O = \emptyset \lor O = 1_{𝑜})) \to (B ≼ O \leftrightarrow \neg O ≺ B)$
32		breq2	$⊢ O = \emptyset \to (B ≼ O \leftrightarrow B ≼ \emptyset)$
33		domtr	$⊢ (B ≼ \emptyset \land \emptyset ≼ 1_{𝑜}) \to B ≼ 1_{𝑜}$
34	17 33	mpan2	$⊢ B ≼ \emptyset \to B ≼ 1_{𝑜}$
35	32 34	syl6bi	$⊢ O = \emptyset \to (B ≼ O \to B ≼ 1_{𝑜})$
36		breq2	$⊢ O = 1_{𝑜} \to (B ≼ O \leftrightarrow B ≼ 1_{𝑜})$
37	36	biimpd	$⊢ O = 1_{𝑜} \to (B ≼ O \to B ≼ 1_{𝑜})$
38	35 37	jaoi	$⊢ (O = \emptyset \lor O = 1_{𝑜}) \to (B ≼ O \to B ≼ 1_{𝑜})$
39	38	adantl	$⊢ (B \in Fin \land (O = \emptyset \lor O = 1_{𝑜})) \to (B ≼ O \to B ≼ 1_{𝑜})$
40	31 39	sylbird	$⊢ (B \in Fin \land (O = \emptyset \lor O = 1_{𝑜})) \to (\neg O ≺ B \to B ≼ 1_{𝑜})$
41	2 1 40	syl2anc	$⊢ φ \to (\neg O ≺ B \to B ≼ 1_{𝑜})$
42	41	imp	$⊢ (φ \land \neg O ≺ B) \to B ≼ 1_{𝑜}$
43	23 42	eqbrtrd	$⊢ (φ \land \neg O ≺ B) \to if (O ≺ B, \{sup (B, A, R)\}, B) ≼ 1_{𝑜}$
44	21 43	pm2.61dan	$⊢ φ \to if (O ≺ B, \{sup (B, A, R)\}, B) ≼ 1_{𝑜}$

Metamath Proof Explorer

Theorem safesnsupfidom1o

Proof