infleinf

Description: If any element of B can be approximated from above by members of A , then the infimum of A is less than or equal to the infimum of B . (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	infleinf.a	$⊢ φ \to A \subseteq ℝ^{*}$
	infleinf.b	$⊢ φ \to B \subseteq ℝ^{*}$
	infleinf.c	$⊢ (φ \land x \in B \land y \in ℝ^{+}) \to \exists z \in A z \leq x +_{𝑒} y$
Assertion	infleinf	$⊢ φ \to sup (A ℝ^{} <) \leq sup (B ℝ^{} <)$

Proof

Step	Hyp	Ref	Expression
1		infleinf.a	$⊢ φ \to A \subseteq ℝ^{*}$
2		infleinf.b	$⊢ φ \to B \subseteq ℝ^{*}$
3		infleinf.c	$⊢ (φ \land x \in B \land y \in ℝ^{+}) \to \exists z \in A z \leq x +_{𝑒} y$
4		infxrcl	$⊢ A \subseteq ℝ^{} \to sup (A ℝ^{} <) \in ℝ^{*}$
5	1 4	syl	$⊢ φ \to sup (A ℝ^{} <) \in ℝ^{}$
6		pnfge	$⊢ sup (A ℝ^{} <) \in ℝ^{} \to sup (A ℝ^{*} <) \leq +∞$
7	5 6	syl	$⊢ φ \to sup (A ℝ^{*} <) \leq +∞$
8	7	adantr	$⊢ (φ \land B = \emptyset) \to sup (A ℝ^{*} <) \leq +∞$
9		infeq1	$⊢ B = \emptyset \to sup (B ℝ^{} <) = sup (\emptyset ℝ^{} <)$
10		xrinf0	$⊢ sup (\emptyset ℝ^{*} <) = +∞$
11	10	a1i	$⊢ B = \emptyset \to sup (\emptyset ℝ^{*} <) = +∞$
12	9 11	eqtrd	$⊢ B = \emptyset \to sup (B ℝ^{*} <) = +∞$
13	12	eqcomd	$⊢ B = \emptyset \to +∞ = sup (B ℝ^{*} <)$
14	13	adantl	$⊢ (φ \land B = \emptyset) \to +∞ = sup (B ℝ^{*} <)$
15	8 14	breqtrd	$⊢ (φ \land B = \emptyset) \to sup (A ℝ^{} <) \leq sup (B ℝ^{} <)$
16		neqne	$⊢ \neg B = \emptyset \to B \neq \emptyset$
17	16	adantl	$⊢ (φ \land \neg B = \emptyset) \to B \neq \emptyset$
18	5	adantr	$⊢ (φ \land sup (B ℝ^{} <) = −∞) \to sup (A ℝ^{} <) \in ℝ^{*}$
19		id	$⊢ r \in ℝ \to r \in ℝ$
20		2re	$⊢ 2 \in ℝ$
21	20	a1i	$⊢ r \in ℝ \to 2 \in ℝ$
22	19 21	resubcld	$⊢ r \in ℝ \to r - 2 \in ℝ$
23	22	adantl	$⊢ ((φ \land sup (B ℝ^{*} <) = −∞) \land r \in ℝ) \to r - 2 \in ℝ$
24		simpr	$⊢ (φ \land sup (B ℝ^{} <) = −∞) \to sup (B ℝ^{} <) = −∞$
25		infxrunb2	$⊢ B \subseteq ℝ^{} \to (\forall y \in ℝ \exists x \in B x < y \leftrightarrow sup (B ℝ^{} <) = −∞)$
26	2 25	syl	$⊢ φ \to (\forall y \in ℝ \exists x \in B x < y \leftrightarrow sup (B ℝ^{*} <) = −∞)$
27	26	adantr	$⊢ (φ \land sup (B ℝ^{} <) = −∞) \to (\forall y \in ℝ \exists x \in B x < y \leftrightarrow sup (B ℝ^{} <) = −∞)$
28	24 27	mpbird	$⊢ (φ \land sup (B ℝ^{*} <) = −∞) \to \forall y \in ℝ \exists x \in B x < y$
29	28	adantr	$⊢ ((φ \land sup (B ℝ^{*} <) = −∞) \land r \in ℝ) \to \forall y \in ℝ \exists x \in B x < y$
30		breq2	$⊢ y = r - 2 \to (x < y \leftrightarrow x < r - 2)$
31	30	rexbidv	$⊢ y = r - 2 \to (\exists x \in B x < y \leftrightarrow \exists x \in B x < r - 2)$
32	31	rspcva	$⊢ (r - 2 \in ℝ \land \forall y \in ℝ \exists x \in B x < y) \to \exists x \in B x < r - 2$
33	23 29 32	syl2anc	$⊢ ((φ \land sup (B ℝ^{*} <) = −∞) \land r \in ℝ) \to \exists x \in B x < r - 2$
34		simpl	$⊢ (φ \land x \in B) \to φ$
35		simpr	$⊢ (φ \land x \in B) \to x \in B$
36		1rp	$⊢ 1 \in ℝ^{+}$
37	36	a1i	$⊢ (φ \land x \in B) \to 1 \in ℝ^{+}$
38		1ex	$⊢ 1 \in V$
39		eleq1	$⊢ y = 1 \to (y \in ℝ^{+} \leftrightarrow 1 \in ℝ^{+})$
40	39	3anbi3d	$⊢ y = 1 \to ((φ \land x \in B \land y \in ℝ^{+}) \leftrightarrow (φ \land x \in B \land 1 \in ℝ^{+}))$
41		oveq2	$⊢ y = 1 \to x +_{𝑒} y = x +_{𝑒} 1$
42	41	breq2d	$⊢ y = 1 \to (z \leq x +_{𝑒} y \leftrightarrow z \leq x +_{𝑒} 1)$
43	42	rexbidv	$⊢ y = 1 \to (\exists z \in A z \leq x +_{𝑒} y \leftrightarrow \exists z \in A z \leq x +_{𝑒} 1)$
44	40 43	imbi12d	$⊢ y = 1 \to (((φ \land x \in B \land y \in ℝ^{+}) \to \exists z \in A z \leq x +_{𝑒} y) \leftrightarrow ((φ \land x \in B \land 1 \in ℝ^{+}) \to \exists z \in A z \leq x +_{𝑒} 1))$
45	38 44 3	vtocl	$⊢ (φ \land x \in B \land 1 \in ℝ^{+}) \to \exists z \in A z \leq x +_{𝑒} 1$
46	34 35 37 45	syl3anc	$⊢ (φ \land x \in B) \to \exists z \in A z \leq x +_{𝑒} 1$
47	46	adantlr	$⊢ ((φ \land r \in ℝ) \land x \in B) \to \exists z \in A z \leq x +_{𝑒} 1$
48	47	3adant3	$⊢ ((φ \land r \in ℝ) \land x \in B \land x < r - 2) \to \exists z \in A z \leq x +_{𝑒} 1$
49		simp1l	$⊢ ((φ \land r \in ℝ) \land x \in B \land x < r - 2) \to φ$
50	49	ad2antrr	$⊢ ((((φ \land r \in ℝ) \land x \in B \land x < r - 2) \land z \in A) \land z \leq x +_{𝑒} 1) \to φ$
51	50 1	syl	$⊢ ((((φ \land r \in ℝ) \land x \in B \land x < r - 2) \land z \in A) \land z \leq x +_{𝑒} 1) \to A \subseteq ℝ^{*}$
52	50 2	syl	$⊢ ((((φ \land r \in ℝ) \land x \in B \land x < r - 2) \land z \in A) \land z \leq x +_{𝑒} 1) \to B \subseteq ℝ^{*}$
53		simp1r	$⊢ ((φ \land r \in ℝ) \land x \in B \land x < r - 2) \to r \in ℝ$
54	53	ad2antrr	$⊢ ((((φ \land r \in ℝ) \land x \in B \land x < r - 2) \land z \in A) \land z \leq x +_{𝑒} 1) \to r \in ℝ$
55		simp2	$⊢ ((φ \land r \in ℝ) \land x \in B \land x < r - 2) \to x \in B$
56	55	ad2antrr	$⊢ ((((φ \land r \in ℝ) \land x \in B \land x < r - 2) \land z \in A) \land z \leq x +_{𝑒} 1) \to x \in B$
57		simpll3	$⊢ ((((φ \land r \in ℝ) \land x \in B \land x < r - 2) \land z \in A) \land z \leq x +_{𝑒} 1) \to x < r - 2$
58		simplr	$⊢ ((((φ \land r \in ℝ) \land x \in B \land x < r - 2) \land z \in A) \land z \leq x +_{𝑒} 1) \to z \in A$
59		simpr	$⊢ ((((φ \land r \in ℝ) \land x \in B \land x < r - 2) \land z \in A) \land z \leq x +_{𝑒} 1) \to z \leq x +_{𝑒} 1$
60	51 52 54 56 57 58 59	infleinflem2	$⊢ ((((φ \land r \in ℝ) \land x \in B \land x < r - 2) \land z \in A) \land z \leq x +_{𝑒} 1) \to z < r$
61	60	ex	$⊢ (((φ \land r \in ℝ) \land x \in B \land x < r - 2) \land z \in A) \to (z \leq x +_{𝑒} 1 \to z < r)$
62	61	reximdva	$⊢ ((φ \land r \in ℝ) \land x \in B \land x < r - 2) \to (\exists z \in A z \leq x +_{𝑒} 1 \to \exists z \in A z < r)$
63	48 62	mpd	$⊢ ((φ \land r \in ℝ) \land x \in B \land x < r - 2) \to \exists z \in A z < r$
64	63	3exp	$⊢ (φ \land r \in ℝ) \to (x \in B \to (x < r - 2 \to \exists z \in A z < r))$
65	64	adantlr	$⊢ ((φ \land sup (B ℝ^{*} <) = −∞) \land r \in ℝ) \to (x \in B \to (x < r - 2 \to \exists z \in A z < r))$
66	65	rexlimdv	$⊢ ((φ \land sup (B ℝ^{*} <) = −∞) \land r \in ℝ) \to (\exists x \in B x < r - 2 \to \exists z \in A z < r)$
67	33 66	mpd	$⊢ ((φ \land sup (B ℝ^{*} <) = −∞) \land r \in ℝ) \to \exists z \in A z < r$
68	67	ralrimiva	$⊢ (φ \land sup (B ℝ^{*} <) = −∞) \to \forall r \in ℝ \exists z \in A z < r$
69		infxrunb2	$⊢ A \subseteq ℝ^{} \to (\forall r \in ℝ \exists z \in A z < r \leftrightarrow sup (A ℝ^{} <) = −∞)$
70	1 69	syl	$⊢ φ \to (\forall r \in ℝ \exists z \in A z < r \leftrightarrow sup (A ℝ^{*} <) = −∞)$
71	70	adantr	$⊢ (φ \land sup (B ℝ^{} <) = −∞) \to (\forall r \in ℝ \exists z \in A z < r \leftrightarrow sup (A ℝ^{} <) = −∞)$
72	68 71	mpbid	$⊢ (φ \land sup (B ℝ^{} <) = −∞) \to sup (A ℝ^{} <) = −∞$
73	72 24	eqtr4d	$⊢ (φ \land sup (B ℝ^{} <) = −∞) \to sup (A ℝ^{} <) = sup (B ℝ^{*} <)$
74	18 73	xreqled	$⊢ (φ \land sup (B ℝ^{} <) = −∞) \to sup (A ℝ^{} <) \leq sup (B ℝ^{*} <)$
75	74	adantlr	$⊢ ((φ \land B \neq \emptyset) \land sup (B ℝ^{} <) = −∞) \to sup (A ℝ^{} <) \leq sup (B ℝ^{*} <)$
76		mnfxr	$⊢ −∞ \in ℝ^{*}$
77	76	a1i	$⊢ φ \to −∞ \in ℝ^{*}$
78	77	ad2antrr	$⊢ ((φ \land B \neq \emptyset) \land \neg sup (B ℝ^{} <) = −∞) \to −∞ \in ℝ^{}$
79		infxrcl	$⊢ B \subseteq ℝ^{} \to sup (B ℝ^{} <) \in ℝ^{*}$
80	2 79	syl	$⊢ φ \to sup (B ℝ^{} <) \in ℝ^{}$
81	80	ad2antrr	$⊢ ((φ \land B \neq \emptyset) \land \neg sup (B ℝ^{} <) = −∞) \to sup (B ℝ^{} <) \in ℝ^{*}$
82		mnfle	$⊢ sup (B ℝ^{} <) \in ℝ^{} \to −∞ \leq sup (B ℝ^{*} <)$
83	81 82	syl	$⊢ ((φ \land B \neq \emptyset) \land \neg sup (B ℝ^{} <) = −∞) \to −∞ \leq sup (B ℝ^{} <)$
84		neqne	$⊢ \neg sup (B ℝ^{} <) = −∞ \to sup (B ℝ^{} <) \neq −∞$
85	84	necomd	$⊢ \neg sup (B ℝ^{} <) = −∞ \to −∞ \neq sup (B ℝ^{} <)$
86	85	adantl	$⊢ ((φ \land B \neq \emptyset) \land \neg sup (B ℝ^{} <) = −∞) \to −∞ \neq sup (B ℝ^{} <)$
87	78 81 83 86	xrleneltd	$⊢ ((φ \land B \neq \emptyset) \land \neg sup (B ℝ^{} <) = −∞) \to −∞ < sup (B ℝ^{} <)$
88	5	ad2antrr	$⊢ ((φ \land B \neq \emptyset) \land −∞ < sup (B ℝ^{} <)) \to sup (A ℝ^{} <) \in ℝ^{*}$
89	80	ad2antrr	$⊢ ((φ \land B \neq \emptyset) \land −∞ < sup (B ℝ^{} <)) \to sup (B ℝ^{} <) \in ℝ^{*}$
90		nfv	$⊢ Ⅎ b (((φ \land B \neq \emptyset) \land −∞ < sup (B ℝ^{*} <)) \land w \in ℝ^{+})$
91	2	ad3antrrr	$⊢ (((φ \land B \neq \emptyset) \land −∞ < sup (B ℝ^{} <)) \land w \in ℝ^{+}) \to B \subseteq ℝ^{}$
92		simpllr	$⊢ (((φ \land B \neq \emptyset) \land −∞ < sup (B ℝ^{*} <)) \land w \in ℝ^{+}) \to B \neq \emptyset$
93		simpr	$⊢ (φ \land −∞ < sup (B ℝ^{} <)) \to −∞ < sup (B ℝ^{} <)$
94		infxrbnd2	$⊢ B \subseteq ℝ^{} \to (\exists b \in ℝ \forall x \in B b \leq x \leftrightarrow −∞ < sup (B ℝ^{} <))$
95	2 94	syl	$⊢ φ \to (\exists b \in ℝ \forall x \in B b \leq x \leftrightarrow −∞ < sup (B ℝ^{*} <))$
96	95	adantr	$⊢ (φ \land −∞ < sup (B ℝ^{} <)) \to (\exists b \in ℝ \forall x \in B b \leq x \leftrightarrow −∞ < sup (B ℝ^{} <))$
97	93 96	mpbird	$⊢ (φ \land −∞ < sup (B ℝ^{*} <)) \to \exists b \in ℝ \forall x \in B b \leq x$
98	97	ad4ant13	$⊢ (((φ \land B \neq \emptyset) \land −∞ < sup (B ℝ^{*} <)) \land w \in ℝ^{+}) \to \exists b \in ℝ \forall x \in B b \leq x$
99		simpr	$⊢ (((φ \land B \neq \emptyset) \land −∞ < sup (B ℝ^{*} <)) \land w \in ℝ^{+}) \to w \in ℝ^{+}$
100	99	rphalfcld	$⊢ (((φ \land B \neq \emptyset) \land −∞ < sup (B ℝ^{*} <)) \land w \in ℝ^{+}) \to \frac{w}{2} \in ℝ^{+}$
101	90 91 92 98 100	infrpge	$⊢ (((φ \land B \neq \emptyset) \land −∞ < sup (B ℝ^{} <)) \land w \in ℝ^{+}) \to \exists x \in B x \leq sup (B ℝ^{} <) +_{𝑒} (\frac{w}{2})$
102		simpll	$⊢ ((φ \land w \in ℝ^{+}) \land x \in B) \to φ$
103		simpr	$⊢ ((φ \land w \in ℝ^{+}) \land x \in B) \to x \in B$
104		rphalfcl	$⊢ w \in ℝ^{+} \to \frac{w}{2} \in ℝ^{+}$
105	104	ad2antlr	$⊢ ((φ \land w \in ℝ^{+}) \land x \in B) \to \frac{w}{2} \in ℝ^{+}$
106		ovex	$⊢ \frac{w}{2} \in V$
107		eleq1	$⊢ y = \frac{w}{2} \to (y \in ℝ^{+} \leftrightarrow \frac{w}{2} \in ℝ^{+})$
108	107	3anbi3d	$⊢ y = \frac{w}{2} \to ((φ \land x \in B \land y \in ℝ^{+}) \leftrightarrow (φ \land x \in B \land \frac{w}{2} \in ℝ^{+}))$
109		oveq2	$⊢ y = \frac{w}{2} \to x +_{𝑒} y = x +_{𝑒} (\frac{w}{2})$
110	109	breq2d	$⊢ y = \frac{w}{2} \to (z \leq x +_{𝑒} y \leftrightarrow z \leq x +_{𝑒} (\frac{w}{2}))$
111	110	rexbidv	$⊢ y = \frac{w}{2} \to (\exists z \in A z \leq x +_{𝑒} y \leftrightarrow \exists z \in A z \leq x +_{𝑒} (\frac{w}{2}))$
112	108 111	imbi12d	$⊢ y = \frac{w}{2} \to (((φ \land x \in B \land y \in ℝ^{+}) \to \exists z \in A z \leq x +_{𝑒} y) \leftrightarrow ((φ \land x \in B \land \frac{w}{2} \in ℝ^{+}) \to \exists z \in A z \leq x +_{𝑒} (\frac{w}{2})))$
113	106 112 3	vtocl	$⊢ (φ \land x \in B \land \frac{w}{2} \in ℝ^{+}) \to \exists z \in A z \leq x +_{𝑒} (\frac{w}{2})$
114	102 103 105 113	syl3anc	$⊢ ((φ \land w \in ℝ^{+}) \land x \in B) \to \exists z \in A z \leq x +_{𝑒} (\frac{w}{2})$
115	114	3adant3	$⊢ ((φ \land w \in ℝ^{+}) \land x \in B \land x \leq sup (B ℝ^{*} <) +_{𝑒} (\frac{w}{2})) \to \exists z \in A z \leq x +_{𝑒} (\frac{w}{2})$
116		simp11l	$⊢ (((φ \land w \in ℝ^{+}) \land x \in B \land x \leq sup (B ℝ^{*} <) +_{𝑒} (\frac{w}{2})) \land z \in A \land z \leq x +_{𝑒} (\frac{w}{2})) \to φ$
117	116 1	syl	$⊢ (((φ \land w \in ℝ^{+}) \land x \in B \land x \leq sup (B ℝ^{} <) +_{𝑒} (\frac{w}{2})) \land z \in A \land z \leq x +_{𝑒} (\frac{w}{2})) \to A \subseteq ℝ^{}$
118	116 2	syl	$⊢ (((φ \land w \in ℝ^{+}) \land x \in B \land x \leq sup (B ℝ^{} <) +_{𝑒} (\frac{w}{2})) \land z \in A \land z \leq x +_{𝑒} (\frac{w}{2})) \to B \subseteq ℝ^{}$
119		simp11	$⊢ (((φ \land w \in ℝ^{+}) \land x \in B \land x \leq sup (B ℝ^{*} <) +_{𝑒} (\frac{w}{2})) \land z \in A \land z \leq x +_{𝑒} (\frac{w}{2})) \to (φ \land w \in ℝ^{+})$
120	119	simprd	$⊢ (((φ \land w \in ℝ^{+}) \land x \in B \land x \leq sup (B ℝ^{*} <) +_{𝑒} (\frac{w}{2})) \land z \in A \land z \leq x +_{𝑒} (\frac{w}{2})) \to w \in ℝ^{+}$
121		simp12	$⊢ (((φ \land w \in ℝ^{+}) \land x \in B \land x \leq sup (B ℝ^{*} <) +_{𝑒} (\frac{w}{2})) \land z \in A \land z \leq x +_{𝑒} (\frac{w}{2})) \to x \in B$
122		simp3	$⊢ ((φ \land w \in ℝ^{+}) \land x \in B \land x \leq sup (B ℝ^{} <) +_{𝑒} (\frac{w}{2})) \to x \leq sup (B ℝ^{} <) +_{𝑒} (\frac{w}{2})$
123	122	3ad2ant1	$⊢ (((φ \land w \in ℝ^{+}) \land x \in B \land x \leq sup (B ℝ^{} <) +_{𝑒} (\frac{w}{2})) \land z \in A \land z \leq x +_{𝑒} (\frac{w}{2})) \to x \leq sup (B ℝ^{} <) +_{𝑒} (\frac{w}{2})$
124		simp2	$⊢ (((φ \land w \in ℝ^{+}) \land x \in B \land x \leq sup (B ℝ^{*} <) +_{𝑒} (\frac{w}{2})) \land z \in A \land z \leq x +_{𝑒} (\frac{w}{2})) \to z \in A$
125		simp3	$⊢ (((φ \land w \in ℝ^{+}) \land x \in B \land x \leq sup (B ℝ^{*} <) +_{𝑒} (\frac{w}{2})) \land z \in A \land z \leq x +_{𝑒} (\frac{w}{2})) \to z \leq x +_{𝑒} (\frac{w}{2})$
126	117 118 120 121 123 124 125	infleinflem1	$⊢ (((φ \land w \in ℝ^{+}) \land x \in B \land x \leq sup (B ℝ^{} <) +_{𝑒} (\frac{w}{2})) \land z \in A \land z \leq x +_{𝑒} (\frac{w}{2})) \to sup (A ℝ^{} <) \leq sup (B ℝ^{*} <) +_{𝑒} w$
127	126	3exp	$⊢ ((φ \land w \in ℝ^{+}) \land x \in B \land x \leq sup (B ℝ^{} <) +_{𝑒} (\frac{w}{2})) \to (z \in A \to (z \leq x +_{𝑒} (\frac{w}{2}) \to sup (A ℝ^{} <) \leq sup (B ℝ^{*} <) +_{𝑒} w))$
128	127	rexlimdv	$⊢ ((φ \land w \in ℝ^{+}) \land x \in B \land x \leq sup (B ℝ^{} <) +_{𝑒} (\frac{w}{2})) \to (\exists z \in A z \leq x +_{𝑒} (\frac{w}{2}) \to sup (A ℝ^{} <) \leq sup (B ℝ^{*} <) +_{𝑒} w)$
129	115 128	mpd	$⊢ ((φ \land w \in ℝ^{+}) \land x \in B \land x \leq sup (B ℝ^{} <) +_{𝑒} (\frac{w}{2})) \to sup (A ℝ^{} <) \leq sup (B ℝ^{*} <) +_{𝑒} w$
130	129	3exp	$⊢ (φ \land w \in ℝ^{+}) \to (x \in B \to (x \leq sup (B ℝ^{} <) +_{𝑒} (\frac{w}{2}) \to sup (A ℝ^{} <) \leq sup (B ℝ^{*} <) +_{𝑒} w))$
131	130	rexlimdv	$⊢ (φ \land w \in ℝ^{+}) \to (\exists x \in B x \leq sup (B ℝ^{} <) +_{𝑒} (\frac{w}{2}) \to sup (A ℝ^{} <) \leq sup (B ℝ^{*} <) +_{𝑒} w)$
132	131	ad4ant14	$⊢ (((φ \land B \neq \emptyset) \land −∞ < sup (B ℝ^{} <)) \land w \in ℝ^{+}) \to (\exists x \in B x \leq sup (B ℝ^{} <) +_{𝑒} (\frac{w}{2}) \to sup (A ℝ^{} <) \leq sup (B ℝ^{} <) +_{𝑒} w)$
133	101 132	mpd	$⊢ (((φ \land B \neq \emptyset) \land −∞ < sup (B ℝ^{} <)) \land w \in ℝ^{+}) \to sup (A ℝ^{} <) \leq sup (B ℝ^{*} <) +_{𝑒} w$
134	88 89 133	xrlexaddrp	$⊢ ((φ \land B \neq \emptyset) \land −∞ < sup (B ℝ^{} <)) \to sup (A ℝ^{} <) \leq sup (B ℝ^{*} <)$
135	87 134	syldan	$⊢ ((φ \land B \neq \emptyset) \land \neg sup (B ℝ^{} <) = −∞) \to sup (A ℝ^{} <) \leq sup (B ℝ^{*} <)$
136	75 135	pm2.61dan	$⊢ (φ \land B \neq \emptyset) \to sup (A ℝ^{} <) \leq sup (B ℝ^{} <)$
137	17 136	syldan	$⊢ (φ \land \neg B = \emptyset) \to sup (A ℝ^{} <) \leq sup (B ℝ^{} <)$
138	15 137	pm2.61dan	$⊢ φ \to sup (A ℝ^{} <) \leq sup (B ℝ^{} <)$

Metamath Proof Explorer

Theorem infleinf

Proof