supminfxrrnmpt

Description: The indexed supremum of a set of reals is the negation of the indexed infimum of that set's image under negation. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	supminfxrrnmpt.x	⊢ Ⅎ 𝑥 𝜑
	supminfxrrnmpt.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ^* )
Assertion	supminfxrrnmpt	⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ^* , < ) = -_𝑒 inf ( ran ( 𝑥 ∈ 𝐴 ↦ -_𝑒 𝐵 ) , ℝ^* , < ) )

Proof

Step	Hyp	Ref	Expression
1		supminfxrrnmpt.x	⊢ Ⅎ 𝑥 𝜑
2		supminfxrrnmpt.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ^* )
3		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
4	1 3 2	rnmptssd	⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ^* )
5	4	supminfxr2	⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ^* , < ) = -_𝑒 inf ( { 𝑦 ∈ ℝ^* ∣ -_𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } , ℝ^* , < ) )
6		xnegex	⊢ -_𝑒 𝑦 ∈ V
7	3	elrnmpt	⊢ ( -_𝑒 𝑦 ∈ V → ( -_𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 -_𝑒 𝑦 = 𝐵 ) )
8	6 7	ax-mp	⊢ ( -_𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 -_𝑒 𝑦 = 𝐵 )
9	8	biimpi	⊢ ( -_𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 -_𝑒 𝑦 = 𝐵 )
10		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ -_𝑒 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ -_𝑒 𝐵 )
11		xnegneg	⊢ ( 𝑦 ∈ ℝ^* → -_𝑒 -_𝑒 𝑦 = 𝑦 )
12	11	eqcomd	⊢ ( 𝑦 ∈ ℝ^* → 𝑦 = -_𝑒 -_𝑒 𝑦 )
13	12	adantr	⊢ ( ( 𝑦 ∈ ℝ^* ∧ -_𝑒 𝑦 = 𝐵 ) → 𝑦 = -_𝑒 -_𝑒 𝑦 )
14		xnegeq	⊢ ( -_𝑒 𝑦 = 𝐵 → -_𝑒 -_𝑒 𝑦 = -_𝑒 𝐵 )
15	14	adantl	⊢ ( ( 𝑦 ∈ ℝ^* ∧ -_𝑒 𝑦 = 𝐵 ) → -_𝑒 -_𝑒 𝑦 = -_𝑒 𝐵 )
16	13 15	eqtrd	⊢ ( ( 𝑦 ∈ ℝ^* ∧ -_𝑒 𝑦 = 𝐵 ) → 𝑦 = -_𝑒 𝐵 )
17	16	ex	⊢ ( 𝑦 ∈ ℝ^* → ( -_𝑒 𝑦 = 𝐵 → 𝑦 = -_𝑒 𝐵 ) )
18	17	reximdv	⊢ ( 𝑦 ∈ ℝ^* → ( ∃ 𝑥 ∈ 𝐴 -_𝑒 𝑦 = 𝐵 → ∃ 𝑥 ∈ 𝐴 𝑦 = -_𝑒 𝐵 ) )
19	18	imp	⊢ ( ( 𝑦 ∈ ℝ^* ∧ ∃ 𝑥 ∈ 𝐴 -_𝑒 𝑦 = 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑦 = -_𝑒 𝐵 )
20		simpl	⊢ ( ( 𝑦 ∈ ℝ^* ∧ ∃ 𝑥 ∈ 𝐴 -_𝑒 𝑦 = 𝐵 ) → 𝑦 ∈ ℝ^* )
21	10 19 20	elrnmptd	⊢ ( ( 𝑦 ∈ ℝ^* ∧ ∃ 𝑥 ∈ 𝐴 -_𝑒 𝑦 = 𝐵 ) → 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ -_𝑒 𝐵 ) )
22	9 21	sylan2	⊢ ( ( 𝑦 ∈ ℝ^* ∧ -_𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) → 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ -_𝑒 𝐵 ) )
23	22	ex	⊢ ( 𝑦 ∈ ℝ^* → ( -_𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) → 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ -_𝑒 𝐵 ) ) )
24	23	rgen	⊢ ∀ 𝑦 ∈ ℝ^* ( -_𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) → 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ -_𝑒 𝐵 ) )
25		rabss	⊢ ( { 𝑦 ∈ ℝ^* ∣ -_𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } ⊆ ran ( 𝑥 ∈ 𝐴 ↦ -_𝑒 𝐵 ) ↔ ∀ 𝑦 ∈ ℝ^* ( -_𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) → 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ -_𝑒 𝐵 ) ) )
26	25	biimpri	⊢ ( ∀ 𝑦 ∈ ℝ^* ( -_𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) → 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ -_𝑒 𝐵 ) ) → { 𝑦 ∈ ℝ^* ∣ -_𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } ⊆ ran ( 𝑥 ∈ 𝐴 ↦ -_𝑒 𝐵 ) )
27	24 26	ax-mp	⊢ { 𝑦 ∈ ℝ^* ∣ -_𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } ⊆ ran ( 𝑥 ∈ 𝐴 ↦ -_𝑒 𝐵 )
28	27	a1i	⊢ ( 𝜑 → { 𝑦 ∈ ℝ^* ∣ -_𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } ⊆ ran ( 𝑥 ∈ 𝐴 ↦ -_𝑒 𝐵 ) )
29		nfcv	⊢ Ⅎ 𝑥 -_𝑒 𝑦
30		nfmpt1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
31	30	nfrn	⊢ Ⅎ 𝑥 ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
32	29 31	nfel	⊢ Ⅎ 𝑥 -_𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
33		nfcv	⊢ Ⅎ 𝑥 ℝ^*
34	32 33	nfrabw	⊢ Ⅎ 𝑥 { 𝑦 ∈ ℝ^* ∣ -_𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) }
35		xnegeq	⊢ ( 𝑦 = -_𝑒 𝐵 → -_𝑒 𝑦 = -_𝑒 -_𝑒 𝐵 )
36	35	eleq1d	⊢ ( 𝑦 = -_𝑒 𝐵 → ( -_𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↔ -_𝑒 -_𝑒 𝐵 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) )
37	2	xnegcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → -_𝑒 𝐵 ∈ ℝ^* )
38		xnegneg	⊢ ( 𝐵 ∈ ℝ^* → -_𝑒 -_𝑒 𝐵 = 𝐵 )
39	2 38	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → -_𝑒 -_𝑒 𝐵 = 𝐵 )
40		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
41	3 40 2	elrnmpt1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
42	39 41	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → -_𝑒 -_𝑒 𝐵 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
43	36 37 42	elrabd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → -_𝑒 𝐵 ∈ { 𝑦 ∈ ℝ^* ∣ -_𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } )
44	1 34 10 43	rnmptssdf	⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐴 ↦ -_𝑒 𝐵 ) ⊆ { 𝑦 ∈ ℝ^* ∣ -_𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } )
45	28 44	eqssd	⊢ ( 𝜑 → { 𝑦 ∈ ℝ^* ∣ -_𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } = ran ( 𝑥 ∈ 𝐴 ↦ -_𝑒 𝐵 ) )
46	45	infeq1d	⊢ ( 𝜑 → inf ( { 𝑦 ∈ ℝ^* ∣ -_𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } , ℝ^* , < ) = inf ( ran ( 𝑥 ∈ 𝐴 ↦ -_𝑒 𝐵 ) , ℝ^* , < ) )
47	46	xnegeqd	⊢ ( 𝜑 → -_𝑒 inf ( { 𝑦 ∈ ℝ^* ∣ -_𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } , ℝ^* , < ) = -_𝑒 inf ( ran ( 𝑥 ∈ 𝐴 ↦ -_𝑒 𝐵 ) , ℝ^* , < ) )
48	5 47	eqtrd	⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ^* , < ) = -_𝑒 inf ( ran ( 𝑥 ∈ 𝐴 ↦ -_𝑒 𝐵 ) , ℝ^* , < ) )

Metamath Proof Explorer

Theorem supminfxrrnmpt

Proof