Metamath Proof Explorer

Theorem fsupdm

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

Proof

Step Hyp Ref Expression
1 fsupdm.1 ⊢ Ⅎ 𝑛 𝜑
2 fsupdm.2 ⊢ Ⅎ 𝑥 𝜑
3 fsupdm.3 ⊢ Ⅎ 𝑚 𝜑
4 fsupdm.4 ⊢ Ⅎ 𝑥 𝐹
5 fsupdm.5 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) : dom ( 𝐹 ‘ 𝑛 ) ⟶ ℝ* )
6 fsupdm.6 ⊢ 𝐷 = { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 }
7 fsupdm.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 nfcri ⊢ Ⅎ 𝑛 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 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 simp-4l ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 ) ∧ 𝑛 ∈ 𝑍 ) → 𝜑 )
44 43 3ad2antl1 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 ) ∧ 𝑚 ∈ ℕ ∧ 𝑦 < 𝑚 ) ∧ 𝑛 ∈ 𝑍 ) → 𝜑 )
45 44 40 5 syl2anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 ) ∧ 𝑚 ∈ ℕ ∧ 𝑦 < 𝑚 ) ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) : dom ( 𝐹 ‘ 𝑛 ) ⟶ ℝ* )
46 45 42 ffvelcdmd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 ) ∧ 𝑚 ∈ ℕ ∧ 𝑦 < 𝑚 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ* )
47 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 ) ∧ 𝑛 ∈ 𝑍 ) → 𝑦 ∈ ℝ )
48 47 rexrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 ) ∧ 𝑛 ∈ 𝑍 ) → 𝑦 ∈ ℝ* )
49 48 3ad2antl1 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 ) ∧ 𝑚 ∈ ℕ ∧ 𝑦 < 𝑚 ) ∧ 𝑛 ∈ 𝑍 ) → 𝑦 ∈ ℝ* )
50 simpl2 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 ) ∧ 𝑚 ∈ ℕ ∧ 𝑦 < 𝑚 ) ∧ 𝑛 ∈ 𝑍 ) → 𝑚 ∈ ℕ )
51 50 nnxrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 ) ∧ 𝑚 ∈ ℕ ∧ 𝑦 < 𝑚 ) ∧ 𝑛 ∈ 𝑍 ) → 𝑚 ∈ ℝ* )
52 simpl1r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 ) ∧ 𝑚 ∈ ℕ ∧ 𝑦 < 𝑚 ) ∧ 𝑛 ∈ 𝑍 ) → ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 )
53 rspa ⊢ ( ( ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 )
54 52 40 53 syl2anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 ) ∧ 𝑚 ∈ ℕ ∧ 𝑦 < 𝑚 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 )
55 simpl3 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 ) ∧ 𝑚 ∈ ℕ ∧ 𝑦 < 𝑚 ) ∧ 𝑛 ∈ 𝑍 ) → 𝑦 < 𝑚 )
56 46 49 51 54 55 xrlelttrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 ) ∧ 𝑚 ∈ ℕ ∧ 𝑦 < 𝑚 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) < 𝑚 )
57 42 56 rabidd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 ) ∧ 𝑚 ∈ ℕ ∧ 𝑦 < 𝑚 ) ∧ 𝑛 ∈ 𝑍 ) → 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) < 𝑚 } )
58 trud ⊢ ( 𝑛 ∈ 𝑍 → ⊤ )
59 id ⊢ ( 𝑛 ∈ 𝑍 → 𝑛 ∈ 𝑍 )
60 nfcv ⊢ Ⅎ 𝑛 𝑍
61 nnex ⊢ ℕ ∈ V
62 61 mptex ⊢ ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) < 𝑚 } ) ∈ V
63 62 a1i ⊢ ( ( ⊤ ∧ 𝑛 ∈ 𝑍 ) → ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) < 𝑚 } ) ∈ V )
64 60 7 63 fvmpt2df ⊢ ( ( ⊤ ∧ 𝑛 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑛 ) = ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) < 𝑚 } ) )
65 58 59 64 syl2anc ⊢ ( 𝑛 ∈ 𝑍 → ( 𝐻 ‘ 𝑛 ) = ( 𝑚 ∈ ℕ ↦ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) < 𝑚 } ) )
66 4 14 nffv ⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑛 )
67 66 nfdm ⊢ Ⅎ 𝑥 dom ( 𝐹 ‘ 𝑛 )
68 fvex ⊢ ( 𝐹 ‘ 𝑛 ) ∈ V
69 68 dmex ⊢ dom ( 𝐹 ‘ 𝑛 ) ∈ V
70 67 69 rabexf ⊢ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) < 𝑚 } ∈ V
71 70 a1i ⊢ ( ( 𝑛 ∈ 𝑍 ∧ 𝑚 ∈ ℕ ) → { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) < 𝑚 } ∈ V )
72 65 71 fvmpt2d ⊢ ( ( 𝑛 ∈ 𝑍 ∧ 𝑚 ∈ ℕ ) → ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) = { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) < 𝑚 } )
73 72 eqcomd ⊢ ( ( 𝑛 ∈ 𝑍 ∧ 𝑚 ∈ ℕ ) → { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) < 𝑚 } = ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) )
74 40 50 73 syl2anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 ) ∧ 𝑚 ∈ ℕ ∧ 𝑦 < 𝑚 ) ∧ 𝑛 ∈ 𝑍 ) → { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) < 𝑚 } = ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) )
75 57 74 eleqtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 ) ∧ 𝑚 ∈ ℕ ∧ 𝑦 < 𝑚 ) ∧ 𝑛 ∈ 𝑍 ) → 𝑥 ∈ ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) )
76 35 37 75 eliind2 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 ) ∧ 𝑚 ∈ ℕ ∧ 𝑦 < 𝑚 ) → 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) )
77 arch ⊢ ( 𝑦 ∈ ℝ → ∃ 𝑚 ∈ ℕ 𝑦 < 𝑚 )
78 77 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 ) → ∃ 𝑚 ∈ ℕ 𝑦 < 𝑚 )
79 25 76 78 reximdd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 ) → ∃ 𝑚 ∈ ℕ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) )
80 79 rexlimdva2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ) → ( ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 → ∃ 𝑚 ∈ ℕ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ) )
81 80 3impia ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 ) → ∃ 𝑚 ∈ ℕ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) )
82 eliun ⊢ ( 𝑥 ∈ ∪ 𝑚 ∈ ℕ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ↔ ∃ 𝑚 ∈ ℕ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) )
83 81 82 sylibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 ) → 𝑥 ∈ ∪ 𝑚 ∈ ℕ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) )
84 2 19 83 rabssd ⊢ ( 𝜑 → { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 } ⊆ ∪ 𝑚 ∈ ℕ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) )
85 6 84 eqsstrid ⊢ ( 𝜑 → 𝐷 ⊆ ∪ 𝑚 ∈ ℕ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) )
86 nfcv ⊢ Ⅎ 𝑚 𝐷
87 nfv ⊢ Ⅎ 𝑥 𝑚 ∈ ℕ
88 2 87 nfan ⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑚 ∈ ℕ )
89 nfrab1 ⊢ Ⅎ 𝑥 { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 }
90 6 89 nfcxfr ⊢ Ⅎ 𝑥 𝐷
91 1 33 nfan ⊢ Ⅎ 𝑛 ( 𝜑 ∧ 𝑚 ∈ ℕ )
92 nfii1 ⊢ Ⅎ 𝑛 ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 )
93 92 nfcri ⊢ Ⅎ 𝑛 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 )
94 91 93 nfan ⊢ Ⅎ 𝑛 ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) )
95 36 a1i ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ) → 𝑥 ∈ V )
96 eliinid ⊢ ( ( 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ∧ 𝑛 ∈ 𝑍 ) → 𝑥 ∈ ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) )
97 96 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ) ∧ 𝑛 ∈ 𝑍 ) → 𝑥 ∈ ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) )
98 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ) ∧ 𝑛 ∈ 𝑍 ) → 𝑛 ∈ 𝑍 )
99 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ) ∧ 𝑛 ∈ 𝑍 ) → 𝑚 ∈ ℕ )
100 98 99 72 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) = { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) < 𝑚 } )
101 97 100 eleqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ) ∧ 𝑛 ∈ 𝑍 ) → 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) < 𝑚 } )
102 rabidim1 ⊢ ( 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) < 𝑚 } → 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) )
103 101 102 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ) ∧ 𝑛 ∈ 𝑍 ) → 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) )
104 94 95 103 eliind2 ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ) → 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) )
105 nnre ⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℝ )
106 105 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ) → 𝑚 ∈ ℝ )
107 breq2 ⊢ ( 𝑦 = 𝑚 → ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 ↔ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑚 ) )
108 107 ralbidv ⊢ ( 𝑦 = 𝑚 → ( ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 ↔ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑚 ) )
109 108 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ) ∧ 𝑦 = 𝑚 ) → ( ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 ↔ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑚 ) )
110 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ) ∧ 𝑛 ∈ 𝑍 ) → 𝜑 )
111 5 3adant3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ) → ( 𝐹 ‘ 𝑛 ) : dom ( 𝐹 ‘ 𝑛 ) ⟶ ℝ* )
112 simp3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ) → 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) )
113 111 112 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ* )
114 110 98 103 113 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℝ* )
115 99 nnxrd ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ) ∧ 𝑛 ∈ 𝑍 ) → 𝑚 ∈ ℝ* )
116 rabidim2 ⊢ ( 𝑥 ∈ { 𝑥 ∈ dom ( 𝐹 ‘ 𝑛 ) ∣ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) < 𝑚 } → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) < 𝑚 )
117 101 116 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) < 𝑚 )
118 114 115 117 xrltled ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑚 )
119 94 118 ralrimia ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ) → ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑚 )
120 106 109 119 rspcedvd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 )
121 104 120 rabidd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ) → 𝑥 ∈ { 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom ( 𝐹 ‘ 𝑛 ) ∣ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 } )
122 121 6 eleqtrrdi ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ) → 𝑥 ∈ 𝐷 )
123 88 18 90 122 ssdf2 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ⊆ 𝐷 )
124 3 86 123 iunssdf ⊢ ( 𝜑 → ∪ 𝑚 ∈ ℕ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) ⊆ 𝐷 )
125 85 124 eqssd ⊢ ( 𝜑 → 𝐷 = ∪ 𝑚 ∈ ℕ ∩ 𝑛 ∈ 𝑍 ( ( 𝐻 ‘ 𝑛 ) ‘ 𝑚 ) )