Proofgold Address

Known df_minmar1__df_cpmat__df_mat2pmat__df_cpmat2mat__df_decpmat__df_pm2mp__df_chpmat__df_top__df_topon__df_topsp__df_bases__df_cld__df_ntr__df_cls__df_nei__df_lp__df_perf__df_cn : ∀ x0 : ο . (wceq cminmar1 (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cmpt (λ x3 . cfv (co (cv x1) (cv x2) cmat) cbs) (λ x3 . cmpt2 (λ x4 x5 . cv x1) (λ x4 x5 . cv x1) (λ x4 x5 . cmpt2 (λ x6 x7 . cv x1) (λ x6 x7 . cv x1) (λ x6 x7 . cif (wceq (cv x6) (cv x4)) (cif (wceq (cv x7) (cv x5)) (cfv (cv x2) cur) (cfv (cv x2) c0g)) (co (cv x6) (cv x7) (cv x3))))))) ⟶ wceq ccpmat (cmpt2 (λ x1 x2 . cfn) (λ x1 x2 . cvv) (λ x1 x2 . crab (λ x3 . wral (λ x4 . wral (λ x5 . wral (λ x6 . wceq (cfv (cv x6) (cfv (co (cv x4) (cv x5) (cv x3)) cco1)) (cfv (cv x2) c0g)) (λ x6 . cn)) (λ x5 . cv x1)) (λ x4 . cv x1)) (λ x3 . cfv (co (cv x1) (cfv (cv x2) cpl1) cmat) cbs))) ⟶ wceq cmat2pmat (cmpt2 (λ x1 x2 . cfn) (λ x1 x2 . cvv) (λ x1 x2 . cmpt (λ x3 . cfv (co (cv x1) (cv x2) cmat) cbs) (λ x3 . cmpt2 (λ x4 x5 . cv x1) (λ x4 x5 . cv x1) (λ x4 x5 . cfv (co (cv x4) (cv x5) (cv x3)) (cfv (cfv (cv x2) cpl1) cascl))))) ⟶ wceq ccpmat2mat (cmpt2 (λ x1 x2 . cfn) (λ x1 x2 . cvv) (λ x1 x2 . cmpt (λ x3 . co (cv x1) (cv x2) ccpmat) (λ x3 . cmpt2 (λ x4 x5 . cv x1) (λ x4 x5 . cv x1) (λ x4 x5 . cfv cc0 (cfv (co (cv x4) (cv x5) (cv x3)) cco1))))) ⟶ wceq cdecpmat (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cn0) (λ x1 x2 . cmpt2 (λ x3 x4 . cdm (cdm (cv x1))) (λ x3 x4 . cdm (cdm (cv x1))) (λ x3 x4 . cfv (cv x2) (cfv (co (cv x3) (cv x4) (cv x1)) cco1)))) ⟶ wceq cpm2mp (cmpt2 (λ x1 x2 . cfn) (λ x1 x2 . cvv) (λ x1 x2 . cmpt (λ x3 . cfv (co (cv x1) (cfv (cv x2) cpl1) cmat) cbs) (λ x3 . csb (co (cv x1) (cv x2) cmat) (λ x4 . csb (cfv (cv x4) cpl1) (λ x5 . co (cv x5) (cmpt (λ x6 . cn0) (λ x6 . co (co (cv x3) (cv x6) cdecpmat) (co (cv x6) (cfv (cv x4) cv1) (cfv (cfv (cv x5) cmgp) cmg)) (cfv (cv x5) cvsca))) cgsu))))) ⟶ wceq cchpmat (cmpt2 (λ x1 x2 . cfn) (λ x1 x2 . cvv) (λ x1 x2 . cmpt (λ x3 . cfv (co (cv x1) (cv x2) cmat) cbs) (λ x3 . cfv (co (co (cfv (cv x2) cv1) (cfv (co (cv x1) (cfv (cv x2) cpl1) cmat) cur) (cfv (co (cv x1) (cfv (cv x2) cpl1) cmat) cvsca)) (cfv (cv x3) (co (cv x1) (cv x2) cmat2pmat)) (cfv (co (cv x1) (cfv (cv x2) cpl1) cmat) csg)) (co (cv x1) (cfv (cv x2) cpl1) cmdat)))) ⟶ wceq ctop (cab (λ x1 . wa (wral (λ x2 . wcel (cuni (cv x2)) (cv x1)) (λ x2 . cpw (cv x1))) (wral (λ x2 . wral (λ x3 . wcel (cin (cv x2) (cv x3)) (cv x1)) (λ x3 . cv x1)) (λ x2 . cv x1)))) ⟶ wceq ctopon (cmpt (λ x1 . cvv) (λ x1 . crab (λ x2 . wceq (cv x1) (cuni (cv x2))) (λ x2 . ctop))) ⟶ wceq ctps (cab (λ x1 . wcel (cfv (cv x1) ctopn) (cfv (cfv (cv x1) cbs) ctopon))) ⟶ wceq ctb (cab (λ x1 . wral (λ x2 . wral (λ x3 . wss (cin (cv x2) (cv x3)) (cuni (cin (cv x1) (cpw (cin (cv x2) (cv x3)))))) (λ x3 . cv x1)) (λ x2 . cv x1))) ⟶ wceq ccld (cmpt (λ x1 . ctop) (λ x1 . crab (λ x2 . wcel (cdif (cuni (cv x1)) (cv x2)) (cv x1)) (λ x2 . cpw (cuni (cv x1))))) ⟶ wceq cnt (cmpt (λ x1 . ctop) (λ x1 . cmpt (λ x2 . cpw (cuni (cv x1))) (λ x2 . cuni (cin (cv x1) (cpw (cv x2)))))) ⟶ wceq ccl (cmpt (λ x1 . ctop) (λ x1 . cmpt (λ x2 . cpw (cuni (cv x1))) (λ x2 . cint (crab (λ x3 . wss (cv x2) (cv x3)) (λ x3 . cfv (cv x1) ccld))))) ⟶ wceq cnei (cmpt (λ x1 . ctop) (λ x1 . cmpt (λ x2 . cpw (cuni (cv x1))) (λ x2 . crab (λ x3 . wrex (λ x4 . wa (wss (cv x2) (cv x4)) (wss (cv x4) (cv x3))) (λ x4 . cv x1)) (λ x3 . cpw (cuni (cv x1)))))) ⟶ wceq clp (cmpt (λ x1 . ctop) (λ x1 . cmpt (λ x2 . cpw (cuni (cv x1))) (λ x2 . cab (λ x3 . wcel (cv x3) (cfv (cdif (cv x2) (csn (cv x3))) (cfv (cv x1) ccl)))))) ⟶ wceq cperf (crab (λ x1 . wceq (cfv (cuni (cv x1)) (cfv (cv x1) clp)) (cuni (cv x1))) (λ x1 . ctop)) ⟶ wceq ccn (cmpt2 (λ x1 x2 . ctop) (λ x1 x2 . ctop) (λ x1 x2 . crab (λ x3 . wral (λ x4 . wcel (cima (ccnv (cv x3)) (cv x4)) (cv x1)) (λ x4 . cv x2)) (λ x3 . co (cuni (cv x2)) (cuni (cv x1)) cmap))) ⟶ x0) ⟶ x0
Theorem df_minmar1 : wceq cminmar1 (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cmpt (λ x2 . cfv (co (cv x0) (cv x1) cmat) cbs) (λ x2 . cmpt2 (λ x3 x4 . cv x0) (λ x3 x4 . cv x0) (λ x3 x4 . cmpt2 (λ x5 x6 . cv x0) (λ x5 x6 . cv x0) (λ x5 x6 . cif (wceq (cv x5) (cv x3)) (cif (wceq (cv x6) (cv x4)) (cfv (cv x1) cur) (cfv (cv x1) c0g)) (co (cv x5) (cv x6) (cv x2))))))) (proof)
Theorem df_cpmat : wceq ccpmat (cmpt2 (λ x0 x1 . cfn) (λ x0 x1 . cvv) (λ x0 x1 . crab (λ x2 . wral (λ x3 . wral (λ x4 . wral (λ x5 . wceq (cfv (cv x5) (cfv (co (cv x3) (cv x4) (cv x2)) cco1)) (cfv (cv x1) c0g)) (λ x5 . cn)) (λ x4 . cv x0)) (λ x3 . cv x0)) (λ x2 . cfv (co (cv x0) (cfv (cv x1) cpl1) cmat) cbs))) (proof)
Theorem df_mat2pmat : wceq cmat2pmat (cmpt2 (λ x0 x1 . cfn) (λ x0 x1 . cvv) (λ x0 x1 . cmpt (λ x2 . cfv (co (cv x0) (cv x1) cmat) cbs) (λ x2 . cmpt2 (λ x3 x4 . cv x0) (λ x3 x4 . cv x0) (λ x3 x4 . cfv (co (cv x3) (cv x4) (cv x2)) (cfv (cfv (cv x1) cpl1) cascl))))) (proof)
Theorem df_cpmat2mat : wceq ccpmat2mat (cmpt2 (λ x0 x1 . cfn) (λ x0 x1 . cvv) (λ x0 x1 . cmpt (λ x2 . co (cv x0) (cv x1) ccpmat) (λ x2 . cmpt2 (λ x3 x4 . cv x0) (λ x3 x4 . cv x0) (λ x3 x4 . cfv cc0 (cfv (co (cv x3) (cv x4) (cv x2)) cco1))))) (proof)
Theorem df_decpmat : wceq cdecpmat (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cn0) (λ x0 x1 . cmpt2 (λ x2 x3 . cdm (cdm (cv x0))) (λ x2 x3 . cdm (cdm (cv x0))) (λ x2 x3 . cfv (cv x1) (cfv (co (cv x2) (cv x3) (cv x0)) cco1)))) (proof)
Theorem df_pm2mp : wceq cpm2mp (cmpt2 (λ x0 x1 . cfn) (λ x0 x1 . cvv) (λ x0 x1 . cmpt (λ x2 . cfv (co (cv x0) (cfv (cv x1) cpl1) cmat) cbs) (λ x2 . csb (co (cv x0) (cv x1) cmat) (λ x3 . csb (cfv (cv x3) cpl1) (λ x4 . co (cv x4) (cmpt (λ x5 . cn0) (λ x5 . co (co (cv x2) (cv x5) cdecpmat) (co (cv x5) (cfv (cv x3) cv1) (cfv (cfv (cv x4) cmgp) cmg)) (cfv (cv x4) cvsca))) cgsu))))) (proof)
Theorem df_chpmat : wceq cchpmat (cmpt2 (λ x0 x1 . cfn) (λ x0 x1 . cvv) (λ x0 x1 . cmpt (λ x2 . cfv (co (cv x0) (cv x1) cmat) cbs) (λ x2 . cfv (co (co (cfv (cv x1) cv1) (cfv (co (cv x0) (cfv (cv x1) cpl1) cmat) cur) (cfv (co (cv x0) (cfv (cv x1) cpl1) cmat) cvsca)) (cfv (cv x2) (co (cv x0) (cv x1) cmat2pmat)) (cfv (co (cv x0) (cfv (cv x1) cpl1) cmat) csg)) (co (cv x0) (cfv (cv x1) cpl1) cmdat)))) (proof)
Theorem df_top : wceq ctop (cab (λ x0 . wa (wral (λ x1 . wcel (cuni (cv x1)) (cv x0)) (λ x1 . cpw (cv x0))) (wral (λ x1 . wral (λ x2 . wcel (cin (cv x1) (cv x2)) (cv x0)) (λ x2 . cv x0)) (λ x1 . cv x0)))) (proof)
Theorem df_topon : wceq ctopon (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wceq (cv x0) (cuni (cv x1))) (λ x1 . ctop))) (proof)
Theorem df_topsp : wceq ctps (cab (λ x0 . wcel (cfv (cv x0) ctopn) (cfv (cfv (cv x0) cbs) ctopon))) (proof)
Theorem df_bases : wceq ctb (cab (λ x0 . wral (λ x1 . wral (λ x2 . wss (cin (cv x1) (cv x2)) (cuni (cin (cv x0) (cpw (cin (cv x1) (cv x2)))))) (λ x2 . cv x0)) (λ x1 . cv x0))) (proof)
Theorem df_cld : wceq ccld (cmpt (λ x0 . ctop) (λ x0 . crab (λ x1 . wcel (cdif (cuni (cv x0)) (cv x1)) (cv x0)) (λ x1 . cpw (cuni (cv x0))))) (proof)
Theorem df_ntr : wceq cnt (cmpt (λ x0 . ctop) (λ x0 . cmpt (λ x1 . cpw (cuni (cv x0))) (λ x1 . cuni (cin (cv x0) (cpw (cv x1)))))) (proof)
Theorem df_cls : wceq ccl (cmpt (λ x0 . ctop) (λ x0 . cmpt (λ x1 . cpw (cuni (cv x0))) (λ x1 . cint (crab (λ x2 . wss (cv x1) (cv x2)) (λ x2 . cfv (cv x0) ccld))))) (proof)
Theorem df_nei : wceq cnei (cmpt (λ x0 . ctop) (λ x0 . cmpt (λ x1 . cpw (cuni (cv x0))) (λ x1 . crab (λ x2 . wrex (λ x3 . wa (wss (cv x1) (cv x3)) (wss (cv x3) (cv x2))) (λ x3 . cv x0)) (λ x2 . cpw (cuni (cv x0)))))) (proof)
Theorem df_lp : wceq clp (cmpt (λ x0 . ctop) (λ x0 . cmpt (λ x1 . cpw (cuni (cv x0))) (λ x1 . cab (λ x2 . wcel (cv x2) (cfv (cdif (cv x1) (csn (cv x2))) (cfv (cv x0) ccl)))))) (proof)
Theorem df_perf : wceq cperf (crab (λ x0 . wceq (cfv (cuni (cv x0)) (cfv (cv x0) clp)) (cuni (cv x0))) (λ x0 . ctop)) (proof)
Theorem df_cn : wceq ccn (cmpt2 (λ x0 x1 . ctop) (λ x0 x1 . ctop) (λ x0 x1 . crab (λ x2 . wral (λ x3 . wcel (cima (ccnv (cv x2)) (cv x3)) (cv x0)) (λ x3 . cv x1)) (λ x2 . co (cuni (cv x1)) (cuni (cv x0)) cmap))) (proof)