Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Apply explicit_Group_identity_unique with {x1 ∈ setexp x0 x0|bij x0 x0 (λ x2 . ap x1 x2)}, λ x1 x2 . lam x0 (λ x3 . ap x2 (ap x1 x3)), explicit_Group_identity {x1 ∈ setexp x0 x0|bij x0 x0 (λ x2 . ap x1 x2)} (λ x1 x2 . lam x0 (λ x3 . ap x2 (ap x1 x3))), lam x0 (λ x1 . x1) leaving 4 subgoals.
Apply explicit_Group_identity_in with {x1 ∈ setexp x0 x0|bij x0 x0 (λ x2 . ap x1 x2)}, λ x1 x2 . lam x0 (λ x3 . ap x2 (ap x1 x3)).
The subproof is completed by applying explicit_Group_symgroup with x0.
The subproof is completed by applying unknownprop_5e0fd89c1af2988efb9109729fe2f29a67df0b5d1c5db069bd27d2e54ddad812 with x0.
Apply explicit_Group_identity_lid with {x1 ∈ setexp x0 x0|bij x0 x0 (λ x2 . ap x1 x2)}, λ x1 x2 . lam x0 (λ x3 . ap x2 (ap x1 x3)).
The subproof is completed by applying explicit_Group_symgroup with x0.
Let x1 of type ι be given.
Assume H0: x1 ∈ {x2 ∈ setexp x0 x0|bij x0 x0 (ap x2)}.
Apply SepE with setexp x0 x0, λ x2 . bij x0 x0 (λ x3 . ap x2 x3), x1, lam x0 (λ x2 . ap (lam x0 (λ x3 . x3)) (ap x1 x2)) = x1 leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H1: x1 ∈ setexp x0 x0.
Assume H2: bij x0 x0 (ap x1).
Claim L3: ∀ x2 . x2 ∈ x0 ⟶ ap x1 x2 ∈ x0
Let x2 of type ι be given.
Assume H3: x2 ∈ x0.
Apply ap_Pi with x0, λ x3 . x0, x1, x2 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
Apply Pi_ext with x0, λ x2 . x0, lam x0 (λ x2 . ap (lam x0 (λ x3 . x3)) (ap x1 x2)), x1 leaving 3 subgoals.
Apply lam_Pi with x0, λ x2 . x0, λ x2 . ap (lam x0 (λ x3 . x3)) (ap x1 x2).
Let x2 of type ι be given.
Assume H4: x2 ∈ x0.
Apply beta with x0, λ x3 . x3, ap x1 x2, λ x3 x4 . x4 ∈ x0 leaving 2 subgoals.
Apply L3 with x2.
The subproof is completed by applying H4.
Apply L3 with x2.
The subproof is completed by applying H4.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Assume H4: x2 ∈ x0.
Apply beta with x0, λ x3 . ap (lam x0 (λ x4 . x4)) (ap x1 x3), x2, λ x3 x4 . x4 = ap x1 x2 leaving 2 subgoals.
The subproof is completed by applying H4.
Apply beta with x0, λ x3 . x3, ap x1 x2.
Apply L3 with x2.
The subproof is completed by applying H4.
■