proposition: Lemma doubleI_correct A B T : ordinalp A -> ordinalp B -> doubleI_def A B T (doubleI_transdef A B T).
proof: Proof. move => oA oB. split; [ apply:Lfs_surjective | by rewrite Lfs_source | ]. move=> p pt; rewrite (Lfs_V _ pt). move/setX_P: (pt) => [pp pxA pyB]; set a := P p; set b := Q p. move/(oltP oA):(pxA); rewrite -/a => lxA. move/(oltP oB):(pyB); rewrite -/b => lyB. set T6 := fun fa:Set => _. move:(otrans_defined_pr T6 oA) => [sjf sf fv]; rewrite (fv _ lxA). rewrite {1} /T6; set T5 := fun fb: Set => _. move:(otrans_defined_pr T5 oB) =>[ha hb hc]. have Sr u v: source (restriction1 u v) = v by rewrite /restriction1; aw. rewrite (hc b lyB) /T5 -/(T6 _) Sr Sr pp; congr (T p). set g := (doubleI_transdef A B T). have adm:sub (doubleI_E a b) (A \times B) by apply:doubleI_E_sub. have hd: sub (doubleI_E a b) (source g) by rewrite Lfs_source. have ssg: surjection g by apply: Lfs_surjective. rewrite (Lfs_restriction1 (proj1 ssg) hd); apply:Lfs_exten => q qE. rewrite (Lfs_V _ (adm _ qE)) -/T6. move: (proj1 sjf) => ff. move: (proj31_1 lxA) (proj31_1 lyB) => oa ob. move: (proj33 (proj1 lxA)); rewrite - {1} sf => sas. move: (proj33 (proj1 lyB)); rewrite - {1} hb => sbs. move: (doubleI_E_pair qE) => pq; rewrite - pq in qE. case /(doubleI_E_P1 oa ob):qE. - move => [h1 h2]; move/(oltP ob):(h2) => h3. have nf: ~ P q <o a by case. by rewrite (Y_false nf) (restriction1_V (proj1 ha) sbs h3) h1 (fv a lxA). - by move => [h1 h2]; move/(oltP oa):(h1) => h3; Ytac0; rewrite restriction1_V. - by move =>[h1 h2]; move/(oltP oa):(h1) => h3; Ytac0; rewrite restriction1_V. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)