Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Let x2 of type ι be given.
Assume H1:
∀ x3 . In x3 x0 ⟶ In (ap x2 x3) (x1 x3).
Apply unknownprop_dc1e02deebcd6c87d85e338d34fdf4caf44c0c3d3d8c7882c6574d39d68b0003 with
λ x3 x4 : ι → (ι → ι) → ι . In x2 (x4 x0 (λ x5 . x1 x5)).
Apply unknownprop_646b3add51cf8f8e84959b456822a93c7e59b2f394a14897b6752b9d28c1a75d with
Power (lam x0 (λ x3 . Union (x1 x3))),
λ x3 . ∀ x4 . In x4 x0 ⟶ In (ap x3 x4) (x1 x4),
x2 leaving 2 subgoals.
Apply unknownprop_9a40b4678ae1931e61346f9ab9e405ec760f2f9d44b3be548b52a8b2ddb78559 with
lam x0 (λ x3 . Union (x1 x3)),
x2.
Apply unknownprop_c3fe42b21df0810041479a97b374de73f7754e07c8af1c88386a1e7dc0aad10f with
x2,
lam x0 (λ x3 . Union (x1 x3)).
Let x3 of type ι be given.
Apply andE with
setsum_p x3,
In (ap x3 0) x0,
In x3 (lam x0 (λ x4 . Union (x1 x4))) leaving 2 subgoals.
Apply H0 with
x3.
The subproof is completed by applying H2.
Apply unknownprop_56bd0714abefd533b13603d171a24196c02fb0b6a0af8036287a8ec089f8957d with
λ x4 x5 : ι → ο . x5 x3 ⟶ In (ap x3 0) x0 ⟶ In x3 (lam x0 (λ x6 . Union (x1 x6))).
Assume H4:
In (ap x3 0) x0.
Apply H3 with
λ x4 x5 . In x4 (lam x0 (λ x6 . Union (x1 x6))).
Apply unknownprop_1633a25a08ee627a1613041ad1ebe0a4535d0c6ce109cb609e7d9a519dad2f25 with
x0,
λ x4 . Union (x1 x4),
ap x3 0,
ap x3 1 leaving 2 subgoals.
The subproof is completed by applying H4.
Apply unknownprop_bb7319fda7123d5f775b6b29aaea60dee8b8450dbda3fb13de42ee7deaa111d5 with
x1 (ap x3 0),
ap x3 1,
ap x2 (ap x3 0) leaving 2 subgoals.
Apply unknownprop_5790343a8368d4f3aa514e68a19a3e4824006be2aed8a0a7a707f542e4c79154 with
x2,
ap x3 0,
ap x3 1.
Apply H3 with
λ x4 x5 . In x5 x2.
The subproof is completed by applying H2.
Apply H1 with
ap x3 0.
The subproof is completed by applying H4.
The subproof is completed by applying H1.