smfinflem

Description: The infimum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (c) of Fremlin1 p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	smfinflem.m	$⊢ φ \to M \in ℤ$
	smfinflem.z	$⊢ Z = ℤ_{\geq M}$
	smfinflem.s	$⊢ φ \to S \in SAlg$
	smfinflem.f	$⊢ φ \to F : Z ⟶ SMblFn (S)$
	smfinflem.d	$⊢ D = \{x \in ⋂_{n \in Z} dom F (n) \| \exists y \in ℝ \forall n \in Z y \leq F (n) (x)\}$
	smfinflem.g	$⊢ G = (x \in D ⟼ sup (ran (n \in Z ⟼ F (n) (x)) ℝ <))$
Assertion	smfinflem	$⊢ φ \to G \in SMblFn (S)$

Proof

Step	Hyp	Ref	Expression
1		smfinflem.m	$⊢ φ \to M \in ℤ$
2		smfinflem.z	$⊢ Z = ℤ_{\geq M}$
3		smfinflem.s	$⊢ φ \to S \in SAlg$
4		smfinflem.f	$⊢ φ \to F : Z ⟶ SMblFn (S)$
5		smfinflem.d	$⊢ D = \{x \in ⋂_{n \in Z} dom F (n) \| \exists y \in ℝ \forall n \in Z y \leq F (n) (x)\}$
6		smfinflem.g	$⊢ G = (x \in D ⟼ sup (ran (n \in Z ⟼ F (n) (x)) ℝ <))$
7	6	a1i	$⊢ φ \to G = (x \in D ⟼ sup (ran (n \in Z ⟼ F (n) (x)) ℝ <))$
8		nfv	$⊢ Ⅎ n (φ \land x \in D)$
9	1 2	uzn0d	$⊢ φ \to Z \neq \emptyset$
10	9	adantr	$⊢ (φ \land x \in D) \to Z \neq \emptyset$
11	3	adantr	$⊢ (φ \land n \in Z) \to S \in SAlg$
12	4	ffvelrnda	$⊢ (φ \land n \in Z) \to F (n) \in SMblFn (S)$
13		eqid	$⊢ dom F (n) = dom F (n)$
14	11 12 13	smff	$⊢ (φ \land n \in Z) \to F (n) : dom F (n) ⟶ ℝ$
15	14	adantlr	$⊢ ((φ \land x \in D) \land n \in Z) \to F (n) : dom F (n) ⟶ ℝ$
16		ssrab2	$⊢ \{x \in ⋂_{n \in Z} dom F (n) \| \exists y \in ℝ \forall n \in Z y \leq F (n) (x)\} \subseteq ⋂_{n \in Z} dom F (n)$
17	5	eleq2i	$⊢ x \in D \leftrightarrow x \in \{x \in ⋂_{n \in Z} dom F (n) \| \exists y \in ℝ \forall n \in Z y \leq F (n) (x)\}$
18	17	biimpi	$⊢ x \in D \to x \in \{x \in ⋂_{n \in Z} dom F (n) \| \exists y \in ℝ \forall n \in Z y \leq F (n) (x)\}$
19	16 18	sselid	$⊢ x \in D \to x \in ⋂_{n \in Z} dom F (n)$
20	19	adantr	$⊢ (x \in D \land n \in Z) \to x \in ⋂_{n \in Z} dom F (n)$
21		simpr	$⊢ (x \in D \land n \in Z) \to n \in Z$
22		eliinid	$⊢ (x \in ⋂_{n \in Z} dom F (n) \land n \in Z) \to x \in dom F (n)$
23	20 21 22	syl2anc	$⊢ (x \in D \land n \in Z) \to x \in dom F (n)$
24	23	adantll	$⊢ ((φ \land x \in D) \land n \in Z) \to x \in dom F (n)$
25	15 24	ffvelrnd	$⊢ ((φ \land x \in D) \land n \in Z) \to F (n) (x) \in ℝ$
26		rabidim2	$⊢ x \in \{x \in ⋂_{n \in Z} dom F (n) \| \exists y \in ℝ \forall n \in Z y \leq F (n) (x)\} \to \exists y \in ℝ \forall n \in Z y \leq F (n) (x)$
27	18 26	syl	$⊢ x \in D \to \exists y \in ℝ \forall n \in Z y \leq F (n) (x)$
28	27	adantl	$⊢ (φ \land x \in D) \to \exists y \in ℝ \forall n \in Z y \leq F (n) (x)$
29	8 10 25 28	infnsuprnmpt	$⊢ (φ \land x \in D) \to sup (ran (n \in Z ⟼ F (n) (x)) ℝ <) = - sup (ran (n \in Z ⟼ - F (n) (x)) ℝ <)$
30	29	mpteq2dva	$⊢ φ \to (x \in D ⟼ sup (ran (n \in Z ⟼ F (n) (x)) ℝ <)) = (x \in D ⟼ - sup (ran (n \in Z ⟼ - F (n) (x)) ℝ <))$
31	7 30	eqtrd	$⊢ φ \to G = (x \in D ⟼ - sup (ran (n \in Z ⟼ - F (n) (x)) ℝ <))$
32		nfv	$⊢ Ⅎ x φ$
33		fvex	$⊢ F (n) \in V$
34	33	dmex	$⊢ dom F (n) \in V$
35	34	rgenw	$⊢ \forall n \in Z dom F (n) \in V$
36	35	a1i	$⊢ φ \to \forall n \in Z dom F (n) \in V$
37	9 36	iinexd	$⊢ φ \to ⋂_{n \in Z} dom F (n) \in V$
38	5 37	rabexd	$⊢ φ \to D \in V$
39	25	renegcld	$⊢ ((φ \land x \in D) \land n \in Z) \to - F (n) (x) \in ℝ$
40		fveq2	$⊢ w = x \to F (m) (w) = F (m) (x)$
41	40	breq2d	$⊢ w = x \to (z \leq F (m) (w) \leftrightarrow z \leq F (m) (x))$
42	41	ralbidv	$⊢ w = x \to (\forall m \in Z z \leq F (m) (w) \leftrightarrow \forall m \in Z z \leq F (m) (x))$
43	42	rexbidv	$⊢ w = x \to (\exists z \in ℝ \forall m \in Z z \leq F (m) (w) \leftrightarrow \exists z \in ℝ \forall m \in Z z \leq F (m) (x))$
44		nfcv	$⊢ \underline{Ⅎ} w ⋂_{n \in Z} dom F (n)$
45		nfcv	$⊢ \underline{Ⅎ} x Z$
46		nfcv	$⊢ \underline{Ⅎ} x F (m)$
47	46	nfdm	$⊢ \underline{Ⅎ} x dom F (m)$
48	45 47	nfiin	$⊢ \underline{Ⅎ} x ⋂_{m \in Z} dom F (m)$
49		nfv	$⊢ Ⅎ w \exists y \in ℝ \forall n \in Z y \leq F (n) (x)$
50		nfv	$⊢ Ⅎ x \exists z \in ℝ \forall m \in Z z \leq F (m) (w)$
51		nfcv	$⊢ \underline{Ⅎ} m dom F (n)$
52		nfcv	$⊢ \underline{Ⅎ} n F (m)$
53	52	nfdm	$⊢ \underline{Ⅎ} n dom F (m)$
54		fveq2	$⊢ n = m \to F (n) = F (m)$
55	54	dmeqd	$⊢ n = m \to dom F (n) = dom F (m)$
56	51 53 55	cbviin	$⊢ ⋂_{n \in Z} dom F (n) = ⋂_{m \in Z} dom F (m)$
57	56	a1i	$⊢ x = w \to ⋂_{n \in Z} dom F (n) = ⋂_{m \in Z} dom F (m)$
58		fveq2	$⊢ x = w \to F (n) (x) = F (n) (w)$
59	58	breq2d	$⊢ x = w \to (y \leq F (n) (x) \leftrightarrow y \leq F (n) (w))$
60	59	ralbidv	$⊢ x = w \to (\forall n \in Z y \leq F (n) (x) \leftrightarrow \forall n \in Z y \leq F (n) (w))$
61		nfv	$⊢ Ⅎ m y \leq F (n) (w)$
62		nfcv	$⊢ \underline{Ⅎ} n y$
63		nfcv	$⊢ \underline{Ⅎ} n \leq$
64		nfcv	$⊢ \underline{Ⅎ} n w$
65	52 64	nffv	$⊢ \underline{Ⅎ} n F (m) (w)$
66	62 63 65	nfbr	$⊢ Ⅎ n y \leq F (m) (w)$
67	54	fveq1d	$⊢ n = m \to F (n) (w) = F (m) (w)$
68	67	breq2d	$⊢ n = m \to (y \leq F (n) (w) \leftrightarrow y \leq F (m) (w))$
69	61 66 68	cbvralw	$⊢ \forall n \in Z y \leq F (n) (w) \leftrightarrow \forall m \in Z y \leq F (m) (w)$
70	69	a1i	$⊢ x = w \to (\forall n \in Z y \leq F (n) (w) \leftrightarrow \forall m \in Z y \leq F (m) (w))$
71	60 70	bitrd	$⊢ x = w \to (\forall n \in Z y \leq F (n) (x) \leftrightarrow \forall m \in Z y \leq F (m) (w))$
72	71	rexbidv	$⊢ x = w \to (\exists y \in ℝ \forall n \in Z y \leq F (n) (x) \leftrightarrow \exists y \in ℝ \forall m \in Z y \leq F (m) (w))$
73		breq1	$⊢ y = z \to (y \leq F (m) (w) \leftrightarrow z \leq F (m) (w))$
74	73	ralbidv	$⊢ y = z \to (\forall m \in Z y \leq F (m) (w) \leftrightarrow \forall m \in Z z \leq F (m) (w))$
75	74	cbvrexvw	$⊢ \exists y \in ℝ \forall m \in Z y \leq F (m) (w) \leftrightarrow \exists z \in ℝ \forall m \in Z z \leq F (m) (w)$
76	75	a1i	$⊢ x = w \to (\exists y \in ℝ \forall m \in Z y \leq F (m) (w) \leftrightarrow \exists z \in ℝ \forall m \in Z z \leq F (m) (w))$
77	72 76	bitrd	$⊢ x = w \to (\exists y \in ℝ \forall n \in Z y \leq F (n) (x) \leftrightarrow \exists z \in ℝ \forall m \in Z z \leq F (m) (w))$
78	44 48 49 50 57 77	cbvrabcsfw	$⊢ \{x \in ⋂_{n \in Z} dom F (n) \| \exists y \in ℝ \forall n \in Z y \leq F (n) (x)\} = \{w \in ⋂_{m \in Z} dom F (m) \| \exists z \in ℝ \forall m \in Z z \leq F (m) (w)\}$
79	5 78	eqtri	$⊢ D = \{w \in ⋂_{m \in Z} dom F (m) \| \exists z \in ℝ \forall m \in Z z \leq F (m) (w)\}$
80	43 79	elrab2	$⊢ x \in D \leftrightarrow (x \in ⋂_{m \in Z} dom F (m) \land \exists z \in ℝ \forall m \in Z z \leq F (m) (x))$
81	80	biimpi	$⊢ x \in D \to (x \in ⋂_{m \in Z} dom F (m) \land \exists z \in ℝ \forall m \in Z z \leq F (m) (x))$
82	81	simprd	$⊢ x \in D \to \exists z \in ℝ \forall m \in Z z \leq F (m) (x)$
83	82	adantl	$⊢ (φ \land x \in D) \to \exists z \in ℝ \forall m \in Z z \leq F (m) (x)$
84		renegcl	$⊢ z \in ℝ \to - z \in ℝ$
85	84	ad2antlr	$⊢ (((φ \land x \in D) \land z \in ℝ) \land \forall m \in Z z \leq F (m) (x)) \to - z \in ℝ$
86		fveq2	$⊢ m = n \to F (m) = F (n)$
87	86	fveq1d	$⊢ m = n \to F (m) (x) = F (n) (x)$
88	87	breq2d	$⊢ m = n \to (z \leq F (m) (x) \leftrightarrow z \leq F (n) (x))$
89	88	rspcva	$⊢ (n \in Z \land \forall m \in Z z \leq F (m) (x)) \to z \leq F (n) (x)$
90	89	ancoms	$⊢ (\forall m \in Z z \leq F (m) (x) \land n \in Z) \to z \leq F (n) (x)$
91	90	adantll	$⊢ ((((φ \land x \in D) \land z \in ℝ) \land \forall m \in Z z \leq F (m) (x)) \land n \in Z) \to z \leq F (n) (x)$
92		simpllr	$⊢ ((((φ \land x \in D) \land z \in ℝ) \land \forall m \in Z z \leq F (m) (x)) \land n \in Z) \to z \in ℝ$
93	25	ad4ant14	$⊢ ((((φ \land x \in D) \land z \in ℝ) \land \forall m \in Z z \leq F (m) (x)) \land n \in Z) \to F (n) (x) \in ℝ$
94	92 93	lenegd	$⊢ ((((φ \land x \in D) \land z \in ℝ) \land \forall m \in Z z \leq F (m) (x)) \land n \in Z) \to (z \leq F (n) (x) \leftrightarrow - F (n) (x) \leq - z)$
95	91 94	mpbid	$⊢ ((((φ \land x \in D) \land z \in ℝ) \land \forall m \in Z z \leq F (m) (x)) \land n \in Z) \to - F (n) (x) \leq - z$
96	95	ralrimiva	$⊢ (((φ \land x \in D) \land z \in ℝ) \land \forall m \in Z z \leq F (m) (x)) \to \forall n \in Z - F (n) (x) \leq - z$
97		brralrspcev	$⊢ (- z \in ℝ \land \forall n \in Z - F (n) (x) \leq - z) \to \exists y \in ℝ \forall n \in Z - F (n) (x) \leq y$
98	85 96 97	syl2anc	$⊢ (((φ \land x \in D) \land z \in ℝ) \land \forall m \in Z z \leq F (m) (x)) \to \exists y \in ℝ \forall n \in Z - F (n) (x) \leq y$
99	98	rexlimdva2	$⊢ (φ \land x \in D) \to (\exists z \in ℝ \forall m \in Z z \leq F (m) (x) \to \exists y \in ℝ \forall n \in Z - F (n) (x) \leq y)$
100	83 99	mpd	$⊢ (φ \land x \in D) \to \exists y \in ℝ \forall n \in Z - F (n) (x) \leq y$
101	8 10 39 100	suprclrnmpt	$⊢ (φ \land x \in D) \to sup (ran (n \in Z ⟼ - F (n) (x)) ℝ <) \in ℝ$
102	5	a1i	$⊢ φ \to D = \{x \in ⋂_{n \in Z} dom F (n) \| \exists y \in ℝ \forall n \in Z y \leq F (n) (x)\}$
103		nfv	$⊢ Ⅎ y (φ \land x \in ⋂_{n \in Z} dom F (n))$
104		nfv	$⊢ Ⅎ y \exists z \in ℝ \forall n \in Z - F (n) (x) \leq z$
105		renegcl	$⊢ y \in ℝ \to - y \in ℝ$
106	105	3ad2ant2	$⊢ ((φ \land x \in ⋂_{n \in Z} dom F (n)) \land y \in ℝ \land \forall n \in Z y \leq F (n) (x)) \to - y \in ℝ$
107		nfv	$⊢ Ⅎ n φ$
108		nfcv	$⊢ \underline{Ⅎ} n x$
109		nfii1	$⊢ \underline{Ⅎ} n ⋂_{n \in Z} dom F (n)$
110	108 109	nfel	$⊢ Ⅎ n x \in ⋂_{n \in Z} dom F (n)$
111	107 110	nfan	$⊢ Ⅎ n (φ \land x \in ⋂_{n \in Z} dom F (n))$
112	62	nfel1	$⊢ Ⅎ n y \in ℝ$
113		nfra1	$⊢ Ⅎ n \forall n \in Z y \leq F (n) (x)$
114	111 112 113	nf3an	$⊢ Ⅎ n ((φ \land x \in ⋂_{n \in Z} dom F (n)) \land y \in ℝ \land \forall n \in Z y \leq F (n) (x))$
115		simpl2	$⊢ (((φ \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 ℝ$
116		simpll	$⊢ ((φ \land x \in ⋂_{n \in Z} dom F (n)) \land n \in Z) \to φ$
117		simpr	$⊢ ((φ \land x \in ⋂_{n \in Z} dom F (n)) \land n \in Z) \to n \in Z$
118	22	adantll	$⊢ ((φ \land x \in ⋂_{n \in Z} dom F (n)) \land n \in Z) \to x \in dom F (n)$
119	14	3adant3	$⊢ (φ \land n \in Z \land x \in dom F (n)) \to F (n) : dom F (n) ⟶ ℝ$
120		simp3	$⊢ (φ \land n \in Z \land x \in dom F (n)) \to x \in dom F (n)$
121	119 120	ffvelrnd	$⊢ (φ \land n \in Z \land x \in dom F (n)) \to F (n) (x) \in ℝ$
122	116 117 118 121	syl3anc	$⊢ ((φ \land x \in ⋂_{n \in Z} dom F (n)) \land n \in Z) \to F (n) (x) \in ℝ$
123	122	3ad2antl1	$⊢ (((φ \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 F (n) (x) \in ℝ$
124		rspa	$⊢ (\forall n \in Z y \leq F (n) (x) \land n \in Z) \to y \leq F (n) (x)$
125	124	3ad2antl3	$⊢ (((φ \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 \leq F (n) (x)$
126		leneg	$⊢ (y \in ℝ \land F (n) (x) \in ℝ) \to (y \leq F (n) (x) \leftrightarrow - F (n) (x) \leq - y)$
127	126	biimp3a	$⊢ (y \in ℝ \land F (n) (x) \in ℝ \land y \leq F (n) (x)) \to - F (n) (x) \leq - y$
128	115 123 125 127	syl3anc	$⊢ (((φ \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 - F (n) (x) \leq - y$
129	128	ex	$⊢ ((φ \land x \in ⋂_{n \in Z} dom F (n)) \land y \in ℝ \land \forall n \in Z y \leq F (n) (x)) \to (n \in Z \to - F (n) (x) \leq - y)$
130	114 129	ralrimi	$⊢ ((φ \land x \in ⋂_{n \in Z} dom F (n)) \land y \in ℝ \land \forall n \in Z y \leq F (n) (x)) \to \forall n \in Z - F (n) (x) \leq - y$
131		brralrspcev	$⊢ (- y \in ℝ \land \forall n \in Z - F (n) (x) \leq - y) \to \exists z \in ℝ \forall n \in Z - F (n) (x) \leq z$
132	106 130 131	syl2anc	$⊢ ((φ \land x \in ⋂_{n \in Z} dom F (n)) \land y \in ℝ \land \forall n \in Z y \leq F (n) (x)) \to \exists z \in ℝ \forall n \in Z - F (n) (x) \leq z$
133	132	3exp	$⊢ (φ \land x \in ⋂_{n \in Z} dom F (n)) \to (y \in ℝ \to (\forall n \in Z y \leq F (n) (x) \to \exists z \in ℝ \forall n \in Z - F (n) (x) \leq z))$
134	103 104 133	rexlimd	$⊢ (φ \land x \in ⋂_{n \in Z} dom F (n)) \to (\exists y \in ℝ \forall n \in Z y \leq F (n) (x) \to \exists z \in ℝ \forall n \in Z - F (n) (x) \leq z)$
135	84	3ad2ant2	$⊢ ((φ \land x \in ⋂_{n \in Z} dom F (n)) \land z \in ℝ \land \forall n \in Z - F (n) (x) \leq z) \to - z \in ℝ$
136		nfv	$⊢ Ⅎ n z \in ℝ$
137		nfra1	$⊢ Ⅎ n \forall n \in Z - F (n) (x) \leq z$
138	111 136 137	nf3an	$⊢ Ⅎ n ((φ \land x \in ⋂_{n \in Z} dom F (n)) \land z \in ℝ \land \forall n \in Z - F (n) (x) \leq z)$
139	122	3ad2antl1	$⊢ (((φ \land x \in ⋂_{n \in Z} dom F (n)) \land z \in ℝ \land \forall n \in Z - F (n) (x) \leq z) \land n \in Z) \to F (n) (x) \in ℝ$
140		simpl2	$⊢ (((φ \land x \in ⋂_{n \in Z} dom F (n)) \land z \in ℝ \land \forall n \in Z - F (n) (x) \leq z) \land n \in Z) \to z \in ℝ$
141		rspa	$⊢ (\forall n \in Z - F (n) (x) \leq z \land n \in Z) \to - F (n) (x) \leq z$
142	141	3ad2antl3	$⊢ (((φ \land x \in ⋂_{n \in Z} dom F (n)) \land z \in ℝ \land \forall n \in Z - F (n) (x) \leq z) \land n \in Z) \to - F (n) (x) \leq z$
143		simp3	$⊢ (F (n) (x) \in ℝ \land z \in ℝ \land - F (n) (x) \leq z) \to - F (n) (x) \leq z$
144		renegcl	$⊢ F (n) (x) \in ℝ \to - F (n) (x) \in ℝ$
145	144	adantr	$⊢ (F (n) (x) \in ℝ \land z \in ℝ) \to - F (n) (x) \in ℝ$
146		simpr	$⊢ (F (n) (x) \in ℝ \land z \in ℝ) \to z \in ℝ$
147		leneg	$⊢ (- F (n) (x) \in ℝ \land z \in ℝ) \to (- F (n) (x) \leq z \leftrightarrow - z \leq - (- F (n) (x)))$
148	145 146 147	syl2anc	$⊢ (F (n) (x) \in ℝ \land z \in ℝ) \to (- F (n) (x) \leq z \leftrightarrow - z \leq - (- F (n) (x)))$
149	148	3adant3	$⊢ (F (n) (x) \in ℝ \land z \in ℝ \land - F (n) (x) \leq z) \to (- F (n) (x) \leq z \leftrightarrow - z \leq - (- F (n) (x)))$
150	143 149	mpbid	$⊢ (F (n) (x) \in ℝ \land z \in ℝ \land - F (n) (x) \leq z) \to - z \leq - (- F (n) (x))$
151		recn	$⊢ F (n) (x) \in ℝ \to F (n) (x) \in ℂ$
152	151	negnegd	$⊢ F (n) (x) \in ℝ \to - (- F (n) (x)) = F (n) (x)$
153	152	3ad2ant1	$⊢ (F (n) (x) \in ℝ \land z \in ℝ \land - F (n) (x) \leq z) \to - (- F (n) (x)) = F (n) (x)$
154	150 153	breqtrd	$⊢ (F (n) (x) \in ℝ \land z \in ℝ \land - F (n) (x) \leq z) \to - z \leq F (n) (x)$
155	139 140 142 154	syl3anc	$⊢ (((φ \land x \in ⋂_{n \in Z} dom F (n)) \land z \in ℝ \land \forall n \in Z - F (n) (x) \leq z) \land n \in Z) \to - z \leq F (n) (x)$
156	155	ex	$⊢ ((φ \land x \in ⋂_{n \in Z} dom F (n)) \land z \in ℝ \land \forall n \in Z - F (n) (x) \leq z) \to (n \in Z \to - z \leq F (n) (x))$
157	138 156	ralrimi	$⊢ ((φ \land x \in ⋂_{n \in Z} dom F (n)) \land z \in ℝ \land \forall n \in Z - F (n) (x) \leq z) \to \forall n \in Z - z \leq F (n) (x)$
158		breq1	$⊢ y = - z \to (y \leq F (n) (x) \leftrightarrow - z \leq F (n) (x))$
159	158	ralbidv	$⊢ y = - z \to (\forall n \in Z y \leq F (n) (x) \leftrightarrow \forall n \in Z - z \leq F (n) (x))$
160	159	rspcev	$⊢ (- z \in ℝ \land \forall n \in Z - z \leq F (n) (x)) \to \exists y \in ℝ \forall n \in Z y \leq F (n) (x)$
161	135 157 160	syl2anc	$⊢ ((φ \land x \in ⋂_{n \in Z} dom F (n)) \land z \in ℝ \land \forall n \in Z - F (n) (x) \leq z) \to \exists y \in ℝ \forall n \in Z y \leq F (n) (x)$
162	161	3exp	$⊢ (φ \land x \in ⋂_{n \in Z} dom F (n)) \to (z \in ℝ \to (\forall n \in Z - F (n) (x) \leq z \to \exists y \in ℝ \forall n \in Z y \leq F (n) (x)))$
163	162	rexlimdv	$⊢ (φ \land x \in ⋂_{n \in Z} dom F (n)) \to (\exists z \in ℝ \forall n \in Z - F (n) (x) \leq z \to \exists y \in ℝ \forall n \in Z y \leq F (n) (x))$
164	134 163	impbid	$⊢ (φ \land x \in ⋂_{n \in Z} dom F (n)) \to (\exists y \in ℝ \forall n \in Z y \leq F (n) (x) \leftrightarrow \exists z \in ℝ \forall n \in Z - F (n) (x) \leq z)$
165	32 164	rabbida	$⊢ φ \to \{x \in ⋂_{n \in Z} dom F (n) \| \exists y \in ℝ \forall n \in Z y \leq F (n) (x)\} = \{x \in ⋂_{n \in Z} dom F (n) \| \exists z \in ℝ \forall n \in Z - F (n) (x) \leq z\}$
166	102 165	eqtrd	$⊢ φ \to D = \{x \in ⋂_{n \in Z} dom F (n) \| \exists z \in ℝ \forall n \in Z - F (n) (x) \leq z\}$
167	32 166	alrimi	$⊢ φ \to \forall x D = \{x \in ⋂_{n \in Z} dom F (n) \| \exists z \in ℝ \forall n \in Z - F (n) (x) \leq z\}$
168		eqid	$⊢ sup (ran (n \in Z ⟼ - F (n) (x)) ℝ <) = sup (ran (n \in Z ⟼ - F (n) (x)) ℝ <)$
169	168	rgenw	$⊢ \forall x \in D sup (ran (n \in Z ⟼ - F (n) (x)) ℝ <) = sup (ran (n \in Z ⟼ - F (n) (x)) ℝ <)$
170	169	a1i	$⊢ φ \to \forall x \in D sup (ran (n \in Z ⟼ - F (n) (x)) ℝ <) = sup (ran (n \in Z ⟼ - F (n) (x)) ℝ <)$
171		mpteq12f	$⊢ (\forall x D = \{x \in ⋂_{n \in Z} dom F (n) \| \exists z \in ℝ \forall n \in Z - F (n) (x) \leq z\} \land \forall x \in D sup (ran (n \in Z ⟼ - F (n) (x)) ℝ <) = sup (ran (n \in Z ⟼ - F (n) (x)) ℝ <)) \to (x \in D ⟼ sup (ran (n \in Z ⟼ - F (n) (x)) ℝ <)) = (x \in \{x \in ⋂_{n \in Z} dom F (n) \| \exists z \in ℝ \forall n \in Z - F (n) (x) \leq z\} ⟼ sup (ran (n \in Z ⟼ - F (n) (x)) ℝ <))$
172	167 170 171	syl2anc	$⊢ φ \to (x \in D ⟼ sup (ran (n \in Z ⟼ - F (n) (x)) ℝ <)) = (x \in \{x \in ⋂_{n \in Z} dom F (n) \| \exists z \in ℝ \forall n \in Z - F (n) (x) \leq z\} ⟼ sup (ran (n \in Z ⟼ - F (n) (x)) ℝ <))$
173		nfv	$⊢ Ⅎ z φ$
174	121	renegcld	$⊢ (φ \land n \in Z \land x \in dom F (n)) \to - F (n) (x) \in ℝ$
175		nfv	$⊢ Ⅎ x (φ \land n \in Z)$
176	34	a1i	$⊢ (φ \land n \in Z) \to dom F (n) \in V$
177	121	3expa	$⊢ ((φ \land n \in Z) \land x \in dom F (n)) \to F (n) (x) \in ℝ$
178	14	feqmptd	$⊢ (φ \land n \in Z) \to F (n) = (x \in dom F (n) ⟼ F (n) (x))$
179	178	eqcomd	$⊢ (φ \land n \in Z) \to (x \in dom F (n) ⟼ F (n) (x)) = F (n)$
180	179 12	eqeltrd	$⊢ (φ \land n \in Z) \to (x \in dom F (n) ⟼ F (n) (x)) \in SMblFn (S)$
181	175 11 176 177 180	smfneg	$⊢ (φ \land n \in Z) \to (x \in dom F (n) ⟼ - F (n) (x)) \in SMblFn (S)$
182		eqid	$⊢ \{x \in ⋂_{n \in Z} dom F (n) \| \exists z \in ℝ \forall n \in Z - F (n) (x) \leq z\} = \{x \in ⋂_{n \in Z} dom F (n) \| \exists z \in ℝ \forall n \in Z - F (n) (x) \leq z\}$
183		eqid	$⊢ (x \in \{x \in ⋂_{n \in Z} dom F (n) \| \exists z \in ℝ \forall n \in Z - F (n) (x) \leq z\} ⟼ sup (ran (n \in Z ⟼ - F (n) (x)) ℝ <)) = (x \in \{x \in ⋂_{n \in Z} dom F (n) \| \exists z \in ℝ \forall n \in Z - F (n) (x) \leq z\} ⟼ sup (ran (n \in Z ⟼ - F (n) (x)) ℝ <))$
184	107 32 173 1 2 3 174 181 182 183	smfsupmpt	$⊢ φ \to (x \in \{x \in ⋂_{n \in Z} dom F (n) \| \exists z \in ℝ \forall n \in Z - F (n) (x) \leq z\} ⟼ sup (ran (n \in Z ⟼ - F (n) (x)) ℝ <)) \in SMblFn (S)$
185	172 184	eqeltrd	$⊢ φ \to (x \in D ⟼ sup (ran (n \in Z ⟼ - F (n) (x)) ℝ <)) \in SMblFn (S)$
186	32 3 38 101 185	smfneg	$⊢ φ \to (x \in D ⟼ - sup (ran (n \in Z ⟼ - F (n) (x)) ℝ <)) \in SMblFn (S)$
187	31 186	eqeltrd	$⊢ φ \to G \in SMblFn (S)$

Metamath Proof Explorer

Theorem smfinflem

Proof