Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 finfdm.1 ⊢ Ⅎ 𝑛 𝜑
2 finfdm.2 ⊢ Ⅎ 𝑥 𝜑
3 finfdm.3 ⊢ Ⅎ 𝑚 𝜑
4 finfdm.4 ⊢ Ⅎ 𝑥 𝐹
5 finfdm.5 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) : dom ( 𝐹 ‘ 𝑛 ) ⟶ ℝ* )
6 finfdm.6 ⊢ 𝐷 = { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) }
7 finfdm.7 ⊢ 𝐻 = ( 𝑛 ∈ 𝑍 ↦ ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ - 𝑚 < ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) } ) )
8 nfcv ⊢ Ⅎ 𝑥 ℕ
9 nfcv ⊢ Ⅎ 𝑥 𝑍
10 nfrab1 ⊢ Ⅎ 𝑥 { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ - 𝑚 < ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) }
11 8 10 nfmpt ⊢ Ⅎ 𝑥 ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ - 𝑚 < ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) } )
12 9 11 nfmpt ⊢ Ⅎ 𝑥 ( 𝑛 ∈ 𝑍 ↦ ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ - 𝑚 < ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) } ) )
13 7 12 nfcxfr ⊢ Ⅎ 𝑥 𝐻
14 nfcv ⊢ Ⅎ 𝑥 𝑛
15 13 14 nffv ⊢ Ⅎ 𝑥 ( 𝐻 ‘ 𝑛 )
16 nfcv ⊢ Ⅎ 𝑥 𝑚
17 15 16 nffv ⊢ Ⅎ 𝑥 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 )
18 9 17 nfiin ⊢ Ⅎ 𝑥 ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 )
19 8 18 nfiun ⊢ Ⅎ 𝑥 ∪ 𝑚 ∈ ℕ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 )
20 nfv ⊢ Ⅎ 𝑚 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 )
21 3 20 nfan ⊢ Ⅎ 𝑚 ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) )
22 nfv ⊢ Ⅎ 𝑚 𝑦 ∈ ℝ
23 21 22 nfan ⊢ Ⅎ 𝑚 ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ )
24 nfv ⊢ Ⅎ 𝑚 ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 )
25 23 24 nfan ⊢ Ⅎ 𝑚 ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) )
26 nfii1 ⊢ Ⅎ 𝑛 ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 )
27 26 nfel2 ⊢ Ⅎ 𝑛 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 )
28 1 27 nfan ⊢ Ⅎ 𝑛 ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) )
29 nfv ⊢ Ⅎ 𝑛 𝑦 ∈ ℝ
30 28 29 nfan ⊢ Ⅎ 𝑛 ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ )
31 nfra1 ⊢ Ⅎ 𝑛 ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 )
32 30 31 nfan ⊢ Ⅎ 𝑛 ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) )
33 nfv ⊢ Ⅎ 𝑛 𝑚 ∈ ℕ
34 nfv ⊢ Ⅎ 𝑛 - 𝑦 < 𝑚
35 32 33 34 nf3an ⊢ Ⅎ 𝑛 ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ∧ 𝑚 ∈ ℕ ∧ - 𝑦 < 𝑚 )
36 vex ⊢ 𝑥 ∈ V
37 36 a1i ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ∧ 𝑚 ∈ ℕ ∧ - 𝑦 < 𝑚 ) → 𝑥 ∈ V )
38 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ∧ 𝑛 ∈ 𝑍 ) → 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) )
39 38 3ad2antl1 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ∧ 𝑚 ∈ ℕ ∧ - 𝑦 < 𝑚 ) ∧ 𝑛 ∈ 𝑍 ) → 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) )
40 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ∧ 𝑚 ∈ ℕ ∧ - 𝑦 < 𝑚 ) ∧ 𝑛 ∈ 𝑍 ) → 𝑛 ∈ 𝑍 )
41 eliinid ⊢ ( ( 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∧ 𝑛 ∈ 𝑍 ) → 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) )
42 39 40 41 syl2anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ∧ 𝑚 ∈ ℕ ∧ - 𝑦 < 𝑚 ) ∧ 𝑛 ∈ 𝑍 ) → 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) )
43 simpl2 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ∧ 𝑚 ∈ ℕ ∧ - 𝑦 < 𝑚 ) ∧ 𝑛 ∈ 𝑍 ) → 𝑚 ∈ ℕ )
44 nnre ⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℝ )
45 44 renegcld ⊢ ( 𝑚 ∈ ℕ → - 𝑚 ∈ ℝ )
46 45 rexrd ⊢ ( 𝑚 ∈ ℕ → - 𝑚 ∈ ℝ* )
47 43 46 syl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ∧ 𝑚 ∈ ℕ ∧ - 𝑦 < 𝑚 ) ∧ 𝑛 ∈ 𝑍 ) → - 𝑚 ∈ ℝ* )
48 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ∧ 𝑛 ∈ 𝑍 ) → 𝑦 ∈ ℝ )
49 rexr ⊢ ( 𝑦 ∈ ℝ → 𝑦 ∈ ℝ* )
50 48 49 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ∧ 𝑛 ∈ 𝑍 ) → 𝑦 ∈ ℝ* )
51 50 3ad2antl1 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ∧ 𝑚 ∈ ℕ ∧ - 𝑦 < 𝑚 ) ∧ 𝑛 ∈ 𝑍 ) → 𝑦 ∈ ℝ* )
52 simp-4l ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ∧ 𝑛 ∈ 𝑍 ) → 𝜑 )
53 52 3ad2antl1 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ∧ 𝑚 ∈ ℕ ∧ - 𝑦 < 𝑚 ) ∧ 𝑛 ∈ 𝑍 ) → 𝜑 )
54 5 3adant3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ) → ( 𝐹 ‘ 𝑛 ) : dom ( 𝐹 ‘ 𝑛 ) ⟶ ℝ* )
55 simp3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ) → 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) )
56 54 55 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ* )
57 53 40 42 56 syl3anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ∧ 𝑚 ∈ ℕ ∧ - 𝑦 < 𝑚 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ* )
58 48 3ad2antl1 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ∧ 𝑚 ∈ ℕ ∧ - 𝑦 < 𝑚 ) ∧ 𝑛 ∈ 𝑍 ) → 𝑦 ∈ ℝ )
59 simpl3 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ∧ 𝑚 ∈ ℕ ∧ - 𝑦 < 𝑚 ) ∧ 𝑛 ∈ 𝑍 ) → - 𝑦 < 𝑚 )
60 simp1 ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑚 ∈ ℕ ∧ - 𝑦 < 𝑚 ) → 𝑦 ∈ ℝ )
61 44 3ad2ant2 ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑚 ∈ ℕ ∧ - 𝑦 < 𝑚 ) → 𝑚 ∈ ℝ )
62 simp3 ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑚 ∈ ℕ ∧ - 𝑦 < 𝑚 ) → - 𝑦 < 𝑚 )
63 60 61 62 ltnegcon1d ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑚 ∈ ℕ ∧ - 𝑦 < 𝑚 ) → - 𝑚 < 𝑦 )
64 58 43 59 63 syl3anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ∧ 𝑚 ∈ ℕ ∧ - 𝑦 < 𝑚 ) ∧ 𝑛 ∈ 𝑍 ) → - 𝑚 < 𝑦 )
65 simpl1r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ∧ 𝑚 ∈ ℕ ∧ - 𝑦 < 𝑚 ) ∧ 𝑛 ∈ 𝑍 ) → ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) )
66 rspa ⊢ ( ( ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∧ 𝑛 ∈ 𝑍 ) → 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) )
67 65 40 66 syl2anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ∧ 𝑚 ∈ ℕ ∧ - 𝑦 < 𝑚 ) ∧ 𝑛 ∈ 𝑍 ) → 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) )
68 47 51 57 64 67 xrltletrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ∧ 𝑚 ∈ ℕ ∧ - 𝑦 < 𝑚 ) ∧ 𝑛 ∈ 𝑍 ) → - 𝑚 < ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) )
69 42 68 rabidd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ∧ 𝑚 ∈ ℕ ∧ - 𝑦 < 𝑚 ) ∧ 𝑛 ∈ 𝑍 ) → 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ - 𝑚 < ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) } )
70 id ⊢ ( 𝑛 ∈ 𝑍 → 𝑛 ∈ 𝑍 )
71 nnex ⊢ ℕ ∈ V
72 71 mptex ⊢ ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ - 𝑚 < ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) } ) ∈ V
73 72 a1i ⊢ ( 𝑛 ∈ 𝑍 → ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ - 𝑚 < ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) } ) ∈ V )
74 7 fvmpt2 ⊢ ( ( 𝑛 ∈ 𝑍 ∧ ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ - 𝑚 < ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) } ) ∈ V ) → ( 𝐻 ‘ 𝑛 ) = ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ - 𝑚 < ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) } ) )
75 70 73 74 syl2anc ⊢ ( 𝑛 ∈ 𝑍 → ( 𝐻 ‘ 𝑛 ) = ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ - 𝑚 < ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) } ) )
76 4 14 nffv ⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑛 )
77 76 nfdm ⊢ Ⅎ 𝑥 dom ( 𝐹 ‘ 𝑛 )
78 fvex ⊢ ( 𝐹 ‘ 𝑛 ) ∈ V
79 78 dmex ⊢ dom ( 𝐹 ‘ 𝑛 ) ∈ V
80 77 79 rabexf ⊢ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ - 𝑚 < ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) } ∈ V
81 80 a1i ⊢ ( ( 𝑛 ∈ 𝑍 ∧ 𝑚 ∈ ℕ ) → { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ - 𝑚 < ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) } ∈ V )
82 75 81 fvmpt2d ⊢ ( ( 𝑛 ∈ 𝑍 ∧ 𝑚 ∈ ℕ ) → ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) = { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ - 𝑚 < ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) } )
83 82 eqcomd ⊢ ( ( 𝑛 ∈ 𝑍 ∧ 𝑚 ∈ ℕ ) → { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ - 𝑚 < ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) } = ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) )
84 40 43 83 syl2anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ∧ 𝑚 ∈ ℕ ∧ - 𝑦 < 𝑚 ) ∧ 𝑛 ∈ 𝑍 ) → { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ - 𝑚 < ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) } = ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) )
85 69 84 eleqtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ∧ 𝑚 ∈ ℕ ∧ - 𝑦 < 𝑚 ) ∧ 𝑛 ∈ 𝑍 ) → 𝑥 ∈ ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) )
86 35 37 85 eliind2 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ∧ 𝑚 ∈ ℕ ∧ - 𝑦 < 𝑚 ) → 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) )
87 renegcl ⊢ ( 𝑦 ∈ ℝ → - 𝑦 ∈ ℝ )
88 87 archd ⊢ ( 𝑦 ∈ ℝ → ∃ 𝑚 ∈ ℕ - 𝑦 < 𝑚 )
89 88 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) → ∃ 𝑚 ∈ ℕ - 𝑦 < 𝑚 )
90 25 86 89 reximdd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) → ∃ 𝑚 ∈ ℕ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) )
91 90 rexlimdva2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) → ( ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) → ∃ 𝑚 ∈ ℕ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ) )
92 91 3impia ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) → ∃ 𝑚 ∈ ℕ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) )
93 eliun ⊢ ( 𝑥 ∈ ∪ 𝑚 ∈ ℕ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ↔ ∃ 𝑚 ∈ ℕ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) )
94 92 93 sylibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) → 𝑥 ∈ ∪ 𝑚 ∈ ℕ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) )
95 2 19 94 rabssd ⊢ ( 𝜑 → { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) } ⊆ ∪ 𝑚 ∈ ℕ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) )
96 6 95 eqsstrid ⊢ ( 𝜑 → 𝐷 ⊆ ∪ 𝑚 ∈ ℕ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) )
97 nfcv ⊢ Ⅎ 𝑚 𝐷
98 nfv ⊢ Ⅎ 𝑥 𝑚 ∈ ℕ
99 2 98 nfan ⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑚 ∈ ℕ )
100 nfrab1 ⊢ Ⅎ 𝑥 { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) }
101 6 100 nfcxfr ⊢ Ⅎ 𝑥 𝐷
102 1 33 nfan ⊢ Ⅎ 𝑛 ( 𝜑 ∧ 𝑚 ∈ ℕ )
103 nfii1 ⊢ Ⅎ 𝑛 ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 )
104 103 nfel2 ⊢ Ⅎ 𝑛 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 )
105 102 104 nfan ⊢ Ⅎ 𝑛 ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) )
106 simpr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ) → 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) )
107 eliinid ⊢ ( ( 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ∧ 𝑛 ∈ 𝑍 ) → 𝑥 ∈ ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) )
108 107 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ) ∧ 𝑛 ∈ 𝑍 ) → 𝑥 ∈ ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) )
109 70 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ) ∧ 𝑛 ∈ 𝑍 ) → 𝑛 ∈ 𝑍 )
110 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ) ∧ 𝑛 ∈ 𝑍 ) → 𝑚 ∈ ℕ )
111 109 110 82 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) = { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ - 𝑚 < ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) } )
112 108 111 eleqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ) ∧ 𝑛 ∈ 𝑍 ) → 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ - 𝑚 < ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) } )
113 rabidim1 ⊢ ( 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ - 𝑚 < ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) } → 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) )
114 112 113 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ) ∧ 𝑛 ∈ 𝑍 ) → 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) )
115 105 106 114 eliind2 ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ) → 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) )
116 45 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ) → - 𝑚 ∈ ℝ )
117 breq1 ⊢ ( 𝑦 = - 𝑚 → ( 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ↔ - 𝑚 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) )
118 117 ralbidv ⊢ ( 𝑦 = - 𝑚 → ( ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ↔ ∀ 𝑛 ∈ 𝑍 - 𝑚 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) )
119 118 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ) ∧ 𝑦 = - 𝑚 ) → ( ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ↔ ∀ 𝑛 ∈ 𝑍 - 𝑚 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) )
120 110 46 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ) ∧ 𝑛 ∈ 𝑍 ) → - 𝑚 ∈ ℝ* )
121 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ) ∧ 𝑛 ∈ 𝑍 ) → 𝜑 )
122 121 109 114 56 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ* )
123 rabidim2 ⊢ ( 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ - 𝑚 < ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) } → - 𝑚 < ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) )
124 112 123 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ) ∧ 𝑛 ∈ 𝑍 ) → - 𝑚 < ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) )
125 120 122 124 xrltled ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ) ∧ 𝑛 ∈ 𝑍 ) → - 𝑚 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) )
126 105 125 ralrimia ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ) → ∀ 𝑛 ∈ 𝑍 - 𝑚 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) )
127 116 119 126 rspcedvd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) )
128 115 127 rabidd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ) → 𝑥 ∈ { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 𝑦 ≤ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) } )
129 128 6 eleqtrrdi ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ) → 𝑥 ∈ 𝐷 )
130 99 18 101 129 ssdf2 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ⊆ 𝐷 )
131 3 97 130 iunssdf ⊢ ( 𝜑 → ∪ 𝑚 ∈ ℕ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ⊆ 𝐷 )
132 96 131 eqssd ⊢ ( 𝜑 → 𝐷 = ∪ 𝑚 ∈ ℕ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) )