Let x0 of type ο be given.

Assume H0: ∀ x1 . (∃ x2 : ι → ι . MetaCat_terminal_p struct_c PreContinuousHom struct_id struct_comp x1 x2) ⟶ x0.

Apply H0 with pack_c 1 (λ x1 : ι → ο . False).

Let x1 of type ο be given.

Assume H1: ∀ x2 : ι → ι . MetaCat_terminal_p struct_c PreContinuousHom struct_id struct_comp (pack_c 1 (λ x3 : ι → ο . False)) x2 ⟶ x1.

Apply H1 with λ x2 . lam (ap x2 0) (λ x3 . 0).

Apply andI with struct_c (pack_c 1 (λ x2 : ι → ο . False)), ∀ x2 . struct_c x2 ⟶ and (PreContinuousHom x2 (pack_c 1 (λ x3 : ι → ο . False)) (lam (ap x2 0) (λ x3 . 0))) (∀ x3 . PreContinuousHom x2 (pack_c 1 (λ x4 : ι → ο . False)) x3 ⟶ x3 = lam (ap x2 0) (λ x4 . 0)) leaving 2 subgoals.

The subproof is completed by applying pack_struct_c_I with 1, λ x2 : ι → ο . False.

Let x2 of type ι be given.

Assume H2: struct_c x2.

Apply H2 with λ x3 . and (PreContinuousHom x3 (pack_c 1 (λ x4 : ι → ο . False)) (lam (ap x3 0) (λ x4 . 0))) (∀ x4 . PreContinuousHom x3 (pack_c 1 (λ x5 : ι → ο . False)) x4 ⟶ x4 = lam (ap x3 0) (λ x5 . 0)).

Let x3 of type ι be given.

Let x4 of type (ι → ο) → ο be given.

Apply andI with PreContinuousHom (pack_c x3 x4) (pack_c 1 (λ x5 : ι → ο . False)) (lam (ap (pack_c x3 x4) 0) (λ x5 . 0)), ∀ x5 . PreContinuousHom (pack_c x3 x4) (pack_c 1 (λ x6 : ι → ο . False)) x5 ⟶ x5 = lam (ap (pack_c x3 x4) 0) (λ x6 . 0) leaving 2 subgoals.

Apply pack_c_0_eq2 with x3, x4, λ x5 x6 . PreContinuousHom (pack_c x3 x4) (pack_c 1 (λ x7 : ι → ο . False)) (lam x5 (λ x7 . 0)).

Apply unknownprop_147946d52b6747e7a3735111f3622ca84b157f241b7b107aab3bab9bb651af48 with x3, 1, x4, λ x5 : ι → ο . False, lam x3 (λ x5 . 0), λ x5 x6 : ο . x6.

Apply andI with lam x3 (λ x5 . 0) ∈ setexp 1 x3, ∀ x5 : ι → ο . (∀ x6 . x5 x6 ⟶ x6 ∈ 1) ⟶ (λ x6 : ι → ο . False) x5 ⟶ x4 (λ x6 . and (x6 ∈ x3) (x5 (ap (lam x3 (λ x7 . 0)) x6))) leaving 2 subgoals.

Apply lam_Pi with x3, λ x5 . 1, λ x5 . 0.

Let x5 of type ι be given.

Assume H3: x5 ∈ x3.

The subproof is completed by applying In_0_1.

Let x5 of type ι → ο be given.

Assume H3: ∀ x6 . x5 x6 ⟶ x6 ∈ 1.

Assume H4: (λ x6 : ι → ο . False) x5.

Apply FalseE with x4 (λ x6 . and (x6 ∈ x3) (x5 (ap (lam x3 (λ x7 . 0)) x6))).

The subproof is completed by applying H4.

Let x5 of type ι be given.

Apply unknownprop_147946d52b6747e7a3735111f3622ca84b157f241b7b107aab3bab9bb651af48 with x3, 1, x4, λ x6 : ι → ο . False, x5, λ x6 x7 : ο . x7 ⟶ x5 = lam (ap (pack_c x3 x4) 0) (λ x8 . 0).

Assume H3: and (x5 ∈ setexp 1 x3) (∀ x6 : ι → ο . ... ⟶ ... ⟶ x4 ...).

...

■

Proofgold Proof