fsupdm

Description: The domain of the sup function is defined in Proposition 121F (b) of Fremlin1, p. 38. Note that this definition of the sup function is quite general, as it does not require the original functions to be sigma-measurable, and it could be applied to uncountable sets of functions. The equality proved here is part of the proof of the fourth statement of Proposition 121H in Fremlin1, p. 39. (Contributed by Glauco Siliprandi, 24-Jan-2025)

	Ref	Expression
Hypotheses	fsupdm.1	$⊢ Ⅎ n φ$
	fsupdm.2	$⊢ Ⅎ x φ$
	fsupdm.3	$⊢ Ⅎ m φ$
	fsupdm.4	$⊢ \underline{Ⅎ} x F$
	fsupdm.5	$⊢ (φ \land n \in Z) \to F (n) : dom F (n) ⟶ ℝ^{*}$
	fsupdm.6	$⊢ D = \{x \in ⋂_{n \in Z} dom F (n) \| \exists y \in ℝ \forall n \in Z F (n) (x) \leq y\}$
	fsupdm.7	$⊢ H = (n \in Z ⟼ (m \in ℕ ⟼ \{x \in dom F (n) \| F (n) (x) < m\}))$
Assertion	fsupdm	$⊢ φ \to D = ⋃_{m \in ℕ} ⋂_{n \in Z} H (n) (m)$

Proof

