| pf |
|---|
Apply pred_ext_2 with pair_p, tuple_p 2 leaving 2 subgoals.
Let x0 of type ι be given.
Apply H0 with λ x1 x2 . tuple_p 2 x1.
Let x1 of type ι be given.
Apply pairE with ap x0 0, ap x0 1, x1, ∃ x2 . and (x2 ∈ 2) (∃ x3 . x1 = setsum x2 x3) leaving 3 subgoals.
The subproof is completed by applying H1.
Assume H2: ∃ x2 . and (x2 ∈ ap x0 0) (x1 = setsum 0 x2). Apply exandE_i with λ x2 . x2 ∈ ap x0 0, λ x2 . x1 = setsum 0 x2, ∃ x2 . and (x2 ∈ 2) (∃ x3 . x1 = setsum x2 x3) leaving 2 subgoals.
The subproof is completed by applying H2.
Let x2 of type ι be given.
Let x3 of type ο be given.
Assume H5: ∀ x4 . and (x4 ∈ 2) (∃ x5 . x1 = setsum x4 x5) ⟶ x3. Apply H5 with 0.
Apply andI with 0 ∈ 2, ∃ x4 . x1 = setsum 0 x4 leaving 2 subgoals.
The subproof is completed by applying In_0_2.
Let x4 of type ο be given.
Assume H6: ∀ x5 . x1 = setsum 0 x5 ⟶ x4. Apply H6 with x2.
The subproof is completed by applying H4.
Assume H2: ∃ x2 . and (x2 ∈ ap x0 1) (x1 = setsum 1 x2). Apply exandE_i with λ x2 . x2 ∈ ap x0 1, λ x2 . x1 = setsum 1 x2, ∃ x2 . and (x2 ∈ 2) (∃ x3 . x1 = setsum x2 x3) leaving 2 subgoals.
The subproof is completed by applying H2.
Let x2 of type ι be given.
Let x3 of type ο be given.
Assume H5: ∀ x4 . and (x4 ∈ 2) (∃ x5 . x1 = setsum x4 x5) ⟶ x3. Apply H5 with 1.
Apply andI with 1 ∈ 2, ∃ x4 . x1 = setsum 1 x4 leaving 2 subgoals.
The subproof is completed by applying In_1_2.
Let x4 of type ο be given.
Assume H6: ∀ x5 . x1 = setsum 1 x5 ⟶ x4. Apply H6 with x2.
The subproof is completed by applying H4.
Let x0 of type ι be given.
Apply pair_p_I2 with x0.
Let x1 of type ι be given.
Assume H1: x1 ∈ x0.
Apply exandE_i with λ x2 . x2 ∈ 2, λ x2 . ∃ x3 . x1 = setsum x2 x3, and (pair_p x1) (ap x1 0 ∈ 2) leaving 2 subgoals.
Apply H0 with x1.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Assume H2: x2 ∈ 2.
Assume H3: ∃ x3 . x1 = setsum x2 x3. Apply H3 with and (pair_p x1) (ap x1 0 ∈ 2).
Let x3 of type ι be given.
Apply H4 with λ x4 x5 . and (pair_p x5) (... ∈ 2).
■ |
|