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

Proof

Step	Hyp	Ref	Expression
1		safesnsupfilb.small	$⊢ φ \to (O = \emptyset \lor O = 1_{𝑜})$
2		safesnsupfilb.finite	$⊢ φ \to B \in Fin$
3		safesnsupfilb.subset	$⊢ φ \to B \subseteq A$
4		safesnsupfilb.ordered	$⊢ φ \to R Or A$
5	4	ad2antrr	$⊢ ((φ \land O ≺ B) \land x \in B) \to R Or A$
6	3	ad2antrr	$⊢ ((φ \land O ≺ B) \land x \in B) \to B \subseteq A$
7	2	ad2antrr	$⊢ ((φ \land O ≺ B) \land x \in B) \to B \in Fin$
8		simpr	$⊢ ((φ \land O ≺ B) \land x \in B) \to x \in B$
9		eqidd	$⊢ ((φ \land O ≺ B) \land x \in B) \to sup (B, A, R) = sup (B, A, R)$
10	5 6 7 8 9	supgtoreq	$⊢ ((φ \land O ≺ B) \land x \in B) \to (x R sup (B, A, R) \lor x = sup (B, A, R))$
11		df-or	$⊢ (x = sup (B, A, R) \lor x R sup (B, A, R)) \leftrightarrow (\neg x = sup (B, A, R) \to x R sup (B, A, R))$
12		orcom	$⊢ (x R sup (B, A, R) \lor x = sup (B, A, R)) \leftrightarrow (x = sup (B, A, R) \lor x R sup (B, A, R))$
13		df-ne	$⊢ x \neq sup (B, A, R) \leftrightarrow \neg x = sup (B, A, R)$
14	13	imbi1i	$⊢ (x \neq sup (B, A, R) \to x R sup (B, A, R)) \leftrightarrow (\neg x = sup (B, A, R) \to x R sup (B, A, R))$
15	11 12 14	3bitr4i	$⊢ (x R sup (B, A, R) \lor x = sup (B, A, R)) \leftrightarrow (x \neq sup (B, A, R) \to x R sup (B, A, R))$
16	10 15	sylib	$⊢ ((φ \land O ≺ B) \land x \in B) \to (x \neq sup (B, A, R) \to x R sup (B, A, R))$
17	16	ralrimiva	$⊢ (φ \land O ≺ B) \to \forall x \in B (x \neq sup (B, A, R) \to x R sup (B, A, R))$
18		iftrue	$⊢ O ≺ B \to if (O ≺ B, \{sup (B, A, R)\}, B) = \{sup (B, A, R)\}$
19	18	difeq2d	$⊢ O ≺ B \to B ∖ if (O ≺ B, \{sup (B, A, R)\}, B) = B ∖ \{sup (B, A, R)\}$
20	19	adantl	$⊢ (φ \land O ≺ B) \to B ∖ if (O ≺ B, \{sup (B, A, R)\}, B) = B ∖ \{sup (B, A, R)\}$
21	20	raleqdv	$⊢ (φ \land O ≺ B) \to (\forall x \in (B ∖ if (O ≺ B, \{sup (B, A, R)\}, B)) \forall y \in if (O ≺ B, \{sup (B, A, R)\}, B) x R y \leftrightarrow \forall x \in (B ∖ \{sup (B, A, R)\}) \forall y \in if (O ≺ B, \{sup (B, A, R)\}, B) x R y)$
22		simpr	$⊢ (φ \land O ≺ B) \to O ≺ B$
23	22	iftrued	$⊢ (φ \land O ≺ B) \to if (O ≺ B, \{sup (B, A, R)\}, B) = \{sup (B, A, R)\}$
24	23	raleqdv	$⊢ (φ \land O ≺ B) \to (\forall y \in if (O ≺ B, \{sup (B, A, R)\}, B) x R y \leftrightarrow \forall y \in \{sup (B, A, R)\} x R y)$
25	2	adantr	$⊢ (φ \land O ≺ B) \to B \in Fin$
26	1	adantr	$⊢ (φ \land O ≺ B) \to (O = \emptyset \lor O = 1_{𝑜})$
27		0elon	$⊢ \emptyset \in On$
28		eleq1	$⊢ O = \emptyset \to (O \in On \leftrightarrow \emptyset \in On)$
29	27 28	mpbiri	$⊢ O = \emptyset \to O \in On$
30		1on	$⊢ 1_{𝑜} \in On$
31		eleq1	$⊢ O = 1_{𝑜} \to (O \in On \leftrightarrow 1_{𝑜} \in On)$
32	30 31	mpbiri	$⊢ O = 1_{𝑜} \to O \in On$
33	29 32	jaoi	$⊢ (O = \emptyset \lor O = 1_{𝑜}) \to O \in On$
34	26 33	syl	$⊢ (φ \land O ≺ B) \to O \in On$
35	22 34	sdomne0d	$⊢ (φ \land O ≺ B) \to B \neq \emptyset$
36	3	adantr	$⊢ (φ \land O ≺ B) \to B \subseteq A$
37	25 35 36	3jca	$⊢ (φ \land O ≺ B) \to (B \in Fin \land B \neq \emptyset \land B \subseteq A)$
38		fisupcl	$⊢ (R Or A \land (B \in Fin \land B \neq \emptyset \land B \subseteq A)) \to sup (B, A, R) \in B$
39	4 37 38	syl2an2r	$⊢ (φ \land O ≺ B) \to sup (B, A, R) \in B$
40		breq2	$⊢ y = sup (B, A, R) \to (x R y \leftrightarrow x R sup (B, A, R))$
41	40	ralsng	$⊢ sup (B, A, R) \in B \to (\forall y \in \{sup (B, A, R)\} x R y \leftrightarrow x R sup (B, A, R))$
42	39 41	syl	$⊢ (φ \land O ≺ B) \to (\forall y \in \{sup (B, A, R)\} x R y \leftrightarrow x R sup (B, A, R))$
43	24 42	bitrd	$⊢ (φ \land O ≺ B) \to (\forall y \in if (O ≺ B, \{sup (B, A, R)\}, B) x R y \leftrightarrow x R sup (B, A, R))$
44	43	ralbidv	$⊢ (φ \land O ≺ B) \to (\forall x \in (B ∖ \{sup (B, A, R)\}) \forall y \in if (O ≺ B, \{sup (B, A, R)\}, B) x R y \leftrightarrow \forall x \in (B ∖ \{sup (B, A, R)\}) x R sup (B, A, R))$
45		raldifsnb	$⊢ \forall x \in B (x \neq sup (B, A, R) \to x R sup (B, A, R)) \leftrightarrow \forall x \in (B ∖ \{sup (B, A, R)\}) x R sup (B, A, R)$
46	44 45	bitr4di	$⊢ (φ \land O ≺ B) \to (\forall x \in (B ∖ \{sup (B, A, R)\}) \forall y \in if (O ≺ B, \{sup (B, A, R)\}, B) x R y \leftrightarrow \forall x \in B (x \neq sup (B, A, R) \to x R sup (B, A, R)))$
47	21 46	bitrd	$⊢ (φ \land O ≺ B) \to (\forall x \in (B ∖ if (O ≺ B, \{sup (B, A, R)\}, B)) \forall y \in if (O ≺ B, \{sup (B, A, R)\}, B) x R y \leftrightarrow \forall x \in B (x \neq sup (B, A, R) \to x R sup (B, A, R)))$
48	17 47	mpbird	$⊢ (φ \land O ≺ B) \to \forall x \in (B ∖ if (O ≺ B, \{sup (B, A, R)\}, B)) \forall y \in if (O ≺ B, \{sup (B, A, R)\}, B) x R y$
49		ral0	$⊢ \forall x \in \emptyset \forall y \in if (O ≺ B, \{sup (B, A, R)\}, B) x R y$
50		iffalse	$⊢ \neg O ≺ B \to if (O ≺ B, \{sup (B, A, R)\}, B) = B$
51	50	adantl	$⊢ (φ \land \neg O ≺ B) \to if (O ≺ B, \{sup (B, A, R)\}, B) = B$
52	51	difeq2d	$⊢ (φ \land \neg O ≺ B) \to B ∖ if (O ≺ B, \{sup (B, A, R)\}, B) = B ∖ B$
53		difid	$⊢ B ∖ B = \emptyset$
54	52 53	eqtrdi	$⊢ (φ \land \neg O ≺ B) \to B ∖ if (O ≺ B, \{sup (B, A, R)\}, B) = \emptyset$
55	54	raleqdv	$⊢ (φ \land \neg O ≺ B) \to (\forall x \in (B ∖ if (O ≺ B, \{sup (B, A, R)\}, B)) \forall y \in if (O ≺ B, \{sup (B, A, R)\}, B) x R y \leftrightarrow \forall x \in \emptyset \forall y \in if (O ≺ B, \{sup (B, A, R)\}, B) x R y)$
56	49 55	mpbiri	$⊢ (φ \land \neg O ≺ B) \to \forall x \in (B ∖ if (O ≺ B, \{sup (B, A, R)\}, B)) \forall y \in if (O ≺ B, \{sup (B, A, R)\}, B) x R y$
57	48 56	pm2.61dan	$⊢ φ \to \forall x \in (B ∖ if (O ≺ B, \{sup (B, A, R)\}, B)) \forall y \in if (O ≺ B, \{sup (B, A, R)\}, B) x R y$

Metamath Proof Explorer

Theorem safesnsupfilb

Proof