finfdm

Description: The domain of the inf function is defined in Proposition 121F (c) of Fremlin1, p. 39. See smfinf . Note that this definition of the inf 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 fifth statement of Proposition 121H in Fremlin1, p. 39. (Contributed by Glauco Siliprandi, 1-Feb-2025)

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

Proof

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

Metamath Proof Explorer

Theorem finfdm

Proof