Step	Hyp	Ref	Expression
1		fsupdm.1	$⊢ Ⅎ n φ$
2		fsupdm.2	$⊢ Ⅎ x φ$
3		fsupdm.3	$⊢ Ⅎ m φ$
4		fsupdm.4	$⊢ \underline{Ⅎ} x F$
5		fsupdm.5	$⊢ (φ \land n \in Z) \to F (n) : dom F (n) ⟶ ℝ^{*}$
6		fsupdm.6	$⊢ D = \{x \in ⋂_{n \in Z} dom F (n) \| \exists y \in ℝ \forall n \in Z F (n) (x) \leq y\}$
7		fsupdm.7	$⊢ H = (n \in Z ⟼ (m \in ℕ ⟼ \{x \in dom F (n) \| F (n) (x) < m\}))$
8		nfcv	$⊢ \underline{Ⅎ} x ℕ$
9		nfcv	$⊢ \underline{Ⅎ} x Z$
10		nfrab1	$⊢ \underline{Ⅎ} x \{x \in dom F (n) \| F (n) (x) < m\}$
11	8 10	nfmpt	$⊢ \underline{Ⅎ} x (m \in ℕ ⟼ \{x \in dom F (n) \| F (n) (x) < m\})$
12	9 11	nfmpt	$⊢ \underline{Ⅎ} x (n \in Z ⟼ (m \in ℕ ⟼ \{x \in dom F (n) \| F (n) (x) < m\}))$
13	7 12	nfcxfr	$⊢ \underline{Ⅎ} x H$
14		nfcv	$⊢ \underline{Ⅎ} x n$
15	13 14	nffv	$⊢ \underline{Ⅎ} x H (n)$
16		nfcv	$⊢ \underline{Ⅎ} x m$
17	15 16	nffv	$⊢ \underline{Ⅎ} x H (n) (m)$
18	9 17	nfiin	$⊢ \underline{Ⅎ} x ⋂_{n \in Z} H (n) (m)$
19	8 18	nfiun	$⊢ \underline{Ⅎ} x ⋃_{m \in ℕ} ⋂_{n \in Z} H (n) (m)$
20		nfv	$⊢ Ⅎ m x \in ⋂_{n \in Z} dom F (n)$
21	3 20	nfan	$⊢ Ⅎ m (φ \land x \in ⋂_{n \in Z} dom F (n))$
22		nfv	$⊢ Ⅎ m y \in ℝ$
23	21 22	nfan	$⊢ Ⅎ m ((φ \land x \in ⋂_{n \in Z} dom F (n)) \land y \in ℝ)$
24		nfv	$⊢ Ⅎ m \forall n \in Z F (n) (x) \leq y$
25	23 24	nfan	$⊢ Ⅎ m (((φ \land x \in ⋂_{n \in Z} dom F (n)) \land y \in ℝ) \land \forall n \in Z F (n) (x) \leq y)$
26		nfii1	$⊢ \underline{Ⅎ} n ⋂_{n \in Z} dom F (n)$
27	26	nfcri	$⊢ Ⅎ n x \in ⋂_{n \in Z} dom F (n)$
28	1 27	nfan	$⊢ Ⅎ n (φ \land x \in ⋂_{n \in Z} dom F (n))$
29		nfv	$⊢ Ⅎ n y \in ℝ$
30	28 29	nfan	$⊢ Ⅎ n ((φ \land x \in ⋂_{n \in Z} dom F (n)) \land y \in ℝ)$
31		nfra1	$⊢ Ⅎ n \forall n \in Z F (n) (x) \leq y$
32	30 31	nfan	$⊢ Ⅎ n (((φ \land x \in ⋂_{n \in Z} dom F (n)) \land y \in ℝ) \land \forall n \in Z F (n) (x) \leq y)$
33		nfv	$⊢ Ⅎ n m \in ℕ$
34		nfv	$⊢ Ⅎ n y < m$
35	32 33 34	nf3an	$⊢ Ⅎ n ((((φ \land x \in ⋂_{n \in Z} dom F (n)) \land y \in ℝ) \land \forall n \in Z F (n) (x) \leq y) \land m \in ℕ \land y < m)$
36		vex	$⊢ x \in V$
37	36	a1i	$⊢ ((((φ \land x \in ⋂_{n \in Z} dom F (n)) \land y \in ℝ) \land \forall n \in Z F (n) (x) \leq y) \land m \in ℕ \land y < m) \to x \in V$
38		simp-4r	$⊢ ((((φ \land x \in ⋂_{n \in Z} dom F (n)) \land y \in ℝ) \land \forall n \in Z F (n) (x) \leq y) \land n \in Z) \to x \in ⋂_{n \in Z} dom F (n)$
39	38	3ad2antl1	$⊢ (((((φ \land x \in ⋂_{n \in Z} dom F (n)) \land y \in ℝ) \land \forall n \in Z F (n) (x) \leq y) \land m \in ℕ \land y < m) \land n \in Z) \to x \in ⋂_{n \in Z} dom F (n)$
40		simpr	$⊢ (((((φ \land x \in ⋂_{n \in Z} dom F (n)) \land y \in ℝ) \land \forall n \in Z F (n) (x) \leq y) \land m \in ℕ \land y < m) \land n \in Z) \to n \in Z$
41		eliinid	$⊢ (x \in ⋂_{n \in Z} dom F (n) \land n \in Z) \to x \in dom F (n)$
42	39 40 41	syl2anc	$⊢ (((((φ \land x \in ⋂_{n \in Z} dom F (n)) \land y \in ℝ) \land \forall n \in Z F (n) (x) \leq y) \land m \in ℕ \land y < m) \land n \in Z) \to x \in dom F (n)$
43		simp-4l	$⊢ ((((φ \land x \in ⋂_{n \in Z} dom F (n)) \land y \in ℝ) \land \forall n \in Z F (n) (x) \leq y) \land n \in Z) \to φ$
44	43	3ad2antl1	$⊢ (((((φ \land x \in ⋂_{n \in Z} dom F (n)) \land y \in ℝ) \land \forall n \in Z F (n) (x) \leq y) \land m \in ℕ \land y < m) \land n \in Z) \to φ$
45	44 40 5	syl2anc	$⊢ (((((φ \land x \in ⋂_{n \in Z} dom F (n)) \land y \in ℝ) \land \forall n \in Z F (n) (x) \leq y) \land m \in ℕ \land y < m) \land n \in Z) \to F (n) : dom F (n) ⟶ ℝ^{*}$
46	45 42	ffvelcdmd	$⊢ (((((φ \land x \in ⋂_{n \in Z} dom F (n)) \land y \in ℝ) \land \forall n \in Z F (n) (x) \leq y) \land m \in ℕ \land y < m) \land n \in Z) \to F (n) (x) \in ℝ^{*}$
47		simpllr	$⊢ ((((φ \land x \in ⋂_{n \in Z} dom F (n)) \land y \in ℝ) \land \forall n \in Z F (n) (x) \leq y) \land n \in Z) \to y \in ℝ$
48	47	rexrd	$⊢ ((((φ \land x \in ⋂_{n \in Z} dom F (n)) \land y \in ℝ) \land \forall n \in Z F (n) (x) \leq y) \land n \in Z) \to y \in ℝ^{*}$
49	48	3ad2antl1	$⊢ (((((φ \land x \in ⋂_{n \in Z} dom F (n)) \land y \in ℝ) \land \forall n \in Z F (n) (x) \leq y) \land m \in ℕ \land y < m) \land n \in Z) \to y \in ℝ^{*}$
50		simpl2	$⊢ (((((φ \land x \in ⋂_{n \in Z} dom F (n)) \land y \in ℝ) \land \forall n \in Z F (n) (x) \leq y) \land m \in ℕ \land y < m) \land n \in Z) \to m \in ℕ$
51	50	nnxrd	$⊢ (((((φ \land x \in ⋂_{n \in Z} dom F (n)) \land y \in ℝ) \land \forall n \in Z F (n) (x) \leq y) \land m \in ℕ \land y < m) \land n \in Z) \to m \in ℝ^{*}$
52		simpl1r	$⊢ (((((φ \land x \in ⋂_{n \in Z} dom F (n)) \land y \in ℝ) \land \forall n \in Z F (n) (x) \leq y) \land m \in ℕ \land y < m) \land n \in Z) \to \forall n \in Z F (n) (x) \leq y$
53		rspa	$⊢ (\forall n \in Z F (n) (x) \leq y \land n \in Z) \to F (n) (x) \leq y$
54	52 40 53	syl2anc	$⊢ (((((φ \land x \in ⋂_{n \in Z} dom F (n)) \land y \in ℝ) \land \forall n \in Z F (n) (x) \leq y) \land m \in ℕ \land y < m) \land n \in Z) \to F (n) (x) \leq y$
55		simpl3	$⊢ (((((φ \land x \in ⋂_{n \in Z} dom F (n)) \land y \in ℝ) \land \forall n \in Z F (n) (x) \leq y) \land m \in ℕ \land y < m) \land n \in Z) \to y < m$
56	46 49 51 54 55	xrlelttrd	$⊢ (((((φ \land x \in ⋂_{n \in Z} dom F (n)) \land y \in ℝ) \land \forall n \in Z F (n) (x) \leq y) \land m \in ℕ \land y < m) \land n \in Z) \to F (n) (x) < m$
57	42 56	rabidd	$⊢ (((((φ \land x \in ⋂_{n \in Z} dom F (n)) \land y \in ℝ) \land \forall n \in Z F (n) (x) \leq y) \land m \in ℕ \land y < m) \land n \in Z) \to x \in \{x \in dom F (n) \| F (n) (x) < m\}$
58		trud	$⊢ n \in Z \to ⊤$
59		id	$⊢ n \in Z \to n \in Z$
60		nfcv	$⊢ \underline{Ⅎ} n Z$
61		nnex	$⊢ ℕ \in V$
62	61	mptex	$⊢ (m \in ℕ ⟼ \{x \in dom F (n) \| F (n) (x) < m\}) \in V$
63	62	a1i	$⊢ (⊤ \land n \in Z) \to (m \in ℕ ⟼ \{x \in dom F (n) \| F (n) (x) < m\}) \in V$
64	60 7 63	fvmpt2df	$⊢ (⊤ \land n \in Z) \to H (n) = (m \in ℕ ⟼ \{x \in dom F (n) \| F (n) (x) < m\})$
65	58 59 64	syl2anc	$⊢ n \in Z \to H (n) = (m \in ℕ ⟼ \{x \in dom F (n) \| F (n) (x) < m\})$
66	4 14	nffv	$⊢ \underline{Ⅎ} x F (n)$
67	66	nfdm	$⊢ \underline{Ⅎ} x dom F (n)$
68		fvex	$⊢ F (n) \in V$
69	68	dmex	$⊢ dom F (n) \in V$
70	67 69	rabexf	$⊢ \{x \in dom F (n) \| F (n) (x) < m\} \in V$
71	70	a1i	$⊢ (n \in Z \land m \in ℕ) \to \{x \in dom F (n) \| F (n) (x) < m\} \in V$
72	65 71	fvmpt2d	$⊢ (n \in Z \land m \in ℕ) \to H (n) (m) = \{x \in dom F (n) \| F (n) (x) < m\}$
73	72	eqcomd	$⊢ (n \in Z \land m \in ℕ) \to \{x \in dom F (n) \| F (n) (x) < m\} = H (n) (m)$
74	40 50 73	syl2anc	$⊢ (((((φ \land x \in ⋂_{n \in Z} dom F (n)) \land y \in ℝ) \land \forall n \in Z F (n) (x) \leq y) \land m \in ℕ \land y < m) \land n \in Z) \to \{x \in dom F (n) \| F (n) (x) < m\} = H (n) (m)$
75	57 74	eleqtrd	$⊢ (((((φ \land x \in ⋂_{n \in Z} dom F (n)) \land y \in ℝ) \land \forall n \in Z F (n) (x) \leq y) \land m \in ℕ \land y < m) \land n \in Z) \to x \in H (n) (m)$
76	35 37 75	eliind2	$⊢ ((((φ \land x \in ⋂_{n \in Z} dom F (n)) \land y \in ℝ) \land \forall n \in Z F (n) (x) \leq y) \land m \in ℕ \land y < m) \to x \in ⋂_{n \in Z} H (n) (m)$
77		arch	$⊢ y \in ℝ \to \exists m \in ℕ y < m$
78	77	ad2antlr	$⊢ (((φ \land x \in ⋂_{n \in Z} dom F (n)) \land y \in ℝ) \land \forall n \in Z F (n) (x) \leq y) \to \exists m \in ℕ y < m$
79	25 76 78	reximdd	$⊢ (((φ \land x \in ⋂_{n \in Z} dom F (n)) \land y \in ℝ) \land \forall n \in Z F (n) (x) \leq y) \to \exists m \in ℕ x \in ⋂_{n \in Z} H (n) (m)$
80	79	rexlimdva2	$⊢ (φ \land x \in ⋂_{n \in Z} dom F (n)) \to (\exists y \in ℝ \forall n \in Z F (n) (x) \leq y \to \exists m \in ℕ x \in ⋂_{n \in Z} H (n) (m))$
81	80	3impia	$⊢ (φ \land x \in ⋂_{n \in Z} dom F (n) \land \exists y \in ℝ \forall n \in Z F (n) (x) \leq y) \to \exists m \in ℕ x \in ⋂_{n \in Z} H (n) (m)$
82		eliun	$⊢ x \in ⋃_{m \in ℕ} ⋂_{n \in Z} H (n) (m) \leftrightarrow \exists m \in ℕ x \in ⋂_{n \in Z} H (n) (m)$
83	81 82	sylibr	$⊢ (φ \land x \in ⋂_{n \in Z} dom F (n) \land \exists y \in ℝ \forall n \in Z F (n) (x) \leq y) \to x \in ⋃_{m \in ℕ} ⋂_{n \in Z} H (n) (m)$
84	2 19 83	rabssd	$⊢ φ \to \{x \in ⋂_{n \in Z} dom F (n) \| \exists y \in ℝ \forall n \in Z F (n) (x) \leq y\} \subseteq ⋃_{m \in ℕ} ⋂_{n \in Z} H (n) (m)$
85	6 84	eqsstrid	$⊢ φ \to D \subseteq ⋃_{m \in ℕ} ⋂_{n \in Z} H (n) (m)$
86		nfcv	$⊢ \underline{Ⅎ} m D$
87		nfv	$⊢ Ⅎ x m \in ℕ$
88	2 87	nfan	$⊢ Ⅎ x (φ \land m \in ℕ)$
89		nfrab1	$⊢ \underline{Ⅎ} x \{x \in ⋂_{n \in Z} dom F (n) \| \exists y \in ℝ \forall n \in Z F (n) (x) \leq y\}$
90	6 89	nfcxfr	$⊢ \underline{Ⅎ} x D$
91	1 33	nfan	$⊢ Ⅎ n (φ \land m \in ℕ)$
92		nfii1	$⊢ \underline{Ⅎ} n ⋂_{n \in Z} H (n) (m)$
93	92	nfcri	$⊢ Ⅎ n x \in ⋂_{n \in Z} H (n) (m)$
94	91 93	nfan	$⊢ Ⅎ n ((φ \land m \in ℕ) \land x \in ⋂_{n \in Z} H (n) (m))$
95	36	a1i	$⊢ ((φ \land m \in ℕ) \land x \in ⋂_{n \in Z} H (n) (m)) \to x \in V$
96		eliinid	$⊢ (x \in ⋂_{n \in Z} H (n) (m) \land n \in Z) \to x \in H (n) (m)$
97	96	adantll	$⊢ (((φ \land m \in ℕ) \land x \in ⋂_{n \in Z} H (n) (m)) \land n \in Z) \to x \in H (n) (m)$
98		simpr	$⊢ (((φ \land m \in ℕ) \land x \in ⋂_{n \in Z} H (n) (m)) \land n \in Z) \to n \in Z$
99		simpllr	$⊢ (((φ \land m \in ℕ) \land x \in ⋂_{n \in Z} H (n) (m)) \land n \in Z) \to m \in ℕ$
100	98 99 72	syl2anc	$⊢ (((φ \land m \in ℕ) \land x \in ⋂_{n \in Z} H (n) (m)) \land n \in Z) \to H (n) (m) = \{x \in dom F (n) \| F (n) (x) < m\}$
101	97 100	eleqtrd	$⊢ (((φ \land m \in ℕ) \land x \in ⋂_{n \in Z} H (n) (m)) \land n \in Z) \to x \in \{x \in dom F (n) \| F (n) (x) < m\}$
102		rabidim1	$⊢ x \in \{x \in dom F (n) \| F (n) (x) < m\} \to x \in dom F (n)$
103	101 102	syl	$⊢ (((φ \land m \in ℕ) \land x \in ⋂_{n \in Z} H (n) (m)) \land n \in Z) \to x \in dom F (n)$
104	94 95 103	eliind2	$⊢ ((φ \land m \in ℕ) \land x \in ⋂_{n \in Z} H (n) (m)) \to x \in ⋂_{n \in Z} dom F (n)$
105		nnre	$⊢ m \in ℕ \to m \in ℝ$
106	105	ad2antlr	$⊢ ((φ \land m \in ℕ) \land x \in ⋂_{n \in Z} H (n) (m)) \to m \in ℝ$
107		breq2	$⊢ y = m \to (F (n) (x) \leq y \leftrightarrow F (n) (x) \leq m)$
108	107	ralbidv	$⊢ y = m \to (\forall n \in Z F (n) (x) \leq y \leftrightarrow \forall n \in Z F (n) (x) \leq m)$
109	108	adantl	$⊢ (((φ \land m \in ℕ) \land x \in ⋂_{n \in Z} H (n) (m)) \land y = m) \to (\forall n \in Z F (n) (x) \leq y \leftrightarrow \forall n \in Z F (n) (x) \leq m)$
110		simplll	$⊢ (((φ \land m \in ℕ) \land x \in ⋂_{n \in Z} H (n) (m)) \land n \in Z) \to φ$
111	5	3adant3	$⊢ (φ \land n \in Z \land x \in dom F (n)) \to F (n) : dom F (n) ⟶ ℝ^{*}$
112		simp3	$⊢ (φ \land n \in Z \land x \in dom F (n)) \to x \in dom F (n)$
113	111 112	ffvelcdmd	$⊢ (φ \land n \in Z \land x \in dom F (n)) \to F (n) (x) \in ℝ^{*}$
114	110 98 103 113	syl3anc	$⊢ (((φ \land m \in ℕ) \land x \in ⋂_{n \in Z} H (n) (m)) \land n \in Z) \to F (n) (x) \in ℝ^{*}$
115	99	nnxrd	$⊢ (((φ \land m \in ℕ) \land x \in ⋂_{n \in Z} H (n) (m)) \land n \in Z) \to m \in ℝ^{*}$
116		rabidim2	$⊢ x \in \{x \in dom F (n) \| F (n) (x) < m\} \to F (n) (x) < m$
117	101 116	syl	$⊢ (((φ \land m \in ℕ) \land x \in ⋂_{n \in Z} H (n) (m)) \land n \in Z) \to F (n) (x) < m$
118	114 115 117	xrltled	$⊢ (((φ \land m \in ℕ) \land x \in ⋂_{n \in Z} H (n) (m)) \land n \in Z) \to F (n) (x) \leq m$
119	94 118	ralrimia	$⊢ ((φ \land m \in ℕ) \land x \in ⋂_{n \in Z} H (n) (m)) \to \forall n \in Z F (n) (x) \leq m$
120	106 109 119	rspcedvd	$⊢ ((φ \land m \in ℕ) \land x \in ⋂_{n \in Z} H (n) (m)) \to \exists y \in ℝ \forall n \in Z F (n) (x) \leq y$
121	104 120	rabidd	$⊢ ((φ \land m \in ℕ) \land x \in ⋂_{n \in Z} H (n) (m)) \to x \in \{x \in ⋂_{n \in Z} dom F (n) \| \exists y \in ℝ \forall n \in Z F (n) (x) \leq y\}$
122	121 6	eleqtrrdi	$⊢ ((φ \land m \in ℕ) \land x \in ⋂_{n \in Z} H (n) (m)) \to x \in D$
123	88 18 90 122	ssdf2	$⊢ (φ \land m \in ℕ) \to ⋂_{n \in Z} H (n) (m) \subseteq D$
124	3 86 123	iunssdf	$⊢ φ \to ⋃_{m \in ℕ} ⋂_{n \in Z} H (n) (m) \subseteq D$
125	85 124	eqssd	$⊢ φ \to D = ⋃_{m \in ℕ} ⋂_{n \in Z} H (n) (m)$

Metamath Proof Explorer

Theorem fsupdm

Proof