Metamath Proof Explorer

Theorem fsupdm2

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 fsupdm2.1 ⊢ Ⅎ n φ
fsupdm2.2 ⊢ Ⅎ x φ
fsupdm2.3 ⊢ Ⅎ m φ
fsupdm2.4 ⊢ Ⅎ _ x F
fsupdm2.5 ⊢ φ ∧ n ∈ Z → F ⁡ n : dom ⁡ F ⁡ n ⟶ ℝ *
fsupdm2.6 ⊢ D = x ∈ ⋂ n ∈ Z dom ⁡ F ⁡ n | ∃ y ∈ ℝ ∀ n ∈ Z F ⁡ n ⁡ x ≤ y
fsupdm2.7 ⊢ G = x ∈ D ⟼ sup ran ⁡ n ∈ Z ⟼ F ⁡ n ⁡ x ℝ <
fsupdm2.8 ⊢ H = n ∈ Z ⟼ m ∈ ℕ ⟼ x ∈ dom ⁡ F ⁡ n | F ⁡ n ⁡ x < m
Assertion fsupdm2 ⊢ φ → dom ⁡ G = ⋃ m ∈ ℕ ⋂ n ∈ Z H ⁡ n ⁡ m

Proof

Step Hyp Ref Expression
1 fsupdm2.1 ⊢ Ⅎ n φ
2 fsupdm2.2 ⊢ Ⅎ x φ
3 fsupdm2.3 ⊢ Ⅎ m φ
4 fsupdm2.4 ⊢ Ⅎ _ x F
5 fsupdm2.5 ⊢ φ ∧ n ∈ Z → F ⁡ n : dom ⁡ F ⁡ n ⟶ ℝ *
6 fsupdm2.6 ⊢ D = x ∈ ⋂ n ∈ Z dom ⁡ F ⁡ n | ∃ y ∈ ℝ ∀ n ∈ Z F ⁡ n ⁡ x ≤ y
7 fsupdm2.7 ⊢ G = x ∈ D ⟼ sup ran ⁡ n ∈ Z ⟼ F ⁡ n ⁡ x ℝ <
8 fsupdm2.8 ⊢ H = n ∈ Z ⟼ m ∈ ℕ ⟼ x ∈ dom ⁡ F ⁡ n | F ⁡ n ⁡ x < m
9 nfrab1 ⊢ Ⅎ _ x x ∈ ⋂ n ∈ Z dom ⁡ F ⁡ n | ∃ y ∈ ℝ ∀ n ∈ Z F ⁡ n ⁡ x ≤ y
10 6 9 nfcxfr ⊢ Ⅎ _ x D
11 ltso ⊢ < Or ℝ
12 11 supex ⊢ sup ran ⁡ n ∈ Z ⟼ F ⁡ n ⁡ x ℝ < ∈ V
13 12 a1i ⊢ φ ∧ x ∈ D → sup ran ⁡ n ∈ Z ⟼ F ⁡ n ⁡ x ℝ < ∈ V
14 2 10 7 13 dmmptdff ⊢ φ → dom ⁡ G = D
15 1 2 3 4 5 6 8 fsupdm ⊢ φ → D = ⋃ m ∈ ℕ ⋂ n ∈ Z H ⁡ n ⁡ m
16 14 15 eqtrd ⊢ φ → dom ⁡ G = ⋃ m ∈ ℕ ⋂ n ∈ Z H ⁡ n ⁡ m