Library set11
Theory of Sets : Ordinals
Copyright INRIA (2009) Apics Team (Jose Grimm).
Require Export set10.
Set Implicit Arguments.
Module Ordinals.
Definition sum_of_substrates g := disjoint_union (fam_of_substrates g).
Lemma du_index_pr:forall f x, inc x (disjoint_union f) ->
(inc (Q x) (domain f) & inc (P x) (V (Q x) f) & is_pair x).
Proof. ir. ufi disjoint_union H. ufi disjoint_union_fam H.
nin (unionb_exists H). bwi H0. nin H0. awi H1. nin H1. nin H2.
rw H3. eee. eee.
Qed.
Lemma du_index_pr1: forall g x, inc x (sum_of_substrates g) ->
(inc (Q x) (domain g) & inc (P x) (substrate (V (Q x) g)) & is_pair x).
Proof. uf sum_of_substrates. ir. ufi fam_of_substrates H.
set (du_index_pr H). nin a. bwi H0. bwi H1. eee. am.
Qed.
Lemma inc_disjoint_union: forall f x y,
inc y (domain f) -> inc x (V y f) ->
inc (J x y) (disjoint_union f).
Proof. ir. uf disjoint_union. rw unionb_rw. uf disjoint_union_fam.
exists y. ee. bw. bw. fprops.
Qed.
Lemma inc_disjoint_union1: forall g x y,
inc y (domain g) -> inc x (substrate (V y g)) ->
inc (J x y) (sum_of_substrates g).
Proof. ir. uf sum_of_substrates. uf fam_of_substrates.
app inc_disjoint_union. bw. bw.
Qed.
Lemma order_isomorphism_pr1: forall r r' f a b,
order_isomorphism f r r' -> inc a (source f) -> inc b (source f) ->
(glt r a b = glt r' (W a f) (W b f)).
Proof. ir. red in H. ee. nin H3. uf glt. wrr H6. ap iff_eq; ir; eee; dneg.
nin H3. app H11. ue.
Qed.
Lemma order_isomorphism_pr: forall r r' f a b,
order_isomorphism f r r' -> inc a (substrate r) -> inc b (substrate r) ->
(glt r a b = glt r' (W a f) (W b f)).
Proof. ir. cp H. nin H2. ee. rwi H5 H0. rwi H5 H1.
rww (order_isomorphism_pr1 H H0 H1).
Qed.
Lemma order_isomorphism_pr2: forall r r' f a b,
order_isomorphism f r r' -> glt r a b ->
glt r' (W a f) (W b f).
Proof. ir. assert (inc a (substrate r)). order_tac.
assert (inc b (substrate r)). order_tac.
wrr (order_isomorphism_pr H H1 H2).
Qed.
Definition ordinal_sum_axioms r g:=
order r & substrate r = domain g & fgraph g &
(forall i, inc i (domain g) -> order (V i g)).
Definition ordinal_sum_axioms1 r g:=
ordinal_sum_axioms r g &
(forall i, inc i (domain g) -> nonempty (substrate (V i g))).
Definition ordinal_sum_r (r g:Set): EEP :=
fun x x' =>
(glt r (Q x) (Q x') \/ (Q x = Q x' & gle (V (Q x) g) (P x) (P x'))).
Definition ordinal_sum r g :=
graph_on (ordinal_sum_r r g) (sum_of_substrates g).
Lemma ordinal_sum_order: forall r g,
ordinal_sum_axioms r g -> order (ordinal_sum r g).
Proof. ir. uf ordinal_sum. set (s := ordinal_sum_r r g).
set (x:= (sum_of_substrates g)).
assert (graph_on s x = graph_on (fun a b => inc a x & inc b x & s a b) x).
uf graph_on. set_extens; Ztac. awi H1. eee. eee. rw H0. red in H. ee.
app order_from_rel. uf s. uf ordinal_sum_r. red. ee; red;ir. eee.
nin H9; nin H7. left. order_tac. nin H7. wrr H7. au. nin H9. rww H9. au.
right. ee. ue. wri H9 H10. ufi x H4. nin (du_index_pr1 H4).
set (H3 _ H12). order_tac. ee. ufi x H4. nin (du_index_pr1 H4).
ufi x H8. nin (du_index_pr1 H8). ee. nin H9; nin H7. ee. order_tac. nin H9.
ee. elim H16. au. nin H9; nin H7. elim H17; au. ee. rwi H7 H16.
cp (H3 _ H10). app pair_extensionality. order_tac. nin H4.
ufi x H4. nin (du_index_pr1 H4). cp (H3 _ H6). eee; right; eee.
order_tac. ufi x H5. nin (du_index_pr1 H5). nin H12.
set (H3 _ H11). order_tac.
Qed.
Lemma ordinal_sum_related: forall r g x x',
ordinal_sum_axioms r g ->
related (ordinal_sum r g) x x' =
(inc x (sum_of_substrates g) & inc x' (sum_of_substrates g) &
ordinal_sum_r r g x x').
Proof. ir. uf ordinal_sum. rww graph_on_rw1.
Qed.
Hint Resolve ordinal_sum_order: fprops.
Hint Rewrite ordinal_sum_related : aw.
Lemma ordinal_sum_related1: forall r g x x',
ordinal_sum_axioms r g -> related (ordinal_sum r g) x x' ->
(glt r (Q x) (Q x') \/ (Q x = Q x' & gle (V (Q x) g) (P x) (P x'))).
Proof. ir. rwi ordinal_sum_related H0. ee. am. am.
Qed.
Lemma ordinal_sum_related_id: forall r g x x',
ordinal_sum_axioms r g ->
related (ordinal_sum r g) x x' -> gle r (Q x) (Q x').
Proof. ir. rwii ordinal_sum_related H0. ee. red in H2.
cp (du_index_pr1 H0). red in H. ee. nin H2; nin H2. am. wr H2. cp (H8 _ H3).
order_tac. ue.
Qed.
Lemma ordinal_sum_substrate: forall r g,
ordinal_sum_axioms r g ->
substrate(ordinal_sum r g) = (sum_of_substrates g).
Proof. ir. uf ordinal_sum. rww substrate_graph_on. ir. red. right.
cp (du_index_pr1 H0). red in H. ee. tv. set (H6 _ H1). order_tac.
Qed.
Hint Rewrite ordinal_sum_substrate : aw.
Lemma prod_of_substrates_pr: forall i z g,
inc i (domain g) -> inc z (prod_of_substrates g) ->
inc (V i z) (substrate (V i g)).
Proof. ir. ufi prod_of_substrates H0. ufi fam_of_substrates H0. awi H0. ee.
bwi H1. rwi H1 H2. set (H2 _ H). bwi i0. am. am. gprops.
Qed.
Lemma lexorder_gle1: forall r g x x',
lexicographic_order_axioms r g ->
gle (lexicographic_order r g) x x' =
(inc x (prod_of_substrates g) & inc x' (prod_of_substrates g) &
(x= x' \/ exists j, inc j (substrate r) &
glt (V j g) (V j x) (V j x') &
forall i, glt r i j -> V i x = V i x')).
Proof. ir. rw lexorder_gle.
assert (He: domain (fam_of_substrates g) = domain g).
uf fam_of_substrates. bw.
assert (Hf: fgraph(fam_of_substrates g)). uf fam_of_substrates. gprops.
app iff_eq; ir; eee.
set (s := (Zo (domain g) (fun i : Set => V i x <> V i x'))) in *.
assert (sub s (substrate r)). red in H. ee. rw H3. uf s. app Z_sub.
nin (emptyset_dichot s). left. nin H. ee. ap (productb_exten Hf H0 H1).
ir. ex_middle. assert (inc i s). uf s. Ztac. ue.
rwi H4 H10. elim (emptyset_pr H10). red in H. ee. nin H.
nin (H8 _ H3 H4). right. red in H9. awii H9. ee. exists x0. split. app H3.
split. app H2. red. aw. ee. am. ir. app H10. ir.
ex_middle. assert (inc i s). uf s. Ztac.
wr H5. order_tac. cp (H10 _ H13). cp (related_induced_order1 H14). order_tac.
ir. red in H. ee. assert (Ha : order r). nin H; am.
set (s := (Zo (domain g) (fun i : Set => V i x <> V i x'))) in *.
ee. assert (sub s (substrate r)). rw H4. uf s. app Z_sub.
nin H3. awii H3. nin H2. ufi s H3. Ztac. elim H10. ue. nin H2. ee. awii H8.
assert (inc x0 s). uf s. nin H9. Ztac. ue. cp (H8 _ H11).
cp (related_induced_order1 H12). nin (equal_or_not j x0). ue.
assert (glt r j x0). split; am. cp (H10 _ H15). ufi s H3. Ztac.
contradiction. am.
Qed.
Definition ordinal_product2 r r' :=
lexicographic_order canonical_doubleton_order (variantLc r' r).
Definition ordinal_sum2 r r' :=
ordinal_sum canonical_doubleton_order (variantLc r r').
Lemma ordinal_sum2_axioms: forall r r', order r -> order r' ->
ordinal_sum_axioms canonical_doubleton_order (variantLc r r').
Proof. ir. red. ee. cp worder_canonical_doubleton_order. nin H1; am.
rw substrate_canonical_doubleton_order. bw. fprops. bw.
ir. try_lvariant H1.
Qed.
Lemma ordinal_prod2_axioms: forall r r',
order r -> order r' ->
lexicographic_order_axioms canonical_doubleton_order (variantLc r' r).
Proof. ir. red. cp worder_canonical_doubleton_order. eee.
rw substrate_canonical_doubleton_order. bw. bw. ir. try_lvariant H2.
Qed.
Lemma ordinal_sum2_order: forall r r', order r -> order r' ->
order (ordinal_sum2 r r').
Proof. ir. uf ordinal_sum2. app ordinal_sum_order. app ordinal_sum2_axioms.
Qed.
Lemma ordinal_product2_order: forall r r',
order r -> order r' -> order (ordinal_product2 r r').
Proof. ir. uf ordinal_product2. app lexorder_order.
app ordinal_prod2_axioms.
Qed.
Lemma canonical2_substrate: forall r r',
fam_of_substrates (variantLc r r') = variantLc (substrate r) (substrate r').
Proof. ir. uf fam_of_substrates. uf variantLc.
app fgraph_exten. gprops. fprops. bw. bw. ir.
try_lvariant H. fprops. fprops.
Qed.
Definition canonical_du2 a b :=
disjoint_union (variantLc a b).
Lemma canonical_du2_rw: forall a b,
canonical_du2 a b = union2 (product a (singleton TPa))
(product b (singleton TPb)).
Proof. ir. uf canonical_du2. rww disjoint_union2_rw1.
Qed.
Lemma canonical_du2_pr: forall a b x,
inc x (canonical_du2 a b) = (is_pair x &
((inc (P x) a & Q x = TPa) \/ (inc (P x) b & Q x = TPb))).
Proof. ir. rw canonical_du2_rw. ap iff_eq. ir.
nin (union2_or H); awi H0; eee.
ir. ee. nin H0. app union2_first. aw. au.
app union2_second. aw. au.
Qed.
Lemma ordinal_sum2_substrate: forall r r', order r -> order r' ->
substrate (ordinal_sum2 r r') = canonical_du2 (substrate r) (substrate r').
Proof. ir. uf canonical_du2. uf ordinal_sum2. rw ordinal_sum_substrate.
uf sum_of_substrates. rww canonical2_substrate.
ap (ordinal_sum2_axioms H H0).
Qed.
Lemma ordinal_product2_substrate: forall r r',
order r -> order r' ->
substrate (ordinal_product2 r r') = product2 (substrate r') (substrate r).
Proof. ir. uf ordinal_product2. aw. rw lexorder_substrate.
uf prod_of_substrates. rw canonical2_substrate. uf product2. uf productf.
uf variantLc. uf variantL. rww two_points_pr2. app ordinal_prod2_axioms.
Qed.
Lemma ordinal_sum2_gle: forall r r' x x', order r -> order r' ->
related (ordinal_sum2 r r') x x' =
(inc x (canonical_du2 (substrate r) (substrate r')) &
inc x' (canonical_du2 (substrate r) (substrate r')) &
((Q x = TPa & Q x' = TPa & gle r (P x) (P x'))
\/ (Q x <> TPa & Q x' <> TPa & gle r' (P x) (P x'))
\/ (Q x = TPa & Q x' <> TPa))).
Proof. ir. assert (Ha: TPb <> TPa). fprops.
uf ordinal_sum2. app iff_eq. ir. awi H1.
ufi sum_of_substrates H1. rwi canonical2_substrate H1. eee.
rwi disjoint_union2_rw1 H1.
rwi disjoint_union2_rw1 H2. nin H3. right. right.
red in H3. rwi canonical_doubleton_order_pr H3. nin H3. nin H3. elim H4.
nin H3. rww H5. nin H3. elim H4. nin H3. rww H5. nin H3. wr H3. au.
nin H3. wr H3. nin (union2_or H1). awi H5. ee.
rwi H7 H4. bwi H4. au.
awi H5. ee. rwi H7 H4. rwi variant_V_cb H4.
right. left. rw H7. au. app ordinal_sum2_axioms.
ir. ee. aw. uf sum_of_substrates. rw canonical2_substrate.
eee. rwi canonical_du2_pr H1. rwi canonical_du2_pr H2. ee.
nin H3. right. ee. rww H6. rw H3. bw. nin H3. right.
assert (Q x = TPb). nin H5. ee. elim H3. am. eee.
assert (Q x' = TPb). nin H4. ee. elim H7. am. eee.
ee. rww H7. rw H6. bw.
assert (Q x' = TPb). nin H4. ee. elim H6. am. eee.
left. red. ee. rw canonical_doubleton_order_pr. au.
rw H3; rww H6. intuition. app ordinal_sum2_axioms.
Qed.
Hint Resolve ordinal_sum2_order: fprops.
Hint Rewrite ordinal_sum2_gle : aw.
Lemma ordinal_sum2_gle_spec: forall r r' x x', order r -> order r' ->
inc x (substrate r) -> inc x' (substrate r') ->
glt (ordinal_sum2 r r') (J x TPa) (J x' TPb).
Proof. ir. red. ee. aw. ee. rw canonical_du2_pr. ee. fprops. aw. au.
rw canonical_du2_pr. ee. fprops. aw. au.
right. right. eee.
red. ir. cp (pr2_def H3). app two_points_distinct.
Qed.
Lemma ordinal_product2_gle: forall r r' a b,
order r -> order r' ->
related (ordinal_product2 r r') a b =
(inc a (product2 (substrate r') (substrate r))
& inc b (product2 (substrate r') (substrate r))
& ( (V TPa a = V TPa b & gle r (V TPb a) (V TPb b))
\/ (glt r' (V TPa a)(V TPa b)))).
Proof. ir. uf ordinal_product2. cp (ordinal_prod2_axioms H H0).
rww lexorder_gle1. rw substrate_canonical_doubleton_order.
replace (prod_of_substrates (variantLc r' r)) with
(product2 (substrate r') (substrate r)).
app iff_eq. ir. eee. nin H4. left. wr H4. split. tv. order_tac.
rwi product2_rw H2. eee. nin H4. ee. rwi two_points_pr H4. nin H4.
rwi H4 H5. bwi H5. au. rwi H4 H5. bwi H5.
assert (glt canonical_doubleton_order TPa x). split. rw H4.
rw canonical_doubleton_order_pr. au. rw H4. fprops.
cp (H6 _ H7). nin H5. au.
ir. eee. nin H4. nin H4. nin (equal_or_not (V TPb a) (V TPb b)).
rwi product2_rw H2. rwi product2_rw H3. left. ee.
app fgraph_exten. ue. ir. rwi H10 H13. try_lvariant H13.
right. exists TPb. eee. bw. split; am. ir. nin H7.
rwi canonical_doubleton_order_pr H7. nin H7. ee. rww H7. nin H7. nin H7.
contradiction. nin H7. rww H7. right. exists TPa. eee. bw.
ir. nin H5. rwi canonical_doubleton_order_pr H5. nin H5. ee. contradiction.
nin H5. nin H5. elim two_points_distinct. am. nin H5. contradiction.
uf prod_of_substrates. rw canonical2_substrate.
uf variantLc. uf variantL. rww two_points_pr2.
Qed.
Lemma ordinal_sum_worder : forall r g,
ordinal_sum_axioms r g -> worder r ->
(forall i, inc i (domain g) -> worder (V i g))
-> worder (ordinal_sum r g).
Proof. ir. split. app ordinal_sum_order. ir. awii H2. cp H. red in H4. ee.
set (A := fun_image x Q). assert (sub A (substrate r)). red. ir. ufi A H8.
awi H8. nin H8. nin H8. cp (H2 _ H8).
nin (du_index_pr1 H10). ue. ue.
assert (nonempty A). nin H3. exists (Q y). uf A. aw. ex_tac.
nin H0. nin (H10 _ H8 H9). nin H11. awii H11. awii H12.
set (B:= Zo x (fun z => Q z = x0)). set (C := fun_image B P).
cp (H8 _ H11). rwi H5 H13.
assert (sub C (substrate (V x0 g))). red. ir. ufi C H14. awi H14.
nin H14. nin H14. wr H15. ufi B H14. Ztac. wr H17.
cp (H2 _ H16). cp (du_index_pr1 H18). eee.
assert (nonempty C). ufi A H11. awi H11. nin H11. exists (P x1).
uf C. aw. exists x1. ee. uf B. Ztac. tv. nin (H1 _ H13).
nin (H17 _ H14 H15). nin H18. cp (H7 _ H13). awii H18. awii H19.
assert (inc (J x1 x0) x). ufi C H18. awi H18. nin H18. nin H18. ufi B H18.
Ztac. cp (H2 _ H22). nin (du_index_pr1 H24). wr H21; wr H23. aw. eee.
assert (order (ordinal_sum r g)). app ordinal_sum_order.
assert(sub x (substrate (ordinal_sum r g))). aw.
exists (J x1 x0). split. aw. aw. ir. aw. ee.
app H2. rwi ordinal_sum_substrate H23. app H23. am.
cp (H2 _ H24). nin (du_index_pr1 H25). nin H27.
assert (inc (Q x2) A). uf A. aw. ex_tac. cp (H12 _ H29). awii H30.
nin (equal_or_not x0 (Q x2)). red. right. aw. ee. am.
assert (inc (P x2) C). uf C. aw. exists x2. ee. uf B. Ztac. tv.
cp (H19 _ H32). awii H33. left. aw. split; am.
Qed.
Lemma lexorder_worder: forall r g,
lexicographic_order_axioms r g ->
(forall i, inc i (domain g) -> worder (V i g)) ->
is_finite_set (substrate r) ->
worder (lexicographic_order r g).
Proof. set (p := fun n => forall r g,
lexicographic_order_axioms r g ->
(forall i, inc i (domain g) -> worder (V i g)) ->
cardinal (substrate r) = n ->
worder (lexicographic_order r g)).
assert (forall n, inc n Bnat -> p n). app cardinal_c_induction_v.
uf p. ir. cp (cardinal_nonemptyset H1). split. fprops. aw. ir. cp H.
red in H. ee. rwi H2 H6. nin H4. exists y. red. aw. split. am. ir.
cp (H3 _ H9). rwi lexorder_substrate H3. ufi prod_of_substrates H3.
ufi fam_of_substrates H3. wri H6 H3. rwi product2_trivial H3.
cp (H3 _ H4). cp (H3 _ H9). awi H11. awi H12. wri H12 H11. rw H11.
rww related_induced_order.
assert (order (lexicographic_order r g)). fprops. order_tac. am. fprops.
ir. ufi p H0. uf p. ir. nin (emptyset_dichot (substrate r)). rwi H4 H3.
rwi cardinal_emptyset H3. symmetry in H3. elim (succ_nonzero H3).
split. fprops. aw. ir. cp H1. red in H7. ee.
rwi lexorder_substrate H5.
assert (exists i, inc i (substrate r) & forall j, inc j (substrate r) ->
gle r i j). nin H7. nin (H11 _ (@sub_refl (substrate r)) H4).
red in H12. awi H12. ee. exists x0. ee. am. ir. cp (H13 _ H14). awii H15. am.
fprops. nin H11. nin H11. rename x0 into i.
set (Y := fun_image x (fun z => V i z)).
assert (sub Y (substrate (V i g))). red. ir. ufi Y H13. awi H13. nin H13.
nin H13. wr H14. cp (H5 _ H13). app prod_of_substrates_pr. ue.
assert (nonempty Y). nin H6. exists (V i y). uf Y. aw. ex_tac.
rwi H8 H11. nin (H2 _ H11). nin (H16 _ H13 H14).
red in H17. awii H17. nin H17. set (X1 := Zo x (fun z => V i z = x0)).
assert (forall a b, inc a x -> inc b x -> inc a X1 -> ~ inc b X1 ->
glt (lexicographic_order r g) a b).
ir. nin H7. split. rw lexorder_gle1. ee. app H5. app H5.
right. exists i. eee. ufi X1 H21. Ztac. rw H25. clear H21. split.
assert (inc (V i b) Y). uf Y. aw. exists b. au. cp (H18 _ H21).
awii H26. dneg. uf X1. Ztac. ir. assert (inc i0 (substrate r)).
nin H24. order_tac. cp (H12 _ H25). order_tac. am. dneg. wrr H24.
set (I1:= complement (substrate r) (singleton i)).
set (r1 := induced_order r I1).
set (g1 := restr g I1).
assert (sub I1 (substrate r)). uf I1. app sub_complement.
assert (domain g1 = I1). uf g1. rww restr_domain1. ue.
assert (sub (domain g1) (domain g)). rw H21. ue.
assert (lexicographic_order_axioms r1 g1). red. uf r1; uf g1.
ee. app worder_restriction. aw. sy; am. nin H7; am. fprops.
ir. ufi g1 H21. rwi H21 H23. rww restr_ev. app H10. ue. ue.
assert (forall i, inc i (domain g1) -> worder (V i g1)). ir. uf g1.
rww restr_ev. app H2. app H22. ue. ue.
assert (cardinal (substrate r1) = n). uf r1. aw.
cp (cardinal_succ_pr1 (substrate r) i). fold I1 in H25.
assert (tack_on I1 i = substrate r). set_extens. rwi tack_on_inc H26.
nin H26. app H20. rww H26. ue. uf I1. nin (equal_or_not x1 i).
rw H27. fprops. app inc_tack_on_y. srw. ee. am. red. ir. awi H28.
contradiction. rwi H26 H25. rwi H3 H25. sy. app succ_injective. fprops.
fprops. nin H7. am.
cp (H0 _ _ H23 H24 H25). cp H26. red in H26; ee.
set (X2 := fun_image X1 (fun z => restr z I1)).
assert (sub X2 (substrate (lexicographic_order r1 g1))). aw.
red. ir. rww lexorder_substrate. uf prod_of_substrates. uf fam_of_substrates.
ufi X2 H29. awi H29. nin H29. nin H29.
assert (inc x2 x). ufi X1 H29. Ztac. am. cp (H5 _ H31).
ufi prod_of_substrates H32. ufi fam_of_substrates H32. awi H32. ee. bwi H33.
assert (domain x1 = domain g1). wr H30. rww restr_domain1. sy; am. ue. ue.
aw. bw. rw H35. ee. wr H30. fprops. tv. ir. bw. uf g1. wr H30.
rww restr_ev. rww restr_ev. rwi H33 H34. cp (H34 _ (H22 _ H36)). bwi H37.
am. app H22. ue. ue. ue. ue. ue. gprops. gprops.
assert (nonempty X2). ufi Y H17. awi H17. nin H17. exists (restr x1 I1).
uf X2. aw. nin H17. exists x1. split. uf X1. Ztac. tv.
nin H27. nin (H28 _ H29 H30).
red in H32. awii H32. nin H32. cp H32. ufi X2 H32. awi H32. nin H32. nin H32.
assert (inc x2 x). ufi X1 H32. Ztac. am.
exists x2. red. aw. ee. am. ir. nin (equal_or_not (V i x3) x0).
assert (inc x3 X1). uf X1. Ztac. assert (inc (restr x3 I1) X2).
uf X2. aw. ex_tac. cp (H33 _ H40).
rwii related_induced_order H41. rww related_induced_order.
rww lexorder_gle. ee. app H5. app H5. ir. red in H42. awii H42. nin H42.
Ztac. clear H42. assert (j <> i). dneg. rw H42. rw H38. ufi X1 H32. Ztac. am.
assert (inc j I1). uf I1. rw H8. srw. ee. am. aw.
cp (H5 _ H37). cp (H5 _ H36). ufi prod_of_substrates H47.
ufi fam_of_substrates H47. ufi prod_of_substrates H48.
ufi fam_of_substrates H48. awi H47. awi H48. ee.
assert (least_element (induced_order r1
(Zo (domain g1) (fun i : Set => V i x1 <> V i (restr x3 I1)))) j).
assert (inc j (Zo (domain g1) (fun i0 => V i0 x1 <> V i0 (restr x3 I1)))).
Ztac. ue. wr H35. rww restr_ev. rww restr_ev. ue. bw. ue. ue. bw. ue.
red. aw. split. am. ir. Ztac. aw.
assert (inc x4 (Zo (domain g) (fun i : Set => V i x2 <> V i x3))).
wri H35 H56. wr H8. app Z_inc. app H20. ue. rwi restr_ev H56.
rwi restr_ev H56. am. am. ue. bw. ue. ue. am. ue. bw. ue. ue.
cp (H43 _ H57). cp (related_induced_order1 H58). uf r1. aw. ue.
nin H23. nin H23. am. nin H23. nin H54. rw H54. app Z_sub.
rwii lexorder_gle H41. ee. cp (H55 _ H53).
wri H35 H56. ufi g1 H56. rwii restr_ev H56. rwii restr_ev H56.
rwii restr_ev H56. ue. bw. ue. ue. bw. ue. ue. gprops. gprops.
nin H7;am. wrr H8. app Z_sub.
assert (~ inc x3 X1). uf X1. red; ir. Ztac. contradiction.
nin (H19 _ _ H36 H37 H32 H39). rww related_induced_order. fprops.
rww lexorder_substrate. am.
ir. red in H2.
set (n := cardinal (substrate r)). assert (inc n Bnat). aw. uf n.
rww inc_Bnat. app (H _ H3).
Qed.
Lemma ordinal_product2_worder: forall r r',
worder r -> worder r' -> worder (ordinal_product2 r r').
Proof. ir. uf ordinal_product2. app lexorder_worder.
app ordinal_prod2_axioms. nin H; am. nin H0; am. bw. ir. try_lvariant H1.
rw substrate_canonical_doubleton_order.
wr two_points_pr2. app doubleton_finite.
Qed.
Lemma ordinal_sum_totalorder: forall r g,
ordinal_sum_axioms1 r g ->
total_order (ordinal_sum r g) = (total_order r &
forall i, inc i (domain g) -> total_order (V i g)).
Proof. ir. nin H. ee. uf total_order. uf gge. cp H. red in H. ee. aw. rw H2.
ap iff_eq. ir. ee. am. ir. nin (H0 _ H7). nin (H0 _ H8).
cp (inc_disjoint_union1 H8 H10). cp (inc_disjoint_union1 H7 H9).
nin (H6 _ _ H11 H12); awii H13; ee; red in H15; awi H15;
[right | left ]; nin H15; nin H15; tv; rw H15; order_tac; ue.
ir. ee. app H4. ir. cp (inc_disjoint_union1 H7 H8).
cp (inc_disjoint_union1 H7 H9).
nin (H6 _ _ H10 H11); cp (ordinal_sum_related1 H1 H12); ee; awi H13; nin H13;
nin H13; au; elim H14; tv.
ir. ee. fprops. ir. aw. uf ordinal_sum_r.
cp (du_index_pr1 H8). cp (du_index_pr1 H9).
ee. nin (equal_or_not (Q x) (Q y)). cp (H6 _ H10). ee. wri H16 H12.
nin (H18 _ _ H14 H12); [ left | right ]; eee.
uf glt; nin (H7 _ _ H10 H11) ; [ left | right ]; eee.
Qed.
Lemma ordinal_sum2_totalorder: forall r r',
total_order r -> total_order r' -> total_order (ordinal_sum2 r r').
Proof. ir. nin H; nin H0. split. fprops. rww ordinal_sum2_substrate.
ir. uf gge. aw. cp H3; cp H4.
rwi canonical_du2_pr H5. rwi canonical_du2_pr H6. ee. nin H8; nin H7.
ee. nin (H1 _ _ H8 H7). left. eee. red in H11. right. eee.
nin H8; nin H7. left. eee. nin H8; nin H7. right. eee.
nin H8; nin H7. ee. rw H9; rw H10. nin (H2 _ _ H8 H7). left. eee.
red in H11. right. eee.
Qed.
Lemma ordinal_sum2_worder: forall r r',
worder r -> worder r' -> worder (ordinal_sum2 r r').
Proof. ir. uf ordinal_sum2. app ordinal_sum_worder. app ordinal_sum2_axioms.
nin H; am. nin H0; am. app worder_canonical_doubleton_order. bw.
ir. try_lvariant H1.
Qed.
Definition order_isomorphic r r':=
exists f, order_isomorphism f r r'.
Lemma order_isomorphic_reflexive: forall r,
order r -> order_isomorphic r r.
Proof. ir. exists (identity (substrate r)).
red. eee. app identity_bijective. aw. aw. aw.
ir. rww identity_W. rww identity_W.
Qed.
Lemma order_isomorphic_symmetric: forall r r',
order_isomorphic r r' -> order_isomorphic r' r.
Proof. ir. nin H. exists (inverse_fun x). red in H. ee.
cp (inverse_bij_is_bij1 H1).
red. eee. aw. aw. aw. ir. assert (target (inverse_fun x) = source x). aw.
set (a :=W x0 (inverse_fun x)). set (b:=W y (inverse_fun x)).
rw (W_inverse H1 H6 (refl_equal a)).
rw (W_inverse H1 H7 (refl_equal b)). sy. app H4.
wr H8. uf a. app inc_W_target. fct_tac. aw.
wr H8. uf b. app inc_W_target. fct_tac. aw.
Qed.
Lemma order_isomorphic_transitive: forall r r' r'',
order_isomorphic r r' -> order_isomorphic r' r'' ->
order_isomorphic r r''.
Proof. ir. nin H; nin H0. red in H; red in H0. ee.
exists (compose x0 x). red.
assert (composable x0 x). red; ee. fct_tac. fct_tac. ue. simpl. eee.
app compose_bijective. aw. aw. aw. ir. rw compose_W. rw compose_W.
rw (H10 _ _ H12 H13). rww H5. wr H3. rw H9. app inc_W_target. fct_tac.
wr H3. rw H9. app inc_W_target. fct_tac. am. am. am. am.
Qed.
Lemma ordinal_product_pr: forall r r',
order r -> order r' ->
order_isomorphic (ordinal_product2 r r')
(ordinal_sum r' (cst_graph (substrate r') r)).
Proof. ir.
assert (ordinal_sum_axioms r'(cst_graph (substrate r') r)).
red. uf cst_graph. ee. am. bw. gprops. bw. ir. bw.
set (fo:=ordinal_sum r' (cst_graph (substrate r') r)).
assert (order fo). uf fo. app ordinal_sum_order.
cp (ordinal_sum_substrate H1).
cp (ordinal_product2_order H H0).
cp (ordinal_product2_substrate H H0).
set (io := ordinal_product2 r r') in *.
set (f := fun x => J (V TPb x) (V TPa x)).
assert (transf_axioms f (substrate io) (substrate fo)). red. ir.
uf fo. rw H3. uf sum_of_substrates. uf fam_of_substrates. uf cst_graph.
rwi H5 H6. rwi product2_rw H6. uf f. ee. app inc_disjoint_union. bw. bw.
assert (bijective (BL f (substrate io) (substrate fo))).
app bl_bijective. ir. ufi f H9. rwi H5 H7. rwi H5 H8.
ufi product2 H7. ufi product2 H8. ap (productf_exten H7 H8).
ir. try_lvariant H10. inter2tac. inter2tac. ir. ufi fo H7. rwi H3 H7.
ufi fam_of_substrates H7. ufi cst_graph H7. bwi H7.
cp (du_index_pr1 H7). bwi H8. nin H8. nin H9.
exists (variantLc (Q y) (P y)). split. rw H5. rw product2_rw. ee.
fprops. bw. bw. bw. uf f. bw. aw. eee.
exists (BL f (substrate io) (substrate fo)). red. eee. aw. aw. aw. ir.
aw. uf io. rw ordinal_product2_gle. wr H5.
uf fo. rww ordinal_sum_related. assert (inc (V TPa x) (substrate r')).
rwi H5 H8. rwi product2_rw H8. ee. am. wr H3. uf cst_graph.
app iff_eq. ir. ee. app H6. app H6. red. uf f. aw. bw.
nin H13; au. ir. ee. am. am. red in H13. ufi f H13. awi H13. bwi H13.
nin H13; au. am. am. am.
Qed.
Definition order_type x := choose (fun z => order_isomorphic x z).
Definition is_order_type x := exists y, order y & x = order_type y.
Definition is_ordinal x := exists y, worder y & x = order_type y.
Lemma ordinal_pr1: forall r, order r -> order_isomorphic r (order_type r).
Proof. ir. uf order_type. app choose_pr. exists r.
app order_isomorphic_reflexive.
Qed.
Lemma ordinal_pr2: forall r, order r -> order (order_type r).
Proof. ir. nin (ordinal_pr1 H). red in H0. ee. am.
Qed.
Lemma ordinal_pr3: forall r, is_order_type r -> order r.
Proof. ir. nin H. nin H. rw H0. app ordinal_pr2.
Qed.
Lemma ordinal_pr4: forall r r', order r -> order r' ->
(order_type r = order_type r') = order_isomorphic r r'.
Proof. ir. app iff_eq. ir. cp (ordinal_pr1 H). cp (ordinal_pr1 H0).
wri H1 H3. cp (order_isomorphic_symmetric H3).
app (order_isomorphic_transitive H2 H4). ir.
uf order_type. app choose_equiv. split. ir.
cp (order_isomorphic_symmetric H1).
app (order_isomorphic_transitive H3 H2). ir.
app (order_isomorphic_transitive H1 H2).
Qed.
Hint Rewrite ordinal_pr4 : aw.
Lemma worder_invariance: forall r r',
order_isomorphic r r' -> worder r -> worder r'.
Proof. ir. nin H. red in H. ee. split. am. ir. nin H7.
set (A := image_by_fun (inverse_fun x) x0). cp (inverse_bij_is_bij1 H2).
assert (Ha: is_function (inverse_fun x)). fct_tac.
assert (sub x0 (source (inverse_fun x))). aw. wrr H4.
assert (Ht:source x = (target (inverse_fun x))). aw.
assert (sub A (source x)). uf A. red. ir. awi H10. nin H10. nin H10.
rw Ht. wr H11. app inc_W_target. app H9. am. am. wri H3 H10.
assert (nonempty A). exists (W y (inverse_fun x)). uf A.
aw. ex_tac. ue. nin H0. nin (H12 _ H10 H11). red in H13. awii H13. nin H13.
ufi A H13. awi H13. nin H13. nin H13. assert (inc x2 (target x)). wr H4.
app H6. symmetry in H15. cp (W_inverse H2 H16 H15).
exists x2. split. aw. aw. ir. aw. rw H17.
set (x4 := W x3 (inverse_fun x)). assert (inc x3 (target x)). wr H4.
app H6. cp (W_inverse H2 H19 (refl_equal x4)). rw H20. wrr H5.
assert (inc x4 A). uf A. aw. exists x3. split. am. tv. ue. cp (H14 _ H21).
cp (related_induced_order1 H22). am. rw Ht. rw H15. app inc_W_target. aw.
rw Ht. uf x4. app inc_W_target. aw. am. am.
Qed.
Lemma ordinal_pr5: forall r, is_ordinal r -> worder r.
Proof. ir. nin H. nin H. cp H. nin H. cp (ordinal_pr1 H).
rw H0. app (worder_invariance H3 H1).
Qed.
Lemma ordinal_pr6 : forall r, order r -> is_order_type (order_type r).
Proof. ir. exists r. split. am. tv. Qed.
Lemma ordinal_pr7 : forall r, worder r -> is_ordinal (order_type r).
Proof. ir. exists r. split. am. tv. Qed.
Lemma ordinal_pr8 : forall y, is_order_type y ->
order_type y = y.
Proof. ir. red in H. nin H. ee. rw H0. aw.
app order_isomorphic_symmetric. app ordinal_pr1. app ordinal_pr2.
Qed.
Lemma ordinal_pr9 : forall x y, order x -> is_order_type y ->
order_isomorphic x y -> order_type x = y.
Proof. ir. cp (ordinal_pr3 H0). wri (ordinal_pr4 H H2) H1. rw H1.
app ordinal_pr8.
Qed.
Lemma ordinal_pr10 : forall x, is_ordinal x -> is_order_type x.
Proof. ir. nin H. red. exists x0. eee. nin H; am.
Qed.
Definition order_type_le r r' :=
is_order_type r & is_order_type r' &
exists f, exists x,
sub x (substrate r') & order_isomorphism f r (induced_order r' x).
Lemma order_type_le_preorder: preorder_r order_type_le.
Proof. split. red. uf order_type_le. ir. ee. am. am. nin H4. nin H2.
nin H4. nin H2. set (Ha:=ordinal_pr3 H1).
set (f := fun z => W (W z x0) x1). set (t := fun_image (substrate x) f).
nin H4. nin H2. red in H5; red in H6. ee. awii H10. awii H15.
assert (sub t (substrate z)). red. ir. ufi t H17. awi H17. nin H17. nin H17.
wr H18. uf f. app H2. rw H10. app inc_W_target. fct_tac. wr H9. app H4.
rw H15. app inc_W_target. fct_tac. ue.
assert (order (induced_order z t)). fprops.
assert (substrate (induced_order z t) = t). aw.
assert (transf_axioms f (substrate x) t). red. ir. uf t. aw. ex_tac.
assert (bijective (BL f (substrate x) t)). app bl_bijective.
ir. ufi f H23. nin H13; nin H13. nin H8. nin H8. rwi H14 H21. rwi H14 H22.
assert (inc (W u x0) (source x1)). wr H9. app H4. rw H15. app inc_W_target.
assert (inc (W v x0) (source x1)). wr H9. app H4. rw H15. app inc_W_target.
cp (H27 _ _ H28 H29 H23). app H25. ir. ufi t H21. awi H21. am.
exists (BL f (substrate x) t). exists t. split. am.
red. eee. aw. aw. aw. ir. cp (H20 _ H22). cp (H20 _ H23). aw.
rwi H14 H22. rwi H14 H23. rw (H16 _ _ H22 H23).
assert (is_function x0). fct_tac. cp (inc_W_target H26 H22).
cp (inc_W_target H26 H23). wri H15 H27. cp (H4 _ H27).
wri H15 H28. cp (H4 _ H28). aw. uf f. rwi H9 H29. rwi H9 H30.
rww (H11 _ _ H29 H30). aw. rw H10. app inc_W_target. fct_tac.
rw H10. app inc_W_target. fct_tac.
red. ir. nin H. nin H0. split. red. eee.
cp (ordinal_pr3 H). nin (order_isomorphic_reflexive H2).
exists x0. exists (substrate x). split. fprops.
rww induced_order_substrate.
red. eee. cp (ordinal_pr3 H0). nin (order_isomorphic_reflexive H2).
exists x0. exists (substrate y). split. fprops.
rww induced_order_substrate.
Qed.
Definition ord_zero := order_type (emptyset).
Definition ord_one := order_type (singleton (J emptyset emptyset)).
Definition ord_two := order_type canonical_doubleton_order.
Definition ord_omega := order_type Bnat_order.
Lemma emptyset_order: order emptyset.
Proof. assert (inclusion_suborder emptyset=emptyset).
app is_emptyset. ir. red. ir. ufi inclusion_suborder H. ufi graph_on H.
Ztac. awi H0. ee. elim (emptyset_pr H2). wr H. fprops.
Qed.
Lemma emptyset_substrate : substrate emptyset = emptyset.
Proof. ir. app is_emptyset. ir. red. ir. cp emptyset_order.
assert (inc (J y y) emptyset). order_tac. elim (emptyset_pr H1).
Qed.
Lemma is_ordinal_0: is_ordinal ord_zero.
Proof. red. uf ord_zero. exists emptyset. split. split.
app emptyset_order. ir. nin H0. cp (H _ H0).
rwi emptyset_substrate H1. elim (emptyset_pr H1). tv.
Qed.
Lemma ordinal0_pr1: forall x, order x -> substrate x = emptyset ->
order_type x = ord_zero.
Proof. ir. uf ord_zero. set emptyset_order.
aw. exists (identity emptyset).
red. rw emptyset_substrate. eee. app identity_bijective. aw. aw. aw.
simpl. ir. elim (emptyset_pr H1).
Qed.
Lemma ordinal0_pr: ord_zero = emptyset.
Proof. cp emptyset_order. cp (ordinal_pr1 H). fold ord_zero in H0.
cp (order_isomorphic_symmetric H0). nin H1. red in H1. ee. app is_emptyset.
red. ir. assert (is_graph ord_zero). fprops.
assert (is_pair y). app H8. assert (y = J (P y) (Q y)). aw.
rwi H10 H7. assert (inc (P y) (substrate ord_zero)). substr_tac.
rwi H4 H11. assert (inc (W (P y) x) (target x)). app inc_W_target. fct_tac.
wri H5 H12. rwi emptyset_substrate H12. elim (emptyset_pr H12).
Qed.
Lemma singleton_worder: forall x,
let E := singleton (J x x) in
substrate E = singleton x & worder E.
Proof. ir.
assert (E = identity_g (singleton x)). uf identity_g. uf E. uf L.
set_extens. aw. ex_tac. awi H. sy; am. awi H. nin H. ee. awi H. aw. ue.
assert (order E). rw H. app diagonal_order.
assert (substrate E = singleton x). set_extens. assert (related E x0 x0).
order_tac. red in H2. ufi E H2. awi H2. rw (pr1_def H2). fprops.
awi H1. rw H1. assert (inc (J x x) E). uf E. fprops. substr_tac.
split. am. split. am. ir. nin H3. exists y. red. aw. split. am. ir. aw.
red. red. rwi H1 H2. cp (H2 _ H3). awi H5. rw H5. cp (H2 _ H4). awi H6.
rw H6. uf E. fprops.
Qed.
Lemma singleton_order_isomorphic: forall x y,
order_isomorphic (singleton (J x x)) (singleton (J y y)).
Proof. ir. set (f := fun _: Set => y).
assert (transf_axioms f (singleton x) (singleton y)). red. ir. uf f. fprops.
assert (bijective (BL f (singleton x) (singleton y))).
app bl_bijective. ir. awi H0. awi H1. ue. ir. awi H0.
exists x. ee. fprops. sy; am.
exists (BL f (singleton x) (singleton y)). red.
nin (singleton_worder x). nin (singleton_worder y). nin H2; nin H4.
eee. aw. aw. aw. ir. awi H7. awi H8. rw H7. rw H8. aw. uf gle. uf related.
uf f. aw. app iff_eq; tv.
Qed.
Lemma singleton_order_isomorphic1: forall x,
order x -> is_singleton (substrate x) ->
exists v, x = singleton (J v v).
Proof. ir. nin H0. exists x0. set_extens.
assert (x1 = J (P x1) (Q x1)). aw. assert (is_graph x). fprops. fprops.
rwi H2 H1. assert (inc (P x1) (substrate x)). substr_tac.
assert (inc (Q x1) (substrate x)). substr_tac. rwi H0 H3. awi H3. rw H2.
rw H3. rwi H0 H4. awi H4. rw H4. fprops. awi H1. rw H1. order_tac.
rw H0. fprops.
Qed.
Lemma singleton_order_isomorphic2: forall x y,
order x -> order y ->
is_singleton (substrate x) -> is_singleton (substrate y)
-> order_isomorphic x y.
Proof. ir. nin (singleton_order_isomorphic1 H H1).
nin (singleton_order_isomorphic1 H0 H2). rw H3; rw H4.
app singleton_order_isomorphic.
Qed.
Lemma is_ordinal_1: is_ordinal ord_one.
Proof. uf ord_one. app ordinal_pr7.
nin (singleton_worder emptyset). am.
Qed.
Lemma ordinal_1_indep: forall x, order x -> is_singleton (substrate x) ->
ord_one = order_type x.
Proof. ir. uf ord_one. nin (singleton_worder x). nin H2.
nin (singleton_worder emptyset). nin H5.
aw. nin (singleton_order_isomorphic1 H H0). rw H7.
app singleton_order_isomorphic.
Qed.
Lemma ordinal_1_value: is_singleton (substrate ord_one).
Proof. nin (singleton_worder emptyset). nin H0. cp (ordinal_pr1 H0).
fold ord_one in H2. nin H2. red in H2. ee.
set (a := W emptyset x). rwi H H5. assert (inc a (target x)).
uf a. app inc_W_target. fct_tac. wr H5. fprops.
assert (target x = singleton a). set_extens. nin H4.
cp (surjective_pr2 H10 H9). nin H11. nin H11. wri H5 H11. awi H11.
wr H12. rw H11. uf a. fprops. awi H9. ue. rw H6. rw H9. exists a. tv.
Qed.
Lemma ordinal_1_value_bis: exists x, ord_one = singleton (J x x).
Proof. nin (ordinal_pr5 is_ordinal_1). app singleton_order_isomorphic1.
app ordinal_1_value.
Qed.
Lemma is_ordinal_2: is_ordinal ord_two.
Proof. uf ord_two. app ordinal_pr7. app worder_canonical_doubleton_order.
Qed.
Lemma is_ordinal_omega: is_ordinal ord_omega.
Proof. uf ord_omega. app ordinal_pr7. app Bnat_order_worder.
Qed.
Definition ord_sum r g := order_type (ordinal_sum r g).
Definition ord_prod r g := order_type (lexicographic_order r g).
Definition ord_sum2 a b := order_type (ordinal_sum2 a b).
Definition ord_prod2 a b := order_type (ordinal_product2 a b).
Lemma ord_sum2_pr: forall a b,
ord_sum2 a b = ord_sum canonical_doubleton_order (variantLc a b).
Proof. ir. tv.
Qed.
Lemma ord_prod2_pr: forall a b,
ord_prod2 a b = ord_prod canonical_doubleton_order (variantLc b a).
Proof. ir. tv.
Qed.
Lemma ord_sum_type: forall r g,
order r -> substrate r = domain g -> fgraph g ->
(forall i, inc i (domain g) -> order (V i g))
-> is_order_type (ord_sum r g).
Proof. ir. uf ord_sum. app ordinal_pr6. app ordinal_sum_order. red. eee.
Qed.
Lemma ord_sum_ordinal: forall r g,
worder r -> substrate r = domain g -> fgraph g ->
(forall i, inc i (domain g) -> is_ordinal (V i g))
-> is_ordinal (ord_sum r g).
Proof. ir. uf ord_sum. app ordinal_pr7.
app ordinal_sum_worder. red. eee. nin H. am. ir. cp (H2 _ H3).
nin (ordinal_pr5 H4). am. ir. cp (H2 _ H3). app (ordinal_pr5 H4).
Qed.
Lemma ord_prod_type: forall r g,
worder r -> substrate r = domain g -> fgraph g ->
(forall i, inc i (domain g) -> order (V i g))
-> is_order_type (ord_prod r g).
Proof. ir. uf ord_prod. app ordinal_pr6. app lexorder_order. red. eee.
Qed.
Lemma ord_prod_ordinal: forall r g,
worder r -> substrate r = domain g -> fgraph g ->
(forall i, inc i (domain g) -> is_ordinal (V i g))
-> is_finite_set (substrate r)
-> is_ordinal (ord_prod r g).
Proof. ir. uf ord_prod. app ordinal_pr7.
app lexorder_worder. red. eee. ir. cp (H2 _ H4).
nin (ordinal_pr5 H5). am. ir. cp (H2 _ H4). app (ordinal_pr5 H5).
Qed.
Lemma ord_sum2_type: forall a b, order a -> order b ->
is_order_type (ord_sum2 a b).
Proof. ir. uf ord_sum2. app ordinal_pr6. app ordinal_sum2_order.
Qed.
Lemma ord_sum2_ordinal: forall a b, worder a -> worder b ->
is_ordinal (ord_sum2 a b).
Proof. ir. uf ord_sum2. app ordinal_pr7. app ordinal_sum2_worder.
Qed.
Lemma ord_prod2_type: forall a b, order a -> order b ->
is_order_type (ord_prod2 a b).
Proof. ir. uf ord_prod2. app ordinal_pr6. app ordinal_product2_order.
Qed.
Lemma ord_prod2_ordinal: forall a b, worder a -> worder b ->
is_ordinal (ord_prod2 a b).
Proof. ir. uf ord_prod2. app ordinal_pr7. app ordinal_product2_worder.
Qed.
Lemma ord_sum_invariant1: forall r r' f g g',
order r -> substrate r = domain g -> fgraph g ->
order r' -> substrate r' = domain g' -> fgraph g' ->
order_isomorphism f r r' ->
(forall i, inc i (substrate r) -> order_isomorphic (V i g) (V (W i f) g'))
-> ord_sum r g = ord_sum r' g'.
Proof. ir. uf ord_sum.
assert (ordinal_sum_axioms r g). red. eee. ir. wri H0 H7.
nin (H6 _ H7). red in H8. ee. am.
assert (ordinal_sum_axioms r' g'). red. eee. ir. wri H3 H8.
red in H5. ee. nin H10. rwi H12 H8. nin (surjective_pr2 H14 H8). nin H15.
wr H16. wri H11 H15. nin (H6 _ H15). red in H17. ee. am.
cp (ordinal_sum_order H7). cp (ordinal_sum_order H8).
aw. set (fa := fam_of_substrates g).
set (fb := fam_of_substrates g').
set (oi := fun i =>
choose (fun z => order_isomorphism z(V i g) (V (W i f) g'))).
assert (forall i, inc i (substrate r) ->
order_isomorphism (oi i) (V i g) (V (W i f) g')).
ir. uf oi. app choose_pr. cp (H6 _ H11). nin H12. exists x. am.
set (h := fun x=> J (W (P x) (oi (Q x))) (W (Q x) f)).
assert (forall x, inc x (disjoint_union fa) -> inc (h x) (disjoint_union fb)).
ir. cp (du_index_pr H12). ufi fa H13. ufi fam_of_substrates H13.
nin H13. bwi H13. bwi H14. assert (inc (W (Q x) f) (domain g')).
red in H5. ee. wr H3. rw H19. app inc_W_target. fct_tac. wrr H18. ue.
nin H14. uf h. uf fb. uf fam_of_substrates.
app inc_disjoint_union. bw. bw. wri H0 H13. cp (H11 _ H13). red in H17. ee.
rw H21. app inc_W_target. fct_tac. wr H20. am. am.
assert (transf_axioms h (substrate (ordinal_sum r g))
(substrate(ordinal_sum r' g'))). rw ordinal_sum_substrate.
rw ordinal_sum_substrate. red. ir. app H12. am. am.
set (hh:= BL h (substrate (ordinal_sum r g)) (substrate (ordinal_sum r' g'))).
assert (bijective hh). uf hh. app bl_bijective.
rww ordinal_sum_substrate. ir.
cp (du_index_pr1 H14). cp (du_index_pr1 H15). ee. ufi h H16.
cp (pr2_def H16).
assert (Q u = Q v). red in H5. ee. nin H25; nin H25. app H30. wr H26; ue.
wr H26; ue. cp (pr1_def H16). wri H24 H25.
wri H0 H17. cp (H11 _ H17). red in H26. ee. rwi H29 H21. wri H24 H19.
rwi H29 H19. nin H28. nin H28. app pair_extensionality. app H33.
rww ordinal_sum_substrate.
ir. cp (du_index_pr1 H14). ee.
red in H5. ee. nin H19. wri H3 H15. rwi H21 H15. nin (surjective_pr2 H23 H15).
nin H24. uf h. wri H20 H24. cp (H11 _ H24). red in H26. ee. nin H28.
rwi H25 H30. rwi H30 H16. nin (surjective_pr2 H32 H16). nin H33.
wri H29 H33. assert (inc (J x0 x) (substrate (ordinal_sum r g))).
rw ordinal_sum_substrate. app inc_disjoint_union1.
ue. bw. exists (J x0 x). ee. am. aw. rw H34. rw H25. aw.
exists hh. red. eee. uf hh. aw. uf hh. aw. uf hh. aw. ir. aw. aw.
set (q1:= inc (h x) (sum_of_substrates g')).
set (q2:= inc (h y) (sum_of_substrates g')).
uf h. aw.
cp (du_index_pr1 H15). cp (du_index_pr1 H16). ee.
red in H5; ee. wri H25 H27.
assert (glt r' (W (Q x) f) (W (Q y) f) = glt r (Q x) (Q y)).
uf glt. rwi H0 H27. wr (H27 _ _ H17 H18). ap iff_eq. ir. eee. dneg. ue.
ir. eee. dneg. nin H24; nin H24. app H32. wr H25. ue. wr H25. ue.
uf ordinal_sum_r. aw. rw H28.
do 2 rwii ordinal_sum_substrate H13.
rwi H0 H11. cp (H11 _ H18). red in H29. ee. wri H32 H34.
ap iff_eq; ir. ee. uf q1. app H13. uf q2. app H13. nin H37. au. nin H37.
right. split. ue. rw H37. wrr H34. ue.
cp (du_index_pr1 H35). eee.
eee. nin H37. au. ee. nin H24. nin H24. wri H25 H40. rwi H0 H40.
cp (H40 _ _ H17 H18 H37). right. ee. am. rw H41. rwi H41 H38. rww H34. ue.
Qed.
Lemma ord_sum_invariant2: forall r g g',
order r -> substrate r = domain g -> fgraph g ->
substrate r = domain g' -> fgraph g' ->
(forall i, inc i (substrate r) -> order_isomorphic (V i g) (V i g'))
-> ord_sum r g = ord_sum r g'.
Proof. ir. ap (ord_sum_invariant1 H H0 H1 H H2 H3 (identity_isomorphism H)).
ir. rw identity_W. app H4. am.
Qed.
Lemma ord_prod_invariant1: forall r r' f g g',
worder r -> substrate r = domain g -> fgraph g ->
order r' -> substrate r' = domain g' -> fgraph g' ->
order_isomorphism f r r' ->
(forall i, inc i (substrate r) -> order_isomorphic (V i g) (V (W i f) g'))
-> ord_prod r g = ord_prod r' g'.
Proof. ir. uf ord_prod. assert (He: is_function f). red in H5. ee. fct_tac.
assert (lexicographic_order_axioms r g). red. eee. ir. wri H0 H7.
nin (H6 _ H7). red in H8. ee. am.
assert (lexicographic_order_axioms r' g'). red. eee.
assert (order_isomorphic r r'). exists f. am. app (worder_invariance H8 H).
ir. wri H3 H8. red in H5. ee. nin H10. rwi H12 H8.
nin (surjective_pr2 H14 H8). nin H15.
wr H16. wri H11 H15. nin (H6 _ H15). red in H17. ee. am.
cp (lexorder_order H7). cp (lexorder_order H8).
aw. set (fa := fam_of_substrates g).
set (fb := fam_of_substrates g').
set (oi := fun i =>
choose (fun z => order_isomorphism z(V i g) (V (W i f) g'))).
assert (forall i, inc i (substrate r) ->
order_isomorphism (oi i) (V i g) (V (W i f) g')).
ir. uf oi. app choose_pr. cp (H6 _ H11). nin H12. exists x. am.
set (fi := fun i => W i (inverse_fun f)).
assert (forall i, inc i (substrate r') -> W (fi i) f =i).
ir. red in H5. ee. uf fi. rwi H16 H12. sy.
ap (W_inverse H14 H12 (refl_equal (W i (inverse_fun f)))).
assert (forall i, inc i (substrate r') -> inc (fi i) (substrate r)).
ir. red in H5. ee. uf fi. rwi H17 H13. rw H16. app W_inverse3.
set (fj := fun i => W i f).
assert (Ha: forall i, inc i (substrate r) -> (inc (fj i) (substrate r'))).
red in H5. ee. ir. rw H17. uf fj. app inc_W_target. ue.
assert (Hb: forall i, inc i (substrate r) -> fi (fj i) = i). ir.
cp (Ha _ H14). cp (H12 _ H15). ufi fj H16. uf fj. red in H5. ee.
nin H18; nin H18. app H23. ue. ue.
set (h := fun z=> L (substrate r') (fun i => W (V (fi i) z) (oi (fi i)))).
set (A := substrate(lexicographic_order r g)).
set (B := substrate(lexicographic_order r' g')).
assert (HA : A = (prod_of_substrates g)). uf A. rww lexorder_substrate.
assert (HB : B = (prod_of_substrates g')). uf B. rww lexorder_substrate.
assert (forall z, inc z A -> inc (h z) B).
rw HA; rw HB. uf prod_of_substrates. uf fam_of_substrates. ir. uf h.
awi H14. aw. eee. gprops. bw. bw. ir. bw. cp (H13 _ H17). cp (H11 _ H18).
red in H19. ee. rwi (H12 _ H17) H23. rw H23. app inc_W_target. fct_tac.
wrr H22. rwi H15 H16. wri H0 H16. bwi H16. cp (H16 _ H18). bwi H25. am. am.
ue. gprops. gprops.
assert (forall w, inc w B -> exists z, w = h z & inc z A).
rw HA; rw HB. uf prod_of_substrates. uf fam_of_substrates. ir. awi H15.
ee. bwi H16.
exists (L (substrate r) (fun i => W (V (fj i) w) (inverse_fun (oi i)))).
uf h. split. app fgraph_exten. gprops. bw. ue. ir. cp (H17 _ H18).
rwi H16 H18. bwi H19; tv. wri H3 H18. cp (H13 _ H18). bw. uf fj.
set (H12 _ H18). rw e. cp (H11 _ H20). nin H21. ee.
assert (inc (V x w) (target (oi (fi x)))). wr H25. rww e.
app (W_inverse H23 H27 (refl_equal (W (V x w) (inverse_fun (oi (fi x)))))).
aw. ee. gprops. bw. bw. ir. bw. cp (Ha _ H18). cp (H11 _ H18).
red in H20. ee. rw H23. app W_inverse3. wr H24. rwi H16 H17. rwi H3 H19.
cp (H17 _ H19). bwi H26. am. am. ue. gprops. gprops.
assert (forall z z', inc z A -> inc z' A -> h z = h z' -> z = z').
assert (fgraph (fam_of_substrates g)). uf fam_of_substrates. gprops.
rw HA. ir. cp H17; cp H18. ufi prod_of_substrates H17.
ufi prod_of_substrates H18. ap (productb_exten H16 H17 H18).
uf fam_of_substrates. bw. ir. cp (prod_of_substrates_pr H22 H20).
cp (prod_of_substrates_pr H22 H21). wri H0 H22. cp (Ha _ H22). cp (Hb _ H22).
assert (V (fj i) (h z) = V (fj i) (h z')). rww H19. ufi h H27. bwi H27; tv.
rwi H26 H27. cp (H11 _ H22). red in H28. ee. nin H30. nin H30.
app H35. ue. ue.
assert (transf_axioms h A B). am.
set (hh:= BL h A B). assert (bijective hh). uf hh. app bl_bijective.
ir. nin (H15 _ H18). ee. exists x. ee. am. sy; am.
exists hh. red. eee. uf hh. aw. uf hh. aw. uf hh. aw. ir. rww bl_W. rww bl_W.
rww lexorder_gle1. rww lexorder_gle1. wr HA. wr HB.
cp (H14 _ H19). cp (H14 _ H20).
ap iff_eq. ir. eee. nin H25. rw H25. au. nin H25. right. ee.
cp (Ha _ H25). cp (Hb _ H25). exists (fj x0). split. am. cp (H11 _ H25).
uf h. bw. rw H29. split. uf fj.
app (order_isomorphism_pr2 H30 (a:= (V x0 x)) (b:= (V x0 y))).
ir. assert (inc i (substrate r')). order_tac. bw. rww (H27 (fi i)).
wri (H12 _ H32) H31. ufi fj H31.
rww (order_isomorphism_pr H5 (a:= fi i) (b:= x0)). app H13.
ir. ee. am. am. nin H25. left. app H16. nin H25. ee. right.
cp (H13 _ H25). cp (H11 _ H28).
exists (fi x0). ee. am. ufi h H26. bwi H26; tv.
rww (order_isomorphism_pr H29 (a:= (V (fi x0) x)) (b:= (V (fi x0) y))).
rww (H12 _ H25). app prod_of_substrates_pr. ue. ue.
app prod_of_substrates_pr. ue. ue.
ir. cp (order_isomorphism_pr2 H5 H30).
assert (inc (W i f) (substrate r')). order_tac. rwii H12 H31. cp (H27 _ H31).
ufi h H33. bwi H33; tv. assert (inc i (substrate r)). order_tac.
cp (Hb _ H34). ufi fj H35. rwi H35 H33. cp (H11 _ H34). red in H36. ee.
nin H38. nin H38. app H43. wr H39. app prod_of_substrates_pr. ue. ue.
wr H39. app prod_of_substrates_pr. ue. ue.
Qed.
Lemma ord_prod_invariant2: forall r g g',
worder r -> substrate r = domain g -> fgraph g ->
substrate r = domain g' -> fgraph g' ->
(forall i, inc i (substrate r) -> order_isomorphic (V i g) (V i g'))
-> ord_prod r g = ord_prod r g'.
Proof. ir. assert (order r). nin H; am.
ap (ord_prod_invariant1 H H0 H1 H5 H2 H3 (identity_isomorphism H5)).
ir. rw identity_W. app H4. am.
Qed.
Lemma ord_sum_invariant3: forall r g,
order r -> substrate r = domain g -> fgraph g ->
(forall i, inc i (substrate r) -> order (V i g)) ->
ord_sum r g = ord_sum r (L (substrate r) (fun i => order_type (V i g))).
Proof. ir. set (g' := (L (substrate r) (fun i : Set => order_type (V i g)))).
assert (substrate r = domain g'). uf g'. bw.
assert (fgraph g'). uf g'. gprops.
assert (forall i, inc i (substrate r) -> order_isomorphic (V i g) (V i g')).
ir. uf g'. bw. app ordinal_pr1. app H2.
app (ord_sum_invariant2 H H0 H1 H3 H4 H5).
Qed.
Lemma ord_prod_invariant3: forall r g,
worder r -> substrate r = domain g -> fgraph g ->
(forall i, inc i (substrate r) -> order (V i g)) ->
ord_prod r g = ord_prod r (L (substrate r) (fun i => order_type (V i g))).
Proof. ir. set (g' := (L (substrate r) (fun i : Set => order_type (V i g)))).
assert (substrate r = domain g'). uf g'. bw.
assert (fgraph g'). uf g'. gprops.
assert (forall i, inc i (substrate r) -> order_isomorphic (V i g) (V i g')).
ir. uf g'. bw. app ordinal_pr1. app H2.
app (ord_prod_invariant2 H H0 H1 H3 H4 H5).
Qed.
Lemma ord_0_plus_unit_l: forall x, is_order_type x ->
ord_sum2 ord_zero x = x.
Proof. ir. cp (ordinal_pr3 H). cp (ordinal_pr5 (is_ordinal_0)). nin H1.
clear H2. rwi ordinal0_pr H1. rw ordinal0_pr. cp (ordinal_sum2_order H1 H0).
uf ord_sum2. app ordinal_pr9. app order_isomorphic_symmetric.
set (f := fun z => J z TPb).
assert (transf_axioms f(substrate x) (substrate (ordinal_sum2 emptyset x))).
red. ir. rww ordinal_sum2_substrate. rw canonical_du2_pr. uf f. split.
fprops. aw. au.
exists (BL f (substrate x) (substrate (ordinal_sum2 emptyset x))).
red. ee. am. am. app bl_bijective. uf f. ir. inter2tac.
rww ordinal_sum2_substrate. ir. rwi canonical_du2_pr H4. nin H4.
nin H5. nin H5. rwi emptyset_substrate H5. elim (emptyset_pr H5).
exists (P y). eee. uf f. wr H6. aw. aw. aw. aw. ir. aw.
uf f.
rw canonical_du2_pr. rw canonical_du2_pr. aw. app iff_eq; ir. ee. fprops. au.
fprops. au. right. left. eee. ee. nin H8. ee. elim two_points_distinctb.
am. nin H8. eee; am. nin H8. contradiction.
Qed.
Lemma ord_sum_emptyset: forall r x,
order r -> substrate r = domain x -> fgraph x ->
substrate r = emptyset ->
ord_sum r x = ord_zero.
Proof. ir. assert (ordinal_sum_axioms r x). red. ee. am. am. am. wr H0. rw H2.
ir. elim (emptyset_pr H3).
uf ord_sum. app ordinal0_pr1. app ordinal_sum_order.
rww ordinal_sum_substrate.
app is_emptyset. ir. red. ir. nin (du_index_pr1 H4).
wri H0 H5. rwi H2 H5. elim (emptyset_pr H5).
Qed.
Lemma ord_sum_singleton: forall r x e,
order r -> substrate r = domain x -> fgraph x ->
(forall i, inc i (domain x) -> order (V i x)) ->
substrate r = singleton e ->
ord_sum r x = order_type (V e x).
Proof. ir. rwi H0 H3. assert (ordinal_sum_axioms r x). red. eee.
cp (ordinal_sum_order H4).
assert (inc e (domain x)). rw H3. fprops. cp (H2 _ H6). uf ord_sum. aw.
set (E:= substrate (ordinal_sum r x)).
assert (He:E =sum_of_substrates x). uf E. rww ordinal_sum_substrate.
assert (forall u, inc u E =
(is_pair u & Q u = e & inc (P u) (substrate (V e x)))).
ir. rw He. app iff_eq. ir.
cp (du_index_pr1 H8). rwi H3 H9. awi H9. eee.
ir. ee. assert (u = J (P u) (Q u)). aw. rw H11. rw H9.
app inc_disjoint_union1. bw. bw.
assert (transf_axioms P E (substrate (V e x))).
red. ir. rwi H8 H9. ee; am.
exists (BL P E (substrate (V e x))).
red. eee. app bl_bijective. ir. rwi H8 H10. rwi H8 H11.
ee. app pair_extensionality. ue. ir. exists (J y e). rw H8. aw. eee.
aw. aw. aw. ir. aw.
cp H10; cp H11. uf ordinal_sum_r. rwi H8 H12. rwi H8 H13. ee. rw H16. rw H14.
app iff_eq. ir. ee. nin H20. nin H20. elim H21. tv. nin H20; am.
ir. ee. ue. ue. au.
Qed.
Lemma ord_prod_singleton: forall r x e,
worder r -> substrate r = domain x -> fgraph x ->
(forall i, inc i (domain x) -> order (V i x)) ->
substrate r = singleton e ->
ord_prod r x = order_type (V e x).
Proof. ir. rwi H0 H3. assert (lexicographic_order_axioms r x). red. eee.
cp (lexorder_order H4). assert (Ha: inc e (singleton e)). fprops.
assert (inc e (domain x)). rw H3. fprops. cp (H2 _ H6). uf ord_prod. aw.
cp (lexorder_substrate H4).
set (E:= substrate (lexicographic_order r x)) in *.
cp H8. ufi prod_of_substrates H8. ufi fam_of_substrates H8. rwi H3 H8.
assert (transf_axioms (V e) E (substrate (V e x))). red. ir. rwi H9 H10.
app prod_of_substrates_pr.
assert (Hc:forall a b, inc a E-> inc b E -> V e a = V e b -> a = b).
ir. rwi H8 H11. rwi H8 H12.
assert (fgraph (L (singleton e) (fun i : Set => substrate (V i x)))). gprops.
ap (productb_exten H14 H11 H12). bw. ir. awi H15. ue.
exists (BL (V e) E (substrate (V e x))).
red. eee. app bl_bijective. ir.
exists (L (singleton e) (fun _:Set => y)). rw H8. aw. bw. eee.
gprops. ir. bw. awi H12. ue. gprops. aw. aw. aw. ir. rww bl_W.
rww bl_W. cp (H10 _ H11). nin (equal_or_not x0 y). wr H14.
app iff_eq. ir. order_tac. ir. order_tac. rww lexorder_gle1. wr H9.
app iff_eq; ir; eee. nin H17. contradiction. nin H17. ee.
rwi H0 H17. rwii H3 H17. awi H17. nin H18. wrr H17.
ir. eee. right. exists e. eee. split. am.
assert (V e x0 <> V e y). dneg. app (Hc _ _ H11 H12 H16). am.
ir. assert (inc i (substrate r)). order_tac. rwi H0 H17; rwi H3 H17. awi H17.
nin H16. contradiction.
Qed.
Lemma ord_prod_emptyset: forall r x,
worder r -> substrate r = domain x -> fgraph x ->
substrate r = emptyset ->
ord_prod r x = ord_one.
Proof. ir. assert (lexicographic_order_axioms r x). red. ee. am. am. am. wr H0. rw H2.
ir. elim (emptyset_pr H3). cp (lexorder_order H3).
cp (ordinal_pr10 is_ordinal_1).
assert (is_singleton (substrate (lexicographic_order r x))).
rww lexorder_substrate. uf prod_of_substrates. uf fam_of_substrates.
wr H0. rw H2. rw trivial_fgraph. rw product_trivial. exists emptyset. tv.
uf ord_prod. app ordinal_pr9. app singleton_order_isomorphic2.
app ordinal_pr3. app ordinal_1_value.
Qed.
Lemma ordinal_product_pr1: forall a b,
is_order_type a -> is_order_type b ->
ord_prod2 a b = (ord_sum b (cst_graph (substrate b) a)).
Proof. ir. cp (ordinal_pr3 H). cp (ordinal_pr3 H0).
cp (ordinal_product_pr H1 H2). uf ord_prod2. uf ord_sum.
cp H3. nin H3. red in H3. ee. aw.
Qed.
Lemma ordinal_product_pr2: forall a b c,
is_order_type a -> is_order_type b -> order_isomorphic b c ->
ord_prod2 a b = (ord_sum c (cst_graph (substrate c) a)).
Proof. ir. rw (ordinal_product_pr1 H H0).
assert (order b). app (ordinal_pr3 H0).
assert (substrate b = domain (cst_graph (substrate b) a)). uf cst_graph. bw.
assert (fgraph (cst_graph (substrate b) a)). uf cst_graph. gprops.
assert (order c). nin H1. red in H1. ee. am.
assert (substrate c = domain (cst_graph (substrate c) a)). uf cst_graph. bw.
assert (fgraph (cst_graph (substrate c) a)). uf cst_graph. gprops.
nin H1. ap (ord_sum_invariant1 H2 H3 H4 H5 H6 H7 H1).
ir. uf cst_graph. bw. app order_isomorphic_reflexive.
app (ordinal_pr3 H). red in H1. ee. rw H12. app inc_W_target. fct_tac. ue.
Qed.
Lemma ordinal_product_pr3: forall a b,
is_ordinal a -> is_ordinal b ->
ord_prod2 a b = (ord_sum b (cst_graph (substrate b) a)).
Proof. ir. app ordinal_product_pr1. app ordinal_pr10. app ordinal_pr10.
Qed.
Lemma ordinal_product_pr4: forall a b c,
is_ordinal a -> is_ordinal b -> order_isomorphic b c ->
ord_prod2 a b = (ord_sum c (cst_graph (substrate c) a)).
Proof. ir. app ordinal_product_pr2. app ordinal_pr10. app ordinal_pr10.
Qed.
Lemma ord_0_plus_unit_r: forall x, is_order_type x ->
ord_sum2 x ord_zero = x.
Proof. ir. cp (ordinal_pr3 H). cp (ordinal_pr5 (is_ordinal_0)). nin H1.
clear H2. rwi ordinal0_pr H1. rw ordinal0_pr. cp (ordinal_sum2_order H0 H1).
uf ord_sum2. app ordinal_pr9. app order_isomorphic_symmetric.
set (f := fun z => J z TPa).
assert (transf_axioms f(substrate x) (substrate (ordinal_sum2 x emptyset))).
red. ir. rww ordinal_sum2_substrate. rw canonical_du2_pr. uf f. split.
fprops. aw. au.
exists (BL f (substrate x) (substrate (ordinal_sum2 x emptyset))).
red. ee. am. am. app bl_bijective. uf f. ir. inter2tac.
rww ordinal_sum2_substrate. ir. rwi canonical_du2_pr H4. nin H4.
nin H5. exists (P y). eee. uf f. wr H6. aw.
nin H5. rwi emptyset_substrate H5. elim (emptyset_pr H5). aw. aw. aw. ir. aw.
uf f.
rw canonical_du2_pr. rw canonical_du2_pr. aw. app iff_eq; ir. ee. fprops. au.
fprops. au. au. ee. nin H8. ee; am. nin H8. nin H8. elim H8; tv.
nin H8. contradiction.
Qed.
Lemma ord_0_prod_r: forall x, is_order_type x ->
ord_prod2 x ord_zero = ord_zero.
Proof. ir. uf ord_prod2. set (t := (ordinal_product2 x ord_zero)).
uf ord_zero. uf t. rw ordinal0_pr.
cp (ordinal_pr3 H). cp (ordinal_pr5 (is_ordinal_0)). nin H1. clear H2.
rwi ordinal0_pr H1. cp (ordinal_product2_order H0 H1). aw.
exists (identity emptyset). red. eee. app identity_bijective. aw.
rw ordinal_product2_substrate. rw emptyset_substrate.
uf product2. simpl. app is_emptyset. red. ir.
awi H3. ee. assert (inc TPa two_points). fprops.
wri H4 H6. cp (H5 _ H6). rwii variant_if_rw H7. elim (emptyset_pr H7).
am. am. aw. rww emptyset_substrate. aw. ir. elim (emptyset_pr H3).
Qed.
Lemma ord_0_prod_l: forall x, is_order_type x ->
ord_prod2 ord_zero x = ord_zero.
Proof. ir. uf ord_prod2. set (t := (ordinal_product2 ord_zero x)).
uf ord_zero. uf t. rw ordinal0_pr.
cp (ordinal_pr3 H). cp (ordinal_pr5 (is_ordinal_0)). nin H1. clear H2.
rwi ordinal0_pr H1. cp (ordinal_product2_order H1 H0). aw.
exists (identity emptyset). red. eee. app identity_bijective.
rw ordinal_product2_substrate. rw emptyset_substrate.
uf product2. aw. app is_emptyset. red. ir.
awi H3. ee. assert (inc TPb two_points). fprops.
wri H4 H6. cp (H5 _ H6). rwii variant_if_not_rw H7. elim (emptyset_pr H7).
fprops. am. am. aw. rww emptyset_substrate. aw. ir. elim (emptyset_pr H3).
Qed.
Lemma ord_1_mult_unit_r: forall x, is_order_type x ->
ord_prod2 x ord_one = x.
Proof. ir. cp (ordinal_pr10 is_ordinal_1). rww ordinal_product_pr1.
cp (ordinal_pr3 H0). nin ordinal_1_value. rw H2.
set (f := (cst_graph (singleton x0) x)).
assert (substrate ord_one = domain f). uf f. uf cst_graph. bw.
assert (fgraph f). uf f. uf cst_graph. gprops.
assert (forall i, inc i (domain f) -> order (V i f)).
uf f. uf cst_graph. bw. ir. bw. app ordinal_pr3.
rw (ord_sum_singleton H1 H3 H4 H5 H2). uf f. uf cst_graph. bw.
app ordinal_pr8. fprops.
Qed.
Lemma ord_1_mult_unit_l: forall x, is_order_type x ->
ord_prod2 ord_one x = x.
Proof. ir. cp (ordinal_pr3 H). cp (ordinal_pr5 (is_ordinal_1)). nin H1.
clear H2. assert (order (ordinal_product2 ord_one x)).
app ordinal_product2_order. uf ord_prod2. app ordinal_pr9.
cp (ordinal_product2_substrate H1 H0).
nin ordinal_1_value.
assert (transf_axioms (V TPa) (substrate (ordinal_product2 ord_one x))
(substrate x)). red. ir. rwi H3 H5. rwi product2_rw H5. eee.
exists (BL (V TPa) (substrate (ordinal_product2 ord_one x)) (substrate x)).
red. eee. app bl_bijective. ir.
rwi H3 H6. rwi H3 H7. rwi product2_rw H6. ee. rwi product2_rw H7. ee.
rwi H4 H11; awi H11. rwi H4 H14; awi H14. app fgraph_exten.
ue. ir. rwi H9 H15. try_lvariant H15. ue. ir.
exists (variantLc y x0). rw H3. ee. rw product2_rw. bw. eee. bw.
aw. aw. aw. ir. aw. rw ordinal_product2_gle.
cp H6. cp H7. rwi H3 H8; rwi H3 H9. rwi product2_rw H8.
rwi product2_rw H9. ee. rwi H4 H15. awi H15. rw H15. rwi H4 H12.
awi H12. rw H12. app iff_eq;ir; eee. nin H18. nin H18. rw H18.
order_tac. nin H18. am. nin (equal_or_not (V TPa x1) (V TPa y)).
left. ee. am. order_tac. rw H4. fprops. right. split; am. am. am.
Qed.
Lemma order_prod_invariant4: forall a b c d,
order_isomorphic a b -> order_isomorphic c d ->
ord_prod2 a c = ord_prod2 b d.
Proof. ir. uf ord_prod2. uf ordinal_product2.
set (r := canonical_doubleton_order). cp substrate_canonical_doubleton_order.
change (ord_prod r (variantLc c a) = (ord_prod r (variantLc d b))).
app ord_prod_invariant2. uf r. app worder_canonical_doubleton_order. bw.
fprops. bw. fprops. ir. ufi r H2. rwi H1 H2. try_lvariant H2.
Qed.
Lemma order_sum_invariant4: forall a b c d,
order_isomorphic a b -> order_isomorphic c d ->
ord_sum2 a c = ord_sum2 b d.
Proof. ir.
set (r := canonical_doubleton_order). cp substrate_canonical_doubleton_order.
change (ord_sum r (variantLc a c) = (ord_sum r (variantLc b d))).
app ord_sum_invariant2. uf r. nin worder_canonical_doubleton_order. am. bw.
fprops. bw. fprops. ir. ufi r H2. rwi H1 H2. try_lvariant H2.
Qed.
Lemma ordinal_sum_distributive: forall x y z,
order x -> order y -> order z ->
ord_prod2 z (ord_sum2 x y) = ord_sum2 (ord_prod2 z x) (ord_prod2 z y).
Proof. ir. cp (ordinal_sum2_order H H0).
assert (ord_prod2 z (ord_sum2 x y) = ord_prod2 z (ordinal_sum2 x y)).
app order_prod_invariant4. app order_isomorphic_reflexive. uf ord_sum2.
app order_isomorphic_symmetric. app ordinal_pr1. rw H3.
cp (ordinal_product2_order H1 H). cp (ordinal_product2_order H1 H0).
cp (order_sum_invariant4 (ordinal_pr1 H4) (ordinal_pr1 H5)). uf ord_prod2.
wr H6. uf ord_sum2. cp (ordinal_product2_order H1 H2).
cp (ordinal_sum2_order H4 H5). rww ordinal_pr4.
set (f := fun z => J (variantLc (P (V TPa z)) (V TPb z)) (Q (V TPa z))).
assert (transf_axioms f (substrate (ordinal_product2 z (ordinal_sum2 x y)))
(substrate (ordinal_sum2 (ordinal_product2 z x) (ordinal_product2 z y)))).
red. ir. rwii ordinal_product2_substrate H9. rwi product2_rw H9. ee.
rwii ordinal_sum2_substrate H11. rwi canonical_du2_pr H11. ee.
rww ordinal_sum2_substrate. rww ordinal_product2_substrate.
rww canonical_du2_pr. uf f. aw. split. fprops. nin H13. left.
rww product2_rw. bw. eee. right. rww ordinal_product2_substrate.
rww product2_rw. eee. bw. bw. bw.
assert (forall u v : Set,
inc u (substrate (ordinal_product2 z (ordinal_sum2 x y))) ->
inc v (substrate (ordinal_product2 z (ordinal_sum2 x y))) ->
f u = f v -> u = v). uf f. rww ordinal_product2_substrate. ir.
rwi product2_rw H10. ee. rwi product2_rw H11. ee.
cp (pr1_def H12). cp (pr2_def H12).
cp (f_equal (V TPa) H19). bwi H21. cp (f_equal (V TPb) H19). bwi H22.
app fgraph_exten. ue. ir. rwi H13 H23. try_lvariant H23.
app pair_extensionality. rwii ordinal_sum2_substrate H14.
rwi canonical_du2_pr H14. ee; am.
rwii ordinal_sum2_substrate H17. rwi canonical_du2_pr H17. ee. am.
exists (BL f (substrate (ordinal_product2 z (ordinal_sum2 x y)))
(substrate (ordinal_sum2 (ordinal_product2 z x) (ordinal_product2 z y)))).
red. eee. app bl_bijective. ir.
rwii ordinal_sum2_substrate H11. rwi canonical_du2_pr H11. ee.
rwii ordinal_product2_substrate H12. rwii ordinal_product2_substrate H12.
exists (variantLc (J (V TPa (P y0)) (Q y0)) (V TPb (P y0))).
ee. rww ordinal_product2_substrate. rw product2_rw. eee. bw. bw.
rww ordinal_sum2_substrate. rw canonical_du2_pr. aw. ee. fprops.
nin H12; nin H12; rwi product2_rw H12; eee.
nin H12; nin H12; ee; rwi product2_rw H12; rw H13; bw; eee.
uf f. app pair_extensionality. fprops. aw.
nin H12; nin H12; rwi product2_rw H12; rw H13; bw;ee; aw;
app fgraph_exten. fprops. bw. sy; am. bw. ir. try_lvariant H17.
fprops. bw. sy; am. bw. ir. try_lvariant H17. bw. aw. aw. aw. aw.
ir. cp H11. cp H12. rww bl_W. rww bl_W.
rwii ordinal_product2_substrate H13. rwii ordinal_product2_substrate H14.
rwi product2_rw H13. rwi product2_rw H14. ee.
rww ordinal_sum2_gle. rwii ordinal_sum2_substrate H9.
set (WW:= canonical_du2 (substrate (ordinal_product2 z x))
(substrate (ordinal_product2 z y))) in *.
rwii ordinal_sum2_substrate H19. rwii ordinal_sum2_substrate H16.
rwi canonical_du2_pr H19. rwi canonical_du2_pr H16. ee.
assert (Q (V TPa x0) = TPa -> inc (variantLc (P (V TPa x0)) (V TPb x0))
(product2 (substrate x) (substrate z))).
ir. rww product2_rw. eee. bw. bw. nin H22. ee. am. nin H22.
elim two_points_distinct. wr H23; wrr H24. bw.
assert (Q (V TPa y0) = TPa -> inc (variantLc (P (V TPa y0)) (V TPb y0))
(product2 (substrate x) (substrate z))).
ir. rww product2_rw. eee. bw. bw. nin H21. ee. am. nin H21.
elim two_points_distinct. wr H24; wrr H25. bw.
assert (Q (V TPa x0) = TPb -> inc (variantLc (P (V TPa x0)) (V TPb x0))
(product2 (substrate y) (substrate z))).
ir. rww product2_rw. eee. bw. bw. nin H22. ee.
elim two_points_distinct. wr H26; wrr H25. ee. am. bw.
assert (Q (V TPa y0) = TPb -> inc (variantLc (P (V TPa y0)) (V TPb y0))
(product2 (substrate y) (substrate z))).
ir. rww product2_rw. eee. bw. bw. nin H21. ee.
elim two_points_distinct. wr H27; wrr H26. ee; am. bw.
app iff_eq. ir. ee. app H9. app H9. uf f. aw.
nin H22; nin H22; rw H28; nin H21; nin H21 ; rw H29. left. eee.
rwi ordinal_product2_gle H27. ee.
rww ordinal_product2_gle. ee. app H23. app H24. bw.
nin H31. nin H31. wr H31. au. nin H31.
rwi ordinal_sum2_gle H31. ee. nin H34. ee.
nin (equal_or_not (P (V TPa x0)) (P (V TPa y0))).
elim H32. app pair_extensionality. ue. right. split; am. nin H34.
ee. contradiction. ee. contradiction. am. am. am. am. right. right. eee.
rwi ordinal_product2_gle H27. ee. nin H31. ee.
cp (f_equal Q H31). rwi H28 H33. rwi H29 H33. elim two_points_distinctb. am.
nin H31. rwi ordinal_sum2_gle H31. ee. rwi H28 H34. rwi H29 H34.
nin H34. ee. elim two_points_distinctb. am. nin H34. ee. elim H35. tv.
nin H34. elim H35. tv. am. am. am. am. right. left. ee. fprops. fprops.
rwi ordinal_product2_gle H27. ee.
rww ordinal_product2_gle. ee. app H25. app H26. bw.
nin H31. nin H31. wr H31. au. nin H31.
rwi ordinal_sum2_gle H31. ee. nin H34. ee.
elim two_points_distinctb. wr H34. rw H28. tv. nin H34. ee.
nin (equal_or_not (P (V TPa x0)) (P (V TPa y0))).
elim H32. app pair_extensionality. ue. right. split; am. nin H34.
elim two_points_distinctb. wr H34. rw H28. tv. am. am. am. am.
ir. ee. ufi f H29. awi H29. rw ordinal_product2_gle.
rwii ordinal_product2_substrate H11. rwii ordinal_product2_substrate H12.
ee. am. am. rwi product2_rw H11. ee. rwi product2_rw H12. ee.
rwii ordinal_sum2_substrate H31. rwii ordinal_sum2_substrate H34.
uf glt. rwii ordinal_product2_gle H29. bwi H29.
nin H29. ee. nin H39. ee. left. ee. app pair_extensionality. rw H29. ue.
am. nin H39. right. split. rw ordinal_sum2_gle. ee. am. am. au.
am. am. dneg. rww H41. nin H29. ee. rwii ordinal_product2_gle H37.
ee. bwi H39. nin H39. ee. left. ee. app pair_extensionality.
nin H21. ee. contradiction. nin H21. nin H22. ee. contradiction. nin H22.
rw H41; rw H42. tv. am. nin H39. right. split.
rw ordinal_sum2_gle. ee. am. am. au. am. am. dneg. rww H41.
right. split. rw ordinal_sum2_gle. ee. am. am. au. am. am.
nin H29. dneg. wrr H37. am. am.
Qed.
Section Ordinal_assoc.
Variables r g r' g':Set.
Hypothesis oa_axiom : ordinal_sum_axioms r g.
Hypothesis oa_axiom' : ordinal_sum_axioms r' g'.
Hypothesis oa_link : r = ordinal_sum r' g'.
Lemma ordinal_sum_assoc_aux1 :forall l,
inc l (substrate r') ->
ordinal_sum_axioms (V l g')
(L (substrate (V l g')) (fun i => V (J i l) g)).
Proof. ir. cp oa_axiom; cp oa_axiom'. red in H0; red in H1. ee. red. ee.
app H4. ue. bw. gprops. bw. ir. bw. app H7. wr H5. rw oa_link.
rw ordinal_sum_substrate. ap inc_disjoint_union1. ue. am. am.
Qed.
Definition ordinal_sum_assoc_aux l:=
ordinal_sum (V l g') (L (substrate (V l g')) (fun i => V (J i l) g)).
Lemma ordinal_sum_assoc_aux2 :forall l,
inc l (domain g') -> order (ordinal_sum_assoc_aux l).
Proof. ir. uf ordinal_sum_assoc_aux. assert (inc l (substrate r')).
red in oa_axiom'. nin oa_axiom'. nin H1. rw H1. am. app ordinal_sum_order.
ap ordinal_sum_assoc_aux1. am.
Qed.
Lemma ordinal_sum_assoc_aux3 :
ordinal_sum_axioms r'
(L (domain g') (fun l=> ordinal_sum_assoc_aux l)).
Proof. ir. red. bw. cp oa_axiom; cp oa_axiom'. red in H; red in H0. eee.
eee. gprops. gprops. ir. bw. ap ordinal_sum_assoc_aux2. am.
Qed.
Definition ordinal_sum_assoc :=
ordinal_sum r' (L (domain g') (fun l=> ordinal_sum_assoc_aux l)).
Lemma ordinal_sum_assoc1: order ordinal_sum_assoc.
Proof. ir. uf ordinal_sum_assoc. app ordinal_sum_order.
ap ordinal_sum_assoc_aux3.
Qed.
Lemma ordinal_sum_assoc_iso:
order_isomorphism (BL (fun x=> J (J (P x) (P (Q x))) (Q (Q x)))
(sum_of_substrates g) (substrate (ordinal_sum_assoc)))
(ordinal_sum r g) (ordinal_sum_assoc).
Proof. ir. assert (transf_axioms (fun x => J (J (P x) (P (Q x))) (Q (Q x)))
(sum_of_substrates g) (substrate ordinal_sum_assoc)). red. ir.
uf ordinal_sum_assoc. aw. cp (du_index_pr1 H). ee.
cp oa_axiom. red in H3; ee. wri H4 H0. rwi oa_link H0. awi H0.
cp (du_index_pr1 H0). ee. ap inc_disjoint_union1. bw. bw.
uf ordinal_sum_assoc_aux. aw. app inc_disjoint_union1. bw. bw.
assert (J (P (Q c)) (Q (Q c)) = Q c). app pair_extensionality. fprops. aw.
aw. rww H10. app ordinal_sum_assoc_aux1. red in oa_axiom'.
nin oa_axiom'. nin H11. ue. am. app ordinal_sum_assoc_aux3.
set(FF:= BL (fun x => J (J (P x) (P (Q x))) (Q (Q x)))
(sum_of_substrates g) (substrate ordinal_sum_assoc)).
assert (is_function FF). uf FF. app bl_function.
assert (injective FF). red. ee. am. uf FF. aw. ir.
rwii bl_W H3. rwii bl_W H3. cp (pr1_def H3). cp (pr2_def H3).
cp (pr1_def H4). cp (pr2_def H4).
cp (du_index_pr1 H1). cp (du_index_pr1 H2). ee. app pair_extensionality.
cp oa_axiom. red in H14; ee. wri H15 H8. wri H15 H9. rwi oa_link H8.
rwi oa_link H9. awi H8. awi H9. cp (du_index_pr1 H8). cp (du_index_pr1 H9).
ee. app pair_extensionality. am. am.
assert (bijective FF). red. ee. am. app surjective_pr6. uf FF.
simpl. ir. ufi ordinal_sum_assoc H2. awi H2.
cp (du_index_pr1 H2). bwi H3. ee. ufi ordinal_sum_assoc_aux H4. awi H4.
cp (du_index_pr1 H4). bwi H6. ee.
set (x:= J (P (P y)) (J (Q (P y)) (Q y))).
assert (inc x (sum_of_substrates g)). uf x. ap inc_disjoint_union1.
cp oa_axiom. red in H9; ee. wr H10. rw oa_link. aw. app inc_disjoint_union1.
am. aw. exists x. ee. am. rww bl_W. uf x. aw. eee. eee.
ap ordinal_sum_assoc_aux1. cp oa_axiom'. red in H6; ee. ue. nin H3. am.
ap ordinal_sum_assoc_aux3.
red. eee. app ordinal_sum_assoc1. aw. uf FF. aw. uf FF. aw. ir.
ufi FF H3; ufi FF H4. awi H3. awi H4.
uf FF. rww bl_W. rww bl_W. cp (H _ H3). cp (H _ H4). simpl in H5. simpl in H6.
cp (du_index_pr1 H3). cp (du_index_pr1 H4). ee. cp oa_axiom. red in H13; ee.
wri H14 H7. wri H14 H8. rwi oa_link H7. rwi oa_link H8. awi H7. awi H8.
cp (du_index_pr1 H7). cp (du_index_pr1 H8). ee.
rw ordinal_sum_related. sy. ap iff_eq. uf ordinal_sum_assoc.
rw ordinal_sum_related. uf ordinal_sum_r. ir. eee. awi H25.
nin H25. left. rw oa_link. red; ee. aw. ee.
wr (pair_recov H22). app inc_disjoint_union1.
wr (pair_recov H20). app inc_disjoint_union1. left. am. red in H25. ee.
dneg. ue. ee. bwi H26. ufi ordinal_sum_assoc_aux H26.
rwi ordinal_sum_related H26. ee. red in H28. awi H28.
nin H28. left. rw oa_link. red. ee. aw. ee.
wr (pair_recov H22). app inc_disjoint_union1.
wr (pair_recov H20). app inc_disjoint_union1. red. right. ee. am.
red in H28; eee. red in H28. ee. dneg. ue. ee. right. bwi H29. awi H29.
assert (Q x = Q y). app pair_extensionality. ee. am. am. am. ue. ue.
app ordinal_sum_assoc_aux1. cp oa_axiom'. red in H27. ee. rw H28. am. am.
app ordinal_sum_assoc_aux3.
ir. uf ordinal_sum_assoc. aw. ee.
ufi ordinal_sum_assoc H5. awi H5. am. ap ordinal_sum_assoc_aux3.
ufi ordinal_sum_assoc H6. awi H6. am. ap ordinal_sum_assoc_aux3.
assert (J (P (Q x)) (Q (Q x)) = Q x). app pair_recov.
assert (J (P (Q y)) (Q (Q y)) = Q y). app pair_recov.
assert (inc (J (P x) (P (Q x))) (sum_of_substrates
(L (substrate (V (Q (Q x)) g')) (fun i : Set => V (J i (Q (Q x))) g)))).
app inc_disjoint_union1. bw. bw. rw H26. am.
assert (inc (J (P y) (P (Q y))) (sum_of_substrates
(L (substrate (V (Q (Q y)) g')) (fun i : Set => V (J i (Q (Q y))) g)))).
app inc_disjoint_union1. bw. bw. rw H27. am.
nin H25. rwi oa_link H25. red in H25. ee. awi H25. ee. nin H32. left. aw.
right. ee. aw. aw. uf ordinal_sum_assoc_aux. bw. aw. ee. am. rww H32.
nin (equal_or_not (P (Q x)) (P (Q y))). right. ee. aw. aw. elim H30.
wr H26. rw H34. rw H32. am. left. ee. red. ee. aw. aw.
ap ordinal_sum_assoc_aux1. cp oa_axiom'. red in H34; ee. ue. am.
right. ee. aw. ue. uf ordinal_sum_assoc_aux. bw. aw. ee. am. rww H25.
right. ee. aw. rww H25. uf ordinal_sum_assoc_aux. bw. aw. ee. aw.
ap ordinal_sum_assoc_aux1. cp oa_axiom'. red in H31; ee. ue.
rw pr2_pair. ue. ap ordinal_sum_assoc_aux3. am. am. am.
Qed.
End Ordinal_assoc.
End Ordinals.
Export Ordinals.