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 0fi ⊢ ∅ ∈ 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 sselid ⊢ 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 bilani ⊢ φ ∧ 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
229 simplll ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ a ∈ ℝ y ∪ z ∧ y = ∅ → φ
230 eldifi ⊢ z ∈ X ∖ y → z ∈ X
231 230 adantl ⊢ φ ∧ z ∈ X ∖ y → z ∈ X
232 231 adantrl ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y → z ∈ X
233 232 ad2antrr ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ a ∈ ℝ y ∪ z ∧ y = ∅ → z ∈ X
234 simpl ⊢ a ∈ ℝ y ∪ z ∧ y = ∅ → a ∈ ℝ y ∪ z
235 uneq1 ⊢ y = ∅ → y ∪ z = ∅ ∪ z
236 0un ⊢ ∅ ∪ z = z
237 236 a1i ⊢ y = ∅ → ∅ ∪ z = z
238 235 237 eqtr2d ⊢ y = ∅ → z = y ∪ z
239 238 eqcomd ⊢ y = ∅ → y ∪ z = z
240 239 oveq2d ⊢ y = ∅ → ℝ y ∪ z = ℝ z
241 240 adantl ⊢ a ∈ ℝ y ∪ z ∧ y = ∅ → ℝ y ∪ z = ℝ z
242 234 241 eleqtrd ⊢ a ∈ ℝ y ∪ z ∧ y = ∅ → a ∈ ℝ z
243 242 adantll ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ a ∈ ℝ y ∪ z ∧ y = ∅ → a ∈ ℝ z
244 229 233 243 jca31 ⊢ φ ∧ y ⊆ X ∧ z ∈ X ∖ y ∧ a ∈ ℝ y ∪ z ∧ y = ∅ → φ ∧ z ∈ X ∧ a ∈ ℝ z
245 244 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
246 245 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
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 ∧ c ∈ ℝ y ∪ z ℕ ∧ y = ∅ → φ ∧ z ∈ X ∧ a ∈ ℝ z
248 simpl ⊢ b ∈ ℝ y ∪ z ∧ y = ∅ → b ∈ ℝ y ∪ z
249 240 adantl ⊢ b ∈ ℝ y ∪ z ∧ y = ∅ → ℝ y ∪ z = ℝ z
250 248 249 eleqtrd ⊢ b ∈ ℝ y ∪ z ∧ y = ∅ → b ∈ ℝ z
251 250 adantlr ⊢ b ∈ ℝ y ∪ z ∧ c ∈ ℝ y ∪ z ℕ ∧ y = ∅ → b ∈ ℝ z
252 251 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
253 simpl ⊢ c ∈ ℝ y ∪ z ℕ ∧ y = ∅ → c ∈ ℝ y ∪ z ℕ
254 240 oveq1d ⊢ y = ∅ → ℝ y ∪ z ℕ = ℝ z ℕ
255 254 adantl ⊢ c ∈ ℝ y ∪ z ℕ ∧ y = ∅ → ℝ y ∪ z ℕ = ℝ z ℕ
256 253 255 eleqtrd ⊢ c ∈ ℝ y ∪ z ℕ ∧ y = ∅ → c ∈ ℝ z ℕ
257 256 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 ℕ
258 247 252 257 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 ℕ
259 258 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 ℕ
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 ℕ ∧ ⨉ 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 ℕ
261 simpl ⊢ d ∈ ℝ y ∪ z ℕ ∧ y = ∅ → d ∈ ℝ y ∪ z ℕ
262 254 adantl ⊢ d ∈ ℝ y ∪ z ℕ ∧ y = ∅ → ℝ y ∪ z ℕ = ℝ z ℕ
263 261 262 eleqtrd ⊢ d ∈ ℝ y ∪ z ℕ ∧ y = ∅ → d ∈ ℝ z ℕ
264 263 adantlr ⊢ d ∈ ℝ y ∪ z ℕ ∧ ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k ⊆ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k ∧ y = ∅ → d ∈ ℝ z ℕ
265 264 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 ℕ
266 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
267 238 ixpeq1d ⊢ y = ∅ → ⨉ k ∈ z a ⁡ k b ⁡ k = ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k
268 267 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
269 238 ixpeq1d ⊢ y = ∅ → ⨉ k ∈ z c ⁡ i ⁡ k d ⁡ i ⁡ k = ⨉ k ∈ y ∪ z c ⁡ i ⁡ k d ⁡ i ⁡ k
270 269 adantr ⊢ y = ∅ ∧ i ∈ ℕ → ⨉ k ∈ z c ⁡ i ⁡ k d ⁡ i ⁡ k = ⨉ k ∈ y ∪ z c ⁡ i ⁡ k d ⁡ i ⁡ k
271 270 iuneq2dv ⊢ y = ∅ → ⋃ i ∈ ℕ ⨉ k ∈ z c ⁡ i ⁡ k d ⁡ i ⁡ k = ⋃ i ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ i ⁡ k d ⁡ i ⁡ k
272 fveq2 ⊢ i = j → c ⁡ i = c ⁡ j
273 272 fveq1d ⊢ i = j → c ⁡ i ⁡ k = c ⁡ j ⁡ k
274 fveq2 ⊢ i = j → d ⁡ i = d ⁡ j
275 274 fveq1d ⊢ i = j → d ⁡ i ⁡ k = d ⁡ j ⁡ k
276 273 275 oveq12d ⊢ i = j → c ⁡ i ⁡ k d ⁡ i ⁡ k = c ⁡ j ⁡ k d ⁡ j ⁡ k
277 276 ixpeq2dv ⊢ i = j → ⨉ k ∈ y ∪ z c ⁡ i ⁡ k d ⁡ i ⁡ k = ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k
278 277 cbviunv ⊢ ⋃ i ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ i ⁡ k d ⁡ i ⁡ k = ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k
279 278 a1i ⊢ y = ∅ → ⋃ i ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ i ⁡ k d ⁡ i ⁡ k = ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k
280 271 279 eqtrd ⊢ y = ∅ → ⋃ i ∈ ℕ ⨉ k ∈ z c ⁡ i ⁡ k d ⁡ i ⁡ k = ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k
281 280 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
282 268 281 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
283 266 282 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
284 283 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
285 260 265 284 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
286 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 = ∅
287 fveq1 ⊢ a = u → a ⁡ k = u ⁡ k
288 287 oveq1d ⊢ a = u → a ⁡ k b ⁡ k = u ⁡ k b ⁡ k
289 288 fveq2d ⊢ a = u → vol ⁡ a ⁡ k b ⁡ k = vol ⁡ u ⁡ k b ⁡ k
290 289 prodeq2ad ⊢ a = u → ∏ k ∈ x vol ⁡ a ⁡ k b ⁡ k = ∏ k ∈ x vol ⁡ u ⁡ k b ⁡ k
291 290 ifeq2d ⊢ a = u → if x = ∅ 0 ∏ k ∈ x vol ⁡ a ⁡ k b ⁡ k = if x = ∅ 0 ∏ k ∈ x vol ⁡ u ⁡ k b ⁡ k
292 fveq2 ⊢ k = l → u ⁡ k = u ⁡ l
293 fveq2 ⊢ k = l → b ⁡ k = b ⁡ l
294 292 293 oveq12d ⊢ k = l → u ⁡ k b ⁡ k = u ⁡ l b ⁡ l
295 294 fveq2d ⊢ k = l → vol ⁡ u ⁡ k b ⁡ k = vol ⁡ u ⁡ l b ⁡ l
296 295 cbvprodv ⊢ ∏ k ∈ x vol ⁡ u ⁡ k b ⁡ k = ∏ l ∈ x vol ⁡ u ⁡ l b ⁡ l
297 296 a1i ⊢ b = v → ∏ k ∈ x vol ⁡ u ⁡ k b ⁡ k = ∏ l ∈ x vol ⁡ u ⁡ l b ⁡ l
298 fveq1 ⊢ b = v → b ⁡ l = v ⁡ l
299 298 oveq2d ⊢ b = v → u ⁡ l b ⁡ l = u ⁡ l v ⁡ l
300 299 fveq2d ⊢ b = v → vol ⁡ u ⁡ l b ⁡ l = vol ⁡ u ⁡ l v ⁡ l
301 300 prodeq2ad ⊢ b = v → ∏ l ∈ x vol ⁡ u ⁡ l b ⁡ l = ∏ l ∈ x vol ⁡ u ⁡ l v ⁡ l
302 297 301 eqtrd ⊢ b = v → ∏ k ∈ x vol ⁡ u ⁡ k b ⁡ k = ∏ l ∈ x vol ⁡ u ⁡ l v ⁡ l
303 302 ifeq2d ⊢ b = v → if x = ∅ 0 ∏ k ∈ x vol ⁡ u ⁡ k b ⁡ k = if x = ∅ 0 ∏ l ∈ x vol ⁡ u ⁡ l v ⁡ l
304 291 303 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
305 304 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
306 1 305 eqtri ⊢ L = x ∈ Fin ⟼ u ∈ ℝ x , v ∈ ℝ x ⟼ if x = ∅ 0 ∏ l ∈ x vol ⁡ u ⁡ l v ⁡ l
307 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
308 eqid ⊢ z = z
309 elmapi ⊢ a ∈ ℝ z → a : z ⟶ ℝ
310 309 ad2antlr ⊢ φ ∧ z ∈ X ∧ a ∈ ℝ z ∧ b ∈ ℝ z → a : z ⟶ ℝ
311 310 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 ⟶ ℝ
312 elmapi ⊢ b ∈ ℝ z → b : z ⟶ ℝ
313 312 adantl ⊢ φ ∧ z ∈ X ∧ a ∈ ℝ z ∧ b ∈ ℝ z → b : z ⟶ ℝ
314 313 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 ⟶ ℝ
315 elmapi ⊢ c ∈ ℝ z ℕ → c : ℕ ⟶ ℝ z
316 315 adantl ⊢ φ ∧ z ∈ X ∧ a ∈ ℝ z ∧ b ∈ ℝ z ∧ c ∈ ℝ z ℕ → c : ℕ ⟶ ℝ z
317 316 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
318 elmapi ⊢ d ∈ ℝ z ℕ → d : ℕ ⟶ ℝ z
319 318 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
320 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
321 fveq2 ⊢ k = l → a ⁡ k = a ⁡ l
322 321 293 oveq12d ⊢ k = l → a ⁡ k b ⁡ k = a ⁡ l b ⁡ l
323 eqcom ⊢ k = l ↔ l = k
324 323 imbi1i ⊢ k = l → a ⁡ k b ⁡ k = a ⁡ l b ⁡ l ↔ l = k → a ⁡ k b ⁡ k = a ⁡ l b ⁡ l
325 eqcom ⊢ a ⁡ k b ⁡ k = a ⁡ l b ⁡ l ↔ a ⁡ l b ⁡ l = a ⁡ k b ⁡ k
326 325 imbi2i ⊢ l = k → a ⁡ k b ⁡ k = a ⁡ l b ⁡ l ↔ l = k → a ⁡ l b ⁡ l = a ⁡ k b ⁡ k
327 324 326 bitri ⊢ k = l → a ⁡ k b ⁡ k = a ⁡ l b ⁡ l ↔ l = k → a ⁡ l b ⁡ l = a ⁡ k b ⁡ k
328 322 327 mpbi ⊢ l = k → a ⁡ l b ⁡ l = a ⁡ k b ⁡ k
329 328 cbvixpv ⊢ ⨉ l ∈ z a ⁡ l b ⁡ l = ⨉ k ∈ z a ⁡ k b ⁡ k
330 329 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
331 276 ixpeq2dv ⊢ i = j → ⨉ k ∈ z c ⁡ i ⁡ k d ⁡ i ⁡ k = ⨉ k ∈ z c ⁡ j ⁡ k d ⁡ j ⁡ k
332 331 cbviunv ⊢ ⋃ i ∈ ℕ ⨉ k ∈ z c ⁡ i ⁡ k d ⁡ i ⁡ k = ⋃ j ∈ ℕ ⨉ k ∈ z c ⁡ j ⁡ k d ⁡ j ⁡ k
333 fveq2 ⊢ k = l → c ⁡ j ⁡ k = c ⁡ j ⁡ l
334 fveq2 ⊢ k = l → d ⁡ j ⁡ k = d ⁡ j ⁡ l
335 333 334 oveq12d ⊢ k = l → c ⁡ j ⁡ k d ⁡ j ⁡ k = c ⁡ j ⁡ l d ⁡ j ⁡ l
336 335 cbvixpv ⊢ ⨉ k ∈ z c ⁡ j ⁡ k d ⁡ j ⁡ k = ⨉ l ∈ z c ⁡ j ⁡ l d ⁡ j ⁡ l
337 336 a1i ⊢ j ∈ ℕ → ⨉ k ∈ z c ⁡ j ⁡ k d ⁡ j ⁡ k = ⨉ l ∈ z c ⁡ j ⁡ l d ⁡ j ⁡ l
338 337 iuneq2i ⊢ ⋃ j ∈ ℕ ⨉ k ∈ z c ⁡ j ⁡ k d ⁡ j ⁡ k = ⋃ j ∈ ℕ ⨉ l ∈ z c ⁡ j ⁡ l d ⁡ j ⁡ l
339 332 338 eqtr2i ⊢ ⋃ j ∈ ℕ ⨉ l ∈ z c ⁡ j ⁡ l d ⁡ j ⁡ l = ⋃ i ∈ ℕ ⨉ k ∈ z c ⁡ i ⁡ k d ⁡ i ⁡ k
340 339 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
341 330 340 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
342 320 341 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
343 342 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
344 306 307 308 311 314 317 319 343 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
345 344 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
346 235 237 eqtrd ⊢ y = ∅ → y ∪ z = z
347 346 fveq2d ⊢ y = ∅ → L ⁡ y ∪ z = L ⁡ z
348 347 oveqd ⊢ y = ∅ → a L ⁡ y ∪ z b = a L ⁡ z b
349 348 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
350 347 oveqd ⊢ y = ∅ → c ⁡ j L ⁡ y ∪ z d ⁡ j = c ⁡ j L ⁡ z d ⁡ j
351 350 mpteq2dv ⊢ y = ∅ → j ∈ ℕ ⟼ c ⁡ j L ⁡ y ∪ z d ⁡ j = j ∈ ℕ ⟼ c ⁡ j L ⁡ z d ⁡ j
352 351 fveq2d ⊢ y = ∅ → sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y ∪ z d ⁡ j = sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ z d ⁡ j
353 352 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
354 349 353 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
355 345 354 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
356 285 286 355 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
357 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
358 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
359 358 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 ℕ → y ⊆ X
360 359 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 = ∅ → y ⊆ X
361 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
362 361 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 ℕ → z ∈ X ∖ y
363 362 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 = ∅ → z ∈ X ∖ y
364 eqid ⊢ y ∪ z = y ∪ z
365 elmapi ⊢ a ∈ ℝ y ∪ z → a : y ∪ z ⟶ ℝ
366 365 adantr ⊢ a ∈ ℝ y ∪ z ∧ b ∈ ℝ y ∪ z → a : y ∪ z ⟶ ℝ
367 366 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 ⟶ ℝ
368 367 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 ⟶ ℝ
369 elmapi ⊢ b ∈ ℝ y ∪ z → b : y ∪ z ⟶ ℝ
370 369 adantl ⊢ a ∈ ℝ y ∪ z ∧ b ∈ ℝ y ∪ z → b : y ∪ z ⟶ ℝ
371 370 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 ⟶ ℝ
372 371 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 ⟶ ℝ
373 elmapi ⊢ c ∈ ℝ y ∪ z ℕ → c : ℕ ⟶ ℝ y ∪ z
374 373 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
375 374 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
376 elmapi ⊢ d ∈ ℝ y ∪ z ℕ → d : ℕ ⟶ ℝ y ∪ z
377 376 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
378 377 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
379 fveq2 ⊢ k = l → e ⁡ k = e ⁡ l
380 fveq2 ⊢ k = l → f ⁡ k = f ⁡ l
381 379 380 oveq12d ⊢ k = l → e ⁡ k f ⁡ k = e ⁡ l f ⁡ l
382 381 cbvixpv ⊢ ⨉ k ∈ y e ⁡ k f ⁡ k = ⨉ l ∈ y e ⁡ l f ⁡ l
383 382 a1i ⊢ h = o → ⨉ k ∈ y e ⁡ k f ⁡ k = ⨉ l ∈ y e ⁡ l f ⁡ l
384 fveq2 ⊢ j = i → g ⁡ j = g ⁡ i
385 384 fveq1d ⊢ j = i → g ⁡ j ⁡ k = g ⁡ i ⁡ k
386 fveq2 ⊢ j = i → h ⁡ j = h ⁡ i
387 386 fveq1d ⊢ j = i → h ⁡ j ⁡ k = h ⁡ i ⁡ k
388 385 387 oveq12d ⊢ j = i → g ⁡ j ⁡ k h ⁡ j ⁡ k = g ⁡ i ⁡ k h ⁡ i ⁡ k
389 388 ixpeq2dv ⊢ j = i → ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k = ⨉ k ∈ y g ⁡ i ⁡ k h ⁡ i ⁡ k
390 389 cbviunv ⊢ ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k = ⋃ i ∈ ℕ ⨉ k ∈ y g ⁡ i ⁡ k h ⁡ i ⁡ k
391 390 a1i ⊢ h = o → ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k = ⋃ i ∈ ℕ ⨉ k ∈ y g ⁡ i ⁡ k h ⁡ i ⁡ k
392 fveq2 ⊢ k = l → g ⁡ i ⁡ k = g ⁡ i ⁡ l
393 fveq2 ⊢ k = l → h ⁡ i ⁡ k = h ⁡ i ⁡ l
394 392 393 oveq12d ⊢ k = l → g ⁡ i ⁡ k h ⁡ i ⁡ k = g ⁡ i ⁡ l h ⁡ i ⁡ l
395 394 cbvixpv ⊢ ⨉ k ∈ y g ⁡ i ⁡ k h ⁡ i ⁡ k = ⨉ l ∈ y g ⁡ i ⁡ l h ⁡ i ⁡ l
396 395 a1i ⊢ h = o → ⨉ k ∈ y g ⁡ i ⁡ k h ⁡ i ⁡ k = ⨉ l ∈ y g ⁡ i ⁡ l h ⁡ i ⁡ l
397 fveq1 ⊢ h = o → h ⁡ i = o ⁡ i
398 397 fveq1d ⊢ h = o → h ⁡ i ⁡ l = o ⁡ i ⁡ l
399 398 oveq2d ⊢ h = o → g ⁡ i ⁡ l h ⁡ i ⁡ l = g ⁡ i ⁡ l o ⁡ i ⁡ l
400 399 ixpeq2dv ⊢ h = o → ⨉ l ∈ y g ⁡ i ⁡ l h ⁡ i ⁡ l = ⨉ l ∈ y g ⁡ i ⁡ l o ⁡ i ⁡ l
401 396 400 eqtrd ⊢ h = o → ⨉ k ∈ y g ⁡ i ⁡ k h ⁡ i ⁡ k = ⨉ l ∈ y g ⁡ i ⁡ l o ⁡ i ⁡ l
402 401 adantr ⊢ h = o ∧ i ∈ ℕ → ⨉ k ∈ y g ⁡ i ⁡ k h ⁡ i ⁡ k = ⨉ l ∈ y g ⁡ i ⁡ l o ⁡ i ⁡ l
403 402 iuneq2dv ⊢ h = o → ⋃ i ∈ ℕ ⨉ k ∈ y g ⁡ i ⁡ k h ⁡ i ⁡ k = ⋃ i ∈ ℕ ⨉ l ∈ y g ⁡ i ⁡ l o ⁡ i ⁡ l
404 391 403 eqtrd ⊢ h = o → ⋃ j ∈ ℕ ⨉ k ∈ y g ⁡ j ⁡ k h ⁡ j ⁡ k = ⋃ i ∈ ℕ ⨉ l ∈ y g ⁡ i ⁡ l o ⁡ i ⁡ l
405 383 404 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
406 384 386 oveq12d ⊢ j = i → g ⁡ j L ⁡ y h ⁡ j = g ⁡ i L ⁡ y h ⁡ i
407 406 cbvmptv ⊢ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j = i ∈ ℕ ⟼ g ⁡ i L ⁡ y h ⁡ i
408 407 a1i ⊢ h = o → j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j = i ∈ ℕ ⟼ g ⁡ i L ⁡ y h ⁡ i
409 397 oveq2d ⊢ h = o → g ⁡ i L ⁡ y h ⁡ i = g ⁡ i L ⁡ y o ⁡ i
410 409 mpteq2dv ⊢ h = o → i ∈ ℕ ⟼ g ⁡ i L ⁡ y h ⁡ i = i ∈ ℕ ⟼ g ⁡ i L ⁡ y o ⁡ i
411 408 410 eqtrd ⊢ h = o → j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j = i ∈ ℕ ⟼ g ⁡ i L ⁡ y o ⁡ i
412 411 fveq2d ⊢ h = o → sum^ ⁡ j ∈ ℕ ⟼ g ⁡ j L ⁡ y h ⁡ j = sum^ ⁡ i ∈ ℕ ⟼ g ⁡ i L ⁡ y o ⁡ i
413 412 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
414 405 413 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
415 414 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
416 415 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
417 416 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
418 417 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
419 418 bilani ⊢ φ ∧ 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
420 419 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
421 322 cbvixpv ⊢ ⨉ k ∈ y ∪ z a ⁡ k b ⁡ k = ⨉ l ∈ y ∪ z a ⁡ l b ⁡ l
422 335 cbvixpv ⊢ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k = ⨉ l ∈ y ∪ z c ⁡ j ⁡ l d ⁡ j ⁡ l
423 422 a1i ⊢ j = i → ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k = ⨉ l ∈ y ∪ z c ⁡ j ⁡ l d ⁡ j ⁡ l
424 fveq2 ⊢ j = i → c ⁡ j = c ⁡ i
425 424 fveq1d ⊢ j = i → c ⁡ j ⁡ l = c ⁡ i ⁡ l
426 fveq2 ⊢ j = i → d ⁡ j = d ⁡ i
427 426 fveq1d ⊢ j = i → d ⁡ j ⁡ l = d ⁡ i ⁡ l
428 425 427 oveq12d ⊢ j = i → c ⁡ j ⁡ l d ⁡ j ⁡ l = c ⁡ i ⁡ l d ⁡ i ⁡ l
429 428 ixpeq2dv ⊢ j = i → ⨉ l ∈ y ∪ z c ⁡ j ⁡ l d ⁡ j ⁡ l = ⨉ l ∈ y ∪ z c ⁡ i ⁡ l d ⁡ i ⁡ l
430 423 429 eqtrd ⊢ j = i → ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k = ⨉ l ∈ y ∪ z c ⁡ i ⁡ l d ⁡ i ⁡ l
431 430 cbviunv ⊢ ⋃ j ∈ ℕ ⨉ k ∈ y ∪ z c ⁡ j ⁡ k d ⁡ j ⁡ k = ⋃ i ∈ ℕ ⨉ l ∈ y ∪ z c ⁡ i ⁡ l d ⁡ i ⁡ l
432 421 431 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
433 432 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
434 433 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
435 neqne ⊢ ¬ y = ∅ → y ≠ ∅
436 435 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 ≠ ∅
437 306 357 360 363 364 368 372 375 378 420 434 436 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
438 272 274 oveq12d ⊢ i = j → c ⁡ i L ⁡ y ∪ z d ⁡ i = c ⁡ j L ⁡ y ∪ z d ⁡ j
439 438 cbvmptv ⊢ i ∈ ℕ ⟼ c ⁡ i L ⁡ y ∪ z d ⁡ i = j ∈ ℕ ⟼ c ⁡ j L ⁡ y ∪ z d ⁡ j
440 439 fveq2i ⊢ sum^ ⁡ i ∈ ℕ ⟼ c ⁡ i L ⁡ y ∪ z d ⁡ i = sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ y ∪ z d ⁡ j
441 440 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
442 437 441 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
443 356 442 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
444 443 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
445 444 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
446 445 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
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 177 228 448 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
450 449 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
451 51 76 101 126 176 450 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
452 fveq1 ⊢ a = A → a ⁡ k = A ⁡ k
453 452 oveq1d ⊢ a = A → a ⁡ k b ⁡ k = A ⁡ k b ⁡ k
454 453 ixpeq2dv ⊢ a = A → ⨉ k ∈ X a ⁡ k b ⁡ k = ⨉ k ∈ X A ⁡ k b ⁡ k
455 454 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
456 oveq1 ⊢ a = A → a L ⁡ X b = A L ⁡ X b
457 456 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
458 455 457 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
459 458 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
460 459 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
461 460 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
462 461 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
463 26 451 462 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
464 fveq1 ⊢ b = B → b ⁡ k = B ⁡ k
465 464 oveq2d ⊢ b = B → A ⁡ k b ⁡ k = A ⁡ k B ⁡ k
466 465 ixpeq2dv ⊢ b = B → ⨉ k ∈ X A ⁡ k b ⁡ k = ⨉ k ∈ X A ⁡ k B ⁡ k
467 466 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
468 oveq2 ⊢ b = B → A L ⁡ X b = A L ⁡ X B
469 468 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
470 467 469 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
471 470 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
472 471 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
473 472 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
474 23 463 473 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
475 fveq1 ⊢ c = C → c ⁡ j = C ⁡ j
476 475 fveq1d ⊢ c = C → c ⁡ j ⁡ k = C ⁡ j ⁡ k
477 476 oveq1d ⊢ c = C → c ⁡ j ⁡ k d ⁡ j ⁡ k = C ⁡ j ⁡ k d ⁡ j ⁡ k
478 477 ixpeq2dv ⊢ c = C → ⨉ k ∈ X c ⁡ j ⁡ k d ⁡ j ⁡ k = ⨉ k ∈ X C ⁡ j ⁡ k d ⁡ j ⁡ k
479 478 adantr ⊢ c = C ∧ j ∈ ℕ → ⨉ k ∈ X c ⁡ j ⁡ k d ⁡ j ⁡ k = ⨉ k ∈ X C ⁡ j ⁡ k d ⁡ j ⁡ k
480 479 iuneq2dv ⊢ c = C → ⋃ j ∈ ℕ ⨉ k ∈ X c ⁡ j ⁡ k d ⁡ j ⁡ k = ⋃ j ∈ ℕ ⨉ k ∈ X C ⁡ j ⁡ k d ⁡ j ⁡ k
481 480 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
482 475 oveq1d ⊢ c = C → c ⁡ j L ⁡ X d ⁡ j = C ⁡ j L ⁡ X d ⁡ j
483 482 mpteq2dv ⊢ c = C → j ∈ ℕ ⟼ c ⁡ j L ⁡ X d ⁡ j = j ∈ ℕ ⟼ C ⁡ j L ⁡ X d ⁡ j
484 483 fveq2d ⊢ c = C → sum^ ⁡ j ∈ ℕ ⟼ c ⁡ j L ⁡ X d ⁡ j = sum^ ⁡ j ∈ ℕ ⟼ C ⁡ j L ⁡ X d ⁡ j
485 484 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
486 481 485 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
487 486 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
488 487 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
489 17 474 488 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
490 fveq1 ⊢ d = D → d ⁡ j = D ⁡ j
491 490 fveq1d ⊢ d = D → d ⁡ j ⁡ k = D ⁡ j ⁡ k
492 491 oveq2d ⊢ d = D → C ⁡ j ⁡ k d ⁡ j ⁡ k = C ⁡ j ⁡ k D ⁡ j ⁡ k
493 492 ixpeq2dv ⊢ d = D → ⨉ k ∈ X C ⁡ j ⁡ k d ⁡ j ⁡ k = ⨉ k ∈ X C ⁡ j ⁡ k D ⁡ j ⁡ k
494 493 adantr ⊢ d = D ∧ j ∈ ℕ → ⨉ k ∈ X C ⁡ j ⁡ k d ⁡ j ⁡ k = ⨉ k ∈ X C ⁡ j ⁡ k D ⁡ j ⁡ k
495 494 iuneq2dv ⊢ d = D → ⋃ j ∈ ℕ ⨉ k ∈ X C ⁡ j ⁡ k d ⁡ j ⁡ k = ⋃ j ∈ ℕ ⨉ k ∈ X C ⁡ j ⁡ k D ⁡ j ⁡ k
496 495 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
497 490 oveq2d ⊢ d = D → C ⁡ j L ⁡ X d ⁡ j = C ⁡ j L ⁡ X D ⁡ j
498 497 mpteq2dv ⊢ d = D → j ∈ ℕ ⟼ C ⁡ j L ⁡ X d ⁡ j = j ∈ ℕ ⟼ C ⁡ j L ⁡ X D ⁡ j
499 498 fveq2d ⊢ d = D → sum^ ⁡ j ∈ ℕ ⟼ C ⁡ j L ⁡ X d ⁡ j = sum^ ⁡ j ∈ ℕ ⟼ C ⁡ j L ⁡ X D ⁡ j
500 499 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
501 496 500 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
502 501 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
503 14 489 502 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
504 7 503 mpd ⊢ φ → A L ⁡ X B ≤ sum^ ⁡ j ∈ ℕ ⟼ C ⁡ j L ⁡ X D ⁡ j