set-theory/vbg/ordinalScript.sml

33   rw[iseg_def, SUBSET_def, SPEC0] >- metis_tac [] >>
51   rw[woclass_def, totalR_def, poc_def, LE_ANTISYM]
75   rw[ordle_def])
82   rw[woclass_def, EQ_IMP_THM]
84   rw[totalR_def, poc_def]
88            by (rw[Once EXTENSION] >> metis_tac [SET_def]) >>
94            by rw[Once EXTENSION, EXISTS_OR_THM] >>
100            by rw[Once EXTENSION, EXISTS_OR_THM] >>
106   rw[ordinal_def, transitive_def])
112   rw[ordinal_def]
116         qx_gen_tac `x` >> rw[] >>
131   Induct_on `SET a` >> rw[] >> metis_tac [ORDINALS_CONTAIN_ORDINALS]);
137   Induct_on `ordinal ��` >> rw[] >>
138   Cases_on `�� = {}` >> rw[] >>
146   rw[Ord_def, ordinal_def, iseg_def] >> rw[Once EXTENSION] >>
147   rw[EQ_IMP_THM] >| [
154     rw[ordle_def],
161   rw[ordinal_def, iseg_def] >> rw[Once EXTENSION] >>
177   rw[woclass_thm, Ord_def]
180         Cases_on `x = y` >- rw[] >>
185         qexists_tac `x` >> rw[] >>
201     >- (rw[orderiso_def]>>
204         qexists_tac `g` >> qunabbrev_tac `g` >> rw[] >| [
205           SELECT_ELIM_TAC >> rw[] >> metis_tac [],
206           SELECT_ELIM_TAC >> conj_tac >- metis_tac [] >> rw[] >>
208           qexists_tac `f y` >> rw[] >> SELECT_ELIM_TAC >>
210           SELECT_ELIM_TAC >> conj_tac >- metis_tac [] >> rw[] >>
212           qx_gen_tac `b` >> rw[] >>
214              rw[ordle_def],
215              rw[ordle_def],
216              `b ��� x` by rw[ordle_def] >>
219              rw[] >> fs[ordle_def] >> metis_tac [IN_ANTISYM, IN_REFL]
228   `E ��� {}` by (rw[Once EXTENSION, Abbr`E`] >> metis_tac[SET_def]) >>
229   `E ��� ��` by rw[SUBSET_def, Abbr`E`] >>
244      by (rw[iseg_def] >> simp[Once EXTENSION] >>
245          qx_gen_tac `e'` >> EQ_TAC >> rw[] >-
249      by (rw[iseg_def] >> simp[Once EXTENSION] >>