Proofgold Address

Known df_oposet__df_cmtN__df_ol__df_oml__df_covers__df_ats__df_atl__df_cvlat__df_hlat__df_llines__df_lplanes__df_lvols__df_lines__df_pointsN__df_psubsp__df_pmap__df_padd__df_pclN : ∀ x0 : ο . (wceq cops (crab (λ x1 . wa (wa (wcel (cfv (cv x1) cbs) (cdm (cfv (cv x1) club))) (wcel (cfv (cv x1) cbs) (cdm (cfv (cv x1) cglb)))) (wex (λ x2 . wa (wceq (cv x2) (cfv (cv x1) coc)) (wral (λ x3 . wral (λ x4 . w3a (w3a (wcel (cfv (cv x3) (cv x2)) (cfv (cv x1) cbs)) (wceq (cfv (cfv (cv x3) (cv x2)) (cv x2)) (cv x3)) (wbr (cv x3) (cv x4) (cfv (cv x1) cple) ⟶ wbr (cfv (cv x4) (cv x2)) (cfv (cv x3) (cv x2)) (cfv (cv x1) cple))) (wceq (co (cv x3) (cfv (cv x3) (cv x2)) (cfv (cv x1) cjn)) (cfv (cv x1) cp1)) (wceq (co (cv x3) (cfv (cv x3) (cv x2)) (cfv (cv x1) cmee)) (cfv (cv x1) cp0))) (λ x4 . cfv (cv x1) cbs)) (λ x3 . cfv (cv x1) cbs))))) (λ x1 . cpo)) ⟶ wceq ccmtN (cmpt (λ x1 . cvv) (λ x1 . copab (λ x2 x3 . w3a (wcel (cv x2) (cfv (cv x1) cbs)) (wcel (cv x3) (cfv (cv x1) cbs)) (wceq (cv x2) (co (co (cv x2) (cv x3) (cfv (cv x1) cmee)) (co (cv x2) (cfv (cv x3) (cfv (cv x1) coc)) (cfv (cv x1) cmee)) (cfv (cv x1) cjn)))))) ⟶ wceq col (cin clat cops) ⟶ wceq coml (crab (λ x1 . wral (λ x2 . wral (λ x3 . wbr (cv x2) (cv x3) (cfv (cv x1) cple) ⟶ wceq (cv x3) (co (cv x2) (co (cv x3) (cfv (cv x2) (cfv (cv x1) coc)) (cfv (cv x1) cmee)) (cfv (cv x1) cjn))) (λ x3 . cfv (cv x1) cbs)) (λ x2 . cfv (cv x1) cbs)) (λ x1 . col)) ⟶ wceq ccvr (cmpt (λ x1 . cvv) (λ x1 . copab (λ x2 x3 . w3a (wa (wcel (cv x2) (cfv (cv x1) cbs)) (wcel (cv x3) (cfv (cv x1) cbs))) (wbr (cv x2) (cv x3) (cfv (cv x1) cplt)) (wn (wrex (λ x4 . wa (wbr (cv x2) (cv x4) (cfv (cv x1) cplt)) (wbr (cv x4) (cv x3) (cfv (cv x1) cplt))) (λ x4 . cfv (cv x1) cbs)))))) ⟶ wceq catm (cmpt (λ x1 . cvv) (λ x1 . crab (λ x2 . wbr (cfv (cv x1) cp0) (cv x2) (cfv (cv x1) ccvr)) (λ x2 . cfv (cv x1) cbs))) ⟶ wceq cal (crab (λ x1 . wa (wcel (cfv (cv x1) cbs) (cdm (cfv (cv x1) cglb))) (wral (λ x2 . wne (cv x2) (cfv (cv x1) cp0) ⟶ wrex (λ x3 . wbr (cv x3) (cv x2) (cfv (cv x1) cple)) (λ x3 . cfv (cv x1) catm)) (λ x2 . cfv (cv x1) cbs))) (λ x1 . clat)) ⟶ wceq clc (crab (λ x1 . wral (λ x2 . wral (λ x3 . wral (λ x4 . wa (wn (wbr (cv x2) (cv x4) (cfv (cv x1) cple))) (wbr (cv x2) (co (cv x4) (cv x3) (cfv (cv x1) cjn)) (cfv (cv x1) cple)) ⟶ wbr (cv x3) (co (cv x4) (cv x2) (cfv (cv x1) cjn)) (cfv (cv x1) cple)) (λ x4 . cfv (cv x1) cbs)) (λ x3 . cfv (cv x1) catm)) (λ x2 . cfv (cv x1) catm)) (λ x1 . cal)) ⟶ wceq chlt (crab (λ x1 . wa (wral (λ x2 . wral (λ x3 . wne (cv x2) (cv x3) ⟶ wrex (λ x4 . w3a (wne (cv x4) (cv x2)) (wne (cv x4) (cv x3)) (wbr (cv x4) (co (cv x2) (cv x3) (cfv (cv x1) cjn)) (cfv (cv x1) cple))) (λ x4 . cfv (cv x1) catm)) (λ x3 . cfv (cv x1) catm)) (λ x2 . cfv (cv x1) catm)) (wrex (λ x2 . wrex (λ x3 . wrex (λ x4 . wa (wa (wbr (cfv (cv x1) cp0) (cv x2) (cfv (cv x1) cplt)) (wbr (cv x2) (cv x3) (cfv (cv x1) cplt))) (wa (wbr (cv x3) (cv x4) (cfv (cv x1) cplt)) (wbr (cv x4) (cfv (cv x1) cp1) (cfv (cv x1) cplt)))) (λ x4 . cfv (cv x1) cbs)) (λ x3 . cfv (cv x1) cbs)) (λ x2 . cfv (cv x1) cbs))) (λ x1 . cin (cin coml ccla) clc)) ⟶ wceq clln (cmpt (λ x1 . cvv) (λ x1 . crab (λ x2 . wrex (λ x3 . wbr (cv x3) (cv x2) (cfv (cv x1) ccvr)) (λ x3 . cfv (cv x1) catm)) (λ x2 . cfv (cv x1) cbs))) ⟶ wceq clpl (cmpt (λ x1 . cvv) (λ x1 . crab (λ x2 . wrex (λ x3 . wbr (cv x3) (cv x2) (cfv (cv x1) ccvr)) (λ x3 . cfv (cv x1) clln)) (λ x2 . cfv (cv x1) cbs))) ⟶ wceq clvol (cmpt (λ x1 . cvv) (λ x1 . crab (λ x2 . wrex (λ x3 . wbr (cv x3) (cv x2) (cfv (cv x1) ccvr)) (λ x3 . cfv (cv x1) clpl)) (λ x2 . cfv (cv x1) cbs))) ⟶ wceq clines (cmpt (λ x1 . cvv) (λ x1 . cab (λ x2 . wrex (λ x3 . wrex (λ x4 . wa (wne (cv x3) (cv x4)) (wceq (cv x2) (crab (λ x5 . wbr (cv x5) (co (cv x3) (cv x4) (cfv (cv x1) cjn)) (cfv (cv x1) cple)) (λ x5 . cfv (cv x1) catm)))) (λ x4 . cfv (cv x1) catm)) (λ x3 . cfv (cv x1) catm)))) ⟶ wceq cpointsN (cmpt (λ x1 . cvv) (λ x1 . cab (λ x2 . wrex (λ x3 . wceq (cv x2) (csn (cv x3))) (λ x3 . cfv (cv x1) catm)))) ⟶ wceq cpsubsp (cmpt (λ x1 . cvv) (λ x1 . cab (λ x2 . wa (wss (cv x2) (cfv (cv x1) catm)) (wral (λ x3 . wral (λ x4 . wral (λ x5 . wbr (cv x5) (co (cv x3) (cv x4) (cfv (cv x1) cjn)) (cfv (cv x1) cple) ⟶ wcel (cv x5) (cv x2)) (λ x5 . cfv (cv x1) catm)) (λ x4 . cv x2)) (λ x3 . cv x2))))) ⟶ wceq cpmap (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) cbs) (λ x2 . crab (λ x3 . wbr (cv x3) (cv x2) (cfv (cv x1) cple)) (λ x3 . cfv (cv x1) catm)))) ⟶ wceq cpadd (cmpt (λ x1 . cvv) (λ x1 . cmpt2 (λ x2 x3 . cpw (cfv (cv x1) catm)) (λ x2 x3 . cpw (cfv (cv x1) catm)) (λ x2 x3 . cun (cun (cv x2) (cv x3)) (crab (λ x4 . wrex (λ x5 . wrex (λ x6 . wbr (cv x4) (co (cv x5) (cv x6) (cfv (cv x1) cjn)) (cfv (cv x1) cple)) (λ x6 . cv x3)) (λ x5 . cv x2)) (λ x4 . cfv (cv x1) catm))))) ⟶ wceq cpclN (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cpw (cfv (cv x1) catm)) (λ x2 . cint (crab (λ x3 . wss (cv x2) (cv x3)) (λ x3 . cfv (cv x1) cpsubsp))))) ⟶ x0) ⟶ x0
Theorem df_oposet : wceq cops (crab (λ x0 . wa (wa (wcel (cfv (cv x0) cbs) (cdm (cfv (cv x0) club))) (wcel (cfv (cv x0) cbs) (cdm (cfv (cv x0) cglb)))) (wex (λ x1 . wa (wceq (cv x1) (cfv (cv x0) coc)) (wral (λ x2 . wral (λ x3 . w3a (w3a (wcel (cfv (cv x2) (cv x1)) (cfv (cv x0) cbs)) (wceq (cfv (cfv (cv x2) (cv x1)) (cv x1)) (cv x2)) (wbr (cv x2) (cv x3) (cfv (cv x0) cple) ⟶ wbr (cfv (cv x3) (cv x1)) (cfv (cv x2) (cv x1)) (cfv (cv x0) cple))) (wceq (co (cv x2) (cfv (cv x2) (cv x1)) (cfv (cv x0) cjn)) (cfv (cv x0) cp1)) (wceq (co (cv x2) (cfv (cv x2) (cv x1)) (cfv (cv x0) cmee)) (cfv (cv x0) cp0))) (λ x3 . cfv (cv x0) cbs)) (λ x2 . cfv (cv x0) cbs))))) (λ x0 . cpo))
Theorem df_cmtN : wceq ccmtN (cmpt (λ x0 . cvv) (λ x0 . copab (λ x1 x2 . w3a (wcel (cv x1) (cfv (cv x0) cbs)) (wcel (cv x2) (cfv (cv x0) cbs)) (wceq (cv x1) (co (co (cv x1) (cv x2) (cfv (cv x0) cmee)) (co (cv x1) (cfv (cv x2) (cfv (cv x0) coc)) (cfv (cv x0) cmee)) (cfv (cv x0) cjn))))))
Theorem df_ol : wceq col (cin clat cops)
Theorem df_oml : wceq coml (crab (λ x0 . wral (λ x1 . wral (λ x2 . wbr (cv x1) (cv x2) (cfv (cv x0) cple) ⟶ wceq (cv x2) (co (cv x1) (co (cv x2) (cfv (cv x1) (cfv (cv x0) coc)) (cfv (cv x0) cmee)) (cfv (cv x0) cjn))) (λ x2 . cfv (cv x0) cbs)) (λ x1 . cfv (cv x0) cbs)) (λ x0 . col))
Theorem df_covers : wceq ccvr (cmpt (λ x0 . cvv) (λ x0 . copab (λ x1 x2 . w3a (wa (wcel (cv x1) (cfv (cv x0) cbs)) (wcel (cv x2) (cfv (cv x0) cbs))) (wbr (cv x1) (cv x2) (cfv (cv x0) cplt)) (wn (wrex (λ x3 . wa (wbr (cv x1) (cv x3) (cfv (cv x0) cplt)) (wbr (cv x3) (cv x2) (cfv (cv x0) cplt))) (λ x3 . cfv (cv x0) cbs))))))
Theorem df_ats : wceq catm (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wbr (cfv (cv x0) cp0) (cv x1) (cfv (cv x0) ccvr)) (λ x1 . cfv (cv x0) cbs)))
Theorem df_atl : wceq cal (crab (λ x0 . wa (wcel (cfv (cv x0) cbs) (cdm (cfv (cv x0) cglb))) (wral (λ x1 . wne (cv x1) (cfv (cv x0) cp0) ⟶ wrex (λ x2 . wbr (cv x2) (cv x1) (cfv (cv x0) cple)) (λ x2 . cfv (cv x0) catm)) (λ x1 . cfv (cv x0) cbs))) (λ x0 . clat))
Theorem df_cvlat : wceq clc (crab (λ x0 . wral (λ x1 . wral (λ x2 . wral (λ x3 . wa (wn (wbr (cv x1) (cv x3) (cfv (cv x0) cple))) (wbr (cv x1) (co (cv x3) (cv x2) (cfv (cv x0) cjn)) (cfv (cv x0) cple)) ⟶ wbr (cv x2) (co (cv x3) (cv x1) (cfv (cv x0) cjn)) (cfv (cv x0) cple)) (λ x3 . cfv (cv x0) cbs)) (λ x2 . cfv (cv x0) catm)) (λ x1 . cfv (cv x0) catm)) (λ x0 . cal))
Theorem df_hlat : wceq chlt (crab (λ x0 . wa (wral (λ x1 . wral (λ x2 . wne (cv x1) (cv x2) ⟶ wrex (λ x3 . w3a (wne (cv x3) (cv x1)) (wne (cv x3) (cv x2)) (wbr (cv x3) (co (cv x1) (cv x2) (cfv (cv x0) cjn)) (cfv (cv x0) cple))) (λ x3 . cfv (cv x0) catm)) (λ x2 . cfv (cv x0) catm)) (λ x1 . cfv (cv x0) catm)) (wrex (λ x1 . wrex (λ x2 . wrex (λ x3 . wa (wa (wbr (cfv (cv x0) cp0) (cv x1) (cfv (cv x0) cplt)) (wbr (cv x1) (cv x2) (cfv (cv x0) cplt))) (wa (wbr (cv x2) (cv x3) (cfv (cv x0) cplt)) (wbr (cv x3) (cfv (cv x0) cp1) (cfv (cv x0) cplt)))) (λ x3 . cfv (cv x0) cbs)) (λ x2 . cfv (cv x0) cbs)) (λ x1 . cfv (cv x0) cbs))) (λ x0 . cin (cin coml ccla) clc))
Theorem df_llines : wceq clln (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wrex (λ x2 . wbr (cv x2) (cv x1) (cfv (cv x0) ccvr)) (λ x2 . cfv (cv x0) catm)) (λ x1 . cfv (cv x0) cbs)))
Theorem df_lplanes : wceq clpl (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wrex (λ x2 . wbr (cv x2) (cv x1) (cfv (cv x0) ccvr)) (λ x2 . cfv (cv x0) clln)) (λ x1 . cfv (cv x0) cbs)))
Theorem df_lvols : wceq clvol (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wrex (λ x2 . wbr (cv x2) (cv x1) (cfv (cv x0) ccvr)) (λ x2 . cfv (cv x0) clpl)) (λ x1 . cfv (cv x0) cbs)))
Theorem df_lines : wceq clines (cmpt (λ x0 . cvv) (λ x0 . cab (λ x1 . wrex (λ x2 . wrex (λ x3 . wa (wne (cv x2) (cv x3)) (wceq (cv x1) (crab (λ x4 . wbr (cv x4) (co (cv x2) (cv x3) (cfv (cv x0) cjn)) (cfv (cv x0) cple)) (λ x4 . cfv (cv x0) catm)))) (λ x3 . cfv (cv x0) catm)) (λ x2 . cfv (cv x0) catm))))
Theorem df_pointsN : wceq cpointsN (cmpt (λ x0 . cvv) (λ x0 . cab (λ x1 . wrex (λ x2 . wceq (cv x1) (csn (cv x2))) (λ x2 . cfv (cv x0) catm))))
Theorem df_psubsp : wceq cpsubsp (cmpt (λ x0 . cvv) (λ x0 . cab (λ x1 . wa (wss (cv x1) (cfv (cv x0) catm)) (wral (λ x2 . wral (λ x3 . wral (λ x4 . wbr (cv x4) (co (cv x2) (cv x3) (cfv (cv x0) cjn)) (cfv (cv x0) cple) ⟶ wcel (cv x4) (cv x1)) (λ x4 . cfv (cv x0) catm)) (λ x3 . cv x1)) (λ x2 . cv x1)))))
Theorem df_pmap : wceq cpmap (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) cbs) (λ x1 . crab (λ x2 . wbr (cv x2) (cv x1) (cfv (cv x0) cple)) (λ x2 . cfv (cv x0) catm))))
Theorem df_padd : wceq cpadd (cmpt (λ x0 . cvv) (λ x0 . cmpt2 (λ x1 x2 . cpw (cfv (cv x0) catm)) (λ x1 x2 . cpw (cfv (cv x0) catm)) (λ x1 x2 . cun (cun (cv x1) (cv x2)) (crab (λ x3 . wrex (λ x4 . wrex (λ x5 . wbr (cv x3) (co (cv x4) (cv x5) (cfv (cv x0) cjn)) (cfv (cv x0) cple)) (λ x5 . cv x2)) (λ x4 . cv x1)) (λ x3 . cfv (cv x0) catm)))))
Theorem df_pclN : wceq cpclN (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cpw (cfv (cv x0) catm)) (λ x1 . cint (crab (λ x2 . wss (cv x1) (cv x2)) (λ x2 . cfv (cv x0) cpsubsp)))))