# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1679122757 -32400
# Node ID 2fccbe475cf7d3a6acc37c1d7afca77dcda57c23
# Parent  8a8052df52540241b628771bc478ed4428ddd53a
lemma232 (Generic filter is not an element of M)

diff -r 8a8052df5254 -r 2fccbe475cf7 src/generic-filter.agda
--- a/src/generic-filter.agda	Sat Mar 18 11:30:42 2023 +0900
+++ b/src/generic-filter.agda	Sat Mar 18 15:59:17 2023 +0900
@@ -298,12 +298,20 @@
     M = ctl-M C
     D : HOD  
     D = L ＼ rgf
+    D<M : & D o< & (ctl-M C)
+    D<M = ordtrans≤-<  (⊆→o≤ proj1 ) (odef< ML)
     M∋DM : M ∋ (D ∩ M )
-    M∋DM = is-model C D ?
-    -- M∋G : M ∋ rgf
-    -- M∋G = MF
+    M∋DM = is-model C D D<M
+    -- G⊆M : rgf ⊆ M  
+    -- G⊆M {x} rx = TC C ML (subst (λ k → odef k x) (sym *iso) (⊆-Ideal.i⊆L GF rx))
+    -- D⊆M : D ⊆ M
+    -- D⊆M {x} dx = TC C ML (subst (λ k → odef k x) (sym *iso) (proj1 dx))
+    D=D∩M : D ≡ D ∩ M 
+    D=D∩M = ==→o≡ record { eq→ = ddm00 ; eq← = proj1 } where
+        ddm00 : {x : Ordinal} → odef D x → odef (D ∩ M) x
+        ddm00 {x} ⟪ Lx , ¬Gx ⟫ = ⟪ ⟪ Lx , ¬Gx  ⟫  , TC C ML (subst (λ k → odef k x) (sym *iso) Lx ) ⟫
     M∋D : M ∋ D 
-    M∋D = ?
+    M∋D = subst (λ k → M ∋ k ) (sym D=D∩M) M∋DM
     D⊆PP : D ⊆ Power P
     D⊆PP {x} ⟪ Lx , ngx ⟫  = LPP Lx 
     DD : Dense L 
@@ -353,8 +361,8 @@
      p∈G : odef (* oG) op
      is-val : odef (* ox) ( & < * oy , * op >  )
 
-val : (x : HOD) {P L : HOD } {LP : L ⊆ Power P}
-    →  (G : GenericFilter {L} {P} LP {!!} )
+val : (x : HOD) {P L M : HOD } {LP : L ⊆ Power P}
+    →  (G : GenericFilter {L} {P} LP M )
     →  HOD
 val x G = TransFinite {λ x → HOD } ind (& x) where
   ind : (x : Ordinal) → ((y : Ordinal) → y o< x → HOD) → HOD