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	⊢ Ⅎ 𝑛 𝜑
	fsupdm2.2	⊢ Ⅎ 𝑥 𝜑
	fsupdm2.3	⊢ Ⅎ 𝑚 𝜑
	fsupdm2.4	⊢ Ⅎ 𝑥 𝐹
	fsupdm2.5	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) : dom ( 𝐹 ‘ 𝑛 ) ⟶ ℝ* )
	fsupdm2.6	⊢ 𝐷 = { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 }
	fsupdm2.7	⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) )
	fsupdm2.8	⊢ 𝐻 = ( 𝑛 ∈ 𝑍 ↦ ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) < 𝑚 } ) )
Assertion	fsupdm2	⊢ ( 𝜑 → dom 𝐺 = ∪ 𝑚 ∈ ℕ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) )

Proof

Step	Hyp	Ref	Expression
1		fsupdm2.1	⊢ Ⅎ 𝑛 𝜑
2		fsupdm2.2	⊢ Ⅎ 𝑥 𝜑
3		fsupdm2.3	⊢ Ⅎ 𝑚 𝜑
4		fsupdm2.4	⊢ Ⅎ 𝑥 𝐹
5		fsupdm2.5	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) : dom ( 𝐹 ‘ 𝑛 ) ⟶ ℝ* )
6		fsupdm2.6	⊢ 𝐷 = { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 }
7		fsupdm2.7	⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) )
8		fsupdm2.8	⊢ 𝐻 = ( 𝑛 ∈ 𝑍 ↦ ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) < 𝑚 } ) )
9		nfrab1	⊢ Ⅎ 𝑥 { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 }
10	6 9	nfcxfr	⊢ Ⅎ 𝑥 𝐷
11		ltso	⊢ < Or ℝ
12	11	supex	⊢ sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ∈ V
13	12	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → sup ( ran ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) ∈ V )
14	2 10 7 13	dmmptdff	⊢ ( 𝜑 → dom 𝐺 = 𝐷 )
15	1 2 3 4 5 6 8	fsupdm	⊢ ( 𝜑 → 𝐷 = ∪ 𝑚 ∈ ℕ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) )
16	14 15	eqtrd	⊢ ( 𝜑 → dom 𝐺 = ∪ 𝑚 ∈ ℕ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) )