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⟼ifx=∅0∏k∈xvol⁡a⁡kb⁡k
hoidmvle.x ⊢φ→X∈Fin
hoidmvle.a ⊢φ→A:X⟶ℝ
hoidmvle.b ⊢φ→B:X⟶ℝ
hoidmvle.c ⊢φ→C:ℕ⟶ℝX
hoidmvle.d ⊢φ→D:ℕ⟶ℝX
hoidmvle.s ⊢φ→⨉k∈XA⁡kB⁡k⊆⋃j∈ℕ⨉k∈XC⁡j⁡kD⁡j⁡k
Assertion hoidmvle ⊢φ→AL⁡XB≤sum^⁡j∈ℕ⟼C⁡jL⁡XD⁡j

Proof

Step Hyp Ref Expression
1 hoidmvle.l ⊢L=x∈Fin⟼a∈ℝx,b∈ℝx⟼ifx=∅0∏k∈xvol⁡a⁡kb⁡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∈XA⁡kB⁡k⊆⋃j∈ℕ⨉k∈XC⁡j⁡kD⁡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∈xa⁡kb⁡k=⨉k∈∅a⁡kb⁡k
34 ixpeq1 ⊢x=∅→⨉k∈xc⁡j⁡kd⁡j⁡k=⨉k∈∅c⁡j⁡kd⁡j⁡k
35 34 iuneq2d ⊢x=∅→⋃j∈ℕ⨉k∈xc⁡j⁡kd⁡j⁡k=⋃j∈ℕ⨉k∈∅c⁡j⁡kd⁡j⁡k
36 33 35 sseq12d ⊢x=∅→⨉k∈xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈xc⁡j⁡kd⁡j⁡k↔⨉k∈∅a⁡kb⁡k⊆⋃j∈ℕ⨉k∈∅c⁡j⁡kd⁡j⁡k
37 fveq2 ⊢x=∅→L⁡x=L⁡∅
38 37 oveqd ⊢x=∅→aL⁡xb=aL⁡∅b
39 37 oveqd ⊢x=∅→c⁡jL⁡xd⁡j=c⁡jL⁡∅d⁡j
40 39 mpteq2dv ⊢x=∅→j∈ℕ⟼c⁡jL⁡xd⁡j=j∈ℕ⟼c⁡jL⁡∅d⁡j
41 40 fveq2d ⊢x=∅→sum^⁡j∈ℕ⟼c⁡jL⁡xd⁡j=sum^⁡j∈ℕ⟼c⁡jL⁡∅d⁡j
42 38 41 breq12d ⊢x=∅→aL⁡xb≤sum^⁡j∈ℕ⟼c⁡jL⁡xd⁡j↔aL⁡∅b≤sum^⁡j∈ℕ⟼c⁡jL⁡∅d⁡j
43 36 42 imbi12d ⊢x=∅→⨉k∈xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈xc⁡j⁡kd⁡j⁡k→aL⁡xb≤sum^⁡j∈ℕ⟼c⁡jL⁡xd⁡j↔⨉k∈∅a⁡kb⁡k⊆⋃j∈ℕ⨉k∈∅c⁡j⁡kd⁡j⁡k→aL⁡∅b≤sum^⁡j∈ℕ⟼c⁡jL⁡∅d⁡j
44 32 43 imbi12d ⊢x=∅→d∈ℝxℕ→⨉k∈xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈xc⁡j⁡kd⁡j⁡k→aL⁡xb≤sum^⁡j∈ℕ⟼c⁡jL⁡xd⁡j↔d∈ℝ∅ℕ→⨉k∈∅a⁡kb⁡k⊆⋃j∈ℕ⨉k∈∅c⁡j⁡kd⁡j⁡k→aL⁡∅b≤sum^⁡j∈ℕ⟼c⁡jL⁡∅d⁡j
45 44 ralbidv2 ⊢x=∅→∀d∈ℝxℕ⨉k∈xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈xc⁡j⁡kd⁡j⁡k→aL⁡xb≤sum^⁡j∈ℕ⟼c⁡jL⁡xd⁡j↔∀d∈ℝ∅ℕ⨉k∈∅a⁡kb⁡k⊆⋃j∈ℕ⨉k∈∅c⁡j⁡kd⁡j⁡k→aL⁡∅b≤sum^⁡j∈ℕ⟼c⁡jL⁡∅d⁡j
46 31 45 imbi12d ⊢x=∅→c∈ℝxℕ→∀d∈ℝxℕ⨉k∈xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈xc⁡j⁡kd⁡j⁡k→aL⁡xb≤sum^⁡j∈ℕ⟼c⁡jL⁡xd⁡j↔c∈ℝ∅ℕ→∀d∈ℝ∅ℕ⨉k∈∅a⁡kb⁡k⊆⋃j∈ℕ⨉k∈∅c⁡j⁡kd⁡j⁡k→aL⁡∅b≤sum^⁡j∈ℕ⟼c⁡jL⁡∅d⁡j
47 46 ralbidv2 ⊢x=∅→∀c∈ℝxℕ∀d∈ℝxℕ⨉k∈xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈xc⁡j⁡kd⁡j⁡k→aL⁡xb≤sum^⁡j∈ℕ⟼c⁡jL⁡xd⁡j↔∀c∈ℝ∅ℕ∀d∈ℝ∅ℕ⨉k∈∅a⁡kb⁡k⊆⋃j∈ℕ⨉k∈∅c⁡j⁡kd⁡j⁡k→aL⁡∅b≤sum^⁡j∈ℕ⟼c⁡jL⁡∅d⁡j
48 29 47 imbi12d ⊢x=∅→b∈ℝx→∀c∈ℝxℕ∀d∈ℝxℕ⨉k∈xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈xc⁡j⁡kd⁡j⁡k→aL⁡xb≤sum^⁡j∈ℕ⟼c⁡jL⁡xd⁡j↔b∈ℝ∅→∀c∈ℝ∅ℕ∀d∈ℝ∅ℕ⨉k∈∅a⁡kb⁡k⊆⋃j∈ℕ⨉k∈∅c⁡j⁡kd⁡j⁡k→aL⁡∅b≤sum^⁡j∈ℕ⟼c⁡jL⁡∅d⁡j
49 48 ralbidv2 ⊢x=∅→∀b∈ℝx∀c∈ℝxℕ∀d∈ℝxℕ⨉k∈xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈xc⁡j⁡kd⁡j⁡k→aL⁡xb≤sum^⁡j∈ℕ⟼c⁡jL⁡xd⁡j↔∀b∈ℝ∅∀c∈ℝ∅ℕ∀d∈ℝ∅ℕ⨉k∈∅a⁡kb⁡k⊆⋃j∈ℕ⨉k∈∅c⁡j⁡kd⁡j⁡k→aL⁡∅b≤sum^⁡j∈ℕ⟼c⁡jL⁡∅d⁡j
50 28 49 imbi12d ⊢x=∅→a∈ℝx→∀b∈ℝx∀c∈ℝxℕ∀d∈ℝxℕ⨉k∈xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈xc⁡j⁡kd⁡j⁡k→aL⁡xb≤sum^⁡j∈ℕ⟼c⁡jL⁡xd⁡j↔a∈ℝ∅→∀b∈ℝ∅∀c∈ℝ∅ℕ∀d∈ℝ∅ℕ⨉k∈∅a⁡kb⁡k⊆⋃j∈ℕ⨉k∈∅c⁡j⁡kd⁡j⁡k→aL⁡∅b≤sum^⁡j∈ℕ⟼c⁡jL⁡∅d⁡j
51 50 ralbidv2 ⊢x=∅→∀a∈ℝx∀b∈ℝx∀c∈ℝxℕ∀d∈ℝxℕ⨉k∈xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈xc⁡j⁡kd⁡j⁡k→aL⁡xb≤sum^⁡j∈ℕ⟼c⁡jL⁡xd⁡j↔∀a∈ℝ∅∀b∈ℝ∅∀c∈ℝ∅ℕ∀d∈ℝ∅ℕ⨉k∈∅a⁡kb⁡k⊆⋃j∈ℕ⨉k∈∅c⁡j⁡kd⁡j⁡k→aL⁡∅b≤sum^⁡j∈ℕ⟼c⁡jL⁡∅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∈xa⁡kb⁡k=⨉k∈ya⁡kb⁡k
59 ixpeq1 ⊢x=y→⨉k∈xc⁡j⁡kd⁡j⁡k=⨉k∈yc⁡j⁡kd⁡j⁡k
60 59 iuneq2d ⊢x=y→⋃j∈ℕ⨉k∈xc⁡j⁡kd⁡j⁡k=⋃j∈ℕ⨉k∈yc⁡j⁡kd⁡j⁡k
61 58 60 sseq12d ⊢x=y→⨉k∈xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈xc⁡j⁡kd⁡j⁡k↔⨉k∈ya⁡kb⁡k⊆⋃j∈ℕ⨉k∈yc⁡j⁡kd⁡j⁡k
62 fveq2 ⊢x=y→L⁡x=L⁡y
63 62 oveqd ⊢x=y→aL⁡xb=aL⁡yb
64 62 oveqd ⊢x=y→c⁡jL⁡xd⁡j=c⁡jL⁡yd⁡j
65 64 mpteq2dv ⊢x=y→j∈ℕ⟼c⁡jL⁡xd⁡j=j∈ℕ⟼c⁡jL⁡yd⁡j
66 65 fveq2d ⊢x=y→sum^⁡j∈ℕ⟼c⁡jL⁡xd⁡j=sum^⁡j∈ℕ⟼c⁡jL⁡yd⁡j
67 63 66 breq12d ⊢x=y→aL⁡xb≤sum^⁡j∈ℕ⟼c⁡jL⁡xd⁡j↔aL⁡yb≤sum^⁡j∈ℕ⟼c⁡jL⁡yd⁡j
68 61 67 imbi12d ⊢x=y→⨉k∈xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈xc⁡j⁡kd⁡j⁡k→aL⁡xb≤sum^⁡j∈ℕ⟼c⁡jL⁡xd⁡j↔⨉k∈ya⁡kb⁡k⊆⋃j∈ℕ⨉k∈yc⁡j⁡kd⁡j⁡k→aL⁡yb≤sum^⁡j∈ℕ⟼c⁡jL⁡yd⁡j
69 57 68 imbi12d ⊢x=y→d∈ℝxℕ→⨉k∈xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈xc⁡j⁡kd⁡j⁡k→aL⁡xb≤sum^⁡j∈ℕ⟼c⁡jL⁡xd⁡j↔d∈ℝyℕ→⨉k∈ya⁡kb⁡k⊆⋃j∈ℕ⨉k∈yc⁡j⁡kd⁡j⁡k→aL⁡yb≤sum^⁡j∈ℕ⟼c⁡jL⁡yd⁡j
70 69 ralbidv2 ⊢x=y→∀d∈ℝxℕ⨉k∈xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈xc⁡j⁡kd⁡j⁡k→aL⁡xb≤sum^⁡j∈ℕ⟼c⁡jL⁡xd⁡j↔∀d∈ℝyℕ⨉k∈ya⁡kb⁡k⊆⋃j∈ℕ⨉k∈yc⁡j⁡kd⁡j⁡k→aL⁡yb≤sum^⁡j∈ℕ⟼c⁡jL⁡yd⁡j
71 56 70 imbi12d ⊢x=y→c∈ℝxℕ→∀d∈ℝxℕ⨉k∈xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈xc⁡j⁡kd⁡j⁡k→aL⁡xb≤sum^⁡j∈ℕ⟼c⁡jL⁡xd⁡j↔c∈ℝyℕ→∀d∈ℝyℕ⨉k∈ya⁡kb⁡k⊆⋃j∈ℕ⨉k∈yc⁡j⁡kd⁡j⁡k→aL⁡yb≤sum^⁡j∈ℕ⟼c⁡jL⁡yd⁡j
72 71 ralbidv2 ⊢x=y→∀c∈ℝxℕ∀d∈ℝxℕ⨉k∈xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈xc⁡j⁡kd⁡j⁡k→aL⁡xb≤sum^⁡j∈ℕ⟼c⁡jL⁡xd⁡j↔∀c∈ℝyℕ∀d∈ℝyℕ⨉k∈ya⁡kb⁡k⊆⋃j∈ℕ⨉k∈yc⁡j⁡kd⁡j⁡k→aL⁡yb≤sum^⁡j∈ℕ⟼c⁡jL⁡yd⁡j
73 54 72 imbi12d ⊢x=y→b∈ℝx→∀c∈ℝxℕ∀d∈ℝxℕ⨉k∈xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈xc⁡j⁡kd⁡j⁡k→aL⁡xb≤sum^⁡j∈ℕ⟼c⁡jL⁡xd⁡j↔b∈ℝy→∀c∈ℝyℕ∀d∈ℝyℕ⨉k∈ya⁡kb⁡k⊆⋃j∈ℕ⨉k∈yc⁡j⁡kd⁡j⁡k→aL⁡yb≤sum^⁡j∈ℕ⟼c⁡jL⁡yd⁡j
74 73 ralbidv2 ⊢x=y→∀b∈ℝx∀c∈ℝxℕ∀d∈ℝxℕ⨉k∈xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈xc⁡j⁡kd⁡j⁡k→aL⁡xb≤sum^⁡j∈ℕ⟼c⁡jL⁡xd⁡j↔∀b∈ℝy∀c∈ℝyℕ∀d∈ℝyℕ⨉k∈ya⁡kb⁡k⊆⋃j∈ℕ⨉k∈yc⁡j⁡kd⁡j⁡k→aL⁡yb≤sum^⁡j∈ℕ⟼c⁡jL⁡yd⁡j
75 53 74 imbi12d ⊢x=y→a∈ℝx→∀b∈ℝx∀c∈ℝxℕ∀d∈ℝxℕ⨉k∈xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈xc⁡j⁡kd⁡j⁡k→aL⁡xb≤sum^⁡j∈ℕ⟼c⁡jL⁡xd⁡j↔a∈ℝy→∀b∈ℝy∀c∈ℝyℕ∀d∈ℝyℕ⨉k∈ya⁡kb⁡k⊆⋃j∈ℕ⨉k∈yc⁡j⁡kd⁡j⁡k→aL⁡yb≤sum^⁡j∈ℕ⟼c⁡jL⁡yd⁡j
76 75 ralbidv2 ⊢x=y→∀a∈ℝx∀b∈ℝx∀c∈ℝxℕ∀d∈ℝxℕ⨉k∈xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈xc⁡j⁡kd⁡j⁡k→aL⁡xb≤sum^⁡j∈ℕ⟼c⁡jL⁡xd⁡j↔∀a∈ℝy∀b∈ℝy∀c∈ℝyℕ∀d∈ℝyℕ⨉k∈ya⁡kb⁡k⊆⋃j∈ℕ⨉k∈yc⁡j⁡kd⁡j⁡k→aL⁡yb≤sum^⁡j∈ℕ⟼c⁡jL⁡yd⁡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∈xa⁡kb⁡k=⨉k∈y∪za⁡kb⁡k
84 ixpeq1 ⊢x=y∪z→⨉k∈xc⁡j⁡kd⁡j⁡k=⨉k∈y∪zc⁡j⁡kd⁡j⁡k
85 84 iuneq2d ⊢x=y∪z→⋃j∈ℕ⨉k∈xc⁡j⁡kd⁡j⁡k=⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡j⁡k
86 83 85 sseq12d ⊢x=y∪z→⨉k∈xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈xc⁡j⁡kd⁡j⁡k↔⨉k∈y∪za⁡kb⁡k⊆⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡j⁡k
87 fveq2 ⊢x=y∪z→L⁡x=L⁡y∪z
88 87 oveqd ⊢x=y∪z→aL⁡xb=aL⁡y∪zb
89 87 oveqd ⊢x=y∪z→c⁡jL⁡xd⁡j=c⁡jL⁡y∪zd⁡j
90 89 mpteq2dv ⊢x=y∪z→j∈ℕ⟼c⁡jL⁡xd⁡j=j∈ℕ⟼c⁡jL⁡y∪zd⁡j
91 90 fveq2d ⊢x=y∪z→sum^⁡j∈ℕ⟼c⁡jL⁡xd⁡j=sum^⁡j∈ℕ⟼c⁡jL⁡y∪zd⁡j
92 88 91 breq12d ⊢x=y∪z→aL⁡xb≤sum^⁡j∈ℕ⟼c⁡jL⁡xd⁡j↔aL⁡y∪zb≤sum^⁡j∈ℕ⟼c⁡jL⁡y∪zd⁡j
93 86 92 imbi12d ⊢x=y∪z→⨉k∈xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈xc⁡j⁡kd⁡j⁡k→aL⁡xb≤sum^⁡j∈ℕ⟼c⁡jL⁡xd⁡j↔⨉k∈y∪za⁡kb⁡k⊆⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡j⁡k→aL⁡y∪zb≤sum^⁡j∈ℕ⟼c⁡jL⁡y∪zd⁡j
94 82 93 imbi12d ⊢x=y∪z→d∈ℝxℕ→⨉k∈xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈xc⁡j⁡kd⁡j⁡k→aL⁡xb≤sum^⁡j∈ℕ⟼c⁡jL⁡xd⁡j↔d∈ℝy∪zℕ→⨉k∈y∪za⁡kb⁡k⊆⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡j⁡k→aL⁡y∪zb≤sum^⁡j∈ℕ⟼c⁡jL⁡y∪zd⁡j
95 94 ralbidv2 ⊢x=y∪z→∀d∈ℝxℕ⨉k∈xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈xc⁡j⁡kd⁡j⁡k→aL⁡xb≤sum^⁡j∈ℕ⟼c⁡jL⁡xd⁡j↔∀d∈ℝy∪zℕ⨉k∈y∪za⁡kb⁡k⊆⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡j⁡k→aL⁡y∪zb≤sum^⁡j∈ℕ⟼c⁡jL⁡y∪zd⁡j
96 81 95 imbi12d ⊢x=y∪z→c∈ℝxℕ→∀d∈ℝxℕ⨉k∈xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈xc⁡j⁡kd⁡j⁡k→aL⁡xb≤sum^⁡j∈ℕ⟼c⁡jL⁡xd⁡j↔c∈ℝy∪zℕ→∀d∈ℝy∪zℕ⨉k∈y∪za⁡kb⁡k⊆⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡j⁡k→aL⁡y∪zb≤sum^⁡j∈ℕ⟼c⁡jL⁡y∪zd⁡j
97 96 ralbidv2 ⊢x=y∪z→∀c∈ℝxℕ∀d∈ℝxℕ⨉k∈xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈xc⁡j⁡kd⁡j⁡k→aL⁡xb≤sum^⁡j∈ℕ⟼c⁡jL⁡xd⁡j↔∀c∈ℝy∪zℕ∀d∈ℝy∪zℕ⨉k∈y∪za⁡kb⁡k⊆⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡j⁡k→aL⁡y∪zb≤sum^⁡j∈ℕ⟼c⁡jL⁡y∪zd⁡j
98 79 97 imbi12d ⊢x=y∪z→b∈ℝx→∀c∈ℝxℕ∀d∈ℝxℕ⨉k∈xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈xc⁡j⁡kd⁡j⁡k→aL⁡xb≤sum^⁡j∈ℕ⟼c⁡jL⁡xd⁡j↔b∈ℝy∪z→∀c∈ℝy∪zℕ∀d∈ℝy∪zℕ⨉k∈y∪za⁡kb⁡k⊆⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡j⁡k→aL⁡y∪zb≤sum^⁡j∈ℕ⟼c⁡jL⁡y∪zd⁡j
99 98 ralbidv2 ⊢x=y∪z→∀b∈ℝx∀c∈ℝxℕ∀d∈ℝxℕ⨉k∈xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈xc⁡j⁡kd⁡j⁡k→aL⁡xb≤sum^⁡j∈ℕ⟼c⁡jL⁡xd⁡j↔∀b∈ℝy∪z∀c∈ℝy∪zℕ∀d∈ℝy∪zℕ⨉k∈y∪za⁡kb⁡k⊆⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡j⁡k→aL⁡y∪zb≤sum^⁡j∈ℕ⟼c⁡jL⁡y∪zd⁡j
100 78 99 imbi12d ⊢x=y∪z→a∈ℝx→∀b∈ℝx∀c∈ℝxℕ∀d∈ℝxℕ⨉k∈xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈xc⁡j⁡kd⁡j⁡k→aL⁡xb≤sum^⁡j∈ℕ⟼c⁡jL⁡xd⁡j↔a∈ℝy∪z→∀b∈ℝy∪z∀c∈ℝy∪zℕ∀d∈ℝy∪zℕ⨉k∈y∪za⁡kb⁡k⊆⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡j⁡k→aL⁡y∪zb≤sum^⁡j∈ℕ⟼c⁡jL⁡y∪zd⁡j
101 100 ralbidv2 ⊢x=y∪z→∀a∈ℝx∀b∈ℝx∀c∈ℝxℕ∀d∈ℝxℕ⨉k∈xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈xc⁡j⁡kd⁡j⁡k→aL⁡xb≤sum^⁡j∈ℕ⟼c⁡jL⁡xd⁡j↔∀a∈ℝy∪z∀b∈ℝy∪z∀c∈ℝy∪zℕ∀d∈ℝy∪zℕ⨉k∈y∪za⁡kb⁡k⊆⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡j⁡k→aL⁡y∪zb≤sum^⁡j∈ℕ⟼c⁡jL⁡y∪zd⁡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∈xa⁡kb⁡k=⨉k∈Xa⁡kb⁡k
109 ixpeq1 ⊢x=X→⨉k∈xc⁡j⁡kd⁡j⁡k=⨉k∈Xc⁡j⁡kd⁡j⁡k
110 109 iuneq2d ⊢x=X→⋃j∈ℕ⨉k∈xc⁡j⁡kd⁡j⁡k=⋃j∈ℕ⨉k∈Xc⁡j⁡kd⁡j⁡k
111 108 110 sseq12d ⊢x=X→⨉k∈xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈xc⁡j⁡kd⁡j⁡k↔⨉k∈Xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈Xc⁡j⁡kd⁡j⁡k
112 fveq2 ⊢x=X→L⁡x=L⁡X
113 112 oveqd ⊢x=X→aL⁡xb=aL⁡Xb
114 112 oveqd ⊢x=X→c⁡jL⁡xd⁡j=c⁡jL⁡Xd⁡j
115 114 mpteq2dv ⊢x=X→j∈ℕ⟼c⁡jL⁡xd⁡j=j∈ℕ⟼c⁡jL⁡Xd⁡j
116 115 fveq2d ⊢x=X→sum^⁡j∈ℕ⟼c⁡jL⁡xd⁡j=sum^⁡j∈ℕ⟼c⁡jL⁡Xd⁡j
117 113 116 breq12d ⊢x=X→aL⁡xb≤sum^⁡j∈ℕ⟼c⁡jL⁡xd⁡j↔aL⁡Xb≤sum^⁡j∈ℕ⟼c⁡jL⁡Xd⁡j
118 111 117 imbi12d ⊢x=X→⨉k∈xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈xc⁡j⁡kd⁡j⁡k→aL⁡xb≤sum^⁡j∈ℕ⟼c⁡jL⁡xd⁡j↔⨉k∈Xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈Xc⁡j⁡kd⁡j⁡k→aL⁡Xb≤sum^⁡j∈ℕ⟼c⁡jL⁡Xd⁡j
119 107 118 imbi12d ⊢x=X→d∈ℝxℕ→⨉k∈xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈xc⁡j⁡kd⁡j⁡k→aL⁡xb≤sum^⁡j∈ℕ⟼c⁡jL⁡xd⁡j↔d∈ℝXℕ→⨉k∈Xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈Xc⁡j⁡kd⁡j⁡k→aL⁡Xb≤sum^⁡j∈ℕ⟼c⁡jL⁡Xd⁡j
120 119 ralbidv2 ⊢x=X→∀d∈ℝxℕ⨉k∈xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈xc⁡j⁡kd⁡j⁡k→aL⁡xb≤sum^⁡j∈ℕ⟼c⁡jL⁡xd⁡j↔∀d∈ℝXℕ⨉k∈Xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈Xc⁡j⁡kd⁡j⁡k→aL⁡Xb≤sum^⁡j∈ℕ⟼c⁡jL⁡Xd⁡j
121 106 120 imbi12d ⊢x=X→c∈ℝxℕ→∀d∈ℝxℕ⨉k∈xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈xc⁡j⁡kd⁡j⁡k→aL⁡xb≤sum^⁡j∈ℕ⟼c⁡jL⁡xd⁡j↔c∈ℝXℕ→∀d∈ℝXℕ⨉k∈Xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈Xc⁡j⁡kd⁡j⁡k→aL⁡Xb≤sum^⁡j∈ℕ⟼c⁡jL⁡Xd⁡j
122 121 ralbidv2 ⊢x=X→∀c∈ℝxℕ∀d∈ℝxℕ⨉k∈xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈xc⁡j⁡kd⁡j⁡k→aL⁡xb≤sum^⁡j∈ℕ⟼c⁡jL⁡xd⁡j↔∀c∈ℝXℕ∀d∈ℝXℕ⨉k∈Xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈Xc⁡j⁡kd⁡j⁡k→aL⁡Xb≤sum^⁡j∈ℕ⟼c⁡jL⁡Xd⁡j
123 104 122 imbi12d ⊢x=X→b∈ℝx→∀c∈ℝxℕ∀d∈ℝxℕ⨉k∈xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈xc⁡j⁡kd⁡j⁡k→aL⁡xb≤sum^⁡j∈ℕ⟼c⁡jL⁡xd⁡j↔b∈ℝX→∀c∈ℝXℕ∀d∈ℝXℕ⨉k∈Xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈Xc⁡j⁡kd⁡j⁡k→aL⁡Xb≤sum^⁡j∈ℕ⟼c⁡jL⁡Xd⁡j
124 123 ralbidv2 ⊢x=X→∀b∈ℝx∀c∈ℝxℕ∀d∈ℝxℕ⨉k∈xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈xc⁡j⁡kd⁡j⁡k→aL⁡xb≤sum^⁡j∈ℕ⟼c⁡jL⁡xd⁡j↔∀b∈ℝX∀c∈ℝXℕ∀d∈ℝXℕ⨉k∈Xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈Xc⁡j⁡kd⁡j⁡k→aL⁡Xb≤sum^⁡j∈ℕ⟼c⁡jL⁡Xd⁡j
125 103 124 imbi12d ⊢x=X→a∈ℝx→∀b∈ℝx∀c∈ℝxℕ∀d∈ℝxℕ⨉k∈xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈xc⁡j⁡kd⁡j⁡k→aL⁡xb≤sum^⁡j∈ℕ⟼c⁡jL⁡xd⁡j↔a∈ℝX→∀b∈ℝX∀c∈ℝXℕ∀d∈ℝXℕ⨉k∈Xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈Xc⁡j⁡kd⁡j⁡k→aL⁡Xb≤sum^⁡j∈ℕ⟼c⁡jL⁡Xd⁡j
126 125 ralbidv2 ⊢x=X→∀a∈ℝx∀b∈ℝx∀c∈ℝxℕ∀d∈ℝxℕ⨉k∈xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈xc⁡j⁡kd⁡j⁡k→aL⁡xb≤sum^⁡j∈ℕ⟼c⁡jL⁡xd⁡j↔∀a∈ℝX∀b∈ℝX∀c∈ℝXℕ∀d∈ℝXℕ⨉k∈Xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈Xc⁡j⁡kd⁡j⁡k→aL⁡Xb≤sum^⁡j∈ℕ⟼c⁡jL⁡Xd⁡j
127 fveq1 ⊢a=e→a⁡k=e⁡k
128 127 oveq1d ⊢a=e→a⁡kb⁡k=e⁡kb⁡k
129 128 fveq2d ⊢a=e→vol⁡a⁡kb⁡k=vol⁡e⁡kb⁡k
130 129 prodeq2ad ⊢a=e→∏k∈xvol⁡a⁡kb⁡k=∏k∈xvol⁡e⁡kb⁡k
131 130 ifeq2d ⊢a=e→ifx=∅0∏k∈xvol⁡a⁡kb⁡k=ifx=∅0∏k∈xvol⁡e⁡kb⁡k
132 fveq1 ⊢b=f→b⁡k=f⁡k
133 132 oveq2d ⊢b=f→e⁡kb⁡k=e⁡kf⁡k
134 133 fveq2d ⊢b=f→vol⁡e⁡kb⁡k=vol⁡e⁡kf⁡k
135 134 prodeq2ad ⊢b=f→∏k∈xvol⁡e⁡kb⁡k=∏k∈xvol⁡e⁡kf⁡k
136 135 ifeq2d ⊢b=f→ifx=∅0∏k∈xvol⁡e⁡kb⁡k=ifx=∅0∏k∈xvol⁡e⁡kf⁡k
137 131 136 cbvmpov ⊢a∈ℝx,b∈ℝx⟼ifx=∅0∏k∈xvol⁡a⁡kb⁡k=e∈ℝx,f∈ℝx⟼ifx=∅0∏k∈xvol⁡e⁡kf⁡k
138 137 mpteq2i ⊢x∈Fin⟼a∈ℝx,b∈ℝx⟼ifx=∅0∏k∈xvol⁡a⁡kb⁡k=x∈Fin⟼e∈ℝx,f∈ℝx⟼ifx=∅0∏k∈xvol⁡e⁡kf⁡k
139 1 138 eqtri ⊢L=x∈Fin⟼e∈ℝx,f∈ℝx⟼ifx=∅0∏k∈xvol⁡e⁡kf⁡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∈ℝ∅→aL⁡∅b=0
145 144 ad5ant23 ⊢φ∧a∈ℝ∅∧b∈ℝ∅∧c∈ℝ∅ℕ∧d∈ℝ∅ℕ→aL⁡∅b=0
146 nfv ⊢Ⅎjc∈ℝ∅ℕ∧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⁡jL⁡∅d⁡j∈0+∞
168 148 167 sselid ⊢c∈ℝ∅ℕ∧d∈ℝ∅ℕ∧j∈ℕ→c⁡jL⁡∅d⁡j∈0+∞
169 146 147 168 sge0ge0mpt ⊢c∈ℝ∅ℕ∧d∈ℝ∅ℕ→0≤sum^⁡j∈ℕ⟼c⁡jL⁡∅d⁡j
170 169 adantll ⊢φ∧a∈ℝ∅∧b∈ℝ∅∧c∈ℝ∅ℕ∧d∈ℝ∅ℕ→0≤sum^⁡j∈ℕ⟼c⁡jL⁡∅d⁡j
171 145 170 eqbrtrd ⊢φ∧a∈ℝ∅∧b∈ℝ∅∧c∈ℝ∅ℕ∧d∈ℝ∅ℕ→aL⁡∅b≤sum^⁡j∈ℕ⟼c⁡jL⁡∅d⁡j
172 171 a1d ⊢φ∧a∈ℝ∅∧b∈ℝ∅∧c∈ℝ∅ℕ∧d∈ℝ∅ℕ→⨉k∈∅a⁡kb⁡k⊆⋃j∈ℕ⨉k∈∅c⁡j⁡kd⁡j⁡k→aL⁡∅b≤sum^⁡j∈ℕ⟼c⁡jL⁡∅d⁡j
173 172 ralrimiva ⊢φ∧a∈ℝ∅∧b∈ℝ∅∧c∈ℝ∅ℕ→∀d∈ℝ∅ℕ⨉k∈∅a⁡kb⁡k⊆⋃j∈ℕ⨉k∈∅c⁡j⁡kd⁡j⁡k→aL⁡∅b≤sum^⁡j∈ℕ⟼c⁡jL⁡∅d⁡j
174 173 ralrimiva ⊢φ∧a∈ℝ∅∧b∈ℝ∅→∀c∈ℝ∅ℕ∀d∈ℝ∅ℕ⨉k∈∅a⁡kb⁡k⊆⋃j∈ℕ⨉k∈∅c⁡j⁡kd⁡j⁡k→aL⁡∅b≤sum^⁡j∈ℕ⟼c⁡jL⁡∅d⁡j
175 174 ralrimiva ⊢φ∧a∈ℝ∅→∀b∈ℝ∅∀c∈ℝ∅ℕ∀d∈ℝ∅ℕ⨉k∈∅a⁡kb⁡k⊆⋃j∈ℕ⨉k∈∅c⁡j⁡kd⁡j⁡k→aL⁡∅b≤sum^⁡j∈ℕ⟼c⁡jL⁡∅d⁡j
176 175 ralrimiva ⊢φ→∀a∈ℝ∅∀b∈ℝ∅∀c∈ℝ∅ℕ∀d∈ℝ∅ℕ⨉k∈∅a⁡kb⁡k⊆⋃j∈ℕ⨉k∈∅c⁡j⁡kd⁡j⁡k→aL⁡∅b≤sum^⁡j∈ℕ⟼c⁡jL⁡∅d⁡j
177 simpl ⊢φ∧y⊆X∧z∈X∖y∧∀a∈ℝy∀b∈ℝy∀c∈ℝyℕ∀d∈ℝyℕ⨉k∈ya⁡kb⁡k⊆⋃j∈ℕ⨉k∈yc⁡j⁡kd⁡j⁡k→aL⁡yb≤sum^⁡j∈ℕ⟼c⁡jL⁡yd⁡j→φ∧y⊆X∧z∈X∖y
178 128 ixpeq2dv ⊢a=e→⨉k∈ya⁡kb⁡k=⨉k∈ye⁡kb⁡k
179 178 sseq1d ⊢a=e→⨉k∈ya⁡kb⁡k⊆⋃j∈ℕ⨉k∈yc⁡j⁡kd⁡j⁡k↔⨉k∈ye⁡kb⁡k⊆⋃j∈ℕ⨉k∈yc⁡j⁡kd⁡j⁡k
180 oveq1 ⊢a=e→aL⁡yb=eL⁡yb
181 180 breq1d ⊢a=e→aL⁡yb≤sum^⁡j∈ℕ⟼c⁡jL⁡yd⁡j↔eL⁡yb≤sum^⁡j∈ℕ⟼c⁡jL⁡yd⁡j
182 179 181 imbi12d ⊢a=e→⨉k∈ya⁡kb⁡k⊆⋃j∈ℕ⨉k∈yc⁡j⁡kd⁡j⁡k→aL⁡yb≤sum^⁡j∈ℕ⟼c⁡jL⁡yd⁡j↔⨉k∈ye⁡kb⁡k⊆⋃j∈ℕ⨉k∈yc⁡j⁡kd⁡j⁡k→eL⁡yb≤sum^⁡j∈ℕ⟼c⁡jL⁡yd⁡j
183 182 ralbidv ⊢a=e→∀d∈ℝyℕ⨉k∈ya⁡kb⁡k⊆⋃j∈ℕ⨉k∈yc⁡j⁡kd⁡j⁡k→aL⁡yb≤sum^⁡j∈ℕ⟼c⁡jL⁡yd⁡j↔∀d∈ℝyℕ⨉k∈ye⁡kb⁡k⊆⋃j∈ℕ⨉k∈yc⁡j⁡kd⁡j⁡k→eL⁡yb≤sum^⁡j∈ℕ⟼c⁡jL⁡yd⁡j
184 183 ralbidv ⊢a=e→∀c∈ℝyℕ∀d∈ℝyℕ⨉k∈ya⁡kb⁡k⊆⋃j∈ℕ⨉k∈yc⁡j⁡kd⁡j⁡k→aL⁡yb≤sum^⁡j∈ℕ⟼c⁡jL⁡yd⁡j↔∀c∈ℝyℕ∀d∈ℝyℕ⨉k∈ye⁡kb⁡k⊆⋃j∈ℕ⨉k∈yc⁡j⁡kd⁡j⁡k→eL⁡yb≤sum^⁡j∈ℕ⟼c⁡jL⁡yd⁡j
185 184 ralbidv ⊢a=e→∀b∈ℝy∀c∈ℝyℕ∀d∈ℝyℕ⨉k∈ya⁡kb⁡k⊆⋃j∈ℕ⨉k∈yc⁡j⁡kd⁡j⁡k→aL⁡yb≤sum^⁡j∈ℕ⟼c⁡jL⁡yd⁡j↔∀b∈ℝy∀c∈ℝyℕ∀d∈ℝyℕ⨉k∈ye⁡kb⁡k⊆⋃j∈ℕ⨉k∈yc⁡j⁡kd⁡j⁡k→eL⁡yb≤sum^⁡j∈ℕ⟼c⁡jL⁡yd⁡j
186 133 ixpeq2dv ⊢b=f→⨉k∈ye⁡kb⁡k=⨉k∈ye⁡kf⁡k
187 186 sseq1d ⊢b=f→⨉k∈ye⁡kb⁡k⊆⋃j∈ℕ⨉k∈yc⁡j⁡kd⁡j⁡k↔⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yc⁡j⁡kd⁡j⁡k
188 oveq2 ⊢b=f→eL⁡yb=eL⁡yf
189 188 breq1d ⊢b=f→eL⁡yb≤sum^⁡j∈ℕ⟼c⁡jL⁡yd⁡j↔eL⁡yf≤sum^⁡j∈ℕ⟼c⁡jL⁡yd⁡j
190 187 189 imbi12d ⊢b=f→⨉k∈ye⁡kb⁡k⊆⋃j∈ℕ⨉k∈yc⁡j⁡kd⁡j⁡k→eL⁡yb≤sum^⁡j∈ℕ⟼c⁡jL⁡yd⁡j↔⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yc⁡j⁡kd⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼c⁡jL⁡yd⁡j
191 190 ralbidv ⊢b=f→∀d∈ℝyℕ⨉k∈ye⁡kb⁡k⊆⋃j∈ℕ⨉k∈yc⁡j⁡kd⁡j⁡k→eL⁡yb≤sum^⁡j∈ℕ⟼c⁡jL⁡yd⁡j↔∀d∈ℝyℕ⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yc⁡j⁡kd⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼c⁡jL⁡yd⁡j
192 191 ralbidv ⊢b=f→∀c∈ℝyℕ∀d∈ℝyℕ⨉k∈ye⁡kb⁡k⊆⋃j∈ℕ⨉k∈yc⁡j⁡kd⁡j⁡k→eL⁡yb≤sum^⁡j∈ℕ⟼c⁡jL⁡yd⁡j↔∀c∈ℝyℕ∀d∈ℝyℕ⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yc⁡j⁡kd⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼c⁡jL⁡yd⁡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⁡kd⁡j⁡k=g⁡j⁡kd⁡j⁡k
196 195 ixpeq2dv ⊢c=g→⨉k∈yc⁡j⁡kd⁡j⁡k=⨉k∈yg⁡j⁡kd⁡j⁡k
197 196 adantr ⊢c=g∧j∈ℕ→⨉k∈yc⁡j⁡kd⁡j⁡k=⨉k∈yg⁡j⁡kd⁡j⁡k
198 197 iuneq2dv ⊢c=g→⋃j∈ℕ⨉k∈yc⁡j⁡kd⁡j⁡k=⋃j∈ℕ⨉k∈yg⁡j⁡kd⁡j⁡k
199 198 sseq2d ⊢c=g→⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yc⁡j⁡kd⁡j⁡k↔⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kd⁡j⁡k
200 193 oveq1d ⊢c=g→c⁡jL⁡yd⁡j=g⁡jL⁡yd⁡j
201 200 mpteq2dv ⊢c=g→j∈ℕ⟼c⁡jL⁡yd⁡j=j∈ℕ⟼g⁡jL⁡yd⁡j
202 201 fveq2d ⊢c=g→sum^⁡j∈ℕ⟼c⁡jL⁡yd⁡j=sum^⁡j∈ℕ⟼g⁡jL⁡yd⁡j
203 202 breq2d ⊢c=g→eL⁡yf≤sum^⁡j∈ℕ⟼c⁡jL⁡yd⁡j↔eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yd⁡j
204 199 203 imbi12d ⊢c=g→⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yc⁡j⁡kd⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼c⁡jL⁡yd⁡j↔⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kd⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yd⁡j
205 204 ralbidv ⊢c=g→∀d∈ℝyℕ⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yc⁡j⁡kd⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼c⁡jL⁡yd⁡j↔∀d∈ℝyℕ⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kd⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yd⁡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⁡kd⁡j⁡k=g⁡j⁡kh⁡j⁡k
209 208 ixpeq2dv ⊢d=h→⨉k∈yg⁡j⁡kd⁡j⁡k=⨉k∈yg⁡j⁡kh⁡j⁡k
210 209 adantr ⊢d=h∧j∈ℕ→⨉k∈yg⁡j⁡kd⁡j⁡k=⨉k∈yg⁡j⁡kh⁡j⁡k
211 210 iuneq2dv ⊢d=h→⋃j∈ℕ⨉k∈yg⁡j⁡kd⁡j⁡k=⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k
212 211 sseq2d ⊢d=h→⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kd⁡j⁡k↔⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k
213 206 oveq2d ⊢d=h→g⁡jL⁡yd⁡j=g⁡jL⁡yh⁡j
214 213 mpteq2dv ⊢d=h→j∈ℕ⟼g⁡jL⁡yd⁡j=j∈ℕ⟼g⁡jL⁡yh⁡j
215 214 fveq2d ⊢d=h→sum^⁡j∈ℕ⟼g⁡jL⁡yd⁡j=sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j
216 215 breq2d ⊢d=h→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yd⁡j↔eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j
217 212 216 imbi12d ⊢d=h→⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kd⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yd⁡j↔⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j
218 217 cbvralvw ⊢∀d∈ℝyℕ⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kd⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yd⁡j↔∀h∈ℝyℕ⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j
219 218 a1i ⊢c=g→∀d∈ℝyℕ⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kd⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yd⁡j↔∀h∈ℝyℕ⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j
220 205 219 bitrd ⊢c=g→∀d∈ℝyℕ⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yc⁡j⁡kd⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼c⁡jL⁡yd⁡j↔∀h∈ℝyℕ⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j
221 220 cbvralvw ⊢∀c∈ℝyℕ∀d∈ℝyℕ⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yc⁡j⁡kd⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼c⁡jL⁡yd⁡j↔∀g∈ℝyℕ∀h∈ℝyℕ⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j
222 221 a1i ⊢b=f→∀c∈ℝyℕ∀d∈ℝyℕ⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yc⁡j⁡kd⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼c⁡jL⁡yd⁡j↔∀g∈ℝyℕ∀h∈ℝyℕ⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j
223 192 222 bitrd ⊢b=f→∀c∈ℝyℕ∀d∈ℝyℕ⨉k∈ye⁡kb⁡k⊆⋃j∈ℕ⨉k∈yc⁡j⁡kd⁡j⁡k→eL⁡yb≤sum^⁡j∈ℕ⟼c⁡jL⁡yd⁡j↔∀g∈ℝyℕ∀h∈ℝyℕ⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j
224 223 cbvralvw ⊢∀b∈ℝy∀c∈ℝyℕ∀d∈ℝyℕ⨉k∈ye⁡kb⁡k⊆⋃j∈ℕ⨉k∈yc⁡j⁡kd⁡j⁡k→eL⁡yb≤sum^⁡j∈ℕ⟼c⁡jL⁡yd⁡j↔∀f∈ℝy∀g∈ℝyℕ∀h∈ℝyℕ⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j
225 224 a1i ⊢a=e→∀b∈ℝy∀c∈ℝyℕ∀d∈ℝyℕ⨉k∈ye⁡kb⁡k⊆⋃j∈ℕ⨉k∈yc⁡j⁡kd⁡j⁡k→eL⁡yb≤sum^⁡j∈ℕ⟼c⁡jL⁡yd⁡j↔∀f∈ℝy∀g∈ℝyℕ∀h∈ℝyℕ⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j
226 185 225 bitrd ⊢a=e→∀b∈ℝy∀c∈ℝyℕ∀d∈ℝyℕ⨉k∈ya⁡kb⁡k⊆⋃j∈ℕ⨉k∈yc⁡j⁡kd⁡j⁡k→aL⁡yb≤sum^⁡j∈ℕ⟼c⁡jL⁡yd⁡j↔∀f∈ℝy∀g∈ℝyℕ∀h∈ℝyℕ⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j
227 226 cbvralvw ⊢∀a∈ℝy∀b∈ℝy∀c∈ℝyℕ∀d∈ℝyℕ⨉k∈ya⁡kb⁡k⊆⋃j∈ℕ⨉k∈yc⁡j⁡kd⁡j⁡k→aL⁡yb≤sum^⁡j∈ℕ⟼c⁡jL⁡yd⁡j↔∀e∈ℝy∀f∈ℝy∀g∈ℝyℕ∀h∈ℝyℕ⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j
228 227 biimpi ⊢∀a∈ℝy∀b∈ℝy∀c∈ℝyℕ∀d∈ℝyℕ⨉k∈ya⁡kb⁡k⊆⋃j∈ℕ⨉k∈yc⁡j⁡kd⁡j⁡k→aL⁡yb≤sum^⁡j∈ℕ⟼c⁡jL⁡yd⁡j→∀e∈ℝy∀f∈ℝy∀g∈ℝyℕ∀h∈ℝyℕ⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j
229 228 adantl ⊢φ∧y⊆X∧z∈X∖y∧∀a∈ℝy∀b∈ℝy∀c∈ℝyℕ∀d∈ℝyℕ⨉k∈ya⁡kb⁡k⊆⋃j∈ℕ⨉k∈yc⁡j⁡kd⁡j⁡k→aL⁡yb≤sum^⁡j∈ℕ⟼c⁡jL⁡yd⁡j→∀e∈ℝy∀f∈ℝy∀g∈ℝyℕ∀h∈ℝyℕ⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡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∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡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∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡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∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡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∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡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∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡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∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡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∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡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∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j∧a∈ℝy∪z∧b∈ℝy∪z∧c∈ℝy∪zℕ∧d∈ℝy∪zℕ∧⨉k∈y∪za⁡kb⁡k⊆⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡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∪za⁡kb⁡k⊆⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡j⁡k∧y=∅→d∈ℝzℕ
266 265 adantlll ⊢φ∧y⊆X∧z∈X∖y∧∀e∈ℝy∀f∈ℝy∀g∈ℝyℕ∀h∈ℝyℕ⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j∧a∈ℝy∪z∧b∈ℝy∪z∧c∈ℝy∪zℕ∧d∈ℝy∪zℕ∧⨉k∈y∪za⁡kb⁡k⊆⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡j⁡k∧y=∅→d∈ℝzℕ
267 simpl ⊢⨉k∈y∪za⁡kb⁡k⊆⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡j⁡k∧y=∅→⨉k∈y∪za⁡kb⁡k⊆⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡j⁡k
268 239 ixpeq1d ⊢y=∅→⨉k∈za⁡kb⁡k=⨉k∈y∪za⁡kb⁡k
269 268 adantl ⊢⨉k∈y∪za⁡kb⁡k⊆⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡j⁡k∧y=∅→⨉k∈za⁡kb⁡k=⨉k∈y∪za⁡kb⁡k
270 239 ixpeq1d ⊢y=∅→⨉k∈zc⁡i⁡kd⁡i⁡k=⨉k∈y∪zc⁡i⁡kd⁡i⁡k
271 270 adantr ⊢y=∅∧i∈ℕ→⨉k∈zc⁡i⁡kd⁡i⁡k=⨉k∈y∪zc⁡i⁡kd⁡i⁡k
272 271 iuneq2dv ⊢y=∅→⋃i∈ℕ⨉k∈zc⁡i⁡kd⁡i⁡k=⋃i∈ℕ⨉k∈y∪zc⁡i⁡kd⁡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⁡kd⁡i⁡k=c⁡j⁡kd⁡j⁡k
278 277 ixpeq2dv ⊢i=j→⨉k∈y∪zc⁡i⁡kd⁡i⁡k=⨉k∈y∪zc⁡j⁡kd⁡j⁡k
279 278 cbviunv ⊢⋃i∈ℕ⨉k∈y∪zc⁡i⁡kd⁡i⁡k=⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡j⁡k
280 279 a1i ⊢y=∅→⋃i∈ℕ⨉k∈y∪zc⁡i⁡kd⁡i⁡k=⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡j⁡k
281 272 280 eqtrd ⊢y=∅→⋃i∈ℕ⨉k∈zc⁡i⁡kd⁡i⁡k=⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡j⁡k
282 281 adantl ⊢⨉k∈y∪za⁡kb⁡k⊆⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡j⁡k∧y=∅→⋃i∈ℕ⨉k∈zc⁡i⁡kd⁡i⁡k=⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡j⁡k
283 269 282 sseq12d ⊢⨉k∈y∪za⁡kb⁡k⊆⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡j⁡k∧y=∅→⨉k∈za⁡kb⁡k⊆⋃i∈ℕ⨉k∈zc⁡i⁡kd⁡i⁡k↔⨉k∈y∪za⁡kb⁡k⊆⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡j⁡k
284 267 283 mpbird ⊢⨉k∈y∪za⁡kb⁡k⊆⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡j⁡k∧y=∅→⨉k∈za⁡kb⁡k⊆⋃i∈ℕ⨉k∈zc⁡i⁡kd⁡i⁡k
285 284 adantll ⊢φ∧y⊆X∧z∈X∖y∧∀e∈ℝy∀f∈ℝy∀g∈ℝyℕ∀h∈ℝyℕ⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j∧a∈ℝy∪z∧b∈ℝy∪z∧c∈ℝy∪zℕ∧d∈ℝy∪zℕ∧⨉k∈y∪za⁡kb⁡k⊆⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡j⁡k∧y=∅→⨉k∈za⁡kb⁡k⊆⋃i∈ℕ⨉k∈zc⁡i⁡kd⁡i⁡k
286 261 266 285 jca31 ⊢φ∧y⊆X∧z∈X∖y∧∀e∈ℝy∀f∈ℝy∀g∈ℝyℕ∀h∈ℝyℕ⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j∧a∈ℝy∪z∧b∈ℝy∪z∧c∈ℝy∪zℕ∧d∈ℝy∪zℕ∧⨉k∈y∪za⁡kb⁡k⊆⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡j⁡k∧y=∅→φ∧z∈X∧a∈ℝz∧b∈ℝz∧c∈ℝzℕ∧d∈ℝzℕ∧⨉k∈za⁡kb⁡k⊆⋃i∈ℕ⨉k∈zc⁡i⁡kd⁡i⁡k
287 simpr ⊢φ∧y⊆X∧z∈X∖y∧∀e∈ℝy∀f∈ℝy∀g∈ℝyℕ∀h∈ℝyℕ⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j∧a∈ℝy∪z∧b∈ℝy∪z∧c∈ℝy∪zℕ∧d∈ℝy∪zℕ∧⨉k∈y∪za⁡kb⁡k⊆⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡j⁡k∧y=∅→y=∅
288 fveq1 ⊢a=u→a⁡k=u⁡k
289 288 oveq1d ⊢a=u→a⁡kb⁡k=u⁡kb⁡k
290 289 fveq2d ⊢a=u→vol⁡a⁡kb⁡k=vol⁡u⁡kb⁡k
291 290 prodeq2ad ⊢a=u→∏k∈xvol⁡a⁡kb⁡k=∏k∈xvol⁡u⁡kb⁡k
292 291 ifeq2d ⊢a=u→ifx=∅0∏k∈xvol⁡a⁡kb⁡k=ifx=∅0∏k∈xvol⁡u⁡kb⁡k
293 fveq2 ⊢k=l→u⁡k=u⁡l
294 fveq2 ⊢k=l→b⁡k=b⁡l
295 293 294 oveq12d ⊢k=l→u⁡kb⁡k=u⁡lb⁡l
296 295 fveq2d ⊢k=l→vol⁡u⁡kb⁡k=vol⁡u⁡lb⁡l
297 296 cbvprodv ⊢∏k∈xvol⁡u⁡kb⁡k=∏l∈xvol⁡u⁡lb⁡l
298 297 a1i ⊢b=v→∏k∈xvol⁡u⁡kb⁡k=∏l∈xvol⁡u⁡lb⁡l
299 fveq1 ⊢b=v→b⁡l=v⁡l
300 299 oveq2d ⊢b=v→u⁡lb⁡l=u⁡lv⁡l
301 300 fveq2d ⊢b=v→vol⁡u⁡lb⁡l=vol⁡u⁡lv⁡l
302 301 prodeq2ad ⊢b=v→∏l∈xvol⁡u⁡lb⁡l=∏l∈xvol⁡u⁡lv⁡l
303 298 302 eqtrd ⊢b=v→∏k∈xvol⁡u⁡kb⁡k=∏l∈xvol⁡u⁡lv⁡l
304 303 ifeq2d ⊢b=v→ifx=∅0∏k∈xvol⁡u⁡kb⁡k=ifx=∅0∏l∈xvol⁡u⁡lv⁡l
305 292 304 cbvmpov ⊢a∈ℝx,b∈ℝx⟼ifx=∅0∏k∈xvol⁡a⁡kb⁡k=u∈ℝx,v∈ℝx⟼ifx=∅0∏l∈xvol⁡u⁡lv⁡l
306 305 mpteq2i ⊢x∈Fin⟼a∈ℝx,b∈ℝx⟼ifx=∅0∏k∈xvol⁡a⁡kb⁡k=x∈Fin⟼u∈ℝx,v∈ℝx⟼ifx=∅0∏l∈xvol⁡u⁡lv⁡l
307 1 306 eqtri ⊢L=x∈Fin⟼u∈ℝx,v∈ℝx⟼ifx=∅0∏l∈xvol⁡u⁡lv⁡l
308 simp-6r ⊢φ∧z∈X∧a∈ℝz∧b∈ℝz∧c∈ℝzℕ∧d∈ℝzℕ∧⨉k∈za⁡kb⁡k⊆⋃i∈ℕ⨉k∈zc⁡i⁡kd⁡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∈za⁡kb⁡k⊆⋃i∈ℕ⨉k∈zc⁡i⁡kd⁡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∈za⁡kb⁡k⊆⋃i∈ℕ⨉k∈zc⁡i⁡kd⁡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∈za⁡kb⁡k⊆⋃i∈ℕ⨉k∈zc⁡i⁡kd⁡i⁡k→c:ℕ⟶ℝz
319 elmapi ⊢d∈ℝzℕ→d:ℕ⟶ℝz
320 319 ad2antlr ⊢φ∧z∈X∧a∈ℝz∧b∈ℝz∧c∈ℝzℕ∧d∈ℝzℕ∧⨉k∈za⁡kb⁡k⊆⋃i∈ℕ⨉k∈zc⁡i⁡kd⁡i⁡k→d:ℕ⟶ℝz
321 id ⊢⨉k∈za⁡kb⁡k⊆⋃i∈ℕ⨉k∈zc⁡i⁡kd⁡i⁡k→⨉k∈za⁡kb⁡k⊆⋃i∈ℕ⨉k∈zc⁡i⁡kd⁡i⁡k
322 fveq2 ⊢k=l→a⁡k=a⁡l
323 322 294 oveq12d ⊢k=l→a⁡kb⁡k=a⁡lb⁡l
324 eqcom ⊢k=l↔l=k
325 324 imbi1i ⊢k=l→a⁡kb⁡k=a⁡lb⁡l↔l=k→a⁡kb⁡k=a⁡lb⁡l
326 eqcom ⊢a⁡kb⁡k=a⁡lb⁡l↔a⁡lb⁡l=a⁡kb⁡k
327 326 imbi2i ⊢l=k→a⁡kb⁡k=a⁡lb⁡l↔l=k→a⁡lb⁡l=a⁡kb⁡k
328 325 327 bitri ⊢k=l→a⁡kb⁡k=a⁡lb⁡l↔l=k→a⁡lb⁡l=a⁡kb⁡k
329 323 328 mpbi ⊢l=k→a⁡lb⁡l=a⁡kb⁡k
330 329 cbvixpv ⊢⨉l∈za⁡lb⁡l=⨉k∈za⁡kb⁡k
331 330 a1i ⊢⨉k∈za⁡kb⁡k⊆⋃i∈ℕ⨉k∈zc⁡i⁡kd⁡i⁡k→⨉l∈za⁡lb⁡l=⨉k∈za⁡kb⁡k
332 277 ixpeq2dv ⊢i=j→⨉k∈zc⁡i⁡kd⁡i⁡k=⨉k∈zc⁡j⁡kd⁡j⁡k
333 332 cbviunv ⊢⋃i∈ℕ⨉k∈zc⁡i⁡kd⁡i⁡k=⋃j∈ℕ⨉k∈zc⁡j⁡kd⁡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⁡kd⁡j⁡k=c⁡j⁡ld⁡j⁡l
337 336 cbvixpv ⊢⨉k∈zc⁡j⁡kd⁡j⁡k=⨉l∈zc⁡j⁡ld⁡j⁡l
338 337 a1i ⊢j∈ℕ→⨉k∈zc⁡j⁡kd⁡j⁡k=⨉l∈zc⁡j⁡ld⁡j⁡l
339 338 iuneq2i ⊢⋃j∈ℕ⨉k∈zc⁡j⁡kd⁡j⁡k=⋃j∈ℕ⨉l∈zc⁡j⁡ld⁡j⁡l
340 333 339 eqtr2i ⊢⋃j∈ℕ⨉l∈zc⁡j⁡ld⁡j⁡l=⋃i∈ℕ⨉k∈zc⁡i⁡kd⁡i⁡k
341 340 a1i ⊢⨉k∈za⁡kb⁡k⊆⋃i∈ℕ⨉k∈zc⁡i⁡kd⁡i⁡k→⋃j∈ℕ⨉l∈zc⁡j⁡ld⁡j⁡l=⋃i∈ℕ⨉k∈zc⁡i⁡kd⁡i⁡k
342 331 341 sseq12d ⊢⨉k∈za⁡kb⁡k⊆⋃i∈ℕ⨉k∈zc⁡i⁡kd⁡i⁡k→⨉l∈za⁡lb⁡l⊆⋃j∈ℕ⨉l∈zc⁡j⁡ld⁡j⁡l↔⨉k∈za⁡kb⁡k⊆⋃i∈ℕ⨉k∈zc⁡i⁡kd⁡i⁡k
343 321 342 mpbird ⊢⨉k∈za⁡kb⁡k⊆⋃i∈ℕ⨉k∈zc⁡i⁡kd⁡i⁡k→⨉l∈za⁡lb⁡l⊆⋃j∈ℕ⨉l∈zc⁡j⁡ld⁡j⁡l
344 343 adantl ⊢φ∧z∈X∧a∈ℝz∧b∈ℝz∧c∈ℝzℕ∧d∈ℝzℕ∧⨉k∈za⁡kb⁡k⊆⋃i∈ℕ⨉k∈zc⁡i⁡kd⁡i⁡k→⨉l∈za⁡lb⁡l⊆⋃j∈ℕ⨉l∈zc⁡j⁡ld⁡j⁡l
345 307 308 309 312 315 318 320 344 hoidmv1le ⊢φ∧z∈X∧a∈ℝz∧b∈ℝz∧c∈ℝzℕ∧d∈ℝzℕ∧⨉k∈za⁡kb⁡k⊆⋃i∈ℕ⨉k∈zc⁡i⁡kd⁡i⁡k→aL⁡zb≤sum^⁡j∈ℕ⟼c⁡jL⁡zd⁡j
346 345 adantr ⊢φ∧z∈X∧a∈ℝz∧b∈ℝz∧c∈ℝzℕ∧d∈ℝzℕ∧⨉k∈za⁡kb⁡k⊆⋃i∈ℕ⨉k∈zc⁡i⁡kd⁡i⁡k∧y=∅→aL⁡zb≤sum^⁡j∈ℕ⟼c⁡jL⁡zd⁡j
347 236 238 eqtrd ⊢y=∅→y∪z=z
348 347 fveq2d ⊢y=∅→L⁡y∪z=L⁡z
349 348 oveqd ⊢y=∅→aL⁡y∪zb=aL⁡zb
350 349 adantl ⊢φ∧z∈X∧a∈ℝz∧b∈ℝz∧c∈ℝzℕ∧d∈ℝzℕ∧⨉k∈za⁡kb⁡k⊆⋃i∈ℕ⨉k∈zc⁡i⁡kd⁡i⁡k∧y=∅→aL⁡y∪zb=aL⁡zb
351 348 oveqd ⊢y=∅→c⁡jL⁡y∪zd⁡j=c⁡jL⁡zd⁡j
352 351 mpteq2dv ⊢y=∅→j∈ℕ⟼c⁡jL⁡y∪zd⁡j=j∈ℕ⟼c⁡jL⁡zd⁡j
353 352 fveq2d ⊢y=∅→sum^⁡j∈ℕ⟼c⁡jL⁡y∪zd⁡j=sum^⁡j∈ℕ⟼c⁡jL⁡zd⁡j
354 353 adantl ⊢φ∧z∈X∧a∈ℝz∧b∈ℝz∧c∈ℝzℕ∧d∈ℝzℕ∧⨉k∈za⁡kb⁡k⊆⋃i∈ℕ⨉k∈zc⁡i⁡kd⁡i⁡k∧y=∅→sum^⁡j∈ℕ⟼c⁡jL⁡y∪zd⁡j=sum^⁡j∈ℕ⟼c⁡jL⁡zd⁡j
355 350 354 breq12d ⊢φ∧z∈X∧a∈ℝz∧b∈ℝz∧c∈ℝzℕ∧d∈ℝzℕ∧⨉k∈za⁡kb⁡k⊆⋃i∈ℕ⨉k∈zc⁡i⁡kd⁡i⁡k∧y=∅→aL⁡y∪zb≤sum^⁡j∈ℕ⟼c⁡jL⁡y∪zd⁡j↔aL⁡zb≤sum^⁡j∈ℕ⟼c⁡jL⁡zd⁡j
356 346 355 mpbird ⊢φ∧z∈X∧a∈ℝz∧b∈ℝz∧c∈ℝzℕ∧d∈ℝzℕ∧⨉k∈za⁡kb⁡k⊆⋃i∈ℕ⨉k∈zc⁡i⁡kd⁡i⁡k∧y=∅→aL⁡y∪zb≤sum^⁡j∈ℕ⟼c⁡jL⁡y∪zd⁡j
357 286 287 356 syl2anc ⊢φ∧y⊆X∧z∈X∖y∧∀e∈ℝy∀f∈ℝy∀g∈ℝyℕ∀h∈ℝyℕ⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j∧a∈ℝy∪z∧b∈ℝy∪z∧c∈ℝy∪zℕ∧d∈ℝy∪zℕ∧⨉k∈y∪za⁡kb⁡k⊆⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡j⁡k∧y=∅→aL⁡y∪zb≤sum^⁡j∈ℕ⟼c⁡jL⁡y∪zd⁡j
358 2 ad8antr ⊢φ∧y⊆X∧z∈X∖y∧∀e∈ℝy∀f∈ℝy∀g∈ℝyℕ∀h∈ℝyℕ⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j∧a∈ℝy∪z∧b∈ℝy∪z∧c∈ℝy∪zℕ∧d∈ℝy∪zℕ∧⨉k∈y∪za⁡kb⁡k⊆⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡j⁡k∧¬y=∅→X∈Fin
359 simplrl ⊢φ∧y⊆X∧z∈X∖y∧∀e∈ℝy∀f∈ℝy∀g∈ℝyℕ∀h∈ℝyℕ⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j→y⊆X
360 359 ad5ant12 ⊢φ∧y⊆X∧z∈X∖y∧∀e∈ℝy∀f∈ℝy∀g∈ℝyℕ∀h∈ℝyℕ⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡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∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j∧a∈ℝy∪z∧b∈ℝy∪z∧c∈ℝy∪zℕ∧d∈ℝy∪zℕ∧⨉k∈y∪za⁡kb⁡k⊆⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡j⁡k∧¬y=∅→y⊆X
362 simplrr ⊢φ∧y⊆X∧z∈X∖y∧∀e∈ℝy∀f∈ℝy∀g∈ℝyℕ∀h∈ℝyℕ⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j→z∈X∖y
363 362 ad5ant12 ⊢φ∧y⊆X∧z∈X∖y∧∀e∈ℝy∀f∈ℝy∀g∈ℝyℕ∀h∈ℝyℕ⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡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∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j∧a∈ℝy∪z∧b∈ℝy∪z∧c∈ℝy∪zℕ∧d∈ℝy∪zℕ∧⨉k∈y∪za⁡kb⁡k⊆⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡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∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡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∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j∧a∈ℝy∪z∧b∈ℝy∪z∧c∈ℝy∪zℕ∧d∈ℝy∪zℕ∧⨉k∈y∪za⁡kb⁡k⊆⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡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∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡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∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j∧a∈ℝy∪z∧b∈ℝy∪z∧c∈ℝy∪zℕ∧d∈ℝy∪zℕ∧⨉k∈y∪za⁡kb⁡k⊆⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡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∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡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∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j∧a∈ℝy∪z∧b∈ℝy∪z∧c∈ℝy∪zℕ∧d∈ℝy∪zℕ∧⨉k∈y∪za⁡kb⁡k⊆⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡j⁡k∧¬y=∅→c:ℕ⟶ℝy∪z
377 elmapi ⊢d∈ℝy∪zℕ→d:ℕ⟶ℝy∪z
378 377 ad2antrr ⊢d∈ℝy∪zℕ∧⨉k∈y∪za⁡kb⁡k⊆⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡j⁡k∧¬y=∅→d:ℕ⟶ℝy∪z
379 378 adantlll ⊢φ∧y⊆X∧z∈X∖y∧∀e∈ℝy∀f∈ℝy∀g∈ℝyℕ∀h∈ℝyℕ⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j∧a∈ℝy∪z∧b∈ℝy∪z∧c∈ℝy∪zℕ∧d∈ℝy∪zℕ∧⨉k∈y∪za⁡kb⁡k⊆⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡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⁡kf⁡k=e⁡lf⁡l
383 382 cbvixpv ⊢⨉k∈ye⁡kf⁡k=⨉l∈ye⁡lf⁡l
384 383 a1i ⊢h=o→⨉k∈ye⁡kf⁡k=⨉l∈ye⁡lf⁡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⁡kh⁡j⁡k=g⁡i⁡kh⁡i⁡k
390 389 ixpeq2dv ⊢j=i→⨉k∈yg⁡j⁡kh⁡j⁡k=⨉k∈yg⁡i⁡kh⁡i⁡k
391 390 cbviunv ⊢⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k=⋃i∈ℕ⨉k∈yg⁡i⁡kh⁡i⁡k
392 391 a1i ⊢h=o→⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k=⋃i∈ℕ⨉k∈yg⁡i⁡kh⁡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⁡kh⁡i⁡k=g⁡i⁡lh⁡i⁡l
396 395 cbvixpv ⊢⨉k∈yg⁡i⁡kh⁡i⁡k=⨉l∈yg⁡i⁡lh⁡i⁡l
397 396 a1i ⊢h=o→⨉k∈yg⁡i⁡kh⁡i⁡k=⨉l∈yg⁡i⁡lh⁡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⁡lh⁡i⁡l=g⁡i⁡lo⁡i⁡l
401 400 ixpeq2dv ⊢h=o→⨉l∈yg⁡i⁡lh⁡i⁡l=⨉l∈yg⁡i⁡lo⁡i⁡l
402 397 401 eqtrd ⊢h=o→⨉k∈yg⁡i⁡kh⁡i⁡k=⨉l∈yg⁡i⁡lo⁡i⁡l
403 402 adantr ⊢h=o∧i∈ℕ→⨉k∈yg⁡i⁡kh⁡i⁡k=⨉l∈yg⁡i⁡lo⁡i⁡l
404 403 iuneq2dv ⊢h=o→⋃i∈ℕ⨉k∈yg⁡i⁡kh⁡i⁡k=⋃i∈ℕ⨉l∈yg⁡i⁡lo⁡i⁡l
405 392 404 eqtrd ⊢h=o→⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k=⋃i∈ℕ⨉l∈yg⁡i⁡lo⁡i⁡l
406 384 405 sseq12d ⊢h=o→⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k↔⨉l∈ye⁡lf⁡l⊆⋃i∈ℕ⨉l∈yg⁡i⁡lo⁡i⁡l
407 385 387 oveq12d ⊢j=i→g⁡jL⁡yh⁡j=g⁡iL⁡yh⁡i
408 407 cbvmptv ⊢j∈ℕ⟼g⁡jL⁡yh⁡j=i∈ℕ⟼g⁡iL⁡yh⁡i
409 408 a1i ⊢h=o→j∈ℕ⟼g⁡jL⁡yh⁡j=i∈ℕ⟼g⁡iL⁡yh⁡i
410 398 oveq2d ⊢h=o→g⁡iL⁡yh⁡i=g⁡iL⁡yo⁡i
411 410 mpteq2dv ⊢h=o→i∈ℕ⟼g⁡iL⁡yh⁡i=i∈ℕ⟼g⁡iL⁡yo⁡i
412 409 411 eqtrd ⊢h=o→j∈ℕ⟼g⁡jL⁡yh⁡j=i∈ℕ⟼g⁡iL⁡yo⁡i
413 412 fveq2d ⊢h=o→sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j=sum^⁡i∈ℕ⟼g⁡iL⁡yo⁡i
414 413 breq2d ⊢h=o→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j↔eL⁡yf≤sum^⁡i∈ℕ⟼g⁡iL⁡yo⁡i
415 406 414 imbi12d ⊢h=o→⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j↔⨉l∈ye⁡lf⁡l⊆⋃i∈ℕ⨉l∈yg⁡i⁡lo⁡i⁡l→eL⁡yf≤sum^⁡i∈ℕ⟼g⁡iL⁡yo⁡i
416 415 cbvralvw ⊢∀h∈ℝyℕ⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j↔∀o∈ℝyℕ⨉l∈ye⁡lf⁡l⊆⋃i∈ℕ⨉l∈yg⁡i⁡lo⁡i⁡l→eL⁡yf≤sum^⁡i∈ℕ⟼g⁡iL⁡yo⁡i
417 416 ralbii ⊢∀g∈ℝyℕ∀h∈ℝyℕ⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j↔∀g∈ℝyℕ∀o∈ℝyℕ⨉l∈ye⁡lf⁡l⊆⋃i∈ℕ⨉l∈yg⁡i⁡lo⁡i⁡l→eL⁡yf≤sum^⁡i∈ℕ⟼g⁡iL⁡yo⁡i
418 417 ralbii ⊢∀f∈ℝy∀g∈ℝyℕ∀h∈ℝyℕ⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j↔∀f∈ℝy∀g∈ℝyℕ∀o∈ℝyℕ⨉l∈ye⁡lf⁡l⊆⋃i∈ℕ⨉l∈yg⁡i⁡lo⁡i⁡l→eL⁡yf≤sum^⁡i∈ℕ⟼g⁡iL⁡yo⁡i
419 418 ralbii ⊢∀e∈ℝy∀f∈ℝy∀g∈ℝyℕ∀h∈ℝyℕ⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j↔∀e∈ℝy∀f∈ℝy∀g∈ℝyℕ∀o∈ℝyℕ⨉l∈ye⁡lf⁡l⊆⋃i∈ℕ⨉l∈yg⁡i⁡lo⁡i⁡l→eL⁡yf≤sum^⁡i∈ℕ⟼g⁡iL⁡yo⁡i
420 419 biimpi ⊢∀e∈ℝy∀f∈ℝy∀g∈ℝyℕ∀h∈ℝyℕ⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j→∀e∈ℝy∀f∈ℝy∀g∈ℝyℕ∀o∈ℝyℕ⨉l∈ye⁡lf⁡l⊆⋃i∈ℕ⨉l∈yg⁡i⁡lo⁡i⁡l→eL⁡yf≤sum^⁡i∈ℕ⟼g⁡iL⁡yo⁡i
421 420 adantl ⊢φ∧y⊆X∧z∈X∖y∧∀e∈ℝy∀f∈ℝy∀g∈ℝyℕ∀h∈ℝyℕ⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j→∀e∈ℝy∀f∈ℝy∀g∈ℝyℕ∀o∈ℝyℕ⨉l∈ye⁡lf⁡l⊆⋃i∈ℕ⨉l∈yg⁡i⁡lo⁡i⁡l→eL⁡yf≤sum^⁡i∈ℕ⟼g⁡iL⁡yo⁡i
422 421 ad6antr ⊢φ∧y⊆X∧z∈X∖y∧∀e∈ℝy∀f∈ℝy∀g∈ℝyℕ∀h∈ℝyℕ⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j∧a∈ℝy∪z∧b∈ℝy∪z∧c∈ℝy∪zℕ∧d∈ℝy∪zℕ∧⨉k∈y∪za⁡kb⁡k⊆⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡j⁡k∧¬y=∅→∀e∈ℝy∀f∈ℝy∀g∈ℝyℕ∀o∈ℝyℕ⨉l∈ye⁡lf⁡l⊆⋃i∈ℕ⨉l∈yg⁡i⁡lo⁡i⁡l→eL⁡yf≤sum^⁡i∈ℕ⟼g⁡iL⁡yo⁡i
423 323 cbvixpv ⊢⨉k∈y∪za⁡kb⁡k=⨉l∈y∪za⁡lb⁡l
424 336 cbvixpv ⊢⨉k∈y∪zc⁡j⁡kd⁡j⁡k=⨉l∈y∪zc⁡j⁡ld⁡j⁡l
425 424 a1i ⊢j=i→⨉k∈y∪zc⁡j⁡kd⁡j⁡k=⨉l∈y∪zc⁡j⁡ld⁡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⁡ld⁡j⁡l=c⁡i⁡ld⁡i⁡l
431 430 ixpeq2dv ⊢j=i→⨉l∈y∪zc⁡j⁡ld⁡j⁡l=⨉l∈y∪zc⁡i⁡ld⁡i⁡l
432 425 431 eqtrd ⊢j=i→⨉k∈y∪zc⁡j⁡kd⁡j⁡k=⨉l∈y∪zc⁡i⁡ld⁡i⁡l
433 432 cbviunv ⊢⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡j⁡k=⋃i∈ℕ⨉l∈y∪zc⁡i⁡ld⁡i⁡l
434 423 433 sseq12i ⊢⨉k∈y∪za⁡kb⁡k⊆⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡j⁡k↔⨉l∈y∪za⁡lb⁡l⊆⋃i∈ℕ⨉l∈y∪zc⁡i⁡ld⁡i⁡l
435 434 biimpi ⊢⨉k∈y∪za⁡kb⁡k⊆⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡j⁡k→⨉l∈y∪za⁡lb⁡l⊆⋃i∈ℕ⨉l∈y∪zc⁡i⁡ld⁡i⁡l
436 435 ad2antlr ⊢φ∧y⊆X∧z∈X∖y∧∀e∈ℝy∀f∈ℝy∀g∈ℝyℕ∀h∈ℝyℕ⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j∧a∈ℝy∪z∧b∈ℝy∪z∧c∈ℝy∪zℕ∧d∈ℝy∪zℕ∧⨉k∈y∪za⁡kb⁡k⊆⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡j⁡k∧¬y=∅→⨉l∈y∪za⁡lb⁡l⊆⋃i∈ℕ⨉l∈y∪zc⁡i⁡ld⁡i⁡l
437 neqne ⊢¬y=∅→y≠∅
438 437 adantl ⊢φ∧y⊆X∧z∈X∖y∧∀e∈ℝy∀f∈ℝy∀g∈ℝyℕ∀h∈ℝyℕ⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j∧a∈ℝy∪z∧b∈ℝy∪z∧c∈ℝy∪zℕ∧d∈ℝy∪zℕ∧⨉k∈y∪za⁡kb⁡k⊆⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡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∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j∧a∈ℝy∪z∧b∈ℝy∪z∧c∈ℝy∪zℕ∧d∈ℝy∪zℕ∧⨉k∈y∪za⁡kb⁡k⊆⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡j⁡k∧¬y=∅→aL⁡y∪zb≤sum^⁡i∈ℕ⟼c⁡iL⁡y∪zd⁡i
440 273 275 oveq12d ⊢i=j→c⁡iL⁡y∪zd⁡i=c⁡jL⁡y∪zd⁡j
441 440 cbvmptv ⊢i∈ℕ⟼c⁡iL⁡y∪zd⁡i=j∈ℕ⟼c⁡jL⁡y∪zd⁡j
442 441 fveq2i ⊢sum^⁡i∈ℕ⟼c⁡iL⁡y∪zd⁡i=sum^⁡j∈ℕ⟼c⁡jL⁡y∪zd⁡j
443 442 breq2i ⊢aL⁡y∪zb≤sum^⁡i∈ℕ⟼c⁡iL⁡y∪zd⁡i↔aL⁡y∪zb≤sum^⁡j∈ℕ⟼c⁡jL⁡y∪zd⁡j
444 439 443 sylib ⊢φ∧y⊆X∧z∈X∖y∧∀e∈ℝy∀f∈ℝy∀g∈ℝyℕ∀h∈ℝyℕ⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j∧a∈ℝy∪z∧b∈ℝy∪z∧c∈ℝy∪zℕ∧d∈ℝy∪zℕ∧⨉k∈y∪za⁡kb⁡k⊆⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡j⁡k∧¬y=∅→aL⁡y∪zb≤sum^⁡j∈ℕ⟼c⁡jL⁡y∪zd⁡j
445 357 444 pm2.61dan ⊢φ∧y⊆X∧z∈X∖y∧∀e∈ℝy∀f∈ℝy∀g∈ℝyℕ∀h∈ℝyℕ⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j∧a∈ℝy∪z∧b∈ℝy∪z∧c∈ℝy∪zℕ∧d∈ℝy∪zℕ∧⨉k∈y∪za⁡kb⁡k⊆⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡j⁡k→aL⁡y∪zb≤sum^⁡j∈ℕ⟼c⁡jL⁡y∪zd⁡j
446 445 ex ⊢φ∧y⊆X∧z∈X∖y∧∀e∈ℝy∀f∈ℝy∀g∈ℝyℕ∀h∈ℝyℕ⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j∧a∈ℝy∪z∧b∈ℝy∪z∧c∈ℝy∪zℕ∧d∈ℝy∪zℕ→⨉k∈y∪za⁡kb⁡k⊆⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡j⁡k→aL⁡y∪zb≤sum^⁡j∈ℕ⟼c⁡jL⁡y∪zd⁡j
447 446 ralrimiva ⊢φ∧y⊆X∧z∈X∖y∧∀e∈ℝy∀f∈ℝy∀g∈ℝyℕ∀h∈ℝyℕ⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j∧a∈ℝy∪z∧b∈ℝy∪z∧c∈ℝy∪zℕ→∀d∈ℝy∪zℕ⨉k∈y∪za⁡kb⁡k⊆⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡j⁡k→aL⁡y∪zb≤sum^⁡j∈ℕ⟼c⁡jL⁡y∪zd⁡j
448 447 ralrimiva ⊢φ∧y⊆X∧z∈X∖y∧∀e∈ℝy∀f∈ℝy∀g∈ℝyℕ∀h∈ℝyℕ⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j∧a∈ℝy∪z∧b∈ℝy∪z→∀c∈ℝy∪zℕ∀d∈ℝy∪zℕ⨉k∈y∪za⁡kb⁡k⊆⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡j⁡k→aL⁡y∪zb≤sum^⁡j∈ℕ⟼c⁡jL⁡y∪zd⁡j
449 448 ralrimiva ⊢φ∧y⊆X∧z∈X∖y∧∀e∈ℝy∀f∈ℝy∀g∈ℝyℕ∀h∈ℝyℕ⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j∧a∈ℝy∪z→∀b∈ℝy∪z∀c∈ℝy∪zℕ∀d∈ℝy∪zℕ⨉k∈y∪za⁡kb⁡k⊆⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡j⁡k→aL⁡y∪zb≤sum^⁡j∈ℕ⟼c⁡jL⁡y∪zd⁡j
450 449 ralrimiva ⊢φ∧y⊆X∧z∈X∖y∧∀e∈ℝy∀f∈ℝy∀g∈ℝyℕ∀h∈ℝyℕ⨉k∈ye⁡kf⁡k⊆⋃j∈ℕ⨉k∈yg⁡j⁡kh⁡j⁡k→eL⁡yf≤sum^⁡j∈ℕ⟼g⁡jL⁡yh⁡j→∀a∈ℝy∪z∀b∈ℝy∪z∀c∈ℝy∪zℕ∀d∈ℝy∪zℕ⨉k∈y∪za⁡kb⁡k⊆⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡j⁡k→aL⁡y∪zb≤sum^⁡j∈ℕ⟼c⁡jL⁡y∪zd⁡j
451 177 229 450 syl2anc ⊢φ∧y⊆X∧z∈X∖y∧∀a∈ℝy∀b∈ℝy∀c∈ℝyℕ∀d∈ℝyℕ⨉k∈ya⁡kb⁡k⊆⋃j∈ℕ⨉k∈yc⁡j⁡kd⁡j⁡k→aL⁡yb≤sum^⁡j∈ℕ⟼c⁡jL⁡yd⁡j→∀a∈ℝy∪z∀b∈ℝy∪z∀c∈ℝy∪zℕ∀d∈ℝy∪zℕ⨉k∈y∪za⁡kb⁡k⊆⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡j⁡k→aL⁡y∪zb≤sum^⁡j∈ℕ⟼c⁡jL⁡y∪zd⁡j
452 451 ex ⊢φ∧y⊆X∧z∈X∖y→∀a∈ℝy∀b∈ℝy∀c∈ℝyℕ∀d∈ℝyℕ⨉k∈ya⁡kb⁡k⊆⋃j∈ℕ⨉k∈yc⁡j⁡kd⁡j⁡k→aL⁡yb≤sum^⁡j∈ℕ⟼c⁡jL⁡yd⁡j→∀a∈ℝy∪z∀b∈ℝy∪z∀c∈ℝy∪zℕ∀d∈ℝy∪zℕ⨉k∈y∪za⁡kb⁡k⊆⋃j∈ℕ⨉k∈y∪zc⁡j⁡kd⁡j⁡k→aL⁡y∪zb≤sum^⁡j∈ℕ⟼c⁡jL⁡y∪zd⁡j
453 51 76 101 126 176 452 2 findcard2d ⊢φ→∀a∈ℝX∀b∈ℝX∀c∈ℝXℕ∀d∈ℝXℕ⨉k∈Xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈Xc⁡j⁡kd⁡j⁡k→aL⁡Xb≤sum^⁡j∈ℕ⟼c⁡jL⁡Xd⁡j
454 fveq1 ⊢a=A→a⁡k=A⁡k
455 454 oveq1d ⊢a=A→a⁡kb⁡k=A⁡kb⁡k
456 455 ixpeq2dv ⊢a=A→⨉k∈Xa⁡kb⁡k=⨉k∈XA⁡kb⁡k
457 456 sseq1d ⊢a=A→⨉k∈Xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈Xc⁡j⁡kd⁡j⁡k↔⨉k∈XA⁡kb⁡k⊆⋃j∈ℕ⨉k∈Xc⁡j⁡kd⁡j⁡k
458 oveq1 ⊢a=A→aL⁡Xb=AL⁡Xb
459 458 breq1d ⊢a=A→aL⁡Xb≤sum^⁡j∈ℕ⟼c⁡jL⁡Xd⁡j↔AL⁡Xb≤sum^⁡j∈ℕ⟼c⁡jL⁡Xd⁡j
460 457 459 imbi12d ⊢a=A→⨉k∈Xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈Xc⁡j⁡kd⁡j⁡k→aL⁡Xb≤sum^⁡j∈ℕ⟼c⁡jL⁡Xd⁡j↔⨉k∈XA⁡kb⁡k⊆⋃j∈ℕ⨉k∈Xc⁡j⁡kd⁡j⁡k→AL⁡Xb≤sum^⁡j∈ℕ⟼c⁡jL⁡Xd⁡j
461 460 ralbidv ⊢a=A→∀d∈ℝXℕ⨉k∈Xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈Xc⁡j⁡kd⁡j⁡k→aL⁡Xb≤sum^⁡j∈ℕ⟼c⁡jL⁡Xd⁡j↔∀d∈ℝXℕ⨉k∈XA⁡kb⁡k⊆⋃j∈ℕ⨉k∈Xc⁡j⁡kd⁡j⁡k→AL⁡Xb≤sum^⁡j∈ℕ⟼c⁡jL⁡Xd⁡j
462 461 ralbidv ⊢a=A→∀c∈ℝXℕ∀d∈ℝXℕ⨉k∈Xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈Xc⁡j⁡kd⁡j⁡k→aL⁡Xb≤sum^⁡j∈ℕ⟼c⁡jL⁡Xd⁡j↔∀c∈ℝXℕ∀d∈ℝXℕ⨉k∈XA⁡kb⁡k⊆⋃j∈ℕ⨉k∈Xc⁡j⁡kd⁡j⁡k→AL⁡Xb≤sum^⁡j∈ℕ⟼c⁡jL⁡Xd⁡j
463 462 ralbidv ⊢a=A→∀b∈ℝX∀c∈ℝXℕ∀d∈ℝXℕ⨉k∈Xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈Xc⁡j⁡kd⁡j⁡k→aL⁡Xb≤sum^⁡j∈ℕ⟼c⁡jL⁡Xd⁡j↔∀b∈ℝX∀c∈ℝXℕ∀d∈ℝXℕ⨉k∈XA⁡kb⁡k⊆⋃j∈ℕ⨉k∈Xc⁡j⁡kd⁡j⁡k→AL⁡Xb≤sum^⁡j∈ℕ⟼c⁡jL⁡Xd⁡j
464 463 rspcva ⊢A∈ℝX∧∀a∈ℝX∀b∈ℝX∀c∈ℝXℕ∀d∈ℝXℕ⨉k∈Xa⁡kb⁡k⊆⋃j∈ℕ⨉k∈Xc⁡j⁡kd⁡j⁡k→aL⁡Xb≤sum^⁡j∈ℕ⟼c⁡jL⁡Xd⁡j→∀b∈ℝX∀c∈ℝXℕ∀d∈ℝXℕ⨉k∈XA⁡kb⁡k⊆⋃j∈ℕ⨉k∈Xc⁡j⁡kd⁡j⁡k→AL⁡Xb≤sum^⁡j∈ℕ⟼c⁡jL⁡Xd⁡j
465 26 453 464 syl2anc ⊢φ→∀b∈ℝX∀c∈ℝXℕ∀d∈ℝXℕ⨉k∈XA⁡kb⁡k⊆⋃j∈ℕ⨉k∈Xc⁡j⁡kd⁡j⁡k→AL⁡Xb≤sum^⁡j∈ℕ⟼c⁡jL⁡Xd⁡j
466 fveq1 ⊢b=B→b⁡k=B⁡k
467 466 oveq2d ⊢b=B→A⁡kb⁡k=A⁡kB⁡k
468 467 ixpeq2dv ⊢b=B→⨉k∈XA⁡kb⁡k=⨉k∈XA⁡kB⁡k
469 468 sseq1d ⊢b=B→⨉k∈XA⁡kb⁡k⊆⋃j∈ℕ⨉k∈Xc⁡j⁡kd⁡j⁡k↔⨉k∈XA⁡kB⁡k⊆⋃j∈ℕ⨉k∈Xc⁡j⁡kd⁡j⁡k
470 oveq2 ⊢b=B→AL⁡Xb=AL⁡XB
471 470 breq1d ⊢b=B→AL⁡Xb≤sum^⁡j∈ℕ⟼c⁡jL⁡Xd⁡j↔AL⁡XB≤sum^⁡j∈ℕ⟼c⁡jL⁡Xd⁡j
472 469 471 imbi12d ⊢b=B→⨉k∈XA⁡kb⁡k⊆⋃j∈ℕ⨉k∈Xc⁡j⁡kd⁡j⁡k→AL⁡Xb≤sum^⁡j∈ℕ⟼c⁡jL⁡Xd⁡j↔⨉k∈XA⁡kB⁡k⊆⋃j∈ℕ⨉k∈Xc⁡j⁡kd⁡j⁡k→AL⁡XB≤sum^⁡j∈ℕ⟼c⁡jL⁡Xd⁡j
473 472 ralbidv ⊢b=B→∀d∈ℝXℕ⨉k∈XA⁡kb⁡k⊆⋃j∈ℕ⨉k∈Xc⁡j⁡kd⁡j⁡k→AL⁡Xb≤sum^⁡j∈ℕ⟼c⁡jL⁡Xd⁡j↔∀d∈ℝXℕ⨉k∈XA⁡kB⁡k⊆⋃j∈ℕ⨉k∈Xc⁡j⁡kd⁡j⁡k→AL⁡XB≤sum^⁡j∈ℕ⟼c⁡jL⁡Xd⁡j
474 473 ralbidv ⊢b=B→∀c∈ℝXℕ∀d∈ℝXℕ⨉k∈XA⁡kb⁡k⊆⋃j∈ℕ⨉k∈Xc⁡j⁡kd⁡j⁡k→AL⁡Xb≤sum^⁡j∈ℕ⟼c⁡jL⁡Xd⁡j↔∀c∈ℝXℕ∀d∈ℝXℕ⨉k∈XA⁡kB⁡k⊆⋃j∈ℕ⨉k∈Xc⁡j⁡kd⁡j⁡k→AL⁡XB≤sum^⁡j∈ℕ⟼c⁡jL⁡Xd⁡j
475 474 rspcva ⊢B∈ℝX∧∀b∈ℝX∀c∈ℝXℕ∀d∈ℝXℕ⨉k∈XA⁡kb⁡k⊆⋃j∈ℕ⨉k∈Xc⁡j⁡kd⁡j⁡k→AL⁡Xb≤sum^⁡j∈ℕ⟼c⁡jL⁡Xd⁡j→∀c∈ℝXℕ∀d∈ℝXℕ⨉k∈XA⁡kB⁡k⊆⋃j∈ℕ⨉k∈Xc⁡j⁡kd⁡j⁡k→AL⁡XB≤sum^⁡j∈ℕ⟼c⁡jL⁡Xd⁡j
476 23 465 475 syl2anc ⊢φ→∀c∈ℝXℕ∀d∈ℝXℕ⨉k∈XA⁡kB⁡k⊆⋃j∈ℕ⨉k∈Xc⁡j⁡kd⁡j⁡k→AL⁡XB≤sum^⁡j∈ℕ⟼c⁡jL⁡Xd⁡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⁡kd⁡j⁡k=C⁡j⁡kd⁡j⁡k
480 479 ixpeq2dv ⊢c=C→⨉k∈Xc⁡j⁡kd⁡j⁡k=⨉k∈XC⁡j⁡kd⁡j⁡k
481 480 adantr ⊢c=C∧j∈ℕ→⨉k∈Xc⁡j⁡kd⁡j⁡k=⨉k∈XC⁡j⁡kd⁡j⁡k
482 481 iuneq2dv ⊢c=C→⋃j∈ℕ⨉k∈Xc⁡j⁡kd⁡j⁡k=⋃j∈ℕ⨉k∈XC⁡j⁡kd⁡j⁡k
483 482 sseq2d ⊢c=C→⨉k∈XA⁡kB⁡k⊆⋃j∈ℕ⨉k∈Xc⁡j⁡kd⁡j⁡k↔⨉k∈XA⁡kB⁡k⊆⋃j∈ℕ⨉k∈XC⁡j⁡kd⁡j⁡k
484 477 oveq1d ⊢c=C→c⁡jL⁡Xd⁡j=C⁡jL⁡Xd⁡j
485 484 mpteq2dv ⊢c=C→j∈ℕ⟼c⁡jL⁡Xd⁡j=j∈ℕ⟼C⁡jL⁡Xd⁡j
486 485 fveq2d ⊢c=C→sum^⁡j∈ℕ⟼c⁡jL⁡Xd⁡j=sum^⁡j∈ℕ⟼C⁡jL⁡Xd⁡j
487 486 breq2d ⊢c=C→AL⁡XB≤sum^⁡j∈ℕ⟼c⁡jL⁡Xd⁡j↔AL⁡XB≤sum^⁡j∈ℕ⟼C⁡jL⁡Xd⁡j
488 483 487 imbi12d ⊢c=C→⨉k∈XA⁡kB⁡k⊆⋃j∈ℕ⨉k∈Xc⁡j⁡kd⁡j⁡k→AL⁡XB≤sum^⁡j∈ℕ⟼c⁡jL⁡Xd⁡j↔⨉k∈XA⁡kB⁡k⊆⋃j∈ℕ⨉k∈XC⁡j⁡kd⁡j⁡k→AL⁡XB≤sum^⁡j∈ℕ⟼C⁡jL⁡Xd⁡j
489 488 ralbidv ⊢c=C→∀d∈ℝXℕ⨉k∈XA⁡kB⁡k⊆⋃j∈ℕ⨉k∈Xc⁡j⁡kd⁡j⁡k→AL⁡XB≤sum^⁡j∈ℕ⟼c⁡jL⁡Xd⁡j↔∀d∈ℝXℕ⨉k∈XA⁡kB⁡k⊆⋃j∈ℕ⨉k∈XC⁡j⁡kd⁡j⁡k→AL⁡XB≤sum^⁡j∈ℕ⟼C⁡jL⁡Xd⁡j
490 489 rspcva ⊢C∈ℝXℕ∧∀c∈ℝXℕ∀d∈ℝXℕ⨉k∈XA⁡kB⁡k⊆⋃j∈ℕ⨉k∈Xc⁡j⁡kd⁡j⁡k→AL⁡XB≤sum^⁡j∈ℕ⟼c⁡jL⁡Xd⁡j→∀d∈ℝXℕ⨉k∈XA⁡kB⁡k⊆⋃j∈ℕ⨉k∈XC⁡j⁡kd⁡j⁡k→AL⁡XB≤sum^⁡j∈ℕ⟼C⁡jL⁡Xd⁡j
491 17 476 490 syl2anc ⊢φ→∀d∈ℝXℕ⨉k∈XA⁡kB⁡k⊆⋃j∈ℕ⨉k∈XC⁡j⁡kd⁡j⁡k→AL⁡XB≤sum^⁡j∈ℕ⟼C⁡jL⁡Xd⁡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⁡kd⁡j⁡k=C⁡j⁡kD⁡j⁡k
495 494 ixpeq2dv ⊢d=D→⨉k∈XC⁡j⁡kd⁡j⁡k=⨉k∈XC⁡j⁡kD⁡j⁡k
496 495 adantr ⊢d=D∧j∈ℕ→⨉k∈XC⁡j⁡kd⁡j⁡k=⨉k∈XC⁡j⁡kD⁡j⁡k
497 496 iuneq2dv ⊢d=D→⋃j∈ℕ⨉k∈XC⁡j⁡kd⁡j⁡k=⋃j∈ℕ⨉k∈XC⁡j⁡kD⁡j⁡k
498 497 sseq2d ⊢d=D→⨉k∈XA⁡kB⁡k⊆⋃j∈ℕ⨉k∈XC⁡j⁡kd⁡j⁡k↔⨉k∈XA⁡kB⁡k⊆⋃j∈ℕ⨉k∈XC⁡j⁡kD⁡j⁡k
499 492 oveq2d ⊢d=D→C⁡jL⁡Xd⁡j=C⁡jL⁡XD⁡j
500 499 mpteq2dv ⊢d=D→j∈ℕ⟼C⁡jL⁡Xd⁡j=j∈ℕ⟼C⁡jL⁡XD⁡j
501 500 fveq2d ⊢d=D→sum^⁡j∈ℕ⟼C⁡jL⁡Xd⁡j=sum^⁡j∈ℕ⟼C⁡jL⁡XD⁡j
502 501 breq2d ⊢d=D→AL⁡XB≤sum^⁡j∈ℕ⟼C⁡jL⁡Xd⁡j↔AL⁡XB≤sum^⁡j∈ℕ⟼C⁡jL⁡XD⁡j
503 498 502 imbi12d ⊢d=D→⨉k∈XA⁡kB⁡k⊆⋃j∈ℕ⨉k∈XC⁡j⁡kd⁡j⁡k→AL⁡XB≤sum^⁡j∈ℕ⟼C⁡jL⁡Xd⁡j↔⨉k∈XA⁡kB⁡k⊆⋃j∈ℕ⨉k∈XC⁡j⁡kD⁡j⁡k→AL⁡XB≤sum^⁡j∈ℕ⟼C⁡jL⁡XD⁡j
504 503 rspcva ⊢D∈ℝXℕ∧∀d∈ℝXℕ⨉k∈XA⁡kB⁡k⊆⋃j∈ℕ⨉k∈XC⁡j⁡kd⁡j⁡k→AL⁡XB≤sum^⁡j∈ℕ⟼C⁡jL⁡Xd⁡j→⨉k∈XA⁡kB⁡k⊆⋃j∈ℕ⨉k∈XC⁡j⁡kD⁡j⁡k→AL⁡XB≤sum^⁡j∈ℕ⟼C⁡jL⁡XD⁡j
505 14 491 504 syl2anc ⊢φ→⨉k∈XA⁡kB⁡k⊆⋃j∈ℕ⨉k∈XC⁡j⁡kD⁡j⁡k→AL⁡XB≤sum^⁡j∈ℕ⟼C⁡jL⁡XD⁡j
506 7 505 mpd ⊢φ→AL⁡XB≤sum^⁡j∈ℕ⟼C⁡jL⁡XD⁡j