Grace/Cumulus/Cardinal/Hartogs.g17

Open in Workbench Download source

Imports

Product · Order

Declarations

Source

1-- Hartogs construction2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Cardinal.Hartogs8import Product9import Order1011-- All well-orders carried by subsets of A form a set. The first12-- coordinate is bounded by 𝒫(A), and the relation coordinate by 𝒫(A × A).13-- Hartogs' ordinal will arise from the order types represented here.14def wellOrderCodes (A : Set) : Set := {15  p ∈ 𝒫(A) × 𝒫(A × A) |16  ∃ B, (B ⊆ A) ∧ ∃ r, RelationBetween(r, A, A) ∧ p = (B, r) ∧ WellOrder(B, r)17}1819-- Guarding the relation makes the recursive definition below total in A and20-- r. When r is a well-order this is just r; otherwise it is empty.21def activeWellOrderRelation (A r : Set) : Set := { p ∈ r | WellOrder(A, r) }2223theorem activeWellOrderRelation.relates (x y A r : Set)24  shows relates(activeWellOrderRelation(A, r), x, y) ↔25    relates(r, x, y) ∧ WellOrder(A, r)26proof27  simp [activeWellOrderRelation, relates]2829theorem activeWellOrderRelation.well_founded (A r : Set)30  shows wellFoundedOn(activeWellOrderRelation(A, r), A)31proof32  have alternatives : WellOrder(A, r) ∨ ¬WellOrder(A, r) by tauto33  cases alternatives with wellOrdered | notWellOrdered34  . have founded := WellOrder.well_founded with wellOrdered35    intros s hs36    specialize founded with s, hs37    obtain ⟨m, hm⟩ := founded38    witness m39    rcases hm with ⟨hmS, minimal⟩40    constructor41    . exact hmS42    . intros y hyS hActive43      obtain ⟨hRelation, retainedOrder⟩ := activeWellOrderRelation.relates.forward with hActive44      exact minimal with y, hyS, hRelation45    intros s hs46    rcases hs with ⟨hSubset, hNonempty⟩47    obtain ⟨m2, hm2⟩ := set.foundation with hNonempty48    witness m249    rcases hm2 with ⟨hmS2, minimal2⟩50    constructor51    . exact hmS252    . intros y hyS hActive53      have shape := activeWellOrderRelation.relates.forward with hActive54      tauto5556theorem activeWellOrderRelation.transitive (A r : Set)57  requires order : WellOrder(A, r)58  shows TransitiveOn(A, activeWellOrderRelation(A, r))59proof60  have linear := WellOrder.strict_linear with order61  have transitive := StrictLinearOrder.transitive with linear62  intros x hx y hy z hz hxy hyz63  have xy := activeWellOrderRelation.relates.forward with hxy64  have yz := activeWellOrderRelation.relates.forward with hyz65  rcases xy with ⟨rxy, retainedOrder⟩66  rcases yz with ⟨ryz, retainedOrder2⟩67  specialize transitive with x, hx, y, hy, z, hz, rxy, ryz68  exact activeWellOrderRelation.relates.backward with ⟨transitive, order⟩6970-- The first genuinely recursive layer of the well-order collapse. The value71-- at x is the set of values already assigned to r-predecessors of x.72noncomputable well-founded def wellOrderCollapse (A r x : Set) : Set73  over A ordered by activeWellOrderRelation(A, r)74  certified by activeWellOrderRelation.well_founded75  | x using history => Relation.range(history)7677def wellOrderCollapseGraph (A r : Set) : Set := {78  (x ↦ wellOrderCollapse(A, r, x)) | x ∈ A79}8081def wellOrderType (A r : Set) : Set := Relation.range(wellOrderCollapseGraph(A, r))8283theorem wellOrderCollapse.membership (z A r x : Set)84  requires hx : x ∈ A85  shows z ∈ wellOrderCollapse(A, r, x) ↔86    ∃ y ∈ A, relates(activeWellOrderRelation(A, r), y, x) ∧87      z = wellOrderCollapse(A, r, y)88proof89  have equation := wellOrderCollapse.equation.direct at A, r, x with hx90  rw equation91  constructor92  . intro hz93    obtain ⟨bounded, source, sourcePair⟩ := Relation.range.membership.forward with hz94    obtain ⟨y, hyA, hyx, pairEqual⟩ := wellOrderCollapse.history.membership.forward with sourcePair95    obtain ⟨sourceEqual, valueEqual⟩ := orderedPair.injective with pairEqual96    refine ⟨y, hyA, hyx, valueEqual⟩97  . intro witness98    obtain ⟨y2, hyA2, hyx2, valueEqual2⟩ := witness99    have inHistory : (y2 ↦ wellOrderCollapse(A, r, y2)) ∈ wellOrderCollapse.history(A, r, x)100      exact wellOrderCollapse.history.membership.backward with ⟨y2, hyA2, hyx2, rfl⟩101    have inRange := Relation.range.contains with inHistory102    rwa valueEqual2103104theorem wellOrderCollapseGraph.relates (x y A r : Set)105  shows relates(wellOrderCollapseGraph(A, r), x, y) ↔106    x ∈ A ∧ y = wellOrderCollapse(A, r, x)107proof108  constructor109  . intro hPair110    unfold relates at hPair111    obtain ⟨source, sourceInA, pairEqual⟩ := wellOrderCollapseGraph.membership.forward with hPair112    obtain ⟨sourceEqual, valueEqual⟩ := orderedPair.injective with pairEqual113    constructor114    . rw ← sourceEqual115      exact sourceInA116    . rw [← sourceEqual, valueEqual]117      rfl118  . intro shape119    rcases shape with ⟨hx, valueEqual⟩120    unfold relates121    apply wellOrderCollapseGraph.membership.backward122    witness x123    constructor124    . exact hx125    . rw valueEqual126      rfl127128theorem wellOrderType.membership (y A r : Set)129  shows y ∈ wellOrderType(A, r) ↔130    ∃ x ∈ A, y = wellOrderCollapse(A, r, x)131proof132  constructor133  . intro hy134    unfold wellOrderType at hy135    obtain ⟨bounded, x, pair⟩ := Relation.range.membership.forward with hy136    have graphShape := wellOrderCollapseGraph.relates.forward at x, y, A, r137    have related : relates(wellOrderCollapseGraph(A, r), x, y) by exact pair138    specialize graphShape with related139    witness x140    exact graphShape141  . intro witnessData142    obtain ⟨x2, hxA, valueEqual⟩ := witnessData143    unfold wellOrderType144    apply Relation.range.contains at x2, y, wellOrderCollapseGraph(A, r)145    have graphPair := wellOrderCollapseGraph.relates.backward at x2, y, A, r146    have related : relates(wellOrderCollapseGraph(A, r), x2, y) by simp147  simp [wellOrderType, relates]148149-- The predecessor-collapse at every point of a well-order is a von Neumann150-- ordinal. This is the heart of the Mostowski collapse in the linear case.151theorem wellOrderCollapse.ordinal (A r : Set)152  requires order : WellOrder(A, r)153  shows ∀ x ∈ A, wellOrderCollapse(A, r, x) ∈ Ordinal154proof155  induction x over A ordered by activeWellOrderRelation(A, r) certified by activeWellOrderRelation.well_founded at A, r156  intros x hx ih157  constructor158    intros value valueInCollapse member memberInValue159    have valueShape := wellOrderCollapse.membership at value, A, r, x with hx160    have decodedValue : ∃ y ∈ A, relates(activeWellOrderRelation(A, r), y, x) ∧ value = wellOrderCollapse(A, r, y)161      simp [valueShape]162    obtain ⟨y, hyA, hyx, valueEqual⟩ := decodedValue163    have memberShape := wellOrderCollapse.membership at member, A, r, y with hyA164    rw valueEqual at memberInValue165    have decodedMember : ∃ w ∈ A, relates(activeWellOrderRelation(A, r), w, y) ∧ member = wellOrderCollapse(A, r, w)166      simp [memberShape]167    obtain ⟨w, hwA, hwy, memberEqual⟩ := decodedMember168    have relationTransitive := activeWellOrderRelation.transitive with order, w, hwA, y, hyA, x, hx, hwy, hyx169    have targetShape := wellOrderCollapse.membership at member, A, r, x with hx170    simp [targetShape]171  . intros value valueInCollapse172    have valueShape := wellOrderCollapse.membership at value, A, r, x with hx173    have decodedValue : ∃ y2 ∈ A, relates(activeWellOrderRelation(A, r), y2, x) ∧ value = wellOrderCollapse(A, r, y2)174      simp [valueShape]175    obtain ⟨y2, hyA2, hyx2, valueEqual2⟩ := decodedValue176    specialize ih with y2177    have predecessor : y2 ∈ A ∧ relates(activeWellOrderRelation(A, r), y2, x) by refine ⟨hyA2, hyx2⟩178    specialize ih with predecessor179    have valueOrdinal := ih180    have valueTransitive := Ordinal.transitive with valueOrdinal181    rwa valueEqual2182183theorem wellOrderCollapse.injective (x y A r : Set)184  requires order : WellOrder(A, r)185  requires hx : x ∈ A186  requires hy : y ∈ A187  requires equalValues : wellOrderCollapse(A, r, x) = wellOrderCollapse(A, r, y)188  shows x = y189proof190  by_contra unequal191  have linear := WellOrder.strict_linear with order192  have connected := StrictLinearOrder.connected with linear, x, hx, y, hy, unequal193  cases connected with xBeforeY | yBeforeX194  . have activeXY := activeWellOrderRelation.relates.backward at x, y, A, r195    have active : relates(activeWellOrderRelation(A, r), x, y) by simp196    have memberRule := wellOrderCollapse.membership at wellOrderCollapse(A, r, x), A, r, y with hy197    have member : wellOrderCollapse(A, r, x) ∈ wellOrderCollapse(A, r, y) by simp [memberRule]198    rw equalValues at member199    have irreflexive := membership.irreflexive at wellOrderCollapse(A, r, y)200    apply irreflexive201    exact member202  . have activeYX := activeWellOrderRelation.relates.backward at y, x, A, r203    have active2 : relates(activeWellOrderRelation(A, r), y, x) by simp204    have memberRule2 := wellOrderCollapse.membership at wellOrderCollapse(A, r, y), A, r, x with hx205    have member2 : wellOrderCollapse(A, r, y) ∈ wellOrderCollapse(A, r, x) by simp [memberRule2]206    rw ← equalValues at member2207    have irreflexive2 := membership.irreflexive at wellOrderCollapse(A, r, x)208    apply irreflexive2209    exact member2210211theorem wellOrderCollapseGraph.function (A r : Set)212  shows wellOrderCollapseGraph(A, r) : A → wellOrderType(A, r)213proof214  constructor215    intros p hp216    obtain ⟨x, hxA, pairEqual⟩ := wellOrderCollapseGraph.membership.forward with hp217    rw ← pairEqual218    apply product.pair219    . exact hxA220    . apply wellOrderType.membership.backward at wellOrderCollapse(A, r, x), A, r221      refine ⟨x, hxA, rfl⟩222  . constructor223      intros x2 y hxy z hxz224      have yShape := wellOrderCollapseGraph.relates.forward with hxy225      have zShape := wellOrderCollapseGraph.relates.forward with hxz226      rcases yShape with ⟨hxA2, yEqual⟩227      rcases zShape with ⟨hxA3, zEqual⟩228      rw [yEqual, zEqual]229      rfl230    . intros x3 hxA3231      witness wellOrderCollapse(A, r, x3)232      constructor233      . apply wellOrderType.membership.backward at wellOrderCollapse(A, r, x3), A, r234        refine ⟨x3, hxA3, rfl⟩235      . apply wellOrderCollapseGraph.relates.backward at x3, wellOrderCollapse(A, r, x3), A, r236        refine ⟨hxA3, rfl⟩237238theorem wellOrderCollapseGraph.injective (A r : Set)239  requires order : WellOrder(A, r)240  shows InjectiveBetween(wellOrderCollapseGraph(A, r), A, wellOrderType(A, r))241proof242  constructor243  . exact wellOrderCollapseGraph.function at A, r244  . intros x hx y hy z hz hxz hyz245    have xShape := wellOrderCollapseGraph.relates.forward with hxz246    have yShape := wellOrderCollapseGraph.relates.forward with hyz247    rcases xShape with ⟨hxA, xValue⟩248    rcases yShape with ⟨hyA, yValue⟩249    have equalValues : wellOrderCollapse(A, r, x) = wellOrderCollapse(A, r, y) by cc250    exact wellOrderCollapse.injective with order, hx, hy, equalValues251252theorem wellOrderCollapseGraph.surjective (A r : Set)253  shows SurjectiveBetween(wellOrderCollapseGraph(A, r), A, wellOrderType(A, r))254proof255  constructor256  . exact wellOrderCollapseGraph.function at A, r257  . intros y hy258    obtain ⟨x, hxA, valueEqual⟩ := wellOrderType.membership.forward with hy259    witness x260    constructor261    . exact hxA262    . apply wellOrderCollapseGraph.relates.backward at x, y, A, r263      refine ⟨hxA, valueEqual⟩264265theorem wellOrderCollapseGraph.bijective (A r : Set)266  requires order : WellOrder(A, r)267  shows BijectiveBetween(wellOrderCollapseGraph(A, r), A, wellOrderType(A, r))268proof269  simp [BijectiveBetween, wellOrderCollapseGraph.injective, wellOrderCollapseGraph.surjective]270271theorem wellOrderCollapseGraph.order_isomorphism (A r : Set)272  requires order : WellOrder(A, r)273  shows OrderIsomorphism(274    wellOrderCollapseGraph(A, r), A, activeWellOrderRelation(A, r),275    wellOrderType(A, r), membershipOn(wellOrderType(A, r)))276proof277  constructor278  . have bijective := wellOrderCollapseGraph.bijective at A, r279    exact bijective with order280  . intros x hx y hy u hu v hv hxu hyv281    have uShape := wellOrderCollapseGraph.relates.forward with hxu282    have vShape := wellOrderCollapseGraph.relates.forward with hyv283    rcases uShape with ⟨hxA, uEqual⟩284    rcases vShape with ⟨hyA, vEqual⟩285    constructor286    . intro hxy287      have collapseRule := wellOrderCollapse.membership at wellOrderCollapse(A, r, x), A, r, y with hy288      have collapseMember : wellOrderCollapse(A, r, x) ∈ wellOrderCollapse(A, r, y) by simp [collapseRule]289      have uvMember : u ∈ v by simp290      have membershipRule := membershipOn.relates with hu, hv291      simp292    . intro huv293      have membershipRule := membershipOn.relates with hu, hv294      have uvMember : u ∈ v by simp [membershipRule]295      rw [uEqual, vEqual] at uvMember296      have collapseRule := wellOrderCollapse.membership at wellOrderCollapse(A, r, x), A, r, y with hy297      have predecessorData : ∃ w ∈ A, relates(activeWellOrderRelation(A, r), w, y) ∧ wellOrderCollapse(A, r, x) = wellOrderCollapse(A, r, w)298        simp [collapseRule]299      obtain ⟨w, hwA, hwy, equalValues⟩ := predecessorData300      have injective := wellOrderCollapse.injective with order, hx, hwA, equalValues301      rwa injective302303theorem wellOrderType.ordinal (A r : Set)304  requires order : WellOrder(A, r)305  shows wellOrderType(A, r) ∈ Ordinal306proof307  constructor308    intros value valueInType member memberInValue309    obtain ⟨x, hxA, valueEqual⟩ := wellOrderType.membership.forward with valueInType310    rw valueEqual at memberInValue311    have memberRule := wellOrderCollapse.membership at member, A, r, x with hxA312    have memberShape : ∃ y ∈ A, relates(activeWellOrderRelation(A, r), y, x) ∧ member = wellOrderCollapse(A, r, y)313      simp [memberRule]314    obtain ⟨y, hyA, hyx, memberEqual⟩ := memberShape315    exact wellOrderType.membership.backward with ⟨y, hyA, memberEqual⟩316  . intros value2 valueInType2317    obtain ⟨x2, hxA2, valueEqual2⟩ := wellOrderType.membership.forward with valueInType2318    have collapseOrdinals := wellOrderCollapse.ordinal with order, x2, hxA2319    have collapseTransitive := Ordinal.transitive with collapseOrdinals320    rwa valueEqual2321322theorem wellOrderCodes.empty (A : Set)323  shows (∅, membershipOn(∅)) ∈ wellOrderCodes(A)324proof325  apply wellOrderCodes.membership.backward326  have emptySubset := empty.subset at A327  have emptyRelation := membershipOn.relation at empty328  have relationOnA := RelationBetween.monotone with emptyRelation, emptySubset, emptySubset329  constructor330  . apply product.pair at empty, membershipOn(∅), 𝒫(A), 𝒫(A × A)331    . apply set.powerset.backward at empty, A332      exact emptySubset333    . apply set.powerset.backward at membershipOn(∅), A × A334      have relationBound := relationOnA335      unfold RelationBetween at relationBound336      exact relationBound337  . witness empty338    constructor339    . exact emptySubset340    . witness membershipOn(∅)341      constructor342      . exact relationOnA343      . constructor344        . rfl345        . exact Ordinal.well_order at empty346347theorem wellOrderCodes.nonempty (A : Set)348  shows Nonempty(wellOrderCodes(A))349proof350  witness (∅, membershipOn(∅))351  exact wellOrderCodes.empty352353-- Collapsing an ordinal with its membership order returns the ordinal itself.354-- This will identify order types after transporting an ordinal into a set.355theorem wellOrderCollapse.on_ordinal (α : Set)356  requires ordinal : α ∈ Ordinal357  shows ∀ x ∈ α, wellOrderCollapse(α, membershipOn(α), x) = x358proof359  have order := Ordinal.well_order with ordinal360  have transitive := Ordinal.transitive with ordinal361  induction x over α ordered by membershipOn(α) certified by membershipOn.wellFounded at α362  intros x hx ih363  ext z364  constructor365  . intro member366    have shape := wellOrderCollapse.membership at z, α, membershipOn(α), x with hx367    have decoded : ∃ y ∈ α, relates(activeWellOrderRelation(α, membershipOn(α)), y, x) ∧368      z = wellOrderCollapse(α, membershipOn(α), y)369      exact shape.forward with member370    obtain ⟨y, hy, active, value⟩ := decoded371    obtain ⟨related, ordered⟩ := activeWellOrderRelation.relates.forward with active372    have predecessor : y ∈ α ∧ relates(membershipOn(α), y, x) by refine ⟨hy, related⟩373    have collapsed := ih with y, predecessor374    have rule := membershipOn.relates with hy, hx375    have inside := rule.forward with related376    rw collapsed at value377    rwa value378  . intro insideZ379    have xSubset := transitive with x, hx380    have hz := xSubset with z, insideZ381    have ruleZ := membershipOn.relates with hz, hx382    have relatedZ := ruleZ.backward with insideZ383    have predecessorZ : z ∈ α ∧ relates(membershipOn(α), z, x) by refine ⟨hz, relatedZ⟩384    have collapsedZ := ih with z, predecessorZ385    have activeZ : relates(activeWellOrderRelation(α, membershipOn(α)), z, x)386      exact activeWellOrderRelation.relates.backward with ⟨relatedZ, order⟩387    have shapeZ := wellOrderCollapse.membership at z, α, membershipOn(α), x with hx388    apply shapeZ.backward389    witness z390    constructor391    . exact hz392    . constructor393      . exact activeZ394      . symm395        exact collapsedZ396397theorem wellOrderType.on_ordinal (α : Set)398  requires ordinal : α ∈ Ordinal399  shows wellOrderType(α, membershipOn(α)) = α400proof401  have collapse := wellOrderCollapse.on_ordinal with ordinal402  ext x403  constructor404  . intro member405    obtain ⟨y, hy, value⟩ := wellOrderType.membership.forward with member406    have same := collapse with y, hy407    rw same at value408    rwa value409  . intro hx410    have sameX := collapse with x, hx411    apply wellOrderType.membership.backward412    witness x413    constructor414    . exact hx415    . symm416      exact sameX417418-- The same collapse identity survives transport along any injection.419theorem wellOrderCollapse.on_injected_ordinal (f α A : Set)420  requires ordinal : α ∈ Ordinal421  requires injective : InjectiveBetween(f, α, A)422  shows ∀ x ∈ α,423    wellOrderCollapse(functionImage(f, α, A), transportedOrder(f, α, A, membershipOn(α)), f[x]) = x424proof425  have function := Injective.function with injective426  have originalOrder := Ordinal.well_order with ordinal427  have order := transportedOrder.well_order with *428  have transitive := Ordinal.transitive with ordinal429  induction x over α ordered by membershipOn(α) certified by membershipOn.wellFounded at α430  intros x hx ih431  have fxMember := functionImage.value with *432  ext z433  constructor434  . intro member435    have rule := wellOrderCollapse.membership at z, functionImage(f, α, A),436      transportedOrder(f, α, A, membershipOn(α)), f[x] with fxMember437    obtain ⟨v, vMember, active, value⟩ := rule.forward with member438    obtain ⟨edge, ordered⟩ := activeWellOrderRelation.relates.forward with active439    obtain ⟨bounded, y, hy, vValue⟩ := functionImage.membership.forward with vMember440    rw vValue at edge441    have original := transportedOrder.reflect with *442    have predecessor : y ∈ α ∧ relates(membershipOn(α), y, x) by refine ⟨hy, original⟩443    have collapsed := ih with y, predecessor444    have membershipRule := membershipOn.relates with hy, hx445    have inside := membershipRule.forward with original446    rw [vValue, collapsed] at value447    rwa value448  . intro insideZ449    have xSubset := transitive with x, hx450    have hz := xSubset with z, insideZ451    have membershipRuleZ := membershipOn.relates with hz, hx452    have originalZ := membershipRuleZ.backward with insideZ453    have predecessorZ : z ∈ α ∧ relates(membershipOn(α), z, x) by refine ⟨hz, originalZ⟩454    have collapsedZ := ih with z, predecessorZ455    have fzMember := functionImage.value with hz456    have edgeZ := transportedOrder.edge with *457    have activeZ : relates(activeWellOrderRelation(functionImage(f, α, A),458      transportedOrder(f, α, A, membershipOn(α))), f[z], f[x])459      exact activeWellOrderRelation.relates.backward with ⟨edgeZ, order⟩460    have ruleZ := wellOrderCollapse.membership at z, functionImage(f, α, A),461      transportedOrder(f, α, A, membershipOn(α)), f[x] with fxMember462    apply ruleZ.backward463    witness f[z]464    constructor465    . exact fzMember466    . constructor467      . exact activeZ468      . symm469        exact collapsedZ470471theorem wellOrderType.on_injected_ordinal (f α A : Set)472  requires ordinal : α ∈ Ordinal473  requires injective : InjectiveBetween(f, α, A)474  shows wellOrderType(functionImage(f, α, A), transportedOrder(f, α, A, membershipOn(α))) = α475proof476  have function := Injective.function with injective477  have collapse := wellOrderCollapse.on_injected_ordinal with *478  ext z479  constructor480  . intro member481    obtain ⟨v, vMember, value⟩ := wellOrderType.membership.forward with member482    obtain ⟨bounded, x, hx, vValue⟩ := functionImage.membership.forward with vMember483    have same := collapse with x, hx484    rw [vValue, same] at value485    rwa value486  . intro hz487    have fzMember := functionImage.value with *488    have sameZ := collapse with z, hz489    apply wellOrderType.membership.backward490    witness f[z]491    constructor492    . exact fzMember493    . symm494      exact sameZ495496-- Collect the ordinal types in two bounded stages. This avoids selecting a497-- representative well-order for each type: Replacement takes all of them.498def wellOrdersOn (A B : Set) : Set :=499  {r ∈ 𝒫(A × A) | WellOrder(B, r)}500501def wellOrderTypesOn (A B : Set) : Set :=502  {wellOrderType(B, r) | r ∈ wellOrdersOn(A, B)}503504def wellOrderTypeRows (A : Set) : Set :=505  {wellOrderTypesOn(A, B) | B ∈ 𝒫(A)}506507def wellOrderTypes (A : Set) : Set := ⋃(wellOrderTypeRows(A))508509def wellOrderTypeSuccessors (A : Set) : Set :=510  {next(α) | α ∈ wellOrderTypes(A)}511512-- An ordinal strictly above every ordinal type represented on a subset of A.513-- The non-injection theorem additionally needs transport along an injection.514def hartogsBound (A : Set) : Set := ⋃(wellOrderTypeSuccessors(A))515516theorem wellOrderTypes.membership (α A : Set)517  shows α ∈ wellOrderTypes(A) ↔518    ∃ B ∈ 𝒫(A), ∃ r ∈ wellOrdersOn(A, B), wellOrderType(B, r) = α519proof520  constructor521  . intro member522    unfold wellOrderTypes at member523    obtain ⟨row, rowMember, inRow⟩ := set.union.forward with member524    obtain ⟨B, subset, rowEqual⟩ := wellOrderTypeRows.membership.forward with rowMember525    rw ← rowEqual at inRow526    have represented := wellOrderTypesOn.membership.forward with inRow527    refine ⟨B, subset, represented⟩528  . intro represented529    obtain ⟨C, subsetC, r, order, equal⟩ := represented530    have rowInFamily : wellOrderTypesOn(A, C) ∈ wellOrderTypeRows(A)531      exact wellOrderTypeRows.membership.backward with ⟨C, subsetC, rfl⟩532    have inSelectedRow : α ∈ wellOrderTypesOn(A, C) := wellOrderTypesOn.membership.backward with ⟨r, order, equal⟩533    unfold wellOrderTypes534    exact set.union.backward with ⟨wellOrderTypesOn(A, C), rowInFamily, inSelectedRow⟩535536theorem wellOrderTypes.contains (A B r : Set)537  requires subset : B ⊆ A538  requires order : WellOrder(B, r)539  shows wellOrderType(B, r) ∈ wellOrderTypes(A)540proof541  have strict := WellOrder.strict_linear with order542  have relation := StrictLinearOrder.relation with strict543  have bounded := RelationBetween.monotone with relation, subset, subset544  unfold RelationBetween at bounded545  unfold Subset at bounded546  have relationMember := set.powerset.backward with bounded547  have orderMember : r ∈ wellOrdersOn(A, B) := wellOrdersOn.membership.backward with ⟨relationMember, order⟩548  have subsetLaw := subset549  unfold Subset at subsetLaw550  have carrierMember := set.powerset.backward with subsetLaw551  exact wellOrderTypes.membership.backward with ⟨B, carrierMember, r, orderMember, rfl⟩552553-- The types grow with the carrier: a well-order on a subset of A is a554-- well-order on a subset of any larger set.555theorem wellOrderTypes.monotone (A C : Set)556  requires hAC : A ⊆ C557  shows wellOrderTypes(A) ⊆ wellOrderTypes(C)558proof559  intros α hα560  obtain ⟨B, hB, r, hr, equal⟩ := wellOrderTypes.membership.forward with hα561  have subsetA := powerset.membership_iff.forward with hB562  have subsetC := Subset.transitive with subsetA, hAC563  have parts := wellOrdersOn.membership.forward with hr564  rw ← equal565  exact wellOrderTypes.contains with subsetC, parts.right566567theorem wellOrderTypes.ordinal (α A : Set)568  requires member : α ∈ wellOrderTypes(A)569  shows α ∈ Ordinal570proof571  simp [wellOrderTypes.membership, wellOrdersOn.membership, wellOrderType.ordinal]572573theorem hartogsBound.ordinal (A : Set)574  shows hartogsBound(A) ∈ Ordinal575proof576  unfold hartogsBound577  apply Ordinal.union578  intros β member579  obtain ⟨α, represented, equal⟩ := wellOrderTypeSuccessors.membership.forward with member580  have ordinal := wellOrderTypes.ordinal with represented581  rw ← equal582  exact Ordinal.next with ordinal583584theorem hartogsBound.contains_type (α A : Set)585  requires represented : α ∈ wellOrderTypes(A)586  shows α ∈ hartogsBound(A)587proof588  have successorMember : next(α) ∈ wellOrderTypeSuccessors(A)589    exact wellOrderTypeSuccessors.membership.backward with ⟨α, represented, rfl⟩590  have inside := next.contains at α591  unfold hartogsBound592  exact set.union.backward with ⟨next(α), successorMember, inside⟩593594-- The Hartogs bound grows with its argument.595theorem hartogsBound.monotone (A C : Set)596  requires hAC : A ⊆ C597  shows hartogsBound(A) ⊆ hartogsBound(C)598proof599  intros β hβ600  unfold hartogsBound at hβ601  obtain ⟨S, hS, hβS⟩ := union.membership.forward with hβ602  obtain ⟨α, hα, shape⟩ := wellOrderTypeSuccessors.membership.forward with603    hS604  have typeC := wellOrderTypes.monotone with hAC, α, hα605  have inC := hartogsBound.contains_type with typeC606  rw ← shape at hβS607  have split := next.membership.forward with hβS608  cases split with less | same609  . have inside := Ordinal.member_subset with (hartogsBound.ordinal at C), inC610    exact inside with β, less611  . rw same612    exact inC613614theorem hartogsBound.not_represented (A : Set)615  shows ¬hartogsBound(A) ∈ wellOrderTypes(A)616proof617  simp [hartogsBound.contains_type, membership.irreflexive]618619theorem hartogsBound.above_well_order (A B r : Set)620  requires subset : B ⊆ A621  requires order : WellOrder(B, r)622  shows wellOrderType(B, r) ∈ hartogsBound(A)623proof624  simp [wellOrderTypes.contains, hartogsBound.contains_type]625626theorem hartogsBound.not_order_type (A B r : Set)627  requires subset : B ⊆ A628  requires order : WellOrder(B, r)629  shows wellOrderType(B, r) ≠ hartogsBound(A)630proof631  have represented := wellOrderTypes.contains with *632  intro equal633  rw equal at represented634  exact hartogsBound.not_represented with represented635636theorem hartogsBound.above_ordinal_subset (α A : Set)637  requires ordinal : α ∈ Ordinal638  requires subset : α ⊆ A639  shows α ∈ hartogsBound(A)640proof641  have order := Ordinal.well_order with ordinal642  have above := hartogsBound.above_well_order with *643  have identity := wellOrderType.on_ordinal with ordinal644  rwa identity at above645646-- Hartogs' theorem: the constructed ordinal is too large to inject into A.647theorem hartogsBound.no_injection (A f : Set)648  shows ¬InjectiveBetween(f, hartogsBound(A), A)649proof650  intro injective651  have ordinal := hartogsBound.ordinal at A652  have originalOrder := Ordinal.well_order with ordinal653  have order := transportedOrder.well_order at f, hartogsBound(A), A,654    membershipOn(hartogsBound(A)) with *655  have subset := functionImage.subset at f, hartogsBound(A), A656  have forbidden := hartogsBound.not_order_type at A, functionImage(f, hartogsBound(A), A),657    transportedOrder(f, hartogsBound(A), A, membershipOn(hartogsBound(A))) with *658  have same := wellOrderType.on_injected_ordinal with *659  exact forbidden with same660661theorem Hartogs.theorem (A : Set)662  shows ∃ α, α ∈ Ordinal ∧ (∀ f, ¬InjectiveBetween(f, α, A))663proof664  witness hartogsBound(A)665  intro f666  exact hartogsBound.no_injection667