Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Let x2 of type ι be given.
Apply unknownprop_dc1e02deebcd6c87d85e338d34fdf4caf44c0c3d3d8c7882c6574d39d68b0003 with
λ x3 x4 : ι → (ι → ι) → ι . In x2 (x4 x0 (λ x5 . x1 x5)) ⟶ ∀ x5 : ο . ((∀ x6 . In x6 x2 ⟶ and (setsum_p x6) (In (ap x6 0) x0)) ⟶ (∀ x6 . In x6 x0 ⟶ In (ap x2 x6) (x1 x6)) ⟶ x5) ⟶ x5.
Assume H0:
In x2 ((λ x3 . λ x4 : ι → ι . Sep (Power (lam x3 (λ x5 . Union (x4 x5)))) (λ x5 . ∀ x6 . In x6 x3 ⟶ In (ap x5 x6) (x4 x6))) x0 (λ x3 . x1 x3)).
Let x3 of type ο be given.
Assume H1:
(∀ x4 . In x4 x2 ⟶ and (setsum_p x4) (In (ap x4 0) x0)) ⟶ (∀ x4 . In x4 x0 ⟶ In (ap x2 x4) (x1 x4)) ⟶ x3.
Apply unknownprop_6a6b356f855b99f3fbff4effcb62e3ee6aa23839e10650eb28a503a368c2bb09 with
Power (lam x0 (λ x4 . Union (x1 x4))),
λ x4 . ∀ x5 . In x5 x0 ⟶ In (ap x4 x5) (x1 x5),
x2,
x3 leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H3:
∀ x4 . In x4 x0 ⟶ In (ap x2 x4) (x1 x4).
Apply H1 leaving 2 subgoals.
Let x4 of type ι be given.
Apply unknownprop_b8811722bb772bba243207d8ee471ba24f8b88e821f7737307414168e638d2c6 with
lam x0 (λ x5 . Union (x1 x5)),
x2.
The subproof is completed by applying H2.
Apply unknownprop_cc8f63ddfbec05087d89028647ba2c7b89da93a15671b61ba228d6841bbab5e9 with
x2,
lam x0 (λ x5 . Union (x1 x5)),
x4 leaving 2 subgoals.
The subproof is completed by applying L5.
The subproof is completed by applying H4.
Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with
setsum_p x4,
In (ap x4 0) x0 leaving 2 subgoals.
Apply unknownprop_1006fa3f7c99c66c88f5928e4fedbeb0f7fbd3d083c6fed73e217b8c50a9a235 with
x0,
λ x5 . Union (x1 x5),
x4.
The subproof is completed by applying L6.
Apply L7 with
λ x5 x6 . setsum_p x5.
The subproof is completed by applying unknownprop_f61ccefc6bc57eb6c116b3bc3f27a552fe11c91770c4e9cfa989285bab91c3f5 with
proj0 x4,
proj1 x4.
Apply unknownprop_1196af63ee0683855b52ee91758b2774097fb63c424fb057b925104c7b77f7ef with
x0,
λ x5 . Union (x1 x5),
x4.
The subproof is completed by applying L6.
The subproof is completed by applying H3.