Metamath Proof Explorer

Theorem hoidmvle

Description: The dimensional volume of a n-dimensional half-open interval is less than or equal the generalized sum of the dimensional volumes of countable half-open intervals that cover it. Lemma 115B of Fremlin1 p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses hoidmvle.l ⊢ L = x ∈ Fin ⟼ a ∈ ℝ x , b ∈ ℝ x ⟼ if x = ∅ 0 ∏ k ∈ x vol ⁡ a ⁡ k b ⁡ k
hoidmvle.x ⊢ φ → X ∈ Fin
hoidmvle.a ⊢ φ → A : X ⟶ ℝ
hoidmvle.b ⊢ φ → B : X ⟶ ℝ
hoidmvle.c ⊢ φ → C : ℕ ⟶ ℝ X
hoidmvle.d ⊢ φ → D : ℕ ⟶ ℝ X
hoidmvle.s ⊢ φ → ⨉ k ∈ X A ⁡ k B ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X C ⁡ j ⁡ k D ⁡ j ⁡ k
Assertion hoidmvle ⊢ φ → A L ⁡ X B ≤ sum^ ⁡ j ∈ ℕ ⟼ C ⁡ j L ⁡ X D ⁡ j

Proof

Step Hyp Ref Expression
1 hoidmvle.l ⊢ L = x ∈ Fin ⟼ a ∈ ℝ x , b ∈ ℝ x ⟼ if x = ∅ 0 ∏ k ∈ x vol ⁡ a ⁡ k b ⁡ k
2 hoidmvle.x ⊢ φ → X ∈ Fin
3 hoidmvle.a ⊢ φ → A : X ⟶ ℝ
4 hoidmvle.b ⊢ φ → B : X ⟶ ℝ
5 hoidmvle.c ⊢ φ → C : ℕ ⟶ ℝ X
6 hoidmvle.d ⊢ φ → D : ℕ ⟶ ℝ X
7 hoidmvle.s ⊢ φ → ⨉ k ∈ X A ⁡ k B ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X C ⁡ j ⁡ k D ⁡ j ⁡ k
8 ovex ⊢ ℝ X ∈ V
9 nnex ⊢ ℕ ∈ V
10 8 9 pm3.2i ⊢ ℝ X ∈ V ∧ ℕ ∈ V
11 10 a1i ⊢ φ → ℝ X ∈ V ∧ ℕ ∈ V
12 elmapg ⊢ ℝ X ∈ V ∧ ℕ ∈ V → D ∈ ℝ X ℕ ↔ D : ℕ ⟶ ℝ X
13 11 12 syl ⊢ φ → D ∈ ℝ X ℕ ↔ D : ℕ ⟶ ℝ X
14 6 13 mpbird ⊢ φ → D ∈ ℝ X ℕ
15 elmapg ⊢ ℝ X ∈ V ∧ ℕ ∈ V → C ∈ ℝ X ℕ ↔ C : ℕ ⟶ ℝ X
16 11 15 syl ⊢ φ → C ∈ ℝ X ℕ ↔ C : ℕ ⟶ ℝ X
17 5 16 mpbird ⊢ φ → C ∈ ℝ X ℕ
18 reex ⊢ ℝ ∈ V
19 18 a1i ⊢ φ → ℝ ∈ V
20 19 2 jca ⊢ φ → ℝ ∈ V ∧ X ∈ Fin
21 elmapg ⊢ ℝ ∈ V ∧ X ∈ Fin → B ∈ ℝ X ↔ B : X ⟶ ℝ
22 20 21 syl ⊢ φ → B ∈ ℝ X ↔ B : X ⟶ ℝ
23 4 22 mpbird ⊢ φ → B ∈ ℝ X
24 elmapg ⊢ ℝ ∈ V ∧ X ∈ Fin → A ∈ ℝ X ↔ A : X ⟶ ℝ
25 20 24 syl ⊢ φ → A ∈ ℝ X ↔ A : X ⟶ ℝ
26 3 25 mpbird ⊢ φ → A ∈ ℝ X
27 oveq2 ⊢ x = ∅ → ℝ x = ℝ ∅
28 27 eleq2d ⊢ x = ∅ → a ∈ ℝ x ↔ a ∈ ℝ ∅
29 27 eleq2d ⊢ x = ∅ → b ∈ ℝ x ↔ b ∈ ℝ ∅
30 27 oveq1d ⊢ x = ∅ → ℝ x ℕ = ℝ ∅ ℕ
31 30 eleq2d ⊢ x = ∅ → c ∈ ℝ x ℕ ↔ c ∈ ℝ ∅ ℕ
32 30 eleq2d ⊢ x = ∅ → d ∈ ℝ x ℕ ↔ d ∈ ℝ ∅ ℕ
33 ixpeq1 ⊢ x = ∅ → ⨉ k ∈ x a ⁡ k b ⁡ k = ⨉ k ∈ ∅ a ⁡ k b ⁡ k
34 ixpeq1 ⊢ x = ∅ → ⨉ k ∈ x c ⁡ j ⁡ k d ⁡ j ⁡ k = ⨉ k ∈ ∅ c ⁡ j ⁡ k d ⁡ j ⁡ k
35 34 iuneq2d ⊢ x = ∅ → ⋃ j ∈ ℕ ⨉ k ∈ x c ⁡ j ⁡ k d ⁡ j ⁡ k = ⋃ j ∈ ℕ ⨉ k ∈ ∅ c ⁡ j ⁡ k d ⁡ j ⁡ k
36 33 35 sseq12d ⊢ x = ∅ → ⨉ k ∈ x a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ x c ⁡ j ⁡ k d ⁡ j ⁡ k ↔ ⨉ k ∈ ∅ a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ ∅ c ⁡ j ⁡ k d ⁡ j ⁡ k
37 fveq2 ⊢ x = ∅ → L ⁡ x = L ⁡ ∅
38 37 oveqd ⊢ x = ∅ → a L ⁡ x b = a L ⁡ ∅ b
39 37 oveqd ⊢ x = ∅ → c ⁡ j L ⁡ x d ⁡ j = c ⁡ j L ⁡ ∅ d ⁡ j
40 39 mpteq2dv ⊢ x = ∅ → j ∈ ℕ ⟼ c ⁡ j L ⁡ x d ⁡ j = j ∈ ℕ ⟼ c ⁡ j L ⁡ ∅ d ⁡ j
41 40 fveq2d ⊢ x = ∅ → sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ x d ⁡ j = sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ ∅ d ⁡ j
42 38 41 breq12d ⊢ x = ∅ → a L ⁡ x b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ x d ⁡ j ↔ a L ⁡ ∅ b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ ∅ d ⁡ j
43 36 42 imbi12d ⊢ x = ∅ → ⨉ k ∈ x a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ x c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ x b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ x d ⁡ j ↔ ⨉ k ∈ ∅ a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ ∅ c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ ∅ b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ ∅ d ⁡ j
44 32 43 imbi12d ⊢ x = ∅ → d ∈ ℝ x ℕ → ⨉ k ∈ x a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ x c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ x b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ x d ⁡ j ↔ d ∈ ℝ ∅ ℕ → ⨉ k ∈ ∅ a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ ∅ c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ ∅ b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ ∅ d ⁡ j
45 44 ralbidv2 ⊢ x = ∅ → ∀ d ∈ ℝ x ℕ ⨉ k ∈ x a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ x c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ x b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ x d ⁡ j ↔ ∀ d ∈ ℝ ∅ ℕ ⨉ k ∈ ∅ a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ ∅ c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ ∅ b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ ∅ d ⁡ j
46 31 45 imbi12d ⊢ x = ∅ → c ∈ ℝ x ℕ → ∀ d ∈ ℝ x ℕ ⨉ k ∈ x a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ x c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ x b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ x d ⁡ j ↔ c ∈ ℝ ∅ ℕ → ∀ d ∈ ℝ ∅ ℕ ⨉ k ∈ ∅ a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ ∅ c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ ∅ b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ ∅ d ⁡ j
47 46 ralbidv2 ⊢ x = ∅ → ∀ c ∈ ℝ x ℕ ∀ d ∈ ℝ x ℕ ⨉ k ∈ x a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ x c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ x b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ x d ⁡ j ↔ ∀ c ∈ ℝ ∅ ℕ ∀ d ∈ ℝ ∅ ℕ ⨉ k ∈ ∅ a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ ∅ c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ ∅ b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ ∅ d ⁡ j
48 29 47 imbi12d ⊢ x = ∅ → b ∈ ℝ x → ∀ c ∈ ℝ x ℕ ∀ d ∈ ℝ x ℕ ⨉ k ∈ x a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ x c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ x b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ x d ⁡ j ↔ b ∈ ℝ ∅ → ∀ c ∈ ℝ ∅ ℕ ∀ d ∈ ℝ ∅ ℕ ⨉ k ∈ ∅ a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ ∅ c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ ∅ b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ ∅ d ⁡ j
49 48 ralbidv2 ⊢ x = ∅ → ∀ b ∈ ℝ x ∀ c ∈ ℝ x ℕ ∀ d ∈ ℝ x ℕ ⨉ k ∈ x a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ x c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ x b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ x d ⁡ j ↔ ∀ b ∈ ℝ ∅ ∀ c ∈ ℝ ∅ ℕ ∀ d ∈ ℝ ∅ ℕ ⨉ k ∈ ∅ a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ ∅ c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ ∅ b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ ∅ d ⁡ j
50 28 49 imbi12d ⊢ x = ∅ → a ∈ ℝ x → ∀ b ∈ ℝ x ∀ c ∈ ℝ x ℕ ∀ d ∈ ℝ x ℕ ⨉ k ∈ x a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ x c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ x b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ x d ⁡ j ↔ a ∈ ℝ ∅ → ∀ b ∈ ℝ ∅ ∀ c ∈ ℝ ∅ ℕ ∀ d ∈ ℝ ∅ ℕ ⨉ k ∈ ∅ a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ ∅ c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ ∅ b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ ∅ d ⁡ j
51 50 ralbidv2 ⊢ x = ∅ → ∀ a ∈ ℝ x ∀ b ∈ ℝ x ∀ c ∈ ℝ x ℕ ∀ d ∈ ℝ x ℕ ⨉ k ∈ x a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ x c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ x b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ x d ⁡ j ↔ ∀ a ∈ ℝ ∅ ∀ b ∈ ℝ ∅ ∀ c ∈ ℝ ∅ ℕ ∀ d ∈ ℝ ∅ ℕ ⨉ k ∈ ∅ a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ ∅ c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ ∅ b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ ∅ d ⁡ j
52 oveq2 ⊢ x = y → ℝ x = ℝ y
53 52 eleq2d ⊢ x = y → a ∈ ℝ x ↔ a ∈ ℝ y
54 52 eleq2d ⊢ x = y → b ∈ ℝ x ↔ b ∈ ℝ y
55 52 oveq1d ⊢ x = y → ℝ x ℕ = ℝ y ℕ
56 55 eleq2d ⊢ x = y → c ∈ ℝ x ℕ ↔ c ∈ ℝ y ℕ
57 55 eleq2d ⊢ x = y → d ∈ ℝ x ℕ ↔ d ∈ ℝ y ℕ
58 ixpeq1 ⊢ x = y → ⨉ k ∈ x a ⁡ k b ⁡ k = ⨉ k ∈ y a ⁡ k b ⁡ k
59 ixpeq1 ⊢ x = y → ⨉ k ∈ x c ⁡ j ⁡ k d ⁡ j ⁡ k = ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k
60 59 iuneq2d ⊢ x = y → ⋃ j ∈ ℕ ⨉ k ∈ x c ⁡ j ⁡ k d ⁡ j ⁡ k = ⋃ j ∈ ℕ ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k
61 58 60 sseq12d ⊢ x = y → ⨉ k ∈ x a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ x c ⁡ j ⁡ k d ⁡ j ⁡ k ↔ ⨉ k ∈ y a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k
62 fveq2 ⊢ x = y → L ⁡ x = L ⁡ y
63 62 oveqd ⊢ x = y → a L ⁡ x b = a L ⁡ y b
64 62 oveqd ⊢ x = y → c ⁡ j L ⁡ x d ⁡ j = c ⁡ j L ⁡ y d ⁡ j
65 64 mpteq2dv ⊢ x = y → j ∈ ℕ ⟼ c ⁡ j L ⁡ x d ⁡ j = j ∈ ℕ ⟼ c ⁡ j L ⁡ y d ⁡ j
66 65 fveq2d ⊢ x = y → sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ x d ⁡ j = sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y d ⁡ j
67 63 66 breq12d ⊢ x = y → a L ⁡ x b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ x d ⁡ j ↔ a L ⁡ y b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y d ⁡ j
68 61 67 imbi12d ⊢ x = y → ⨉ k ∈ x a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ x c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ x b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ x d ⁡ j ↔ ⨉ k ∈ y a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ y b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y d ⁡ j
69 57 68 imbi12d ⊢ x = y → d ∈ ℝ x ℕ → ⨉ k ∈ x a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ x c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ x b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ x d ⁡ j ↔ d ∈ ℝ y ℕ → ⨉ k ∈ y a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ y b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y d ⁡ j
70 69 ralbidv2 ⊢ x = y → ∀ d ∈ ℝ x ℕ ⨉ k ∈ x a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ x c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ x b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ x d ⁡ j ↔ ∀ d ∈ ℝ y ℕ ⨉ k ∈ y a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ y b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y d ⁡ j
71 56 70 imbi12d ⊢ x = y → c ∈ ℝ x ℕ → ∀ d ∈ ℝ x ℕ ⨉ k ∈ x a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ x c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ x b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ x d ⁡ j ↔ c ∈ ℝ y ℕ → ∀ d ∈ ℝ y ℕ ⨉ k ∈ y a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ y b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y d ⁡ j
72 71 ralbidv2 ⊢ x = y → ∀ c ∈ ℝ x ℕ ∀ d ∈ ℝ x ℕ ⨉ k ∈ x a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ x c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ x b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ x d ⁡ j ↔ ∀ c ∈ ℝ y ℕ ∀ d ∈ ℝ y ℕ ⨉ k ∈ y a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ y b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y d ⁡ j
73 54 72 imbi12d ⊢ x = y → b ∈ ℝ x → ∀ c ∈ ℝ x ℕ ∀ d ∈ ℝ x ℕ ⨉ k ∈ x a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ x c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ x b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ x d ⁡ j ↔ b ∈ ℝ y → ∀ c ∈ ℝ y ℕ ∀ d ∈ ℝ y ℕ ⨉ k ∈ y a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ y b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y d ⁡ j
74 73 ralbidv2 ⊢ x = y → ∀ b ∈ ℝ x ∀ c ∈ ℝ x ℕ ∀ d ∈ ℝ x ℕ ⨉ k ∈ x a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ x c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ x b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ x d ⁡ j ↔ ∀ b ∈ ℝ y ∀ c ∈ ℝ y ℕ ∀ d ∈ ℝ y ℕ ⨉ k ∈ y a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ y b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y d ⁡ j
75 53 74 imbi12d ⊢ x = y → a ∈ ℝ x → ∀ b ∈ ℝ x ∀ c ∈ ℝ x ℕ ∀ d ∈ ℝ x ℕ ⨉ k ∈ x a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ x c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ x b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ x d ⁡ j ↔ a ∈ ℝ y → ∀ b ∈ ℝ y ∀ c ∈ ℝ y ℕ ∀ d ∈ ℝ y ℕ ⨉ k ∈ y a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ y b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y d ⁡ j
76 75 ralbidv2 ⊢ x = y → ∀ a ∈ ℝ x ∀ b ∈ ℝ x ∀ c ∈ ℝ x ℕ ∀ d ∈ ℝ x ℕ ⨉ k ∈ x a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ x c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ x b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ x d ⁡ j ↔ ∀ a ∈ ℝ y ∀ b ∈ ℝ y ∀ c ∈ ℝ y ℕ ∀ d ∈ ℝ y ℕ ⨉ k ∈ y a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ y b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y d ⁡ j
77 oveq2 ⊢ x = y ∪ z → ℝ x = ℝ y ∪ z
78 77 eleq2d ⊢ x = y ∪ z → a ∈ ℝ x ↔ a ∈ ℝ y ∪ z
79 77 eleq2d ⊢ x = y ∪ z → b ∈ ℝ x ↔ b ∈ ℝ y ∪ z
80 77 oveq1d ⊢ x = y ∪ z → ℝ x ℕ = ℝ y ∪ z ℕ
81 80 eleq2d ⊢ x = y ∪ z → c ∈ ℝ x ℕ ↔ c ∈ ℝ y ∪ z ℕ
82 80 eleq2d ⊢ x = y ∪ z → d ∈ ℝ x ℕ ↔ d ∈ ℝ y ∪ z ℕ
83 ixpeq1 ⊢ x = y ∪ z → ⨉ k ∈ x a ⁡ k b ⁡ k = ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k
84 ixpeq1 ⊢ x = y ∪ z → ⨉ k ∈ x c ⁡ j ⁡ k d ⁡ j ⁡ k = ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k
85 84 iuneq2d ⊢ x = y ∪ z → ⋃ j ∈ ℕ ⨉ k ∈ x c ⁡ j ⁡ k d ⁡ j ⁡ k = ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k
86 83 85 sseq12d ⊢ x = y ∪ z → ⨉ k ∈ x a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ x c ⁡ j ⁡ k d ⁡ j ⁡ k ↔ ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k
87 fveq2 ⊢ x = y ∪ z → L ⁡ x = L ⁡ y ∪ z
88 87 oveqd ⊢ x = y ∪ z → a L ⁡ x b = a L ⁡ y ∪ z b
89 87 oveqd ⊢ x = y ∪ z → c ⁡ j L ⁡ x d ⁡ j = c ⁡ j L ⁡ y ∪ z d ⁡ j
90 89 mpteq2dv ⊢ x = y ∪ z → j ∈ ℕ ⟼ c ⁡ j L ⁡ x d ⁡ j = j ∈ ℕ ⟼ c ⁡ j L ⁡ y ∪ z d ⁡ j
91 90 fveq2d ⊢ x = y ∪ z → sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ x d ⁡ j = sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y ∪ z d ⁡ j
92 88 91 breq12d ⊢ x = y ∪ z → a L ⁡ x b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ x d ⁡ j ↔ a L ⁡ y ∪ z b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y ∪ z d ⁡ j
93 86 92 imbi12d ⊢ x = y ∪ z → ⨉ k ∈ x a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ x c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ x b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ x d ⁡ j ↔ ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ y ∪ z b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y ∪ z d ⁡ j
94 82 93 imbi12d ⊢ x = y ∪ z → d ∈ ℝ x ℕ → ⨉ k ∈ x a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ x c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ x b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ x d ⁡ j ↔ d ∈ ℝ y ∪ z ℕ → ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ y ∪ z b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y ∪ z d ⁡ j
95 94 ralbidv2 ⊢ x = y ∪ z → ∀ d ∈ ℝ x ℕ ⨉ k ∈ x a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ x c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ x b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ x d ⁡ j ↔ ∀ d ∈ ℝ y ∪ z ℕ ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ y ∪ z b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y ∪ z d ⁡ j
96 81 95 imbi12d ⊢ x = y ∪ z → c ∈ ℝ x ℕ → ∀ d ∈ ℝ x ℕ ⨉ k ∈ x a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ x c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ x b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ x d ⁡ j ↔ c ∈ ℝ y ∪ z ℕ → ∀ d ∈ ℝ y ∪ z ℕ ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ y ∪ z b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y ∪ z d ⁡ j
97 96 ralbidv2 ⊢ x = y ∪ z → ∀ c ∈ ℝ x ℕ ∀ d ∈ ℝ x ℕ ⨉ k ∈ x a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ x c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ x b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ x d ⁡ j ↔ ∀ c ∈ ℝ y ∪ z ℕ ∀ d ∈ ℝ y ∪ z ℕ ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ y ∪ z b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y ∪ z d ⁡ j
98 79 97 imbi12d ⊢ x = y ∪ z → b ∈ ℝ x → ∀ c ∈ ℝ x ℕ ∀ d ∈ ℝ x ℕ ⨉ k ∈ x a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ x c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ x b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ x d ⁡ j ↔ b ∈ ℝ y ∪ z → ∀ c ∈ ℝ y ∪ z ℕ ∀ d ∈ ℝ y ∪ z ℕ ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ y ∪ z b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y ∪ z d ⁡ j
99 98 ralbidv2 ⊢ x = y ∪ z → ∀ b ∈ ℝ x ∀ c ∈ ℝ x ℕ ∀ d ∈ ℝ x ℕ ⨉ k ∈ x a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ x c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ x b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ x d ⁡ j ↔ ∀ b ∈ ℝ y ∪ z ∀ c ∈ ℝ y ∪ z ℕ ∀ d ∈ ℝ y ∪ z ℕ ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ y ∪ z b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y ∪ z d ⁡ j
100 78 99 imbi12d ⊢ x = y ∪ z → a ∈ ℝ x → ∀ b ∈ ℝ x ∀ c ∈ ℝ x ℕ ∀ d ∈ ℝ x ℕ ⨉ k ∈ x a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ x c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ x b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ x d ⁡ j ↔ a ∈ ℝ y ∪ z → ∀ b ∈ ℝ y ∪ z ∀ c ∈ ℝ y ∪ z ℕ ∀ d ∈ ℝ y ∪ z ℕ ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ y ∪ z b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y ∪ z d ⁡ j
101 100 ralbidv2 ⊢ x = y ∪ z → ∀ a ∈ ℝ x ∀ b ∈ ℝ x ∀ c ∈ ℝ x ℕ ∀ d ∈ ℝ x ℕ ⨉ k ∈ x a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ x c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ x b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ x d ⁡ j ↔ ∀ a ∈ ℝ y ∪ z ∀ b ∈ ℝ y ∪ z ∀ c ∈ ℝ y ∪ z ℕ ∀ d ∈ ℝ y ∪ z ℕ ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ y ∪ z b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y ∪ z d ⁡ j
102 oveq2 ⊢ x = X → ℝ x = ℝ X
103 102 eleq2d ⊢ x = X → a ∈ ℝ x ↔ a ∈ ℝ X
104 102 eleq2d ⊢ x = X → b ∈ ℝ x ↔ b ∈ ℝ X
105 102 oveq1d ⊢ x = X → ℝ x ℕ = ℝ X ℕ
106 105 eleq2d ⊢ x = X → c ∈ ℝ x ℕ ↔ c ∈ ℝ X ℕ
107 105 eleq2d ⊢ x = X → d ∈ ℝ x ℕ ↔ d ∈ ℝ X ℕ
108 ixpeq1 ⊢ x = X → ⨉ k ∈ x a ⁡ k b ⁡ k = ⨉ k ∈ X a ⁡ k b ⁡ k
109 ixpeq1 ⊢ x = X → ⨉ k ∈ x c ⁡ j ⁡ k d ⁡ j ⁡ k = ⨉ k ∈ X c ⁡ j ⁡ k d ⁡ j ⁡ k
110 109 iuneq2d ⊢ x = X → ⋃ j ∈ ℕ ⨉ k ∈ x c ⁡ j ⁡ k d ⁡ j ⁡ k = ⋃ j ∈ ℕ ⨉ k ∈ X c ⁡ j ⁡ k d ⁡ j ⁡ k
111 108 110 sseq12d ⊢ x = X → ⨉ k ∈ x a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ x c ⁡ j ⁡ k d ⁡ j ⁡ k ↔ ⨉ k ∈ X a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X c ⁡ j ⁡ k d ⁡ j ⁡ k
112 fveq2 ⊢ x = X → L ⁡ x = L ⁡ X
113 112 oveqd ⊢ x = X → a L ⁡ x b = a L ⁡ X b
114 112 oveqd ⊢ x = X → c ⁡ j L ⁡ x d ⁡ j = c ⁡ j L ⁡ X d ⁡ j
115 114 mpteq2dv ⊢ x = X → j ∈ ℕ ⟼ c ⁡ j L ⁡ x d ⁡ j = j ∈ ℕ ⟼ c ⁡ j L ⁡ X d ⁡ j
116 115 fveq2d ⊢ x = X → sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ x d ⁡ j = sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ X d ⁡ j
117 113 116 breq12d ⊢ x = X → a L ⁡ x b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ x d ⁡ j ↔ a L ⁡ X b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ X d ⁡ j
118 111 117 imbi12d ⊢ x = X → ⨉ k ∈ x a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ x c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ x b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ x d ⁡ j ↔ ⨉ k ∈ X a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ X b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ X d ⁡ j
119 107 118 imbi12d ⊢ x = X → d ∈ ℝ x ℕ → ⨉ k ∈ x a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ x c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ x b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ x d ⁡ j ↔ d ∈ ℝ X ℕ → ⨉ k ∈ X a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ X b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ X d ⁡ j
120 119 ralbidv2 ⊢ x = X → ∀ d ∈ ℝ x ℕ ⨉ k ∈ x a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ x c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ x b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ x d ⁡ j ↔ ∀ d ∈ ℝ X ℕ ⨉ k ∈ X a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ X b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ X d ⁡ j
121 106 120 imbi12d ⊢ x = X → c ∈ ℝ x ℕ → ∀ d ∈ ℝ x ℕ ⨉ k ∈ x a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ x c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ x b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ x d ⁡ j ↔ c ∈ ℝ X ℕ → ∀ d ∈ ℝ X ℕ ⨉ k ∈ X a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ X b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ X d ⁡ j
122 121 ralbidv2 ⊢ x = X → ∀ c ∈ ℝ x ℕ ∀ d ∈ ℝ x ℕ ⨉ k ∈ x a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ x c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ x b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ x d ⁡ j ↔ ∀ c ∈ ℝ X ℕ ∀ d ∈ ℝ X ℕ ⨉ k ∈ X a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ X b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ X d ⁡ j
123 104 122 imbi12d ⊢ x = X → b ∈ ℝ x → ∀ c ∈ ℝ x ℕ ∀ d ∈ ℝ x ℕ ⨉ k ∈ x a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ x c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ x b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ x d ⁡ j ↔ b ∈ ℝ X → ∀ c ∈ ℝ X ℕ ∀ d ∈ ℝ X ℕ ⨉ k ∈ X a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ X b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ X d ⁡ j
124 123 ralbidv2 ⊢ x = X → ∀ b ∈ ℝ x ∀ c ∈ ℝ x ℕ ∀ d ∈ ℝ x ℕ ⨉ k ∈ x a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ x c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ x b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ x d ⁡ j ↔ ∀ b ∈ ℝ X ∀ c ∈ ℝ X ℕ ∀ d ∈ ℝ X ℕ ⨉ k ∈ X a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ X b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ X d ⁡ j
125 103 124 imbi12d ⊢ x = X → a ∈ ℝ x → ∀ b ∈ ℝ x ∀ c ∈ ℝ x ℕ ∀ d ∈ ℝ x ℕ ⨉ k ∈ x a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ x c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ x b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ x d ⁡ j ↔ a ∈ ℝ X → ∀ b ∈ ℝ X ∀ c ∈ ℝ X ℕ ∀ d ∈ ℝ X ℕ ⨉ k ∈ X a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ X b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ X d ⁡ j
126 125 ralbidv2 ⊢ x = X → ∀ a ∈ ℝ x ∀ b ∈ ℝ x ∀ c ∈ ℝ x ℕ ∀ d ∈ ℝ x ℕ ⨉ k ∈ x a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ x c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ x b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ x d ⁡ j ↔ ∀ a ∈ ℝ X ∀ b ∈ ℝ X ∀ c ∈ ℝ X ℕ ∀ d ∈ ℝ X ℕ ⨉ k ∈ X a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ X b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ X d ⁡ j
127 fveq1 ⊢ a = e → a ⁡ k = e ⁡ k
128 127 oveq1d ⊢ a = e → a ⁡ k b ⁡ k = e ⁡ k b ⁡ k
129 128 fveq2d ⊢ a = e → vol ⁡ a ⁡ k b ⁡ k = vol ⁡ e ⁡ k b ⁡ k
130 129 prodeq2ad ⊢ a = e → ∏ k ∈ x vol ⁡ a ⁡ k b ⁡ k = ∏ k ∈ x vol ⁡ e ⁡ k b ⁡ k
131 130 ifeq2d ⊢ a = e → if x = ∅ 0 ∏ k ∈ x vol ⁡ a ⁡ k b ⁡ k = if x = ∅ 0 ∏ k ∈ x vol ⁡ e ⁡ k b ⁡ k
132 fveq1 ⊢ b = f → b ⁡ k = f ⁡ k
133 132 oveq2d ⊢ b = f → e ⁡ k b ⁡ k = e ⁡ k f ⁡ k
134 133 fveq2d ⊢ b = f → vol ⁡ e ⁡ k b ⁡ k = vol ⁡ e ⁡ k f ⁡ k
135 134 prodeq2ad ⊢ b = f → ∏ k ∈ x vol ⁡ e ⁡ k b ⁡ k = ∏ k ∈ x vol ⁡ e ⁡ k f ⁡ k
136 135 ifeq2d ⊢ b = f → if x = ∅ 0 ∏ k ∈ x vol ⁡ e ⁡ k b ⁡ k = if x = ∅ 0 ∏ k ∈ x vol ⁡ e ⁡ k f ⁡ k
137 131 136 cbvmpov ⊢ a ∈ ℝ x , b ∈ ℝ x ⟼ if x = ∅ 0 ∏ k ∈ x vol ⁡ a ⁡ k b ⁡ k = e ∈ ℝ x , f ∈ ℝ x ⟼ if x = ∅ 0 ∏ k ∈ x vol ⁡ e ⁡ k f ⁡ k
138 137 mpteq2i ⊢ x ∈ Fin ⟼ a ∈ ℝ x , b ∈ ℝ x ⟼ if x = ∅ 0 ∏ k ∈ x vol ⁡ a ⁡ k b ⁡ k = x ∈ Fin ⟼ e ∈ ℝ x , f ∈ ℝ x ⟼ if x = ∅ 0 ∏ k ∈ x vol ⁡ e ⁡ k f ⁡ k
139 1 138 eqtri ⊢ L = x ∈ Fin ⟼ e ∈ ℝ x , f ∈ ℝ x ⟼ if x = ∅ 0 ∏ k ∈ x vol ⁡ e ⁡ k f ⁡ k
140 elmapi ⊢ a ∈ ℝ ∅ → a : ∅ ⟶ ℝ
141 140 adantr ⊢ a ∈ ℝ ∅ ∧ b ∈ ℝ ∅ → a : ∅ ⟶ ℝ
142 elmapi ⊢ b ∈ ℝ ∅ → b : ∅ ⟶ ℝ
143 142 adantl ⊢ a ∈ ℝ ∅ ∧ b ∈ ℝ ∅ → b : ∅ ⟶ ℝ
144 139 141 143 hoidmv0val ⊢ a ∈ ℝ ∅ ∧ b ∈ ℝ ∅ → a L ⁡ ∅ b = 0
145 144 ad5ant23 ⊢ φ ∧ a ∈ ℝ ∅ ∧ b ∈ ℝ ∅ ∧ c ∈ ℝ ∅ ℕ ∧ d ∈ ℝ ∅ ℕ → a L ⁡ ∅ b = 0
146 nfv ⊢ Ⅎ j c ∈ ℝ ∅ ℕ ∧ d ∈ ℝ ∅ ℕ
147 9 a1i ⊢ c ∈ ℝ ∅ ℕ ∧ d ∈ ℝ ∅ ℕ → ℕ ∈ V
148 icossicc ⊢ 0 +∞ ⊆ 0 +∞
149 0fin ⊢ ∅ ∈ Fin
150 149 a1i ⊢ c ∈ ℝ ∅ ℕ ∧ d ∈ ℝ ∅ ℕ ∧ j ∈ ℕ → ∅ ∈ Fin
151 ovexd ⊢ c ∈ ℝ ∅ ℕ ∧ j ∈ ℕ → ℝ ∅ ∈ V
152 9 a1i ⊢ c ∈ ℝ ∅ ℕ ∧ j ∈ ℕ → ℕ ∈ V
153 simpl ⊢ c ∈ ℝ ∅ ℕ ∧ j ∈ ℕ → c ∈ ℝ ∅ ℕ
154 simpr ⊢ c ∈ ℝ ∅ ℕ ∧ j ∈ ℕ → j ∈ ℕ
155 151 152 153 154 fvmap ⊢ c ∈ ℝ ∅ ℕ ∧ j ∈ ℕ → c ⁡ j ∈ ℝ ∅
156 elmapi ⊢ c ⁡ j ∈ ℝ ∅ → c ⁡ j : ∅ ⟶ ℝ
157 155 156 syl ⊢ c ∈ ℝ ∅ ℕ ∧ j ∈ ℕ → c ⁡ j : ∅ ⟶ ℝ
158 157 adantlr ⊢ c ∈ ℝ ∅ ℕ ∧ d ∈ ℝ ∅ ℕ ∧ j ∈ ℕ → c ⁡ j : ∅ ⟶ ℝ
159 ovexd ⊢ d ∈ ℝ ∅ ℕ ∧ j ∈ ℕ → ℝ ∅ ∈ V
160 9 a1i ⊢ d ∈ ℝ ∅ ℕ ∧ j ∈ ℕ → ℕ ∈ V
161 simpl ⊢ d ∈ ℝ ∅ ℕ ∧ j ∈ ℕ → d ∈ ℝ ∅ ℕ
162 simpr ⊢ d ∈ ℝ ∅ ℕ ∧ j ∈ ℕ → j ∈ ℕ
163 159 160 161 162 fvmap ⊢ d ∈ ℝ ∅ ℕ ∧ j ∈ ℕ → d ⁡ j ∈ ℝ ∅
164 elmapi ⊢ d ⁡ j ∈ ℝ ∅ → d ⁡ j : ∅ ⟶ ℝ
165 163 164 syl ⊢ d ∈ ℝ ∅ ℕ ∧ j ∈ ℕ → d ⁡ j : ∅ ⟶ ℝ
166 165 adantll ⊢ c ∈ ℝ ∅ ℕ ∧ d ∈ ℝ ∅ ℕ ∧ j ∈ ℕ → d ⁡ j : ∅ ⟶ ℝ
167 1 150 158 166 hoidmvcl ⊢ c ∈ ℝ ∅ ℕ ∧ d ∈ ℝ ∅ ℕ ∧ j ∈ ℕ → c ⁡ j L ⁡ ∅ d ⁡ j ∈ 0 +∞
168 148 167 sseldi ⊢ c ∈ ℝ ∅ ℕ ∧ d ∈ ℝ ∅ ℕ ∧ j ∈ ℕ → c ⁡ j L ⁡ ∅ d ⁡ j ∈ 0 +∞
169 146 147 168 sge0ge0mpt ⊢ c ∈ ℝ ∅ ℕ ∧ d ∈ ℝ ∅ ℕ → 0 ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ ∅ d ⁡ j
170 169 adantll ⊢ φ ∧ a ∈ ℝ ∅ ∧ b ∈ ℝ ∅ ∧ c ∈ ℝ ∅ ℕ ∧ d ∈ ℝ ∅ ℕ → 0 ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ ∅ d ⁡ j
171 145 170 eqbrtrd ⊢ φ ∧ a ∈ ℝ ∅ ∧ b ∈ ℝ ∅ ∧ c ∈ ℝ ∅ ℕ ∧ d ∈ ℝ ∅ ℕ → a L ⁡ ∅ b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ ∅ d ⁡ j
172 171 a1d ⊢ φ ∧ a ∈ ℝ ∅ ∧ b ∈ ℝ ∅ ∧ c ∈ ℝ ∅ ℕ ∧ d ∈ ℝ ∅ ℕ → ⨉ k ∈ ∅ a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ ∅ c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ ∅ b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ ∅ d ⁡ j
173 172 ralrimiva ⊢ φ ∧ a ∈ ℝ ∅ ∧ b ∈ ℝ ∅ ∧ c ∈ ℝ ∅ ℕ → ∀ d ∈ ℝ ∅ ℕ ⨉ k ∈ ∅ a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ ∅ c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ ∅ b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ ∅ d ⁡ j
174 173 ralrimiva ⊢ φ ∧ a ∈ ℝ ∅ ∧ b ∈ ℝ ∅ → ∀ c ∈ ℝ ∅ ℕ ∀ d ∈ ℝ ∅ ℕ ⨉ k ∈ ∅ a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ ∅ c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ ∅ b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ ∅ d ⁡ j
175 174 ralrimiva ⊢ φ ∧ a ∈ ℝ ∅ → ∀ b ∈ ℝ ∅ ∀ c ∈ ℝ ∅ ℕ ∀ d ∈ ℝ ∅ ℕ ⨉ k ∈ ∅ a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ ∅ c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ ∅ b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ ∅ d ⁡ j
176 175 ralrimiva ⊢ φ → ∀ a ∈ ℝ ∅ ∀ b ∈ ℝ ∅ ∀ c ∈ ℝ ∅ ℕ ∀ d ∈ ℝ ∅ ℕ ⨉ k ∈ ∅ a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ ∅ c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ ∅ b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ ∅ d ⁡ j
177 simpl ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ ∀ a ∈ ℝ y ∀ b ∈ ℝ y ∀ c ∈ ℝ y ℕ ∀ d ∈ ℝ y ℕ ⨉ k ∈ y a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ y b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y d ⁡ j → φ ∧ y ⊆ X ∧ z ∈ X ∖ y
178 128 ixpeq2dv ⊢ a = e → ⨉ k ∈ y a ⁡ k b ⁡ k = ⨉ k ∈ y e ⁡ k b ⁡ k
179 178 sseq1d ⊢ a = e → ⨉ k ∈ y a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k ↔ ⨉ k ∈ y e ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k
180 oveq1 ⊢ a = e → a L ⁡ y b = e L ⁡ y b
181 180 breq1d ⊢ a = e → a L ⁡ y b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y d ⁡ j ↔ e L ⁡ y b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y d ⁡ j
182 179 181 imbi12d ⊢ a = e → ⨉ k ∈ y a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ y b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y d ⁡ j ↔ ⨉ k ∈ y e ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k → e L ⁡ y b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y d ⁡ j
183 182 ralbidv ⊢ a = e → ∀ d ∈ ℝ y ℕ ⨉ k ∈ y a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ y b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y d ⁡ j ↔ ∀ d ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k → e L ⁡ y b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y d ⁡ j
184 183 ralbidv ⊢ a = e → ∀ c ∈ ℝ y ℕ ∀ d ∈ ℝ y ℕ ⨉ k ∈ y a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ y b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y d ⁡ j ↔ ∀ c ∈ ℝ y ℕ ∀ d ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k → e L ⁡ y b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y d ⁡ j
185 184 ralbidv ⊢ a = e → ∀ b ∈ ℝ y ∀ c ∈ ℝ y ℕ ∀ d ∈ ℝ y ℕ ⨉ k ∈ y a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ y b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y d ⁡ j ↔ ∀ b ∈ ℝ y ∀ c ∈ ℝ y ℕ ∀ d ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k → e L ⁡ y b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y d ⁡ j
186 133 ixpeq2dv ⊢ b = f → ⨉ k ∈ y e ⁡ k b ⁡ k = ⨉ k ∈ y e ⁡ k f ⁡ k
187 186 sseq1d ⊢ b = f → ⨉ k ∈ y e ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k ↔ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k
188 oveq2 ⊢ b = f → e L ⁡ y b = e L ⁡ y f
189 188 breq1d ⊢ b = f → e L ⁡ y b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y d ⁡ j ↔ e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y d ⁡ j
190 187 189 imbi12d ⊢ b = f → ⨉ k ∈ y e ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k → e L ⁡ y b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y d ⁡ j ↔ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y d ⁡ j
191 190 ralbidv ⊢ b = f → ∀ d ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k → e L ⁡ y b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y d ⁡ j ↔ ∀ d ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y d ⁡ j
192 191 ralbidv ⊢ b = f → ∀ c ∈ ℝ y ℕ ∀ d ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k → e L ⁡ y b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y d ⁡ j ↔ ∀ c ∈ ℝ y ℕ ∀ d ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y d ⁡ j
193 fveq1 ⊢ c = g → c ⁡ j = g ⁡ j
194 193 fveq1d ⊢ c = g → c ⁡ j ⁡ k = g ⁡ j ⁡ k
195 194 oveq1d ⊢ c = g → c ⁡ j ⁡ k d ⁡ j ⁡ k = g ⁡ j ⁡ k d ⁡ j ⁡ k
196 195 ixpeq2dv ⊢ c = g → ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k = ⨉ k ∈ y g ⁡ j ⁡ k d ⁡ j ⁡ k
197 196 adantr ⊢ c = g ∧ j ∈ ℕ → ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k = ⨉ k ∈ y g ⁡ j ⁡ k d ⁡ j ⁡ k
198 197 iuneq2dv ⊢ c = g → ⋃ j ∈ ℕ ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k = ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k d ⁡ j ⁡ k
199 198 sseq2d ⊢ c = g → ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k ↔ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k d ⁡ j ⁡ k
200 193 oveq1d ⊢ c = g → c ⁡ j L ⁡ y d ⁡ j = g ⁡ j L ⁡ y d ⁡ j
201 200 mpteq2dv ⊢ c = g → j ∈ ℕ ⟼ c ⁡ j L ⁡ y d ⁡ j = j ∈ ℕ ⟼ g ⁡ j L ⁡ y d ⁡ j
202 201 fveq2d ⊢ c = g → sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y d ⁡ j = sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y d ⁡ j
203 202 breq2d ⊢ c = g → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y d ⁡ j ↔ e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y d ⁡ j
204 199 203 imbi12d ⊢ c = g → ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y d ⁡ j ↔ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k d ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y d ⁡ j
205 204 ralbidv ⊢ c = g → ∀ d ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y d ⁡ j ↔ ∀ d ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k d ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y d ⁡ j
206 fveq1 ⊢ d = h → d ⁡ j = h ⁡ j
207 206 fveq1d ⊢ d = h → d ⁡ j ⁡ k = h ⁡ j ⁡ k
208 207 oveq2d ⊢ d = h → g ⁡ j ⁡ k d ⁡ j ⁡ k = g ⁡ j ⁡ k h ⁡ j ⁡ k
209 208 ixpeq2dv ⊢ d = h → ⨉ k ∈ y g ⁡ j ⁡ k d ⁡ j ⁡ k = ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k
210 209 adantr ⊢ d = h ∧ j ∈ ℕ → ⨉ k ∈ y g ⁡ j ⁡ k d ⁡ j ⁡ k = ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k
211 210 iuneq2dv ⊢ d = h → ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k d ⁡ j ⁡ k = ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k
212 211 sseq2d ⊢ d = h → ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k d ⁡ j ⁡ k ↔ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k
213 206 oveq2d ⊢ d = h → g ⁡ j L ⁡ y d ⁡ j = g ⁡ j L ⁡ y h ⁡ j
214 213 mpteq2dv ⊢ d = h → j ∈ ℕ ⟼ g ⁡ j L ⁡ y d ⁡ j = j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j
215 214 fveq2d ⊢ d = h → sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y d ⁡ j = sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j
216 215 breq2d ⊢ d = h → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y d ⁡ j ↔ e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j
217 212 216 imbi12d ⊢ d = h → ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k d ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y d ⁡ j ↔ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j
218 217 cbvralvw ⊢ ∀ d ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k d ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y d ⁡ j ↔ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j
219 218 a1i ⊢ c = g → ∀ d ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k d ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y d ⁡ j ↔ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j
220 205 219 bitrd ⊢ c = g → ∀ d ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y d ⁡ j ↔ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j
221 220 cbvralvw ⊢ ∀ c ∈ ℝ y ℕ ∀ d ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y d ⁡ j ↔ ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j
222 221 a1i ⊢ b = f → ∀ c ∈ ℝ y ℕ ∀ d ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y d ⁡ j ↔ ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j
223 192 222 bitrd ⊢ b = f → ∀ c ∈ ℝ y ℕ ∀ d ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k → e L ⁡ y b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y d ⁡ j ↔ ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j
224 223 cbvralvw ⊢ ∀ b ∈ ℝ y ∀ c ∈ ℝ y ℕ ∀ d ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k → e L ⁡ y b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y d ⁡ j ↔ ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j
225 224 a1i ⊢ a = e → ∀ b ∈ ℝ y ∀ c ∈ ℝ y ℕ ∀ d ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k → e L ⁡ y b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y d ⁡ j ↔ ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j
226 185 225 bitrd ⊢ a = e → ∀ b ∈ ℝ y ∀ c ∈ ℝ y ℕ ∀ d ∈ ℝ y ℕ ⨉ k ∈ y a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ y b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y d ⁡ j ↔ ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j
227 226 cbvralvw ⊢ ∀ a ∈ ℝ y ∀ b ∈ ℝ y ∀ c ∈ ℝ y ℕ ∀ d ∈ ℝ y ℕ ⨉ k ∈ y a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ y b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y d ⁡ j ↔ ∀ e ∈ ℝ y ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j
228 227 biimpi ⊢ ∀ a ∈ ℝ y ∀ b ∈ ℝ y ∀ c ∈ ℝ y ℕ ∀ d ∈ ℝ y ℕ ⨉ k ∈ y a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ y b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y d ⁡ j → ∀ e ∈ ℝ y ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j
229 228 adantl ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ ∀ a ∈ ℝ y ∀ b ∈ ℝ y ∀ c ∈ ℝ y ℕ ∀ d ∈ ℝ y ℕ ⨉ k ∈ y a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ y b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y d ⁡ j → ∀ e ∈ ℝ y ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j
230 simplll ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ a ∈ ℝ y ∪ z ∧ y = ∅ → φ
231 eldifi ⊢ z ∈ X ∖ y → z ∈ X
232 231 adantl ⊢ φ ∧ z ∈ X ∖ y → z ∈ X
233 232 adantrl ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y → z ∈ X
234 233 ad2antrr ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ a ∈ ℝ y ∪ z ∧ y = ∅ → z ∈ X
235 simpl ⊢ a ∈ ℝ y ∪ z ∧ y = ∅ → a ∈ ℝ y ∪ z
236 uneq1 ⊢ y = ∅ → y ∪ z = ∅ ∪ z
237 0un ⊢ ∅ ∪ z = z
238 237 a1i ⊢ y = ∅ → ∅ ∪ z = z
239 236 238 eqtr2d ⊢ y = ∅ → z = y ∪ z
240 239 eqcomd ⊢ y = ∅ → y ∪ z = z
241 240 oveq2d ⊢ y = ∅ → ℝ y ∪ z = ℝ z
242 241 adantl ⊢ a ∈ ℝ y ∪ z ∧ y = ∅ → ℝ y ∪ z = ℝ z
243 235 242 eleqtrd ⊢ a ∈ ℝ y ∪ z ∧ y = ∅ → a ∈ ℝ z
244 243 adantll ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ a ∈ ℝ y ∪ z ∧ y = ∅ → a ∈ ℝ z
245 230 234 244 jca31 ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ a ∈ ℝ y ∪ z ∧ y = ∅ → φ ∧ z ∈ X ∧ a ∈ ℝ z
246 245 adantllr ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ ∀ e ∈ ℝ y ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j ∧ a ∈ ℝ y ∪ z ∧ y = ∅ → φ ∧ z ∈ X ∧ a ∈ ℝ z
247 246 adantlr ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ ∀ e ∈ ℝ y ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j ∧ a ∈ ℝ y ∪ z ∧ b ∈ ℝ y ∪ z ∧ y = ∅ → φ ∧ z ∈ X ∧ a ∈ ℝ z
248 247 adantlr ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ ∀ e ∈ ℝ y ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j ∧ a ∈ ℝ y ∪ z ∧ b ∈ ℝ y ∪ z ∧ c ∈ ℝ y ∪ z ℕ ∧ y = ∅ → φ ∧ z ∈ X ∧ a ∈ ℝ z
249 simpl ⊢ b ∈ ℝ y ∪ z ∧ y = ∅ → b ∈ ℝ y ∪ z
250 241 adantl ⊢ b ∈ ℝ y ∪ z ∧ y = ∅ → ℝ y ∪ z = ℝ z
251 249 250 eleqtrd ⊢ b ∈ ℝ y ∪ z ∧ y = ∅ → b ∈ ℝ z
252 251 adantlr ⊢ b ∈ ℝ y ∪ z ∧ c ∈ ℝ y ∪ z ℕ ∧ y = ∅ → b ∈ ℝ z
253 252 adantlll ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ ∀ e ∈ ℝ y ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j ∧ a ∈ ℝ y ∪ z ∧ b ∈ ℝ y ∪ z ∧ c ∈ ℝ y ∪ z ℕ ∧ y = ∅ → b ∈ ℝ z
254 simpl ⊢ c ∈ ℝ y ∪ z ℕ ∧ y = ∅ → c ∈ ℝ y ∪ z ℕ
255 241 oveq1d ⊢ y = ∅ → ℝ y ∪ z ℕ = ℝ z ℕ
256 255 adantl ⊢ c ∈ ℝ y ∪ z ℕ ∧ y = ∅ → ℝ y ∪ z ℕ = ℝ z ℕ
257 254 256 eleqtrd ⊢ c ∈ ℝ y ∪ z ℕ ∧ y = ∅ → c ∈ ℝ z ℕ
258 257 adantll ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ ∀ e ∈ ℝ y ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j ∧ a ∈ ℝ y ∪ z ∧ b ∈ ℝ y ∪ z ∧ c ∈ ℝ y ∪ z ℕ ∧ y = ∅ → c ∈ ℝ z ℕ
259 248 253 258 jca31 ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ ∀ e ∈ ℝ y ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j ∧ a ∈ ℝ y ∪ z ∧ b ∈ ℝ y ∪ z ∧ c ∈ ℝ y ∪ z ℕ ∧ y = ∅ → φ ∧ z ∈ X ∧ a ∈ ℝ z ∧ b ∈ ℝ z ∧ c ∈ ℝ z ℕ
260 259 adantlr ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ ∀ e ∈ ℝ y ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j ∧ a ∈ ℝ y ∪ z ∧ b ∈ ℝ y ∪ z ∧ c ∈ ℝ y ∪ z ℕ ∧ d ∈ ℝ y ∪ z ℕ ∧ y = ∅ → φ ∧ z ∈ X ∧ a ∈ ℝ z ∧ b ∈ ℝ z ∧ c ∈ ℝ z ℕ
261 260 adantlr ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ ∀ e ∈ ℝ y ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j ∧ a ∈ ℝ y ∪ z ∧ b ∈ ℝ y ∪ z ∧ c ∈ ℝ y ∪ z ℕ ∧ d ∈ ℝ y ∪ z ℕ ∧ ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k ∧ y = ∅ → φ ∧ z ∈ X ∧ a ∈ ℝ z ∧ b ∈ ℝ z ∧ c ∈ ℝ z ℕ
262 simpl ⊢ d ∈ ℝ y ∪ z ℕ ∧ y = ∅ → d ∈ ℝ y ∪ z ℕ
263 255 adantl ⊢ d ∈ ℝ y ∪ z ℕ ∧ y = ∅ → ℝ y ∪ z ℕ = ℝ z ℕ
264 262 263 eleqtrd ⊢ d ∈ ℝ y ∪ z ℕ ∧ y = ∅ → d ∈ ℝ z ℕ
265 264 adantlr ⊢ d ∈ ℝ y ∪ z ℕ ∧ ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k ∧ y = ∅ → d ∈ ℝ z ℕ
266 265 adantlll ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ ∀ e ∈ ℝ y ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j ∧ a ∈ ℝ y ∪ z ∧ b ∈ ℝ y ∪ z ∧ c ∈ ℝ y ∪ z ℕ ∧ d ∈ ℝ y ∪ z ℕ ∧ ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k ∧ y = ∅ → d ∈ ℝ z ℕ
267 simpl ⊢ ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k ∧ y = ∅ → ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k
268 239 ixpeq1d ⊢ y = ∅ → ⨉ k ∈ z a ⁡ k b ⁡ k = ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k
269 268 adantl ⊢ ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k ∧ y = ∅ → ⨉ k ∈ z a ⁡ k b ⁡ k = ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k
270 239 ixpeq1d ⊢ y = ∅ → ⨉ k ∈ z c ⁡ i ⁡ k d ⁡ i ⁡ k = ⨉ k ∈ y ∪ z c ⁡ i ⁡ k d ⁡ i ⁡ k
271 270 adantr ⊢ y = ∅ ∧ i ∈ ℕ → ⨉ k ∈ z c ⁡ i ⁡ k d ⁡ i ⁡ k = ⨉ k ∈ y ∪ z c ⁡ i ⁡ k d ⁡ i ⁡ k
272 271 iuneq2dv ⊢ y = ∅ → ⋃ i ∈ ℕ ⨉ k ∈ z c ⁡ i ⁡ k d ⁡ i ⁡ k = ⋃ i ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ i ⁡ k d ⁡ i ⁡ k
273 fveq2 ⊢ i = j → c ⁡ i = c ⁡ j
274 273 fveq1d ⊢ i = j → c ⁡ i ⁡ k = c ⁡ j ⁡ k
275 fveq2 ⊢ i = j → d ⁡ i = d ⁡ j
276 275 fveq1d ⊢ i = j → d ⁡ i ⁡ k = d ⁡ j ⁡ k
277 274 276 oveq12d ⊢ i = j → c ⁡ i ⁡ k d ⁡ i ⁡ k = c ⁡ j ⁡ k d ⁡ j ⁡ k
278 277 ixpeq2dv ⊢ i = j → ⨉ k ∈ y ∪ z c ⁡ i ⁡ k d ⁡ i ⁡ k = ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k
279 278 cbviunv ⊢ ⋃ i ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ i ⁡ k d ⁡ i ⁡ k = ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k
280 279 a1i ⊢ y = ∅ → ⋃ i ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ i ⁡ k d ⁡ i ⁡ k = ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k
281 272 280 eqtrd ⊢ y = ∅ → ⋃ i ∈ ℕ ⨉ k ∈ z c ⁡ i ⁡ k d ⁡ i ⁡ k = ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k
282 281 adantl ⊢ ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k ∧ y = ∅ → ⋃ i ∈ ℕ ⨉ k ∈ z c ⁡ i ⁡ k d ⁡ i ⁡ k = ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k
283 269 282 sseq12d ⊢ ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k ∧ y = ∅ → ⨉ k ∈ z a ⁡ k b ⁡ k ⊆ ⋃ i ∈ ℕ ⨉ k ∈ z c ⁡ i ⁡ k d ⁡ i ⁡ k ↔ ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k
284 267 283 mpbird ⊢ ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k ∧ y = ∅ → ⨉ k ∈ z a ⁡ k b ⁡ k ⊆ ⋃ i ∈ ℕ ⨉ k ∈ z c ⁡ i ⁡ k d ⁡ i ⁡ k
285 284 adantll ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ ∀ e ∈ ℝ y ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j ∧ a ∈ ℝ y ∪ z ∧ b ∈ ℝ y ∪ z ∧ c ∈ ℝ y ∪ z ℕ ∧ d ∈ ℝ y ∪ z ℕ ∧ ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k ∧ y = ∅ → ⨉ k ∈ z a ⁡ k b ⁡ k ⊆ ⋃ i ∈ ℕ ⨉ k ∈ z c ⁡ i ⁡ k d ⁡ i ⁡ k
286 261 266 285 jca31 ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ ∀ e ∈ ℝ y ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j ∧ a ∈ ℝ y ∪ z ∧ b ∈ ℝ y ∪ z ∧ c ∈ ℝ y ∪ z ℕ ∧ d ∈ ℝ y ∪ z ℕ ∧ ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k ∧ y = ∅ → φ ∧ z ∈ X ∧ a ∈ ℝ z ∧ b ∈ ℝ z ∧ c ∈ ℝ z ℕ ∧ d ∈ ℝ z ℕ ∧ ⨉ k ∈ z a ⁡ k b ⁡ k ⊆ ⋃ i ∈ ℕ ⨉ k ∈ z c ⁡ i ⁡ k d ⁡ i ⁡ k
287 simpr ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ ∀ e ∈ ℝ y ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j ∧ a ∈ ℝ y ∪ z ∧ b ∈ ℝ y ∪ z ∧ c ∈ ℝ y ∪ z ℕ ∧ d ∈ ℝ y ∪ z ℕ ∧ ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k ∧ y = ∅ → y = ∅
288 fveq1 ⊢ a = u → a ⁡ k = u ⁡ k
289 288 oveq1d ⊢ a = u → a ⁡ k b ⁡ k = u ⁡ k b ⁡ k
290 289 fveq2d ⊢ a = u → vol ⁡ a ⁡ k b ⁡ k = vol ⁡ u ⁡ k b ⁡ k
291 290 prodeq2ad ⊢ a = u → ∏ k ∈ x vol ⁡ a ⁡ k b ⁡ k = ∏ k ∈ x vol ⁡ u ⁡ k b ⁡ k
292 291 ifeq2d ⊢ a = u → if x = ∅ 0 ∏ k ∈ x vol ⁡ a ⁡ k b ⁡ k = if x = ∅ 0 ∏ k ∈ x vol ⁡ u ⁡ k b ⁡ k
293 fveq2 ⊢ k = l → u ⁡ k = u ⁡ l
294 fveq2 ⊢ k = l → b ⁡ k = b ⁡ l
295 293 294 oveq12d ⊢ k = l → u ⁡ k b ⁡ k = u ⁡ l b ⁡ l
296 295 fveq2d ⊢ k = l → vol ⁡ u ⁡ k b ⁡ k = vol ⁡ u ⁡ l b ⁡ l
297 296 cbvprodv ⊢ ∏ k ∈ x vol ⁡ u ⁡ k b ⁡ k = ∏ l ∈ x vol ⁡ u ⁡ l b ⁡ l
298 297 a1i ⊢ b = v → ∏ k ∈ x vol ⁡ u ⁡ k b ⁡ k = ∏ l ∈ x vol ⁡ u ⁡ l b ⁡ l
299 fveq1 ⊢ b = v → b ⁡ l = v ⁡ l
300 299 oveq2d ⊢ b = v → u ⁡ l b ⁡ l = u ⁡ l v ⁡ l
301 300 fveq2d ⊢ b = v → vol ⁡ u ⁡ l b ⁡ l = vol ⁡ u ⁡ l v ⁡ l
302 301 prodeq2ad ⊢ b = v → ∏ l ∈ x vol ⁡ u ⁡ l b ⁡ l = ∏ l ∈ x vol ⁡ u ⁡ l v ⁡ l
303 298 302 eqtrd ⊢ b = v → ∏ k ∈ x vol ⁡ u ⁡ k b ⁡ k = ∏ l ∈ x vol ⁡ u ⁡ l v ⁡ l
304 303 ifeq2d ⊢ b = v → if x = ∅ 0 ∏ k ∈ x vol ⁡ u ⁡ k b ⁡ k = if x = ∅ 0 ∏ l ∈ x vol ⁡ u ⁡ l v ⁡ l
305 292 304 cbvmpov ⊢ a ∈ ℝ x , b ∈ ℝ x ⟼ if x = ∅ 0 ∏ k ∈ x vol ⁡ a ⁡ k b ⁡ k = u ∈ ℝ x , v ∈ ℝ x ⟼ if x = ∅ 0 ∏ l ∈ x vol ⁡ u ⁡ l v ⁡ l
306 305 mpteq2i ⊢ x ∈ Fin ⟼ a ∈ ℝ x , b ∈ ℝ x ⟼ if x = ∅ 0 ∏ k ∈ x vol ⁡ a ⁡ k b ⁡ k = x ∈ Fin ⟼ u ∈ ℝ x , v ∈ ℝ x ⟼ if x = ∅ 0 ∏ l ∈ x vol ⁡ u ⁡ l v ⁡ l
307 1 306 eqtri ⊢ L = x ∈ Fin ⟼ u ∈ ℝ x , v ∈ ℝ x ⟼ if x = ∅ 0 ∏ l ∈ x vol ⁡ u ⁡ l v ⁡ l
308 simp-6r ⊢ φ ∧ z ∈ X ∧ a ∈ ℝ z ∧ b ∈ ℝ z ∧ c ∈ ℝ z ℕ ∧ d ∈ ℝ z ℕ ∧ ⨉ k ∈ z a ⁡ k b ⁡ k ⊆ ⋃ i ∈ ℕ ⨉ k ∈ z c ⁡ i ⁡ k d ⁡ i ⁡ k → z ∈ X
309 eqid ⊢ z = z
310 elmapi ⊢ a ∈ ℝ z → a : z ⟶ ℝ
311 310 ad2antlr ⊢ φ ∧ z ∈ X ∧ a ∈ ℝ z ∧ b ∈ ℝ z → a : z ⟶ ℝ
312 311 ad3antrrr ⊢ φ ∧ z ∈ X ∧ a ∈ ℝ z ∧ b ∈ ℝ z ∧ c ∈ ℝ z ℕ ∧ d ∈ ℝ z ℕ ∧ ⨉ k ∈ z a ⁡ k b ⁡ k ⊆ ⋃ i ∈ ℕ ⨉ k ∈ z c ⁡ i ⁡ k d ⁡ i ⁡ k → a : z ⟶ ℝ
313 elmapi ⊢ b ∈ ℝ z → b : z ⟶ ℝ
314 313 adantl ⊢ φ ∧ z ∈ X ∧ a ∈ ℝ z ∧ b ∈ ℝ z → b : z ⟶ ℝ
315 314 ad3antrrr ⊢ φ ∧ z ∈ X ∧ a ∈ ℝ z ∧ b ∈ ℝ z ∧ c ∈ ℝ z ℕ ∧ d ∈ ℝ z ℕ ∧ ⨉ k ∈ z a ⁡ k b ⁡ k ⊆ ⋃ i ∈ ℕ ⨉ k ∈ z c ⁡ i ⁡ k d ⁡ i ⁡ k → b : z ⟶ ℝ
316 elmapi ⊢ c ∈ ℝ z ℕ → c : ℕ ⟶ ℝ z
317 316 adantl ⊢ φ ∧ z ∈ X ∧ a ∈ ℝ z ∧ b ∈ ℝ z ∧ c ∈ ℝ z ℕ → c : ℕ ⟶ ℝ z
318 317 ad2antrr ⊢ φ ∧ z ∈ X ∧ a ∈ ℝ z ∧ b ∈ ℝ z ∧ c ∈ ℝ z ℕ ∧ d ∈ ℝ z ℕ ∧ ⨉ k ∈ z a ⁡ k b ⁡ k ⊆ ⋃ i ∈ ℕ ⨉ k ∈ z c ⁡ i ⁡ k d ⁡ i ⁡ k → c : ℕ ⟶ ℝ z
319 elmapi ⊢ d ∈ ℝ z ℕ → d : ℕ ⟶ ℝ z
320 319 ad2antlr ⊢ φ ∧ z ∈ X ∧ a ∈ ℝ z ∧ b ∈ ℝ z ∧ c ∈ ℝ z ℕ ∧ d ∈ ℝ z ℕ ∧ ⨉ k ∈ z a ⁡ k b ⁡ k ⊆ ⋃ i ∈ ℕ ⨉ k ∈ z c ⁡ i ⁡ k d ⁡ i ⁡ k → d : ℕ ⟶ ℝ z
321 id ⊢ ⨉ k ∈ z a ⁡ k b ⁡ k ⊆ ⋃ i ∈ ℕ ⨉ k ∈ z c ⁡ i ⁡ k d ⁡ i ⁡ k → ⨉ k ∈ z a ⁡ k b ⁡ k ⊆ ⋃ i ∈ ℕ ⨉ k ∈ z c ⁡ i ⁡ k d ⁡ i ⁡ k
322 fveq2 ⊢ k = l → a ⁡ k = a ⁡ l
323 322 294 oveq12d ⊢ k = l → a ⁡ k b ⁡ k = a ⁡ l b ⁡ l
324 eqcom ⊢ k = l ↔ l = k
325 324 imbi1i ⊢ k = l → a ⁡ k b ⁡ k = a ⁡ l b ⁡ l ↔ l = k → a ⁡ k b ⁡ k = a ⁡ l b ⁡ l
326 eqcom ⊢ a ⁡ k b ⁡ k = a ⁡ l b ⁡ l ↔ a ⁡ l b ⁡ l = a ⁡ k b ⁡ k
327 326 imbi2i ⊢ l = k → a ⁡ k b ⁡ k = a ⁡ l b ⁡ l ↔ l = k → a ⁡ l b ⁡ l = a ⁡ k b ⁡ k
328 325 327 bitri ⊢ k = l → a ⁡ k b ⁡ k = a ⁡ l b ⁡ l ↔ l = k → a ⁡ l b ⁡ l = a ⁡ k b ⁡ k
329 323 328 mpbi ⊢ l = k → a ⁡ l b ⁡ l = a ⁡ k b ⁡ k
330 329 cbvixpv ⊢ ⨉ l ∈ z a ⁡ l b ⁡ l = ⨉ k ∈ z a ⁡ k b ⁡ k
331 330 a1i ⊢ ⨉ k ∈ z a ⁡ k b ⁡ k ⊆ ⋃ i ∈ ℕ ⨉ k ∈ z c ⁡ i ⁡ k d ⁡ i ⁡ k → ⨉ l ∈ z a ⁡ l b ⁡ l = ⨉ k ∈ z a ⁡ k b ⁡ k
332 277 ixpeq2dv ⊢ i = j → ⨉ k ∈ z c ⁡ i ⁡ k d ⁡ i ⁡ k = ⨉ k ∈ z c ⁡ j ⁡ k d ⁡ j ⁡ k
333 332 cbviunv ⊢ ⋃ i ∈ ℕ ⨉ k ∈ z c ⁡ i ⁡ k d ⁡ i ⁡ k = ⋃ j ∈ ℕ ⨉ k ∈ z c ⁡ j ⁡ k d ⁡ j ⁡ k
334 fveq2 ⊢ k = l → c ⁡ j ⁡ k = c ⁡ j ⁡ l
335 fveq2 ⊢ k = l → d ⁡ j ⁡ k = d ⁡ j ⁡ l
336 334 335 oveq12d ⊢ k = l → c ⁡ j ⁡ k d ⁡ j ⁡ k = c ⁡ j ⁡ l d ⁡ j ⁡ l
337 336 cbvixpv ⊢ ⨉ k ∈ z c ⁡ j ⁡ k d ⁡ j ⁡ k = ⨉ l ∈ z c ⁡ j ⁡ l d ⁡ j ⁡ l
338 337 a1i ⊢ j ∈ ℕ → ⨉ k ∈ z c ⁡ j ⁡ k d ⁡ j ⁡ k = ⨉ l ∈ z c ⁡ j ⁡ l d ⁡ j ⁡ l
339 338 iuneq2i ⊢ ⋃ j ∈ ℕ ⨉ k ∈ z c ⁡ j ⁡ k d ⁡ j ⁡ k = ⋃ j ∈ ℕ ⨉ l ∈ z c ⁡ j ⁡ l d ⁡ j ⁡ l
340 333 339 eqtr2i ⊢ ⋃ j ∈ ℕ ⨉ l ∈ z c ⁡ j ⁡ l d ⁡ j ⁡ l = ⋃ i ∈ ℕ ⨉ k ∈ z c ⁡ i ⁡ k d ⁡ i ⁡ k
341 340 a1i ⊢ ⨉ k ∈ z a ⁡ k b ⁡ k ⊆ ⋃ i ∈ ℕ ⨉ k ∈ z c ⁡ i ⁡ k d ⁡ i ⁡ k → ⋃ j ∈ ℕ ⨉ l ∈ z c ⁡ j ⁡ l d ⁡ j ⁡ l = ⋃ i ∈ ℕ ⨉ k ∈ z c ⁡ i ⁡ k d ⁡ i ⁡ k
342 331 341 sseq12d ⊢ ⨉ k ∈ z a ⁡ k b ⁡ k ⊆ ⋃ i ∈ ℕ ⨉ k ∈ z c ⁡ i ⁡ k d ⁡ i ⁡ k → ⨉ l ∈ z a ⁡ l b ⁡ l ⊆ ⋃ j ∈ ℕ ⨉ l ∈ z c ⁡ j ⁡ l d ⁡ j ⁡ l ↔ ⨉ k ∈ z a ⁡ k b ⁡ k ⊆ ⋃ i ∈ ℕ ⨉ k ∈ z c ⁡ i ⁡ k d ⁡ i ⁡ k
343 321 342 mpbird ⊢ ⨉ k ∈ z a ⁡ k b ⁡ k ⊆ ⋃ i ∈ ℕ ⨉ k ∈ z c ⁡ i ⁡ k d ⁡ i ⁡ k → ⨉ l ∈ z a ⁡ l b ⁡ l ⊆ ⋃ j ∈ ℕ ⨉ l ∈ z c ⁡ j ⁡ l d ⁡ j ⁡ l
344 343 adantl ⊢ φ ∧ z ∈ X ∧ a ∈ ℝ z ∧ b ∈ ℝ z ∧ c ∈ ℝ z ℕ ∧ d ∈ ℝ z ℕ ∧ ⨉ k ∈ z a ⁡ k b ⁡ k ⊆ ⋃ i ∈ ℕ ⨉ k ∈ z c ⁡ i ⁡ k d ⁡ i ⁡ k → ⨉ l ∈ z a ⁡ l b ⁡ l ⊆ ⋃ j ∈ ℕ ⨉ l ∈ z c ⁡ j ⁡ l d ⁡ j ⁡ l
345 307 308 309 312 315 318 320 344 hoidmv1le ⊢ φ ∧ z ∈ X ∧ a ∈ ℝ z ∧ b ∈ ℝ z ∧ c ∈ ℝ z ℕ ∧ d ∈ ℝ z ℕ ∧ ⨉ k ∈ z a ⁡ k b ⁡ k ⊆ ⋃ i ∈ ℕ ⨉ k ∈ z c ⁡ i ⁡ k d ⁡ i ⁡ k → a L ⁡ z b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ z d ⁡ j
346 345 adantr ⊢ φ ∧ z ∈ X ∧ a ∈ ℝ z ∧ b ∈ ℝ z ∧ c ∈ ℝ z ℕ ∧ d ∈ ℝ z ℕ ∧ ⨉ k ∈ z a ⁡ k b ⁡ k ⊆ ⋃ i ∈ ℕ ⨉ k ∈ z c ⁡ i ⁡ k d ⁡ i ⁡ k ∧ y = ∅ → a L ⁡ z b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ z d ⁡ j
347 236 238 eqtrd ⊢ y = ∅ → y ∪ z = z
348 347 fveq2d ⊢ y = ∅ → L ⁡ y ∪ z = L ⁡ z
349 348 oveqd ⊢ y = ∅ → a L ⁡ y ∪ z b = a L ⁡ z b
350 349 adantl ⊢ φ ∧ z ∈ X ∧ a ∈ ℝ z ∧ b ∈ ℝ z ∧ c ∈ ℝ z ℕ ∧ d ∈ ℝ z ℕ ∧ ⨉ k ∈ z a ⁡ k b ⁡ k ⊆ ⋃ i ∈ ℕ ⨉ k ∈ z c ⁡ i ⁡ k d ⁡ i ⁡ k ∧ y = ∅ → a L ⁡ y ∪ z b = a L ⁡ z b
351 348 oveqd ⊢ y = ∅ → c ⁡ j L ⁡ y ∪ z d ⁡ j = c ⁡ j L ⁡ z d ⁡ j
352 351 mpteq2dv ⊢ y = ∅ → j ∈ ℕ ⟼ c ⁡ j L ⁡ y ∪ z d ⁡ j = j ∈ ℕ ⟼ c ⁡ j L ⁡ z d ⁡ j
353 352 fveq2d ⊢ y = ∅ → sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y ∪ z d ⁡ j = sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ z d ⁡ j
354 353 adantl ⊢ φ ∧ z ∈ X ∧ a ∈ ℝ z ∧ b ∈ ℝ z ∧ c ∈ ℝ z ℕ ∧ d ∈ ℝ z ℕ ∧ ⨉ k ∈ z a ⁡ k b ⁡ k ⊆ ⋃ i ∈ ℕ ⨉ k ∈ z c ⁡ i ⁡ k d ⁡ i ⁡ k ∧ y = ∅ → sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y ∪ z d ⁡ j = sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ z d ⁡ j
355 350 354 breq12d ⊢ φ ∧ z ∈ X ∧ a ∈ ℝ z ∧ b ∈ ℝ z ∧ c ∈ ℝ z ℕ ∧ d ∈ ℝ z ℕ ∧ ⨉ k ∈ z a ⁡ k b ⁡ k ⊆ ⋃ i ∈ ℕ ⨉ k ∈ z c ⁡ i ⁡ k d ⁡ i ⁡ k ∧ y = ∅ → a L ⁡ y ∪ z b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y ∪ z d ⁡ j ↔ a L ⁡ z b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ z d ⁡ j
356 346 355 mpbird ⊢ φ ∧ z ∈ X ∧ a ∈ ℝ z ∧ b ∈ ℝ z ∧ c ∈ ℝ z ℕ ∧ d ∈ ℝ z ℕ ∧ ⨉ k ∈ z a ⁡ k b ⁡ k ⊆ ⋃ i ∈ ℕ ⨉ k ∈ z c ⁡ i ⁡ k d ⁡ i ⁡ k ∧ y = ∅ → a L ⁡ y ∪ z b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y ∪ z d ⁡ j
357 286 287 356 syl2anc ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ ∀ e ∈ ℝ y ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j ∧ a ∈ ℝ y ∪ z ∧ b ∈ ℝ y ∪ z ∧ c ∈ ℝ y ∪ z ℕ ∧ d ∈ ℝ y ∪ z ℕ ∧ ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k ∧ y = ∅ → a L ⁡ y ∪ z b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y ∪ z d ⁡ j
358 2 ad8antr ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ ∀ e ∈ ℝ y ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j ∧ a ∈ ℝ y ∪ z ∧ b ∈ ℝ y ∪ z ∧ c ∈ ℝ y ∪ z ℕ ∧ d ∈ ℝ y ∪ z ℕ ∧ ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k ∧ ¬ y = ∅ → X ∈ Fin
359 simplrl ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ ∀ e ∈ ℝ y ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j → y ⊆ X
360 359 ad5ant12 ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ ∀ e ∈ ℝ y ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j ∧ a ∈ ℝ y ∪ z ∧ b ∈ ℝ y ∪ z ∧ c ∈ ℝ y ∪ z ℕ → y ⊆ X
361 360 ad5ant12 ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ ∀ e ∈ ℝ y ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j ∧ a ∈ ℝ y ∪ z ∧ b ∈ ℝ y ∪ z ∧ c ∈ ℝ y ∪ z ℕ ∧ d ∈ ℝ y ∪ z ℕ ∧ ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k ∧ ¬ y = ∅ → y ⊆ X
362 simplrr ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ ∀ e ∈ ℝ y ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j → z ∈ X ∖ y
363 362 ad5ant12 ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ ∀ e ∈ ℝ y ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j ∧ a ∈ ℝ y ∪ z ∧ b ∈ ℝ y ∪ z ∧ c ∈ ℝ y ∪ z ℕ → z ∈ X ∖ y
364 363 ad5ant12 ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ ∀ e ∈ ℝ y ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j ∧ a ∈ ℝ y ∪ z ∧ b ∈ ℝ y ∪ z ∧ c ∈ ℝ y ∪ z ℕ ∧ d ∈ ℝ y ∪ z ℕ ∧ ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k ∧ ¬ y = ∅ → z ∈ X ∖ y
365 eqid ⊢ y ∪ z = y ∪ z
366 elmapi ⊢ a ∈ ℝ y ∪ z → a : y ∪ z ⟶ ℝ
367 366 adantr ⊢ a ∈ ℝ y ∪ z ∧ b ∈ ℝ y ∪ z → a : y ∪ z ⟶ ℝ
368 367 ad4ant23 ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ ∀ e ∈ ℝ y ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j ∧ a ∈ ℝ y ∪ z ∧ b ∈ ℝ y ∪ z ∧ c ∈ ℝ y ∪ z ℕ → a : y ∪ z ⟶ ℝ
369 368 ad3antrrr ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ ∀ e ∈ ℝ y ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j ∧ a ∈ ℝ y ∪ z ∧ b ∈ ℝ y ∪ z ∧ c ∈ ℝ y ∪ z ℕ ∧ d ∈ ℝ y ∪ z ℕ ∧ ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k ∧ ¬ y = ∅ → a : y ∪ z ⟶ ℝ
370 elmapi ⊢ b ∈ ℝ y ∪ z → b : y ∪ z ⟶ ℝ
371 370 adantl ⊢ a ∈ ℝ y ∪ z ∧ b ∈ ℝ y ∪ z → b : y ∪ z ⟶ ℝ
372 371 ad4ant23 ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ ∀ e ∈ ℝ y ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j ∧ a ∈ ℝ y ∪ z ∧ b ∈ ℝ y ∪ z ∧ c ∈ ℝ y ∪ z ℕ → b : y ∪ z ⟶ ℝ
373 372 ad3antrrr ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ ∀ e ∈ ℝ y ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j ∧ a ∈ ℝ y ∪ z ∧ b ∈ ℝ y ∪ z ∧ c ∈ ℝ y ∪ z ℕ ∧ d ∈ ℝ y ∪ z ℕ ∧ ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k ∧ ¬ y = ∅ → b : y ∪ z ⟶ ℝ
374 elmapi ⊢ c ∈ ℝ y ∪ z ℕ → c : ℕ ⟶ ℝ y ∪ z
375 374 adantl ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ ∀ e ∈ ℝ y ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j ∧ a ∈ ℝ y ∪ z ∧ b ∈ ℝ y ∪ z ∧ c ∈ ℝ y ∪ z ℕ → c : ℕ ⟶ ℝ y ∪ z
376 375 ad3antrrr ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ ∀ e ∈ ℝ y ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j ∧ a ∈ ℝ y ∪ z ∧ b ∈ ℝ y ∪ z ∧ c ∈ ℝ y ∪ z ℕ ∧ d ∈ ℝ y ∪ z ℕ ∧ ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k ∧ ¬ y = ∅ → c : ℕ ⟶ ℝ y ∪ z
377 elmapi ⊢ d ∈ ℝ y ∪ z ℕ → d : ℕ ⟶ ℝ y ∪ z
378 377 ad2antrr ⊢ d ∈ ℝ y ∪ z ℕ ∧ ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k ∧ ¬ y = ∅ → d : ℕ ⟶ ℝ y ∪ z
379 378 adantlll ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ ∀ e ∈ ℝ y ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j ∧ a ∈ ℝ y ∪ z ∧ b ∈ ℝ y ∪ z ∧ c ∈ ℝ y ∪ z ℕ ∧ d ∈ ℝ y ∪ z ℕ ∧ ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k ∧ ¬ y = ∅ → d : ℕ ⟶ ℝ y ∪ z
380 fveq2 ⊢ k = l → e ⁡ k = e ⁡ l
381 fveq2 ⊢ k = l → f ⁡ k = f ⁡ l
382 380 381 oveq12d ⊢ k = l → e ⁡ k f ⁡ k = e ⁡ l f ⁡ l
383 382 cbvixpv ⊢ ⨉ k ∈ y e ⁡ k f ⁡ k = ⨉ l ∈ y e ⁡ l f ⁡ l
384 383 a1i ⊢ h = o → ⨉ k ∈ y e ⁡ k f ⁡ k = ⨉ l ∈ y e ⁡ l f ⁡ l
385 fveq2 ⊢ j = i → g ⁡ j = g ⁡ i
386 385 fveq1d ⊢ j = i → g ⁡ j ⁡ k = g ⁡ i ⁡ k
387 fveq2 ⊢ j = i → h ⁡ j = h ⁡ i
388 387 fveq1d ⊢ j = i → h ⁡ j ⁡ k = h ⁡ i ⁡ k
389 386 388 oveq12d ⊢ j = i → g ⁡ j ⁡ k h ⁡ j ⁡ k = g ⁡ i ⁡ k h ⁡ i ⁡ k
390 389 ixpeq2dv ⊢ j = i → ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k = ⨉ k ∈ y g ⁡ i ⁡ k h ⁡ i ⁡ k
391 390 cbviunv ⊢ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k = ⋃ i ∈ ℕ ⨉ k ∈ y g ⁡ i ⁡ k h ⁡ i ⁡ k
392 391 a1i ⊢ h = o → ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k = ⋃ i ∈ ℕ ⨉ k ∈ y g ⁡ i ⁡ k h ⁡ i ⁡ k
393 fveq2 ⊢ k = l → g ⁡ i ⁡ k = g ⁡ i ⁡ l
394 fveq2 ⊢ k = l → h ⁡ i ⁡ k = h ⁡ i ⁡ l
395 393 394 oveq12d ⊢ k = l → g ⁡ i ⁡ k h ⁡ i ⁡ k = g ⁡ i ⁡ l h ⁡ i ⁡ l
396 395 cbvixpv ⊢ ⨉ k ∈ y g ⁡ i ⁡ k h ⁡ i ⁡ k = ⨉ l ∈ y g ⁡ i ⁡ l h ⁡ i ⁡ l
397 396 a1i ⊢ h = o → ⨉ k ∈ y g ⁡ i ⁡ k h ⁡ i ⁡ k = ⨉ l ∈ y g ⁡ i ⁡ l h ⁡ i ⁡ l
398 fveq1 ⊢ h = o → h ⁡ i = o ⁡ i
399 398 fveq1d ⊢ h = o → h ⁡ i ⁡ l = o ⁡ i ⁡ l
400 399 oveq2d ⊢ h = o → g ⁡ i ⁡ l h ⁡ i ⁡ l = g ⁡ i ⁡ l o ⁡ i ⁡ l
401 400 ixpeq2dv ⊢ h = o → ⨉ l ∈ y g ⁡ i ⁡ l h ⁡ i ⁡ l = ⨉ l ∈ y g ⁡ i ⁡ l o ⁡ i ⁡ l
402 397 401 eqtrd ⊢ h = o → ⨉ k ∈ y g ⁡ i ⁡ k h ⁡ i ⁡ k = ⨉ l ∈ y g ⁡ i ⁡ l o ⁡ i ⁡ l
403 402 adantr ⊢ h = o ∧ i ∈ ℕ → ⨉ k ∈ y g ⁡ i ⁡ k h ⁡ i ⁡ k = ⨉ l ∈ y g ⁡ i ⁡ l o ⁡ i ⁡ l
404 403 iuneq2dv ⊢ h = o → ⋃ i ∈ ℕ ⨉ k ∈ y g ⁡ i ⁡ k h ⁡ i ⁡ k = ⋃ i ∈ ℕ ⨉ l ∈ y g ⁡ i ⁡ l o ⁡ i ⁡ l
405 392 404 eqtrd ⊢ h = o → ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k = ⋃ i ∈ ℕ ⨉ l ∈ y g ⁡ i ⁡ l o ⁡ i ⁡ l
406 384 405 sseq12d ⊢ h = o → ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k ↔ ⨉ l ∈ y e ⁡ l f ⁡ l ⊆ ⋃ i ∈ ℕ ⨉ l ∈ y g ⁡ i ⁡ l o ⁡ i ⁡ l
407 385 387 oveq12d ⊢ j = i → g ⁡ j L ⁡ y h ⁡ j = g ⁡ i L ⁡ y h ⁡ i
408 407 cbvmptv ⊢ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j = i ∈ ℕ ⟼ g ⁡ i L ⁡ y h ⁡ i
409 408 a1i ⊢ h = o → j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j = i ∈ ℕ ⟼ g ⁡ i L ⁡ y h ⁡ i
410 398 oveq2d ⊢ h = o → g ⁡ i L ⁡ y h ⁡ i = g ⁡ i L ⁡ y o ⁡ i
411 410 mpteq2dv ⊢ h = o → i ∈ ℕ ⟼ g ⁡ i L ⁡ y h ⁡ i = i ∈ ℕ ⟼ g ⁡ i L ⁡ y o ⁡ i
412 409 411 eqtrd ⊢ h = o → j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j = i ∈ ℕ ⟼ g ⁡ i L ⁡ y o ⁡ i
413 412 fveq2d ⊢ h = o → sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j = sum^ ⁡ i ∈ ℕ ⟼ g ⁡ i L ⁡ y o ⁡ i
414 413 breq2d ⊢ h = o → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j ↔ e L ⁡ y f ≤ sum^ ⁡ i ∈ ℕ ⟼ g ⁡ i L ⁡ y o ⁡ i
415 406 414 imbi12d ⊢ h = o → ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j ↔ ⨉ l ∈ y e ⁡ l f ⁡ l ⊆ ⋃ i ∈ ℕ ⨉ l ∈ y g ⁡ i ⁡ l o ⁡ i ⁡ l → e L ⁡ y f ≤ sum^ ⁡ i ∈ ℕ ⟼ g ⁡ i L ⁡ y o ⁡ i
416 415 cbvralvw ⊢ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j ↔ ∀ o ∈ ℝ y ℕ ⨉ l ∈ y e ⁡ l f ⁡ l ⊆ ⋃ i ∈ ℕ ⨉ l ∈ y g ⁡ i ⁡ l o ⁡ i ⁡ l → e L ⁡ y f ≤ sum^ ⁡ i ∈ ℕ ⟼ g ⁡ i L ⁡ y o ⁡ i
417 416 ralbii ⊢ ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j ↔ ∀ g ∈ ℝ y ℕ ∀ o ∈ ℝ y ℕ ⨉ l ∈ y e ⁡ l f ⁡ l ⊆ ⋃ i ∈ ℕ ⨉ l ∈ y g ⁡ i ⁡ l o ⁡ i ⁡ l → e L ⁡ y f ≤ sum^ ⁡ i ∈ ℕ ⟼ g ⁡ i L ⁡ y o ⁡ i
418 417 ralbii ⊢ ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j ↔ ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ o ∈ ℝ y ℕ ⨉ l ∈ y e ⁡ l f ⁡ l ⊆ ⋃ i ∈ ℕ ⨉ l ∈ y g ⁡ i ⁡ l o ⁡ i ⁡ l → e L ⁡ y f ≤ sum^ ⁡ i ∈ ℕ ⟼ g ⁡ i L ⁡ y o ⁡ i
419 418 ralbii ⊢ ∀ e ∈ ℝ y ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j ↔ ∀ e ∈ ℝ y ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ o ∈ ℝ y ℕ ⨉ l ∈ y e ⁡ l f ⁡ l ⊆ ⋃ i ∈ ℕ ⨉ l ∈ y g ⁡ i ⁡ l o ⁡ i ⁡ l → e L ⁡ y f ≤ sum^ ⁡ i ∈ ℕ ⟼ g ⁡ i L ⁡ y o ⁡ i
420 419 biimpi ⊢ ∀ e ∈ ℝ y ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j → ∀ e ∈ ℝ y ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ o ∈ ℝ y ℕ ⨉ l ∈ y e ⁡ l f ⁡ l ⊆ ⋃ i ∈ ℕ ⨉ l ∈ y g ⁡ i ⁡ l o ⁡ i ⁡ l → e L ⁡ y f ≤ sum^ ⁡ i ∈ ℕ ⟼ g ⁡ i L ⁡ y o ⁡ i
421 420 adantl ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ ∀ e ∈ ℝ y ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j → ∀ e ∈ ℝ y ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ o ∈ ℝ y ℕ ⨉ l ∈ y e ⁡ l f ⁡ l ⊆ ⋃ i ∈ ℕ ⨉ l ∈ y g ⁡ i ⁡ l o ⁡ i ⁡ l → e L ⁡ y f ≤ sum^ ⁡ i ∈ ℕ ⟼ g ⁡ i L ⁡ y o ⁡ i
422 421 ad6antr ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ ∀ e ∈ ℝ y ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j ∧ a ∈ ℝ y ∪ z ∧ b ∈ ℝ y ∪ z ∧ c ∈ ℝ y ∪ z ℕ ∧ d ∈ ℝ y ∪ z ℕ ∧ ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k ∧ ¬ y = ∅ → ∀ e ∈ ℝ y ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ o ∈ ℝ y ℕ ⨉ l ∈ y e ⁡ l f ⁡ l ⊆ ⋃ i ∈ ℕ ⨉ l ∈ y g ⁡ i ⁡ l o ⁡ i ⁡ l → e L ⁡ y f ≤ sum^ ⁡ i ∈ ℕ ⟼ g ⁡ i L ⁡ y o ⁡ i
423 323 cbvixpv ⊢ ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k = ⨉ l ∈ y ∪ z a ⁡ l b ⁡ l
424 336 cbvixpv ⊢ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k = ⨉ l ∈ y ∪ z c ⁡ j ⁡ l d ⁡ j ⁡ l
425 424 a1i ⊢ j = i → ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k = ⨉ l ∈ y ∪ z c ⁡ j ⁡ l d ⁡ j ⁡ l
426 fveq2 ⊢ j = i → c ⁡ j = c ⁡ i
427 426 fveq1d ⊢ j = i → c ⁡ j ⁡ l = c ⁡ i ⁡ l
428 fveq2 ⊢ j = i → d ⁡ j = d ⁡ i
429 428 fveq1d ⊢ j = i → d ⁡ j ⁡ l = d ⁡ i ⁡ l
430 427 429 oveq12d ⊢ j = i → c ⁡ j ⁡ l d ⁡ j ⁡ l = c ⁡ i ⁡ l d ⁡ i ⁡ l
431 430 ixpeq2dv ⊢ j = i → ⨉ l ∈ y ∪ z c ⁡ j ⁡ l d ⁡ j ⁡ l = ⨉ l ∈ y ∪ z c ⁡ i ⁡ l d ⁡ i ⁡ l
432 425 431 eqtrd ⊢ j = i → ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k = ⨉ l ∈ y ∪ z c ⁡ i ⁡ l d ⁡ i ⁡ l
433 432 cbviunv ⊢ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k = ⋃ i ∈ ℕ ⨉ l ∈ y ∪ z c ⁡ i ⁡ l d ⁡ i ⁡ l
434 423 433 sseq12i ⊢ ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k ↔ ⨉ l ∈ y ∪ z a ⁡ l b ⁡ l ⊆ ⋃ i ∈ ℕ ⨉ l ∈ y ∪ z c ⁡ i ⁡ l d ⁡ i ⁡ l
435 434 biimpi ⊢ ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k → ⨉ l ∈ y ∪ z a ⁡ l b ⁡ l ⊆ ⋃ i ∈ ℕ ⨉ l ∈ y ∪ z c ⁡ i ⁡ l d ⁡ i ⁡ l
436 435 ad2antlr ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ ∀ e ∈ ℝ y ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j ∧ a ∈ ℝ y ∪ z ∧ b ∈ ℝ y ∪ z ∧ c ∈ ℝ y ∪ z ℕ ∧ d ∈ ℝ y ∪ z ℕ ∧ ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k ∧ ¬ y = ∅ → ⨉ l ∈ y ∪ z a ⁡ l b ⁡ l ⊆ ⋃ i ∈ ℕ ⨉ l ∈ y ∪ z c ⁡ i ⁡ l d ⁡ i ⁡ l
437 neqne ⊢ ¬ y = ∅ → y ≠ ∅
438 437 adantl ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ ∀ e ∈ ℝ y ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j ∧ a ∈ ℝ y ∪ z ∧ b ∈ ℝ y ∪ z ∧ c ∈ ℝ y ∪ z ℕ ∧ d ∈ ℝ y ∪ z ℕ ∧ ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k ∧ ¬ y = ∅ → y ≠ ∅
439 307 358 361 364 365 369 373 376 379 422 436 438 hoidmvlelem5 ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ ∀ e ∈ ℝ y ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j ∧ a ∈ ℝ y ∪ z ∧ b ∈ ℝ y ∪ z ∧ c ∈ ℝ y ∪ z ℕ ∧ d ∈ ℝ y ∪ z ℕ ∧ ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k ∧ ¬ y = ∅ → a L ⁡ y ∪ z b ≤ sum^ ⁡ i ∈ ℕ ⟼ c ⁡ i L ⁡ y ∪ z d ⁡ i
440 273 275 oveq12d ⊢ i = j → c ⁡ i L ⁡ y ∪ z d ⁡ i = c ⁡ j L ⁡ y ∪ z d ⁡ j
441 440 cbvmptv ⊢ i ∈ ℕ ⟼ c ⁡ i L ⁡ y ∪ z d ⁡ i = j ∈ ℕ ⟼ c ⁡ j L ⁡ y ∪ z d ⁡ j
442 441 fveq2i ⊢ sum^ ⁡ i ∈ ℕ ⟼ c ⁡ i L ⁡ y ∪ z d ⁡ i = sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y ∪ z d ⁡ j
443 442 breq2i ⊢ a L ⁡ y ∪ z b ≤ sum^ ⁡ i ∈ ℕ ⟼ c ⁡ i L ⁡ y ∪ z d ⁡ i ↔ a L ⁡ y ∪ z b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y ∪ z d ⁡ j
444 439 443 sylib ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ ∀ e ∈ ℝ y ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j ∧ a ∈ ℝ y ∪ z ∧ b ∈ ℝ y ∪ z ∧ c ∈ ℝ y ∪ z ℕ ∧ d ∈ ℝ y ∪ z ℕ ∧ ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k ∧ ¬ y = ∅ → a L ⁡ y ∪ z b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y ∪ z d ⁡ j
445 357 444 pm2.61dan ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ ∀ e ∈ ℝ y ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j ∧ a ∈ ℝ y ∪ z ∧ b ∈ ℝ y ∪ z ∧ c ∈ ℝ y ∪ z ℕ ∧ d ∈ ℝ y ∪ z ℕ ∧ ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ y ∪ z b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y ∪ z d ⁡ j
446 445 ex ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ ∀ e ∈ ℝ y ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j ∧ a ∈ ℝ y ∪ z ∧ b ∈ ℝ y ∪ z ∧ c ∈ ℝ y ∪ z ℕ ∧ d ∈ ℝ y ∪ z ℕ → ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ y ∪ z b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y ∪ z d ⁡ j
447 446 ralrimiva ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ ∀ e ∈ ℝ y ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j ∧ a ∈ ℝ y ∪ z ∧ b ∈ ℝ y ∪ z ∧ c ∈ ℝ y ∪ z ℕ → ∀ d ∈ ℝ y ∪ z ℕ ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ y ∪ z b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y ∪ z d ⁡ j
448 447 ralrimiva ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ ∀ e ∈ ℝ y ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j ∧ a ∈ ℝ y ∪ z ∧ b ∈ ℝ y ∪ z → ∀ c ∈ ℝ y ∪ z ℕ ∀ d ∈ ℝ y ∪ z ℕ ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ y ∪ z b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y ∪ z d ⁡ j
449 448 ralrimiva ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ ∀ e ∈ ℝ y ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j ∧ a ∈ ℝ y ∪ z → ∀ b ∈ ℝ y ∪ z ∀ c ∈ ℝ y ∪ z ℕ ∀ d ∈ ℝ y ∪ z ℕ ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ y ∪ z b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y ∪ z d ⁡ j
450 449 ralrimiva ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ ∀ e ∈ ℝ y ∀ f ∈ ℝ y ∀ g ∈ ℝ y ℕ ∀ h ∈ ℝ y ℕ ⨉ k ∈ y e ⁡ k f ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k → e L ⁡ y f ≤ sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j → ∀ a ∈ ℝ y ∪ z ∀ b ∈ ℝ y ∪ z ∀ c ∈ ℝ y ∪ z ℕ ∀ d ∈ ℝ y ∪ z ℕ ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ y ∪ z b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y ∪ z d ⁡ j
451 177 229 450 syl2anc ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ ∀ a ∈ ℝ y ∀ b ∈ ℝ y ∀ c ∈ ℝ y ℕ ∀ d ∈ ℝ y ℕ ⨉ k ∈ y a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ y b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y d ⁡ j → ∀ a ∈ ℝ y ∪ z ∀ b ∈ ℝ y ∪ z ∀ c ∈ ℝ y ∪ z ℕ ∀ d ∈ ℝ y ∪ z ℕ ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ y ∪ z b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y ∪ z d ⁡ j
452 451 ex ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y → ∀ a ∈ ℝ y ∀ b ∈ ℝ y ∀ c ∈ ℝ y ℕ ∀ d ∈ ℝ y ℕ ⨉ k ∈ y a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ y b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y d ⁡ j → ∀ a ∈ ℝ y ∪ z ∀ b ∈ ℝ y ∪ z ∀ c ∈ ℝ y ∪ z ℕ ∀ d ∈ ℝ y ∪ z ℕ ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ y ∪ z b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y ∪ z d ⁡ j
453 51 76 101 126 176 452 2 findcard2d ⊢ φ → ∀ a ∈ ℝ X ∀ b ∈ ℝ X ∀ c ∈ ℝ X ℕ ∀ d ∈ ℝ X ℕ ⨉ k ∈ X a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ X b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ X d ⁡ j
454 fveq1 ⊢ a = A → a ⁡ k = A ⁡ k
455 454 oveq1d ⊢ a = A → a ⁡ k b ⁡ k = A ⁡ k b ⁡ k
456 455 ixpeq2dv ⊢ a = A → ⨉ k ∈ X a ⁡ k b ⁡ k = ⨉ k ∈ X A ⁡ k b ⁡ k
457 456 sseq1d ⊢ a = A → ⨉ k ∈ X a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X c ⁡ j ⁡ k d ⁡ j ⁡ k ↔ ⨉ k ∈ X A ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X c ⁡ j ⁡ k d ⁡ j ⁡ k
458 oveq1 ⊢ a = A → a L ⁡ X b = A L ⁡ X b
459 458 breq1d ⊢ a = A → a L ⁡ X b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ X d ⁡ j ↔ A L ⁡ X b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ X d ⁡ j
460 457 459 imbi12d ⊢ a = A → ⨉ k ∈ X a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ X b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ X d ⁡ j ↔ ⨉ k ∈ X A ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X c ⁡ j ⁡ k d ⁡ j ⁡ k → A L ⁡ X b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ X d ⁡ j
461 460 ralbidv ⊢ a = A → ∀ d ∈ ℝ X ℕ ⨉ k ∈ X a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ X b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ X d ⁡ j ↔ ∀ d ∈ ℝ X ℕ ⨉ k ∈ X A ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X c ⁡ j ⁡ k d ⁡ j ⁡ k → A L ⁡ X b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ X d ⁡ j
462 461 ralbidv ⊢ a = A → ∀ c ∈ ℝ X ℕ ∀ d ∈ ℝ X ℕ ⨉ k ∈ X a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ X b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ X d ⁡ j ↔ ∀ c ∈ ℝ X ℕ ∀ d ∈ ℝ X ℕ ⨉ k ∈ X A ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X c ⁡ j ⁡ k d ⁡ j ⁡ k → A L ⁡ X b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ X d ⁡ j
463 462 ralbidv ⊢ a = A → ∀ b ∈ ℝ X ∀ c ∈ ℝ X ℕ ∀ d ∈ ℝ X ℕ ⨉ k ∈ X a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ X b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ X d ⁡ j ↔ ∀ b ∈ ℝ X ∀ c ∈ ℝ X ℕ ∀ d ∈ ℝ X ℕ ⨉ k ∈ X A ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X c ⁡ j ⁡ k d ⁡ j ⁡ k → A L ⁡ X b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ X d ⁡ j
464 463 rspcva ⊢ A ∈ ℝ X ∧ ∀ a ∈ ℝ X ∀ b ∈ ℝ X ∀ c ∈ ℝ X ℕ ∀ d ∈ ℝ X ℕ ⨉ k ∈ X a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X c ⁡ j ⁡ k d ⁡ j ⁡ k → a L ⁡ X b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ X d ⁡ j → ∀ b ∈ ℝ X ∀ c ∈ ℝ X ℕ ∀ d ∈ ℝ X ℕ ⨉ k ∈ X A ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X c ⁡ j ⁡ k d ⁡ j ⁡ k → A L ⁡ X b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ X d ⁡ j
465 26 453 464 syl2anc ⊢ φ → ∀ b ∈ ℝ X ∀ c ∈ ℝ X ℕ ∀ d ∈ ℝ X ℕ ⨉ k ∈ X A ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X c ⁡ j ⁡ k d ⁡ j ⁡ k → A L ⁡ X b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ X d ⁡ j
466 fveq1 ⊢ b = B → b ⁡ k = B ⁡ k
467 466 oveq2d ⊢ b = B → A ⁡ k b ⁡ k = A ⁡ k B ⁡ k
468 467 ixpeq2dv ⊢ b = B → ⨉ k ∈ X A ⁡ k b ⁡ k = ⨉ k ∈ X A ⁡ k B ⁡ k
469 468 sseq1d ⊢ b = B → ⨉ k ∈ X A ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X c ⁡ j ⁡ k d ⁡ j ⁡ k ↔ ⨉ k ∈ X A ⁡ k B ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X c ⁡ j ⁡ k d ⁡ j ⁡ k
470 oveq2 ⊢ b = B → A L ⁡ X b = A L ⁡ X B
471 470 breq1d ⊢ b = B → A L ⁡ X b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ X d ⁡ j ↔ A L ⁡ X B ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ X d ⁡ j
472 469 471 imbi12d ⊢ b = B → ⨉ k ∈ X A ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X c ⁡ j ⁡ k d ⁡ j ⁡ k → A L ⁡ X b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ X d ⁡ j ↔ ⨉ k ∈ X A ⁡ k B ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X c ⁡ j ⁡ k d ⁡ j ⁡ k → A L ⁡ X B ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ X d ⁡ j
473 472 ralbidv ⊢ b = B → ∀ d ∈ ℝ X ℕ ⨉ k ∈ X A ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X c ⁡ j ⁡ k d ⁡ j ⁡ k → A L ⁡ X b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ X d ⁡ j ↔ ∀ d ∈ ℝ X ℕ ⨉ k ∈ X A ⁡ k B ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X c ⁡ j ⁡ k d ⁡ j ⁡ k → A L ⁡ X B ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ X d ⁡ j
474 473 ralbidv ⊢ b = B → ∀ c ∈ ℝ X ℕ ∀ d ∈ ℝ X ℕ ⨉ k ∈ X A ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X c ⁡ j ⁡ k d ⁡ j ⁡ k → A L ⁡ X b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ X d ⁡ j ↔ ∀ c ∈ ℝ X ℕ ∀ d ∈ ℝ X ℕ ⨉ k ∈ X A ⁡ k B ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X c ⁡ j ⁡ k d ⁡ j ⁡ k → A L ⁡ X B ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ X d ⁡ j
475 474 rspcva ⊢ B ∈ ℝ X ∧ ∀ b ∈ ℝ X ∀ c ∈ ℝ X ℕ ∀ d ∈ ℝ X ℕ ⨉ k ∈ X A ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X c ⁡ j ⁡ k d ⁡ j ⁡ k → A L ⁡ X b ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ X d ⁡ j → ∀ c ∈ ℝ X ℕ ∀ d ∈ ℝ X ℕ ⨉ k ∈ X A ⁡ k B ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X c ⁡ j ⁡ k d ⁡ j ⁡ k → A L ⁡ X B ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ X d ⁡ j
476 23 465 475 syl2anc ⊢ φ → ∀ c ∈ ℝ X ℕ ∀ d ∈ ℝ X ℕ ⨉ k ∈ X A ⁡ k B ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X c ⁡ j ⁡ k d ⁡ j ⁡ k → A L ⁡ X B ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ X d ⁡ j
477 fveq1 ⊢ c = C → c ⁡ j = C ⁡ j
478 477 fveq1d ⊢ c = C → c ⁡ j ⁡ k = C ⁡ j ⁡ k
479 478 oveq1d ⊢ c = C → c ⁡ j ⁡ k d ⁡ j ⁡ k = C ⁡ j ⁡ k d ⁡ j ⁡ k
480 479 ixpeq2dv ⊢ c = C → ⨉ k ∈ X c ⁡ j ⁡ k d ⁡ j ⁡ k = ⨉ k ∈ X C ⁡ j ⁡ k d ⁡ j ⁡ k
481 480 adantr ⊢ c = C ∧ j ∈ ℕ → ⨉ k ∈ X c ⁡ j ⁡ k d ⁡ j ⁡ k = ⨉ k ∈ X C ⁡ j ⁡ k d ⁡ j ⁡ k
482 481 iuneq2dv ⊢ c = C → ⋃ j ∈ ℕ ⨉ k ∈ X c ⁡ j ⁡ k d ⁡ j ⁡ k = ⋃ j ∈ ℕ ⨉ k ∈ X C ⁡ j ⁡ k d ⁡ j ⁡ k
483 482 sseq2d ⊢ c = C → ⨉ k ∈ X A ⁡ k B ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X c ⁡ j ⁡ k d ⁡ j ⁡ k ↔ ⨉ k ∈ X A ⁡ k B ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X C ⁡ j ⁡ k d ⁡ j ⁡ k
484 477 oveq1d ⊢ c = C → c ⁡ j L ⁡ X d ⁡ j = C ⁡ j L ⁡ X d ⁡ j
485 484 mpteq2dv ⊢ c = C → j ∈ ℕ ⟼ c ⁡ j L ⁡ X d ⁡ j = j ∈ ℕ ⟼ C ⁡ j L ⁡ X d ⁡ j
486 485 fveq2d ⊢ c = C → sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ X d ⁡ j = sum^ ⁡ j ∈ ℕ ⟼ C ⁡ j L ⁡ X d ⁡ j
487 486 breq2d ⊢ c = C → A L ⁡ X B ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ X d ⁡ j ↔ A L ⁡ X B ≤ sum^ ⁡ j ∈ ℕ ⟼ C ⁡ j L ⁡ X d ⁡ j
488 483 487 imbi12d ⊢ c = C → ⨉ k ∈ X A ⁡ k B ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X c ⁡ j ⁡ k d ⁡ j ⁡ k → A L ⁡ X B ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ X d ⁡ j ↔ ⨉ k ∈ X A ⁡ k B ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X C ⁡ j ⁡ k d ⁡ j ⁡ k → A L ⁡ X B ≤ sum^ ⁡ j ∈ ℕ ⟼ C ⁡ j L ⁡ X d ⁡ j
489 488 ralbidv ⊢ c = C → ∀ d ∈ ℝ X ℕ ⨉ k ∈ X A ⁡ k B ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X c ⁡ j ⁡ k d ⁡ j ⁡ k → A L ⁡ X B ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ X d ⁡ j ↔ ∀ d ∈ ℝ X ℕ ⨉ k ∈ X A ⁡ k B ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X C ⁡ j ⁡ k d ⁡ j ⁡ k → A L ⁡ X B ≤ sum^ ⁡ j ∈ ℕ ⟼ C ⁡ j L ⁡ X d ⁡ j
490 489 rspcva ⊢ C ∈ ℝ X ℕ ∧ ∀ c ∈ ℝ X ℕ ∀ d ∈ ℝ X ℕ ⨉ k ∈ X A ⁡ k B ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X c ⁡ j ⁡ k d ⁡ j ⁡ k → A L ⁡ X B ≤ sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ X d ⁡ j → ∀ d ∈ ℝ X ℕ ⨉ k ∈ X A ⁡ k B ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X C ⁡ j ⁡ k d ⁡ j ⁡ k → A L ⁡ X B ≤ sum^ ⁡ j ∈ ℕ ⟼ C ⁡ j L ⁡ X d ⁡ j
491 17 476 490 syl2anc ⊢ φ → ∀ d ∈ ℝ X ℕ ⨉ k ∈ X A ⁡ k B ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X C ⁡ j ⁡ k d ⁡ j ⁡ k → A L ⁡ X B ≤ sum^ ⁡ j ∈ ℕ ⟼ C ⁡ j L ⁡ X d ⁡ j
492 fveq1 ⊢ d = D → d ⁡ j = D ⁡ j
493 492 fveq1d ⊢ d = D → d ⁡ j ⁡ k = D ⁡ j ⁡ k
494 493 oveq2d ⊢ d = D → C ⁡ j ⁡ k d ⁡ j ⁡ k = C ⁡ j ⁡ k D ⁡ j ⁡ k
495 494 ixpeq2dv ⊢ d = D → ⨉ k ∈ X C ⁡ j ⁡ k d ⁡ j ⁡ k = ⨉ k ∈ X C ⁡ j ⁡ k D ⁡ j ⁡ k
496 495 adantr ⊢ d = D ∧ j ∈ ℕ → ⨉ k ∈ X C ⁡ j ⁡ k d ⁡ j ⁡ k = ⨉ k ∈ X C ⁡ j ⁡ k D ⁡ j ⁡ k
497 496 iuneq2dv ⊢ d = D → ⋃ j ∈ ℕ ⨉ k ∈ X C ⁡ j ⁡ k d ⁡ j ⁡ k = ⋃ j ∈ ℕ ⨉ k ∈ X C ⁡ j ⁡ k D ⁡ j ⁡ k
498 497 sseq2d ⊢ d = D → ⨉ k ∈ X A ⁡ k B ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X C ⁡ j ⁡ k d ⁡ j ⁡ k ↔ ⨉ k ∈ X A ⁡ k B ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X C ⁡ j ⁡ k D ⁡ j ⁡ k
499 492 oveq2d ⊢ d = D → C ⁡ j L ⁡ X d ⁡ j = C ⁡ j L ⁡ X D ⁡ j
500 499 mpteq2dv ⊢ d = D → j ∈ ℕ ⟼ C ⁡ j L ⁡ X d ⁡ j = j ∈ ℕ ⟼ C ⁡ j L ⁡ X D ⁡ j
501 500 fveq2d ⊢ d = D → sum^ ⁡ j ∈ ℕ ⟼ C ⁡ j L ⁡ X d ⁡ j = sum^ ⁡ j ∈ ℕ ⟼ C ⁡ j L ⁡ X D ⁡ j
502 501 breq2d ⊢ d = D → A L ⁡ X B ≤ sum^ ⁡ j ∈ ℕ ⟼ C ⁡ j L ⁡ X d ⁡ j ↔ A L ⁡ X B ≤ sum^ ⁡ j ∈ ℕ ⟼ C ⁡ j L ⁡ X D ⁡ j
503 498 502 imbi12d ⊢ d = D → ⨉ k ∈ X A ⁡ k B ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X C ⁡ j ⁡ k d ⁡ j ⁡ k → A L ⁡ X B ≤ sum^ ⁡ j ∈ ℕ ⟼ C ⁡ j L ⁡ X d ⁡ j ↔ ⨉ k ∈ X A ⁡ k B ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X C ⁡ j ⁡ k D ⁡ j ⁡ k → A L ⁡ X B ≤ sum^ ⁡ j ∈ ℕ ⟼ C ⁡ j L ⁡ X D ⁡ j
504 503 rspcva ⊢ D ∈ ℝ X ℕ ∧ ∀ d ∈ ℝ X ℕ ⨉ k ∈ X A ⁡ k B ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X C ⁡ j ⁡ k d ⁡ j ⁡ k → A L ⁡ X B ≤ sum^ ⁡ j ∈ ℕ ⟼ C ⁡ j L ⁡ X d ⁡ j → ⨉ k ∈ X A ⁡ k B ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X C ⁡ j ⁡ k D ⁡ j ⁡ k → A L ⁡ X B ≤ sum^ ⁡ j ∈ ℕ ⟼ C ⁡ j L ⁡ X D ⁡ j
505 14 491 504 syl2anc ⊢ φ → ⨉ k ∈ X A ⁡ k B ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ X C ⁡ j ⁡ k D ⁡ j ⁡ k → A L ⁡ X B ≤ sum^ ⁡ j ∈ ℕ ⟼ C ⁡ j L ⁡ X D ⁡ j
506 7 505 mpd ⊢ φ → A L ⁡ X B ≤ sum^ ⁡ j ∈ ℕ ⟼ C ⁡ j L ⁡ X D ⁡ j