Search for blocks/addresses/...

Proofgold Proof

pf
Claim L0: ∀ x0 . x0 ∈ prim6 0 ⟶ ∀ x1 . x1 ∈ prim6 0 ⟶ setprod x0 x1 ∈ prim6 0
Apply unknownprop_168889ac2767512e36c59c4d8bc32e41d805ce681fce6d41f1fc82bd258fd1a7 with prim6 0 leaving 2 subgoals.
The subproof is completed by applying UnivOf_TransSet with 0.
The subproof is completed by applying UnivOf_ZF_closed with 0.
Claim L1: ∀ x0 . x0 ∈ prim6 0 ⟶ ∀ x1 . x1 ∈ prim6 0 ⟶ setexp x1 x0 ∈ prim6 0
Apply unknownprop_2485261293fc9246221e480807168b56c614ccc7ff1e05b547a7c25cb11fc16e with prim6 0 leaving 2 subgoals.
The subproof is completed by applying UnivOf_TransSet with 0.
The subproof is completed by applying UnivOf_ZF_closed with 0.
Apply unknownprop_d378b2c894939b96acaefeb7b90d3a62ba779e2a2ea4390f7801c59b07291ce2 with λ x0 . x0 ∈ prim6 0 leaving 2 subgoals.
The subproof is completed by applying L0.
The subproof is completed by applying L1.
■