Primitive. The name Eps_i is a term of type (set → prop) → set.
Axiom. (Eps_i_ax) We take the following as an axiom:
∀P : set → prop, ∀x : set, P x → P (Eps_i P)
In Proofgold the corresponding term root is c3f0de... and proposition id is 756d6e...
Definition. We define True to be ∀p : prop, p → p of type prop.
In Proofgold the corresponding term root is f81b39... and object id is 94e6a7...
Definition. We define False to be ∀p : prop, p of type prop.
In Proofgold the corresponding term root is 1db705... and object id is 266ad5...
Definition. We define not to be λA : prop ⇒ A → False of type prop → prop.
In Proofgold the corresponding term root is f30435... and object id is 0dc3c7...
Notation. We use ¬ as a prefix operator with priority 700 corresponding to applying term not.
Definition. We define and to be λA B : prop ⇒ ∀p : prop, (A → B → p) → p of type prop → prop → prop.
In Proofgold the corresponding term root is 2ba7d0... and object id is 37da83...
Notation. We use ∧ as an infix operator with priority 780 and which associates to the left corresponding to applying term and.
Definition. We define or to be λA B : prop ⇒ ∀p : prop, (A → p) → (B → p) → p of type prop → prop → prop.
In Proofgold the corresponding term root is 957746... and object id is 86ae64...
Notation. We use ∨ as an infix operator with priority 785 and which associates to the left corresponding to applying term or.
Definition. We define iff to be λA B : prop ⇒ and (A → B) (B → A) of type prop → prop → prop.
In Proofgold the corresponding term root is 98aaaf... and object id is 6588e5...
Notation. We use ↔ as an infix operator with priority 805 and no associativity corresponding to applying term iff.
Beginning of Section Eq
Variable A : SType
Definition. We define eq to be λx y : A ⇒ ∀Q : A → A → prop, Q x y → Q y x of type A → A → prop.
Definition. We define neq to be λx y : A ⇒ ¬ eq x y of type A → A → prop.
End of Section Eq
Notation. We use = as an infix operator with priority 502 and no associativity corresponding to applying term eq.
Notation. We use ≠ as an infix operator with priority 502 and no associativity corresponding to applying term neq.
Beginning of Section FE
Variable A B : SType
Axiom. (func_ext) We take the following as an axiom:
∀f g : A → B, (∀x : A, f x = g x) → f = g
End of Section FE
Beginning of Section Ex
Variable A : SType
Definition. We define ex to be λQ : A → prop ⇒ ∀P : prop, (∀x : A, Q x → P) → P of type (A → prop) → prop.
End of Section Ex
Notation. We use ∃ x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using ex.
Axiom. (prop_ext) We take the following as an axiom:
∀p q : prop, iff p q → p = q
In Proofgold the corresponding term root is 00ac81... and proposition id is 1d1e56...
Primitive. The name In is a term of type set → set → prop.
Notation. We use ∈ as an infix operator with priority 500 and no associativity corresponding to applying term In. Furthermore, we may write ∀ x ∈ A, B to mean ∀ x : set, x ∈ A → B.
Definition. We define Subq to be λA B ⇒ ∀x ∈ A, x ∈ B of type set → set → prop.
In Proofgold the corresponding term root is 81c0ef... and object id is 317007...
Notation. We use ⊆ as an infix operator with priority 500 and no associativity corresponding to applying term Subq. Furthermore, we may write ∀ x ⊆ A, B to mean ∀ x : set, x ⊆ A → B.
Axiom. (set_ext) We take the following as an axiom:
∀X Y : set, X ⊆ Y → Y ⊆ X → X = Y
In Proofgold the corresponding term root is b3b698... and proposition id is 21238a...
Axiom. (In_ind) We take the following as an axiom:
∀P : set → prop, (∀X : set, (∀x ∈ X, P x) → P X) → ∀X : set, P X
In Proofgold the corresponding term root is 045211... and proposition id is 20faa5...
Notation. We use ∃ x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using ex and handling ∈ or ⊆ ascriptions using and.
Primitive. The name Empty is a term of type set.
Axiom. (EmptyAx) We take the following as an axiom:
¬ ∃x : set, x ∈ Empty
In Proofgold the corresponding term root is 4da931... and proposition id is c7b0d7...
Primitive. The name ⋃ is a term of type set → set.
Axiom. (UnionEq) We take the following as an axiom:
∀X x, x ∈ ⋃ X ↔ ∃Y, x ∈ Y ∧ Y ∈ X
In Proofgold the corresponding term root is bf4c26... and proposition id is 40660f...
Primitive. The name 𝒫 is a term of type set → set.
Axiom. (PowerEq) We take the following as an axiom:
∀X Y : set, Y ∈ 𝒫 X ↔ Y ⊆ X
In Proofgold the corresponding term root is 746e5a... and proposition id is d67d71...
Primitive. The name Repl is a term of type set → (set → set) → set.
Notation. {B| x ∈ A} is notation for Repl A (λ x . B).
Axiom. (ReplEq) We take the following as an axiom:
∀A : set, ∀F : set → set, ∀y : set, y ∈ {F x|x ∈ A} ↔ ∃x ∈ A, y = F x
In Proofgold the corresponding term root is 4f2357... and proposition id is 471122...
Definition. We define TransSet to be λU : set ⇒ ∀x ∈ U, x ⊆ U of type set → prop.
In Proofgold the corresponding term root is 538bb7... and object id is e69f92...
Definition. We define Union_closed to be λU : set ⇒ ∀X : set, X ∈ U → ⋃ X ∈ U of type set → prop.
In Proofgold the corresponding term root is 57561d... and object id is e45ed9...
Definition. We define Power_closed to be λU : set ⇒ ∀X : set, X ∈ U → 𝒫 X ∈ U of type set → prop.
In Proofgold the corresponding term root is 8b9cc0... and object id is d2954e...
Definition. We define Repl_closed to be λU : set ⇒ ∀X : set, X ∈ U → ∀F : set → set, (∀x : set, x ∈ X → F x ∈ U) → {F x|x ∈ X} ∈ U of type set → prop.
In Proofgold the corresponding term root is 5574bb... and object id is 513534...
Definition. We define ZF_closed to be λU : set ⇒ Union_closed U ∧ Power_closed U ∧ Repl_closed U of type set → prop.
In Proofgold the corresponding term root is 1bd4aa... and object id is e1eccf...
Primitive. The name UnivOf is a term of type set → set.
Axiom. (UnivOf_In) We take the following as an axiom:
∀N : set, N ∈ UnivOf N
In Proofgold the corresponding term root is efcc16... and proposition id is e805d4...
Axiom. (UnivOf_TransSet) We take the following as an axiom:
∀N : set, TransSet (UnivOf N)
In Proofgold the corresponding term root is 053575... and proposition id is cf4f5c...
Axiom. (UnivOf_ZF_closed) We take the following as an axiom:
∀N : set, ZF_closed (UnivOf N)
In Proofgold the corresponding term root is 770e35... and proposition id is 0e7363...
Axiom. (UnivOf_Min) We take the following as an axiom:
∀N U : set, N ∈ U → TransSet U → ZF_closed U → UnivOf N ⊆ U
In Proofgold the corresponding term root is 042dda... and proposition id is 1f7933...
Axiom. (FalseE) We take the following as an axiom:
False → ∀p : prop, p
In Proofgold the corresponding term root is 0dcfe3... and proposition id is f9a230...
Axiom. (TrueI) We take the following as an axiom:
True
In Proofgold the corresponding term root is f81b39... and proposition id is eb5cbf...
Axiom. (andI) We take the following as an axiom:
∀A B : prop, A → B → A ∧ B
In Proofgold the corresponding term root is 3c4f59... and proposition id is 3bf198...
Axiom. (andEL) We take the following as an axiom:
∀A B : prop, A ∧ B → A
In Proofgold the corresponding term root is c2f006... and proposition id is 718be4...
Axiom. (andER) We take the following as an axiom:
∀A B : prop, A ∧ B → B
In Proofgold the corresponding term root is f66b82... and proposition id is 5caea9...
Axiom. (orIL) We take the following as an axiom:
∀A B : prop, A → A ∨ B
In Proofgold the corresponding term root is 55be8c... and proposition id is 382673...
Axiom. (orIR) We take the following as an axiom:
∀A B : prop, B → A ∨ B
In Proofgold the corresponding term root is 3c63fc... and proposition id is 8d8e40...
Beginning of Section PropN
Variable P1 P2 P3 : prop
Axiom. (and3I) We take the following as an axiom:
P1 → P2 → P3 → P1 ∧ P2 ∧ P3
In Proofgold the corresponding term root is 23ac9c... and proposition id is cb999b...
Axiom. (and3E) We take the following as an axiom:
P1 ∧ P2 ∧ P3 → (∀p : prop, (P1 → P2 → P3 → p) → p)
In Proofgold the corresponding term root is 445f76... and proposition id is 50fabe...
Axiom. (or3I1) We take the following as an axiom:
P1 → P1 ∨ P2 ∨ P3
In Proofgold the corresponding term root is e44f34... and proposition id is ef9071...
Axiom. (or3I2) We take the following as an axiom:
P2 → P1 ∨ P2 ∨ P3
In Proofgold the corresponding term root is 8df6e1... and proposition id is 827a91...
Axiom. (or3I3) We take the following as an axiom:
P3 → P1 ∨ P2 ∨ P3
In Proofgold the corresponding term root is 017a00... and proposition id is 3b7f5a...
Axiom. (or3E) We take the following as an axiom:
P1 ∨ P2 ∨ P3 → (∀p : prop, (P1 → p) → (P2 → p) → (P3 → p) → p)
In Proofgold the corresponding term root is 5d069d... and proposition id is 2120c9...
Variable P4 : prop
Axiom. (and4I) We take the following as an axiom:
P1 → P2 → P3 → P4 → P1 ∧ P2 ∧ P3 ∧ P4
In Proofgold the corresponding term root is ed32cb... and proposition id is 906aaf...
Variable P5 : prop
Axiom. (and5I) We take the following as an axiom:
P1 → P2 → P3 → P4 → P5 → P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5
In Proofgold the corresponding term root is 041ced... and proposition id is 11fc47...
End of Section PropN
Axiom. (not_or_and_demorgan) We take the following as an axiom:
∀A B : prop, ¬ (A ∨ B) → ¬ A ∧ ¬ B
In Proofgold the corresponding term root is 8733b0... and proposition id is 27db91...
Axiom. (not_ex_all_demorgan_i) We take the following as an axiom:
∀P : set → prop, (¬ ∃x, P x) → ∀x, ¬ P x
In Proofgold the corresponding term root is 73523e... and proposition id is 075ddf...
Axiom. (iffI) We take the following as an axiom:
∀A B : prop, (A → B) → (B → A) → (A ↔ B)
In Proofgold the corresponding term root is 7516b9... and proposition id is 4d966a...
Axiom. (iffEL) We take the following as an axiom:
∀A B : prop, (A ↔ B) → A → B
In Proofgold the corresponding term root is 0e94c6... and proposition id is 9a07f6...
Axiom. (iffER) We take the following as an axiom:
∀A B : prop, (A ↔ B) → B → A
In Proofgold the corresponding term root is 54702a... and proposition id is f5dfc0...
Axiom. (iff_refl) We take the following as an axiom:
∀A : prop, A ↔ A
In Proofgold the corresponding term root is 01338d... and proposition id is 7b71b5...
Axiom. (iff_sym) We take the following as an axiom:
∀A B : prop, (A ↔ B) → (B ↔ A)
In Proofgold the corresponding term root is 00bac1... and proposition id is 11f51b...
Axiom. (iff_trans) We take the following as an axiom:
∀A B C : prop, (A ↔ B) → (B ↔ C) → (A ↔ C)
In Proofgold the corresponding term root is 363285... and proposition id is c3b8f1...
Axiom. (eq_i_tra) We take the following as an axiom:
∀x y z, x = y → y = z → x = z
In Proofgold the corresponding term root is 193bbf... and proposition id is 7ecbc4...
Axiom. (f_eq_i) We take the following as an axiom:
∀f : set → set, ∀x y, x = y → f x = f y
In Proofgold the corresponding term root is b0871b... and proposition id is 2a60fd...
Axiom. (neq_i_sym) We take the following as an axiom:
∀x y, x ≠ y → y ≠ x
In Proofgold the corresponding term root is 5c0ec9... and proposition id is 1a9898...
Definition. We define nIn to be λx X ⇒ ¬ In x X of type set → set → prop.
In Proofgold the corresponding term root is 36808c... and object id is 253451...
Notation. We use ∉ as an infix operator with priority 502 and no associativity corresponding to applying term nIn.
Axiom. (Eps_i_ex) We take the following as an axiom:
∀P : set → prop, (∃x, P x) → P (Eps_i P)
In Proofgold the corresponding term root is be36f0... and proposition id is 6a2832...
Axiom. (pred_ext) We take the following as an axiom:
∀P Q : set → prop, (∀x, P x ↔ Q x) → P = Q
In Proofgold the corresponding term root is e9e64b... and proposition id is d4b2d3...
Axiom. (prop_ext_2) We take the following as an axiom:
∀p q : prop, (p → q) → (q → p) → p = q
In Proofgold the corresponding term root is a9ede2... and proposition id is a56fc7...
Axiom. (Subq_ref) We take the following as an axiom:
∀X : set, X ⊆ X
In Proofgold the corresponding term root is 4c5395... and proposition id is 2efbac...
Axiom. (Subq_tra) We take the following as an axiom:
∀X Y Z : set, X ⊆ Y → Y ⊆ Z → X ⊆ Z
In Proofgold the corresponding term root is 79accb... and proposition id is fed662...
Axiom. (Subq_contra) We take the following as an axiom:
∀X Y z : set, X ⊆ Y → z ∉ Y → z ∉ X
In Proofgold the corresponding term root is d15e87... and proposition id is bd5a2f...
Axiom. (EmptyE) We take the following as an axiom:
∀x : set, x ∉ Empty
In Proofgold the corresponding term root is 93a77a... and proposition id is 8349ab...
Axiom. (Subq_Empty) We take the following as an axiom:
∀X : set, Empty ⊆ X
In Proofgold the corresponding term root is a517cd... and proposition id is 2faec3...
Axiom. (Empty_Subq_eq) We take the following as an axiom:
∀X : set, X ⊆ Empty → X = Empty
In Proofgold the corresponding term root is 2dd959... and proposition id is 988691...
Axiom. (Empty_eq) We take the following as an axiom:
∀X : set, (∀x, x ∉ X) → X = Empty
In Proofgold the corresponding term root is 3de0fd... and proposition id is 8b915b...
Axiom. (UnionI) We take the following as an axiom:
∀X x Y : set, x ∈ Y → Y ∈ X → x ∈ ⋃ X
In Proofgold the corresponding term root is 51b549... and proposition id is bade05...
Axiom. (UnionE) We take the following as an axiom:
∀X x : set, x ∈ ⋃ X → ∃Y : set, x ∈ Y ∧ Y ∈ X
In Proofgold the corresponding term root is db4bc1... and proposition id is ab781b...
Axiom. (UnionE_impred) We take the following as an axiom:
∀X x : set, x ∈ ⋃ X → ∀p : prop, (∀Y : set, x ∈ Y → Y ∈ X → p) → p
In Proofgold the corresponding term root is 8efd57... and proposition id is d621b2...
Axiom. (PowerI) We take the following as an axiom:
∀X Y : set, Y ⊆ X → Y ∈ 𝒫 X
In Proofgold the corresponding term root is 7143d7... and proposition id is 3c48d3...
Axiom. (PowerE) We take the following as an axiom:
∀X Y : set, Y ∈ 𝒫 X → Y ⊆ X
In Proofgold the corresponding term root is 149030... and proposition id is 647070...
Axiom. (Empty_In_Power) We take the following as an axiom:
∀X : set, Empty ∈ 𝒫 X
In Proofgold the corresponding term root is d2656b... and proposition id is 487855...
Axiom. (Self_In_Power) We take the following as an axiom:
∀X : set, X ∈ 𝒫 X
In Proofgold the corresponding term root is f81ef2... and proposition id is 8336ff...
Axiom. (xm) We take the following as an axiom:
∀P : prop, P ∨ ¬ P
In Proofgold the corresponding term root is 62e4c3... and proposition id is 7b6737...
Axiom. (dneg) We take the following as an axiom:
∀P : prop, ¬ ¬ P → P
In Proofgold the corresponding term root is 852f34... and proposition id is b7cc63...
Axiom. (not_all_ex_demorgan_i) We take the following as an axiom:
∀P : set → prop, ¬ (∀x, P x) → ∃x, ¬ P x
In Proofgold the corresponding term root is 9bfa06... and proposition id is 4b1474...
Axiom. (eq_or_nand) We take the following as an axiom:
or = (λx y : prop ⇒ ¬ (¬ x ∧ ¬ y))
In Proofgold the corresponding term root is 24ac29... and proposition id is d212ef...
Primitive. The name exactly1of2 is a term of type prop → prop → prop.
In Proofgold the corresponding term root is 163602... and object id is a0b944...
Axiom. (exactly1of2_I1) We take the following as an axiom:
∀A B : prop, A → ¬ B → exactly1of2 A B
In Proofgold the corresponding term root is 8e1e45... and proposition id is 4f94fa...
Axiom. (exactly1of2_I2) We take the following as an axiom:
∀A B : prop, ¬ A → B → exactly1of2 A B
In Proofgold the corresponding term root is c9fd90... and proposition id is 6c1ad9...
Axiom. (exactly1of2_E) We take the following as an axiom:
∀A B : prop, exactly1of2 A B → ∀p : prop, (A → ¬ B → p) → (¬ A → B → p) → p
In Proofgold the corresponding term root is 29b901... and proposition id is c67434...
Axiom. (exactly1of2_or) We take the following as an axiom:
∀A B : prop, exactly1of2 A B → A ∨ B
In Proofgold the corresponding term root is 18af73... and proposition id is e092f6...
Axiom. (ReplI) We take the following as an axiom:
∀A : set, ∀F : set → set, ∀x : set, x ∈ A → F x ∈ {F x|x ∈ A}
In Proofgold the corresponding term root is b146c5... and proposition id is f84982...
Axiom. (ReplE) We take the following as an axiom:
∀A : set, ∀F : set → set, ∀y : set, y ∈ {F x|x ∈ A} → ∃x ∈ A, y = F x
In Proofgold the corresponding term root is 311cdf... and proposition id is d07e78...
Axiom. (ReplE_impred) We take the following as an axiom:
∀A : set, ∀F : set → set, ∀y : set, y ∈ {F x|x ∈ A} → ∀p : prop, (∀x : set, x ∈ A → y = F x → p) → p
In Proofgold the corresponding term root is 31e90a... and proposition id is 34fefd...
Axiom. (ReplE') We take the following as an axiom:
∀X, ∀f : set → set, ∀p : set → prop, (∀x ∈ X, p (f x)) → ∀y ∈ {f x|x ∈ X}, p y
In Proofgold the corresponding term root is e374fe... and proposition id is d4b7b0...
Axiom. (Repl_Empty) We take the following as an axiom:
∀F : set → set, {F x|x ∈ Empty} = Empty
In Proofgold the corresponding term root is 2af2ac... and proposition id is 0835bc...
Axiom. (ReplEq_ext_sub) We take the following as an axiom:
∀X, ∀F G : set → set, (∀x ∈ X, F x = G x) → {F x|x ∈ X} ⊆ {G x|x ∈ X}
In Proofgold the corresponding term root is eb4c1d... and proposition id is 56aad0...
Axiom. (ReplEq_ext) We take the following as an axiom:
∀X, ∀F G : set → set, (∀x ∈ X, F x = G x) → {F x|x ∈ X} = {G x|x ∈ X}
In Proofgold the corresponding term root is 81eb90... and proposition id is 781846...
Axiom. (Repl_inv_eq) We take the following as an axiom:
∀P : set → prop, ∀f g : set → set, (∀x, P x → g (f x) = x) → ∀X, (∀x ∈ X, P x) → {g y|y ∈ {f x|x ∈ X}} = X
In Proofgold the corresponding term root is 968c7a... and proposition id is 9ce73d...
Axiom. (Repl_invol_eq) We take the following as an axiom:
∀P : set → prop, ∀f : set → set, (∀x, P x → f (f x) = x) → ∀X, (∀x ∈ X, P x) → {f y|y ∈ {f x|x ∈ X}} = X
In Proofgold the corresponding term root is e15a6b... and proposition id is 5faff0...
Primitive. The name If_i is a term of type prop → set → set → set.
In Proofgold the corresponding term root is b8ff52... and object id is 76c4c0...
Notation. if cond then T else E is notation corresponding to If_i type cond T E where type is the inferred type of T.
Axiom. (If_i_correct) We take the following as an axiom:
∀p : prop, ∀x y : set, p ∧ (if p then x else y) = x ∨ ¬ p ∧ (if p then x else y) = y
In Proofgold the corresponding term root is 2a17ae... and proposition id is b5c26b...
Axiom. (If_i_0) We take the following as an axiom:
∀p : prop, ∀x y : set, ¬ p → (if p then x else y) = y
In Proofgold the corresponding term root is fde1a8... and proposition id is a9abd3...
Axiom. (If_i_1) We take the following as an axiom:
∀p : prop, ∀x y : set, p → (if p then x else y) = x
In Proofgold the corresponding term root is b1aa3f... and proposition id is a93c2c...
Axiom. (If_i_or) We take the following as an axiom:
∀p : prop, ∀x y : set, (if p then x else y) = x ∨ (if p then x else y) = y
In Proofgold the corresponding term root is 3e1439... and proposition id is 4de742...
Primitive. The name UPair is a term of type set → set → set.
In Proofgold the corresponding term root is 742438... and object id is dc3134...
Notation. {x,y} is notation for UPair x y.
Axiom. (UPairE) We take the following as an axiom:
∀x y z : set, x ∈ {y,z} → x = y ∨ x = z
In Proofgold the corresponding term root is 5009cc... and proposition id is e67fc5...
Axiom. (UPairI1) We take the following as an axiom:
∀y z : set, y ∈ {y,z}
In Proofgold the corresponding term root is b1eea2... and proposition id is bf3649...
Axiom. (UPairI2) We take the following as an axiom:
∀y z : set, z ∈ {y,z}
In Proofgold the corresponding term root is 27455b... and proposition id is a0a5b8...
Primitive. The name Sing is a term of type set → set.
In Proofgold the corresponding term root is bd01a8... and object id is b7dfc1...
Notation. {x} is notation for Sing x.
Axiom. (SingI) We take the following as an axiom:
∀x : set, x ∈ {x}
In Proofgold the corresponding term root is 6591bd... and proposition id is 2f93be...
Axiom. (SingE) We take the following as an axiom:
∀x y : set, y ∈ {x} → y = x
In Proofgold the corresponding term root is 9341fe... and proposition id is 3b0dd8...
Primitive. The name binunion is a term of type set → set → set.
In Proofgold the corresponding term root is 5e1ac4... and object id is e14989...
Notation. We use ∪ as an infix operator with priority 345 and which associates to the left corresponding to applying term binunion.
Axiom. (binunionI1) We take the following as an axiom:
∀X Y z : set, z ∈ X → z ∈ X ∪ Y
In Proofgold the corresponding term root is 753b6e... and proposition id is e43c8d...
Axiom. (binunionI2) We take the following as an axiom:
∀X Y z : set, z ∈ Y → z ∈ X ∪ Y
In Proofgold the corresponding term root is b8821c... and proposition id is 959535...
Axiom. (binunionE) We take the following as an axiom:
∀X Y z : set, z ∈ X ∪ Y → z ∈ X ∨ z ∈ Y
In Proofgold the corresponding term root is 5a3195... and proposition id is 1ceeb0...
Axiom. (binunionE') We take the following as an axiom:
∀X Y z, ∀p : prop, (z ∈ X → p) → (z ∈ Y → p) → (z ∈ X ∪ Y → p)
In Proofgold the corresponding term root is e5b951... and proposition id is 570dd1...
Axiom. (binunion_asso) We take the following as an axiom:
∀X Y Z : set, X ∪ (Y ∪ Z) = (X ∪ Y) ∪ Z
In Proofgold the corresponding term root is e0f701... and proposition id is 61dfba...
Axiom. (binunion_com_Subq) We take the following as an axiom:
∀X Y : set, X ∪ Y ⊆ Y ∪ X
In Proofgold the corresponding term root is ee8f5a... and proposition id is d84076...
Axiom. (binunion_com) We take the following as an axiom:
∀X Y : set, X ∪ Y = Y ∪ X
In Proofgold the corresponding term root is e20f4f... and proposition id is bed33e...
Axiom. (binunion_idl) We take the following as an axiom:
∀X : set, Empty ∪ X = X
In Proofgold the corresponding term root is 8dc616... and proposition id is 52cd24...
Axiom. (binunion_idr) We take the following as an axiom:
∀X : set, X ∪ Empty = X
In Proofgold the corresponding term root is 67e82f... and proposition id is d5a005...
Axiom. (binunion_Subq_1) We take the following as an axiom:
∀X Y : set, X ⊆ X ∪ Y
In Proofgold the corresponding term root is b2c658... and proposition id is a9b3a8...
Axiom. (binunion_Subq_2) We take the following as an axiom:
∀X Y : set, Y ⊆ X ∪ Y
In Proofgold the corresponding term root is 3cf229... and proposition id is 1507ce...
Axiom. (binunion_Subq_min) We take the following as an axiom:
∀X Y Z : set, X ⊆ Z → Y ⊆ Z → X ∪ Y ⊆ Z
In Proofgold the corresponding term root is cc32a5... and proposition id is d64da4...
Axiom. (Subq_binunion_eq) We take the following as an axiom:
∀X Y, (X ⊆ Y) = (X ∪ Y = Y)
In Proofgold the corresponding term root is f8ee53... and proposition id is c2d393...
Definition. We define SetAdjoin to be λX y ⇒ X ∪ {y} of type set → set → set.
In Proofgold the corresponding term root is 1f3a09... and object id is 5bdda8...
Notation. We now use the set enumeration notation {...,...,...} in general. If 0 elements are given, then Empty is used to form the corresponding term. If 1 element is given, then Sing is used to form the corresponding term. If 2 elements are given, then UPair is used to form the corresponding term. If more than elements are given, then SetAdjoin is used to reduce to the case with one fewer elements.
Primitive. The name famunion is a term of type set → (set → set) → set.
In Proofgold the corresponding term root is b3e3bf... and object id is 241349...
Notation. We use ⋃ x [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using famunion.
Axiom. (famunionI) We take the following as an axiom:
∀X : set, ∀F : (set → set), ∀x y : set, x ∈ X → y ∈ F x → y ∈ ⋃x ∈ XF x
In Proofgold the corresponding term root is 0c23d0... and proposition id is e4f490...
Axiom. (famunionE) We take the following as an axiom:
∀X : set, ∀F : (set → set), ∀y : set, y ∈ (⋃x ∈ XF x) → ∃x ∈ X, y ∈ F x
In Proofgold the corresponding term root is 48683a... and proposition id is ede6e5...
Axiom. (famunionE_impred) We take the following as an axiom:
∀X : set, ∀F : (set → set), ∀y : set, y ∈ (⋃x ∈ XF x) → ∀p : prop, (∀x, x ∈ X → y ∈ F x → p) → p
In Proofgold the corresponding term root is ab2266... and proposition id is 562023...
Axiom. (famunion_Empty) We take the following as an axiom:
∀F : set → set, (⋃x ∈ EmptyF x) = Empty
In Proofgold the corresponding term root is fc1bdd... and proposition id is 22bd10...
Beginning of Section SepSec
Variable X : set
Variable P : set → prop
Let z : set ≝ Eps_i (λz ⇒ z ∈ X ∧ P z)
Let F : set → set ≝ λx ⇒ if P x then x else z
Primitive. The name Sep is a term of type set.
In Proofgold the corresponding term root is f336a4... and object id is 7008ec...
End of Section SepSec
Notation. {x ∈ A | B} is notation for Sep A (λ x . B).
Axiom. (SepI) We take the following as an axiom:
∀X : set, ∀P : (set → prop), ∀x : set, x ∈ X → P x → x ∈ {x ∈ X|P x}
In Proofgold the corresponding term root is ea56bb... and proposition id is 147a6a...
Axiom. (SepE) We take the following as an axiom:
∀X : set, ∀P : (set → prop), ∀x : set, x ∈ {x ∈ X|P x} → x ∈ X ∧ P x
In Proofgold the corresponding term root is 102830... and proposition id is 00899a...
Axiom. (SepE1) We take the following as an axiom:
∀X : set, ∀P : (set → prop), ∀x : set, x ∈ {x ∈ X|P x} → x ∈ X
In Proofgold the corresponding term root is d83445... and proposition id is 6399b0...
Axiom. (SepE2) We take the following as an axiom:
∀X : set, ∀P : (set → prop), ∀x : set, x ∈ {x ∈ X|P x} → P x
In Proofgold the corresponding term root is aa61ca... and proposition id is 104227...
Axiom. (Sep_Subq) We take the following as an axiom:
∀X : set, ∀P : set → prop, {x ∈ X|P x} ⊆ X
In Proofgold the corresponding term root is 97d080... and proposition id is c17d45...
Axiom. (Sep_In_Power) We take the following as an axiom:
∀X : set, ∀P : set → prop, {x ∈ X|P x} ∈ 𝒫 X
In Proofgold the corresponding term root is 612c94... and proposition id is fba53e...
Primitive. The name ReplSep is a term of type set → (set → prop) → (set → set) → set.
In Proofgold the corresponding term root is ec807b... and object id is 9bdb56...
Notation. {B| x ∈ A, C} is notation for ReplSep A (λ x . C) (λ x . B).
Axiom. (ReplSepI) We take the following as an axiom:
∀X : set, ∀P : set → prop, ∀F : set → set, ∀x : set, x ∈ X → P x → F x ∈ {F x|x ∈ X, P x}
In Proofgold the corresponding term root is 35b8ec... and proposition id is aa7b2b...
Axiom. (ReplSepE) We take the following as an axiom:
∀X : set, ∀P : set → prop, ∀F : set → set, ∀y : set, y ∈ {F x|x ∈ X, P x} → ∃x : set, x ∈ X ∧ P x ∧ y = F x
In Proofgold the corresponding term root is 415ff1... and proposition id is b1bc76...
Axiom. (ReplSepE_impred) We take the following as an axiom:
∀X : set, ∀P : set → prop, ∀F : set → set, ∀y : set, y ∈ {F x|x ∈ X, P x} → ∀p : prop, (∀x ∈ X, P x → y = F x → p) → p
In Proofgold the corresponding term root is 5d26e1... and proposition id is 063cea...
Primitive. The name binintersect is a term of type set → set → set.
In Proofgold the corresponding term root is b2abd2... and object id is 2c68d8...
Notation. We use ∩ as an infix operator with priority 340 and which associates to the left corresponding to applying term binintersect.
Axiom. (binintersectI) We take the following as an axiom:
∀X Y z, z ∈ X → z ∈ Y → z ∈ X ∩ Y
In Proofgold the corresponding term root is fd656d... and proposition id is 9081a0...
Axiom. (binintersectE) We take the following as an axiom:
∀X Y z, z ∈ X ∩ Y → z ∈ X ∧ z ∈ Y
In Proofgold the corresponding term root is 463b5a... and proposition id is ca0636...
Axiom. (binintersectE1) We take the following as an axiom:
∀X Y z, z ∈ X ∩ Y → z ∈ X
In Proofgold the corresponding term root is b12123... and proposition id is 51005e...
Axiom. (binintersectE2) We take the following as an axiom:
∀X Y z, z ∈ X ∩ Y → z ∈ Y
In Proofgold the corresponding term root is 39656f... and proposition id is 599de4...
Axiom. (binintersect_Subq_1) We take the following as an axiom:
∀X Y : set, X ∩ Y ⊆ X
In Proofgold the corresponding term root is f296ad... and proposition id is 303833...
Axiom. (binintersect_Subq_2) We take the following as an axiom:
∀X Y : set, X ∩ Y ⊆ Y
In Proofgold the corresponding term root is fcd5f5... and proposition id is 8b9fd2...
Axiom. (binintersect_Subq_eq_1) We take the following as an axiom:
∀X Y, X ⊆ Y → X ∩ Y = X
In Proofgold the corresponding term root is 277eec... and proposition id is ec1cc3...
Axiom. (binintersect_Subq_max) We take the following as an axiom:
∀X Y Z : set, Z ⊆ X → Z ⊆ Y → Z ⊆ X ∩ Y
In Proofgold the corresponding term root is 95624d... and proposition id is 64636b...
Axiom. (binintersect_com_Subq) We take the following as an axiom:
∀X Y : set, X ∩ Y ⊆ Y ∩ X
In Proofgold the corresponding term root is 410255... and proposition id is 5977b8...
Axiom. (binintersect_com) We take the following as an axiom:
∀X Y : set, X ∩ Y = Y ∩ X
In Proofgold the corresponding term root is 1a2c6f... and proposition id is ea8a1c...
Primitive. The name setminus is a term of type set → set → set.
In Proofgold the corresponding term root is c68e5a... and object id is 913da1...
Notation. We use ∖ as an infix operator with priority 350 and no associativity corresponding to applying term setminus.
Axiom. (setminusI) We take the following as an axiom:
∀X Y z, (z ∈ X) → (z ∉ Y) → z ∈ X ∖ Y
In Proofgold the corresponding term root is 0feeb8... and proposition id is 80db6a...
Axiom. (setminusE) We take the following as an axiom:
∀X Y z, (z ∈ X ∖ Y) → z ∈ X ∧ z ∉ Y
In Proofgold the corresponding term root is 6774f4... and proposition id is 71763a...
Axiom. (setminusE1) We take the following as an axiom:
∀X Y z, (z ∈ X ∖ Y) → z ∈ X
In Proofgold the corresponding term root is 064bd5... and proposition id is d74baf...
Axiom. (setminus_Subq) We take the following as an axiom:
∀X Y : set, X ∖ Y ⊆ X
In Proofgold the corresponding term root is 5a497a... and proposition id is 66f982...
Axiom. (setminus_Subq_contra) We take the following as an axiom:
∀X Y Z : set, Z ⊆ Y → X ∖ Y ⊆ X ∖ Z
In Proofgold the corresponding term root is b1f440... and proposition id is 9a06b2...
Axiom. (setminus_In_Power) We take the following as an axiom:
∀A U, A ∖ U ∈ 𝒫 A
In Proofgold the corresponding term root is 062275... and proposition id is f503e1...
Axiom. (In_irref) We take the following as an axiom:
∀x, x ∉ x
In Proofgold the corresponding term root is 12629a... and proposition id is 7bfd46...
Axiom. (In_no2cycle) We take the following as an axiom:
∀x y, x ∈ y → y ∈ x → False
In Proofgold the corresponding term root is 6d0cb3... and proposition id is 344f30...
Primitive. The name ordsucc is a term of type set → set.
In Proofgold the corresponding term root is 65d883... and object id is 1452f7...
Axiom. (ordsuccI1) We take the following as an axiom:
∀x : set, x ⊆ ordsucc x
In Proofgold the corresponding term root is 5a2f15... and proposition id is 367d80...
Axiom. (ordsuccI2) We take the following as an axiom:
∀x : set, x ∈ ordsucc x
In Proofgold the corresponding term root is 2f6efd... and proposition id is 2be6be...
Axiom. (ordsuccE) We take the following as an axiom:
∀x y : set, y ∈ ordsucc x → y ∈ x ∨ y = x
In Proofgold the corresponding term root is 01c4ee... and proposition id is 3849f5...
Notation. Natural numbers 0,1,2,... are notation for the terms formed using Empty as 0 and forming successors with ordsucc.
Axiom. (neq_0_ordsucc) We take the following as an axiom:
∀a : set, 0 ≠ ordsucc a
In Proofgold the corresponding term root is 1b20cb... and proposition id is 04c410...
Axiom. (neq_ordsucc_0) We take the following as an axiom:
∀a : set, ordsucc a ≠ 0
In Proofgold the corresponding term root is 9b391e... and proposition id is 346ee0...
Axiom. (ordsucc_inj) We take the following as an axiom:
∀a b : set, ordsucc a = ordsucc b → a = b
In Proofgold the corresponding term root is 40cad6... and proposition id is 4869a1...
Axiom. (ordsucc_inj_contra) We take the following as an axiom:
∀a b : set, a ≠ b → ordsucc a ≠ ordsucc b
In Proofgold the corresponding term root is 791304... and proposition id is 66f4df...
Axiom. (In_0_1) We take the following as an axiom:
0 ∈ 1
In Proofgold the corresponding term root is e984b0... and proposition id is 3be80a...
Axiom. (In_0_2) We take the following as an axiom:
0 ∈ 2
In Proofgold the corresponding term root is 56dc2c... and proposition id is 5a202e...
Axiom. (In_1_2) We take the following as an axiom:
1 ∈ 2
In Proofgold the corresponding term root is 8704b3... and proposition id is 431e9e...
Definition. We define nat_p to be λn : set ⇒ ∀p : set → prop, p 0 → (∀x : set, p x → p (ordsucc x)) → p n of type set → prop.
In Proofgold the corresponding term root is 458be3... and object id is cfd8eb...
Axiom. (nat_0) We take the following as an axiom:
nat_p 0
In Proofgold the corresponding term root is 1617bc... and proposition id is 457a72...
Axiom. (nat_ordsucc) We take the following as an axiom:
∀n : set, nat_p n → nat_p (ordsucc n)
In Proofgold the corresponding term root is 87f001... and proposition id is 57e940...
Axiom. (nat_1) We take the following as an axiom:
nat_p 1
In Proofgold the corresponding term root is 2f83fa... and proposition id is 672d0d...
Axiom. (nat_2) We take the following as an axiom:
nat_p 2
In Proofgold the corresponding term root is a8be15... and proposition id is 9112e9...
Axiom. (nat_0_in_ordsucc) We take the following as an axiom:
∀n, nat_p n → 0 ∈ ordsucc n
In Proofgold the corresponding term root is 9b50b9... and proposition id is 251f3d...
Axiom. (nat_ordsucc_in_ordsucc) We take the following as an axiom:
∀n, nat_p n → ∀m ∈ n, ordsucc m ∈ ordsucc n
In Proofgold the corresponding term root is 819399... and proposition id is 4c2c95...
Axiom. (nat_ind) We take the following as an axiom:
∀p : set → prop, p 0 → (∀n, nat_p n → p n → p (ordsucc n)) → ∀n, nat_p n → p n
In Proofgold the corresponding term root is 5d06f5... and proposition id is ecdce8...
Axiom. (nat_inv_impred) We take the following as an axiom:
∀p : set → prop, p 0 → (∀n, nat_p n → p (ordsucc n)) → ∀n, nat_p n → p n
In Proofgold the corresponding term root is eddc5f... and proposition id is 175e22...
Axiom. (nat_inv) We take the following as an axiom:
∀n, nat_p n → n = 0 ∨ ∃x, nat_p x ∧ n = ordsucc x
In Proofgold the corresponding term root is 5d4296... and proposition id is 4f4167...
Axiom. (nat_complete_ind) We take the following as an axiom:
∀p : set → prop, (∀n, nat_p n → (∀m ∈ n, p m) → p n) → ∀n, nat_p n → p n
In Proofgold the corresponding term root is d32e5b... and proposition id is 1e1608...
Axiom. (nat_p_trans) We take the following as an axiom:
∀n, nat_p n → ∀m ∈ n, nat_p m
In Proofgold the corresponding term root is e88449... and proposition id is 03b874...
Axiom. (nat_trans) We take the following as an axiom:
∀n, nat_p n → ∀m ∈ n, m ⊆ n
In Proofgold the corresponding term root is 6bc6e1... and proposition id is cad6fe...
Axiom. (nat_ordsucc_trans) We take the following as an axiom:
∀n, nat_p n → ∀m ∈ ordsucc n, m ⊆ n
In Proofgold the corresponding term root is e42e58... and proposition id is bc868d...
Axiom. (Union_ordsucc_eq) We take the following as an axiom:
∀n, nat_p n → ⋃ (ordsucc n) = n
In Proofgold the corresponding term root is 87308c... and proposition id is e8cdeb...
Axiom. (cases_1) We take the following as an axiom:
∀i ∈ 1, ∀p : set → prop, p 0 → p i
In Proofgold the corresponding term root is 706605... and proposition id is c6f0c0...
Axiom. (cases_2) We take the following as an axiom:
∀i ∈ 2, ∀p : set → prop, p 0 → p 1 → p i
In Proofgold the corresponding term root is 4693b2... and proposition id is 74563a...
Axiom. (cases_3) We take the following as an axiom:
∀i ∈ 3, ∀p : set → prop, p 0 → p 1 → p 2 → p i
In Proofgold the corresponding term root is 2a0ca2... and proposition id is 1a8a20...
Axiom. (neq_0_1) We take the following as an axiom:
0 ≠ 1
In Proofgold the corresponding term root is 9630fd... and proposition id is 74867a...
Axiom. (neq_1_0) We take the following as an axiom:
1 ≠ 0
In Proofgold the corresponding term root is 3a0478... and proposition id is 952fed...
Axiom. (neq_0_2) We take the following as an axiom:
0 ≠ 2
In Proofgold the corresponding term root is 055580... and proposition id is 9c9a3f...
Axiom. (neq_2_0) We take the following as an axiom:
2 ≠ 0
In Proofgold the corresponding term root is 4d54d8... and proposition id is 00b357...
Axiom. (neq_1_2) We take the following as an axiom:
1 ≠ 2
In Proofgold the corresponding term root is 1d088a... and proposition id is e5542e...
Axiom. (ZF_closed_E) We take the following as an axiom:
∀U, ZF_closed U → ∀p : prop, (Union_closed U → Power_closed U → Repl_closed U → p) → p
In Proofgold the corresponding term root is d795d4... and proposition id is c78c79...
Axiom. (ZF_Union_closed) We take the following as an axiom:
∀U, ZF_closed U → ∀X ∈ U, ⋃ X ∈ U
In Proofgold the corresponding term root is a7cdf1... and proposition id is 250496...
Axiom. (ZF_Power_closed) We take the following as an axiom:
∀U, ZF_closed U → ∀X ∈ U, 𝒫 X ∈ U
In Proofgold the corresponding term root is 5d781f... and proposition id is 7411dd...
Axiom. (ZF_Repl_closed) We take the following as an axiom:
∀U, ZF_closed U → ∀X ∈ U, ∀F : set → set, (∀x ∈ X, F x ∈ U) → {F x|x ∈ X} ∈ U
In Proofgold the corresponding term root is 312268... and proposition id is 18f8ac...
Axiom. (ZF_UPair_closed) We take the following as an axiom:
∀U, ZF_closed U → ∀x y ∈ U, {x,y} ∈ U
In Proofgold the corresponding term root is 54256a... and proposition id is ef42d3...
Axiom. (ZF_Sing_closed) We take the following as an axiom:
∀U, ZF_closed U → ∀x ∈ U, {x} ∈ U
In Proofgold the corresponding term root is 5d8a83... and proposition id is d02d66...
Axiom. (ZF_binunion_closed) We take the following as an axiom:
∀U, ZF_closed U → ∀X Y ∈ U, (X ∪ Y) ∈ U
In Proofgold the corresponding term root is 8a6240... and proposition id is 1bacfd...
Axiom. (ZF_ordsucc_closed) We take the following as an axiom:
∀U, ZF_closed U → ∀x ∈ U, ordsucc x ∈ U
In Proofgold the corresponding term root is 68a6ba... and proposition id is 946e61...
Axiom. (nat_p_UnivOf_Empty) We take the following as an axiom:
∀n : set, nat_p n → n ∈ UnivOf Empty
In Proofgold the corresponding term root is c885b4... and proposition id is 645aee...
Primitive. The name ω is a term of type set.
In Proofgold the corresponding term root is 6fc30a... and object id is ad9ad8...
Axiom. (omega_nat_p) We take the following as an axiom:
∀n ∈ ω, nat_p n
In Proofgold the corresponding term root is f44a30... and proposition id is c2c61b...
Axiom. (nat_p_omega) We take the following as an axiom:
∀n : set, nat_p n → n ∈ ω
In Proofgold the corresponding term root is 6a1b44... and proposition id is d5080f...
Axiom. (omega_ordsucc) We take the following as an axiom:
∀n ∈ ω, ordsucc n ∈ ω
In Proofgold the corresponding term root is 246d63... and proposition id is 17fb64...
Definition. We define ordinal to be λalpha : set ⇒ TransSet alpha ∧ ∀beta ∈ alpha, TransSet beta of type set → prop.
In Proofgold the corresponding term root is ee28d9... and object id is 53ee8f...
Axiom. (ordinal_TransSet) We take the following as an axiom:
∀alpha : set, ordinal alpha → TransSet alpha
In Proofgold the corresponding term root is 0dbaa3... and proposition id is c9e708...
Axiom. (ordinal_Empty) We take the following as an axiom:
ordinal Empty
In Proofgold the corresponding term root is ce6bea... and proposition id is 7d95d1...
Axiom. (ordinal_Hered) We take the following as an axiom:
∀alpha : set, ordinal alpha → ∀beta ∈ alpha, ordinal beta
In Proofgold the corresponding term root is a7e78b... and proposition id is 43b0f3...
Axiom. (TransSet_ordsucc) We take the following as an axiom:
∀X : set, TransSet X → TransSet (ordsucc X)
In Proofgold the corresponding term root is fc2157... and proposition id is ebf9e3...
Axiom. (ordinal_ordsucc) We take the following as an axiom:
∀alpha : set, ordinal alpha → ordinal (ordsucc alpha)
In Proofgold the corresponding term root is 0ba97f... and proposition id is ab0f7f...
Axiom. (nat_p_ordinal) We take the following as an axiom:
∀n : set, nat_p n → ordinal n
In Proofgold the corresponding term root is 274fc4... and proposition id is 47cd49...
Axiom. (ordinal_1) We take the following as an axiom:
ordinal 1
In Proofgold the corresponding term root is c94d41... and proposition id is e325a5...
Axiom. (ordinal_2) We take the following as an axiom:
ordinal 2
In Proofgold the corresponding term root is a57075... and proposition id is e64a0d...
Axiom. (omega_TransSet) We take the following as an axiom:
TransSet ω
In Proofgold the corresponding term root is 8e89e6... and proposition id is c79e75...
Axiom. (omega_ordinal) We take the following as an axiom:
ordinal ω
In Proofgold the corresponding term root is 3d621a... and proposition id is 177484...
Axiom. (ordsucc_omega_ordinal) We take the following as an axiom:
ordinal (ordsucc ω)
In Proofgold the corresponding term root is 66659c... and proposition id is ecfad7...
Axiom. (TransSet_ordsucc_In_Subq) We take the following as an axiom:
∀X : set, TransSet X → ∀x ∈ X, ordsucc x ⊆ X
In Proofgold the corresponding term root is d5d882... and proposition id is 3c2e45...
Axiom. (ordinal_ordsucc_In_Subq) We take the following as an axiom:
∀alpha, ordinal alpha → ∀beta ∈ alpha, ordsucc beta ⊆ alpha
In Proofgold the corresponding term root is 57345e... and proposition id is b00304...
Axiom. (ordinal_trichotomy_or) We take the following as an axiom:
∀alpha beta : set, ordinal alpha → ordinal beta → alpha ∈ beta ∨ alpha = beta ∨ beta ∈ alpha
In Proofgold the corresponding term root is 078a34... and proposition id is 21f2d6...
Axiom. (ordinal_trichotomy_or_impred) We take the following as an axiom:
∀alpha beta : set, ordinal alpha → ordinal beta → ∀p : prop, (alpha ∈ beta → p) → (alpha = beta → p) → (beta ∈ alpha → p) → p
In Proofgold the corresponding term root is 7c0f0b... and proposition id is bb6d2d...
Axiom. (ordinal_In_Or_Subq) We take the following as an axiom:
∀alpha beta, ordinal alpha → ordinal beta → alpha ∈ beta ∨ beta ⊆ alpha
In Proofgold the corresponding term root is 70fe0d... and proposition id is 7b99b0...
Axiom. (ordinal_linear) We take the following as an axiom:
∀alpha beta, ordinal alpha → ordinal beta → alpha ⊆ beta ∨ beta ⊆ alpha
In Proofgold the corresponding term root is 3f30a5... and proposition id is 3b1fce...
Axiom. (ordinal_ordsucc_In_eq) We take the following as an axiom:
∀alpha beta, ordinal alpha → beta ∈ alpha → ordsucc beta ∈ alpha ∨ alpha = ordsucc beta
In Proofgold the corresponding term root is 500378... and proposition id is 0c19e7...
Axiom. (ordinal_lim_or_succ) We take the following as an axiom:
∀alpha, ordinal alpha → (∀beta ∈ alpha, ordsucc beta ∈ alpha) ∨ (∃beta ∈ alpha, alpha = ordsucc beta)
In Proofgold the corresponding term root is 4450c0... and proposition id is a12697...
Axiom. (ordinal_ordsucc_In) We take the following as an axiom:
∀alpha, ordinal alpha → ∀beta ∈ alpha, ordsucc beta ∈ ordsucc alpha
In Proofgold the corresponding term root is f4b1ed... and proposition id is 8ab1dc...
Axiom. (ordinal_famunion) We take the following as an axiom:
∀X, ∀F : set → set, (∀x ∈ X, ordinal (F x)) → ordinal (⋃x ∈ XF x)
In Proofgold the corresponding term root is fc0359... and proposition id is b3f1e1...
Axiom. (ordinal_binintersect) We take the following as an axiom:
∀alpha beta, ordinal alpha → ordinal beta → ordinal (alpha ∩ beta)
In Proofgold the corresponding term root is 43d507... and proposition id is 025328...
Axiom. (ordinal_binunion) We take the following as an axiom:
∀alpha beta, ordinal alpha → ordinal beta → ordinal (alpha ∪ beta)
In Proofgold the corresponding term root is 861ae3... and proposition id is b24989...
Axiom. (ordinal_ind) We take the following as an axiom:
∀p : set → prop, (∀alpha, ordinal alpha → (∀beta ∈ alpha, p beta) → p alpha) → ∀alpha, ordinal alpha → p alpha
In Proofgold the corresponding term root is bb5575... and proposition id is 973cd8...
Axiom. (least_ordinal_ex) We take the following as an axiom:
∀p : set → prop, (∃alpha, ordinal alpha ∧ p alpha) → ∃alpha, ordinal alpha ∧ p alpha ∧ ∀beta ∈ alpha, ¬ p beta
In Proofgold the corresponding term root is df6c77... and proposition id is ab6fe1...
Definition. We define inj to be λX Y f ⇒ (∀u ∈ X, f u ∈ Y) ∧ (∀u v ∈ X, f u = f v → u = v) of type set → set → (set → set) → prop.
In Proofgold the corresponding term root is 264b04... and object id is 442958...
Definition. We define bij to be λX Y f ⇒ (∀u ∈ X, f u ∈ Y) ∧ (∀u v ∈ X, f u = f v → u = v) ∧ (∀w ∈ Y, ∃u ∈ X, f u = w) of type set → set → (set → set) → prop.
In Proofgold the corresponding term root is 76bef6... and object id is f7d93b...
Axiom. (bijI) We take the following as an axiom:
∀X Y, ∀f : set → set, (∀u ∈ X, f u ∈ Y) → (∀u v ∈ X, f u = f v → u = v) → (∀w ∈ Y, ∃u ∈ X, f u = w) → bij X Y f
In Proofgold the corresponding term root is a9064f... and proposition id is 3229f9...
Axiom. (bijE) We take the following as an axiom:
∀X Y, ∀f : set → set, bij X Y f → ∀p : prop, ((∀u ∈ X, f u ∈ Y) → (∀u v ∈ X, f u = f v → u = v) → (∀w ∈ Y, ∃u ∈ X, f u = w) → p) → p
In Proofgold the corresponding term root is 2cf278... and proposition id is cf0759...
Primitive. The name inv is a term of type set → (set → set) → set → set.
In Proofgold the corresponding term root is 896fa9... and object id is f3a015...
Axiom. (surj_rinv) We take the following as an axiom:
∀X Y, ∀f : set → set, (∀w ∈ Y, ∃u ∈ X, f u = w) → ∀y ∈ Y, inv X f y ∈ X ∧ f (inv X f y) = y
In Proofgold the corresponding term root is ebf371... and proposition id is 6489d2...
Axiom. (inj_linv) We take the following as an axiom:
∀X, ∀f : set → set, (∀u v ∈ X, f u = f v → u = v) → ∀x ∈ X, inv X f (f x) = x
In Proofgold the corresponding term root is 18ecce... and proposition id is d16557...
Axiom. (bij_inv) We take the following as an axiom:
∀X Y, ∀f : set → set, bij X Y f → bij Y X (inv X f)
In Proofgold the corresponding term root is ff1332... and proposition id is 69c537...
Axiom. (bij_id) We take the following as an axiom:
∀X, bij X X (λx ⇒ x)
In Proofgold the corresponding term root is a8cefb... and proposition id is 707f37...
Axiom. (bij_comp) We take the following as an axiom:
∀X Y Z : set, ∀f g : set → set, bij X Y f → bij Y Z g → bij X Z (λx ⇒ g (f x))
In Proofgold the corresponding term root is abf851... and proposition id is 4c9045...
Definition. We define equip to be λX Y : set ⇒ ∃f : set → set, bij X Y f of type set → set → prop.
In Proofgold the corresponding term root is eb4419... and object id is 7f2bf6...
Axiom. (equip_ref) We take the following as an axiom:
∀X, equip X X
In Proofgold the corresponding term root is cc7e80... and proposition id is c41fb1...
Axiom. (equip_sym) We take the following as an axiom:
∀X Y, equip X Y → equip Y X
In Proofgold the corresponding term root is f28954... and proposition id is 272f04...
Axiom. (equip_tra) We take the following as an axiom:
∀X Y Z, equip X Y → equip Y Z → equip X Z
In Proofgold the corresponding term root is 322bfb... and proposition id is d616c1...
Axiom. (equip_0_Empty) We take the following as an axiom:
∀X, equip X 0 → X = 0
In Proofgold the corresponding term root is 83ab2f... and proposition id is 4c101c...
Beginning of Section SchroederBernstein
Axiom. (KnasterTarski_set) We take the following as an axiom:
∀A, ∀F : set → set, (∀U ∈ 𝒫 A, F U ∈ 𝒫 A) → (∀U V ∈ 𝒫 A, U ⊆ V → F U ⊆ F V) → ∃Y ∈ 𝒫 A, F Y = Y
In Proofgold the corresponding term root is 2ffb9f... and proposition id is 31ef9d...
Axiom. (image_In_Power) We take the following as an axiom:
∀A B, ∀f : set → set, (∀x ∈ A, f x ∈ B) → ∀U ∈ 𝒫 A, {f x|x ∈ U} ∈ 𝒫 B
In Proofgold the corresponding term root is 6799e8... and proposition id is 43ed06...
Axiom. (image_monotone) We take the following as an axiom:
∀f : set → set, ∀U V, U ⊆ V → {f x|x ∈ U} ⊆ {f x|x ∈ V}
In Proofgold the corresponding term root is ac6fe8... and proposition id is f923c6...
Axiom. (setminus_antimonotone) We take the following as an axiom:
∀A U V, U ⊆ V → A ∖ V ⊆ A ∖ U
In Proofgold the corresponding term root is 67bd0e... and proposition id is f9b735...
Axiom. (SchroederBernstein) We take the following as an axiom:
∀A B, ∀f g : set → set, inj A B f → inj B A g → equip A B
In Proofgold the corresponding term root is e247a8... and proposition id is 03a2cd...
End of Section SchroederBernstein
Beginning of Section PigeonHole
Axiom. (PigeonHole_nat) We take the following as an axiom:
∀n, nat_p n → ∀f : set → set, (∀i ∈ ordsucc n, f i ∈ n) → ¬ (∀i j ∈ ordsucc n, f i = f j → i = j)
In Proofgold the corresponding term root is d756b7... and proposition id is 604a84...
Axiom. (PigeonHole_nat_bij) We take the following as an axiom:
∀n, nat_p n → ∀f : set → set, (∀i ∈ n, f i ∈ n) → (∀i j ∈ n, f i = f j → i = j) → bij n n f
In Proofgold the corresponding term root is cd3b8d... and proposition id is 44a08f...
End of Section PigeonHole
Definition. We define finite to be λX ⇒ ∃n ∈ ω, equip X n of type set → prop.
In Proofgold the corresponding term root is 04632d... and object id is 4c54a5...
Axiom. (finite_ind) We take the following as an axiom:
∀p : set → prop, p Empty → (∀X y, finite X → y ∉ X → p X → p (X ∪ {y})) → ∀X, finite X → p X
In Proofgold the corresponding term root is c53cb1... and proposition id is 19baca...
Axiom. (finite_Empty) We take the following as an axiom:
finite 0
In Proofgold the corresponding term root is c073c6... and proposition id is ec2c27...
Axiom. (adjoin_finite) We take the following as an axiom:
∀X y, finite X → finite (X ∪ {y})
In Proofgold the corresponding term root is def317... and proposition id is e6aa6d...
Axiom. (binunion_finite) We take the following as an axiom:
∀X, finite X → ∀Y, finite Y → finite (X ∪ Y)
In Proofgold the corresponding term root is fc26bb... and proposition id is 3365a6...
Axiom. (famunion_nat_finite) We take the following as an axiom:
∀X : set → set, ∀n, nat_p n → (∀i ∈ n, finite (X i)) → finite (⋃i ∈ nX i)
In Proofgold the corresponding term root is 7f709a... and proposition id is f84ed0...
Axiom. (Subq_finite) We take the following as an axiom:
∀X, finite X → ∀Y, Y ⊆ X → finite Y
In Proofgold the corresponding term root is 6b062c... and proposition id is e4e3ee...
Axiom. (TransSet_In_ordsucc_Subq) We take the following as an axiom:
∀x y, TransSet y → x ∈ ordsucc y → x ⊆ y
In Proofgold the corresponding term root is f80c6e... and proposition id is 341993...
Axiom. (exandE_i) We take the following as an axiom:
∀P Q : set → prop, (∃x, P x ∧ Q x) → ∀r : prop, (∀x, P x → Q x → r) → r
In Proofgold the corresponding term root is 083f82... and proposition id is b1b26e...
Axiom. (exandE_ii) We take the following as an axiom:
∀P Q : (set → set) → prop, (∃x : set → set, P x ∧ Q x) → ∀p : prop, (∀x : set → set, P x → Q x → p) → p
In Proofgold the corresponding term root is c3e995... and proposition id is ed9d65...
Axiom. (exandE_iii) We take the following as an axiom:
∀P Q : (set → set → set) → prop, (∃x : set → set → set, P x ∧ Q x) → ∀p : prop, (∀x : set → set → set, P x → Q x → p) → p
In Proofgold the corresponding term root is 028a8f... and proposition id is 80b3b0...
Axiom. (exandE_iiii) We take the following as an axiom:
∀P Q : (set → set → set → set) → prop, (∃x : set → set → set → set, P x ∧ Q x) → ∀p : prop, (∀x : set → set → set → set, P x → Q x → p) → p
In Proofgold the corresponding term root is 7807d4... and proposition id is d1536a...
Beginning of Section Descr_ii
Variable P : (set → set) → prop
Primitive. The name Descr_ii is a term of type set → set.
In Proofgold the corresponding term root is 3bae39... and object id is 3a4ad2...
Hypothesis Pex : ∃f : set → set, P f
Hypothesis Puniq : ∀f g : set → set, P f → P g → f = g
Axiom. (Descr_ii_prop) We take the following as an axiom:
P Descr_ii
In Proofgold the corresponding term root is 45bfc0... and proposition id is e705d1...
End of Section Descr_ii
Beginning of Section Descr_iii
Variable P : (set → set → set) → prop
Primitive. The name Descr_iii is a term of type set → set → set.
In Proofgold the corresponding term root is ca5fc1... and object id is 877e40...
Hypothesis Pex : ∃f : set → set → set, P f
Hypothesis Puniq : ∀f g : set → set → set, P f → P g → f = g
Axiom. (Descr_iii_prop) We take the following as an axiom:
P Descr_iii
In Proofgold the corresponding term root is 261c3d... and proposition id is 160421...
End of Section Descr_iii
Beginning of Section Descr_Vo1
Variable P : Vo 1 → prop
Primitive. The name Descr_Vo1 is a term of type Vo 1.
In Proofgold the corresponding term root is 615c0a... and object id is a4ecdd...
Hypothesis Pex : ∃f : Vo 1, P f
Hypothesis Puniq : ∀f g : Vo 1, P f → P g → f = g
Axiom. (Descr_Vo1_prop) We take the following as an axiom:
P Descr_Vo1
In Proofgold the corresponding term root is f550ef... and proposition id is 2213e2...
End of Section Descr_Vo1
Beginning of Section If_ii
Variable p : prop
Variable f g : set → set
Primitive. The name If_ii is a term of type set → set.
In Proofgold the corresponding term root is 17057f... and object id is e29015...
Axiom. (If_ii_1) We take the following as an axiom:
p → If_ii = f
In Proofgold the corresponding term root is 31521e... and proposition id is 342a1f...
Axiom. (If_ii_0) We take the following as an axiom:
¬ p → If_ii = g
In Proofgold the corresponding term root is 6acab0... and proposition id is 36418b...
End of Section If_ii
Beginning of Section If_iii
Variable p : prop
Variable f g : set → set → set
Primitive. The name If_iii is a term of type set → set → set.
In Proofgold the corresponding term root is 331476... and object id is dd7e2b...
Axiom. (If_iii_1) We take the following as an axiom:
p → If_iii = f
In Proofgold the corresponding term root is 2d62ee... and proposition id is 48bc10...
Axiom. (If_iii_0) We take the following as an axiom:
¬ p → If_iii = g
In Proofgold the corresponding term root is 9b77d9... and proposition id is d11201...
End of Section If_iii
Beginning of Section EpsilonRec_i
Variable F : set → (set → set) → set
Primitive. The name In_rec_i is a term of type set → set.
In Proofgold the corresponding term root is fac413... and object id is 93aac4...
Hypothesis Fr : ∀X : set, ∀g h : set → set, (∀x ∈ X, g x = h x) → F X g = F X h
Axiom. (In_rec_i_eq) We take the following as an axiom:
∀X : set, In_rec_i X = F X In_rec_i
In Proofgold the corresponding term root is 110653... and proposition id is e8653b...
End of Section EpsilonRec_i
Beginning of Section EpsilonRec_ii
Variable F : set → (set → (set → set)) → (set → set)
Primitive. The name In_rec_ii is a term of type set → (set → set).
In Proofgold the corresponding term root is f3c9ab... and object id is 3841bd...
Hypothesis Fr : ∀X : set, ∀g h : set → (set → set), (∀x ∈ X, g x = h x) → F X g = F X h
Axiom. (In_rec_ii_eq) We take the following as an axiom:
∀X : set, In_rec_ii X = F X In_rec_ii
In Proofgold the corresponding term root is f7aff6... and proposition id is 7bb1e9...
End of Section EpsilonRec_ii
Beginning of Section EpsilonRec_iii
Variable F : set → (set → (set → set → set)) → (set → set → set)
Primitive. The name In_rec_iii is a term of type set → (set → set → set).
In Proofgold the corresponding term root is 9b3a85... and object id is 651077...
Hypothesis Fr : ∀X : set, ∀g h : set → (set → set → set), (∀x ∈ X, g x = h x) → F X g = F X h
Axiom. (In_rec_iii_eq) We take the following as an axiom:
∀X : set, In_rec_iii X = F X In_rec_iii
In Proofgold the corresponding term root is 5f0574... and proposition id is a0709d...
End of Section EpsilonRec_iii
Beginning of Section NatRec
Variable z : set
Variable f : set → set → set
Let F : set → (set → set) → set ≝ λn g ⇒ if ⋃ n ∈ n then f (⋃ n) (g (⋃ n)) else z
Definition. We define nat_primrec to be In_rec_i F of type set → set.
In Proofgold the corresponding term root is 3be1c5... and object id is 1a64d5...
Axiom. (nat_primrec_r) We take the following as an axiom:
∀X : set, ∀g h : set → set, (∀x ∈ X, g x = h x) → F X g = F X h
In Proofgold the corresponding term root is c955cd... and proposition id is 9ba887...
Axiom. (nat_primrec_0) We take the following as an axiom:
nat_primrec 0 = z
In Proofgold the corresponding term root is 416eaf... and proposition id is be11a2...
Axiom. (nat_primrec_S) We take the following as an axiom:
∀n : set, nat_p n → nat_primrec (ordsucc n) = f n (nat_primrec n)
In Proofgold the corresponding term root is 797185... and proposition id is fe4c88...
End of Section NatRec
Beginning of Section NatArith
Definition. We define add_nat to be λn m : set ⇒ nat_primrec n (λ_ r ⇒ ordsucc r) m of type set → set → set.
In Proofgold the corresponding term root is afa8ae... and object id is 29768b...
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_nat.
Axiom. (add_nat_0R) We take the following as an axiom:
∀n : set, n + 0 = n
In Proofgold the corresponding term root is 402bcb... and proposition id is 23277f...
Axiom. (add_nat_SR) We take the following as an axiom:
∀n m : set, nat_p m → n + ordsucc m = ordsucc (n + m)
In Proofgold the corresponding term root is a53523... and proposition id is e61e18...
Axiom. (add_nat_p) We take the following as an axiom:
∀n : set, nat_p n → ∀m : set, nat_p m → nat_p (n + m)
In Proofgold the corresponding term root is a68eaa... and proposition id is 4c1d5d...
Axiom. (add_nat_1_1_2) We take the following as an axiom:
1 + 1 = 2
In Proofgold the corresponding term root is 174b87... and proposition id is 77f23f...
Definition. We define mul_nat to be λn m : set ⇒ nat_primrec 0 (λ_ r ⇒ n + r) m of type set → set → set.
In Proofgold the corresponding term root is 35a1ef... and object id is 80ccc6...
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_nat.
Axiom. (mul_nat_0R) We take the following as an axiom:
∀n : set, n * 0 = 0
In Proofgold the corresponding term root is b2f56c... and proposition id is 1e5b2c...
Axiom. (mul_nat_SR) We take the following as an axiom:
∀n m : set, nat_p m → n * ordsucc m = n + n * m
In Proofgold the corresponding term root is 37df54... and proposition id is 6dd6fc...
Axiom. (mul_nat_p) We take the following as an axiom:
∀n : set, nat_p n → ∀m : set, nat_p m → nat_p (n * m)
In Proofgold the corresponding term root is d63438... and proposition id is e910cb...
End of Section NatArith
Definition. We define Inj1 to be In_rec_i (λX f ⇒ {0} ∪ {f x|x ∈ X}) of type set → set.
In Proofgold the corresponding term root is 8f0026... and object id is 7736ca...
Axiom. (Inj1_eq) We take the following as an axiom:
∀X : set, Inj1 X = {0} ∪ {Inj1 x|x ∈ X}
In Proofgold the corresponding term root is 73d189... and proposition id is b80457...
Axiom. (Inj1I1) We take the following as an axiom:
∀X : set, 0 ∈ Inj1 X
In Proofgold the corresponding term root is 3c2cc4... and proposition id is 4ccac3...
Axiom. (Inj1I2) We take the following as an axiom:
∀X x : set, x ∈ X → Inj1 x ∈ Inj1 X
In Proofgold the corresponding term root is b6f23b... and proposition id is 086475...
Axiom. (Inj1E) We take the following as an axiom:
∀X y : set, y ∈ Inj1 X → y = 0 ∨ ∃x ∈ X, y = Inj1 x
In Proofgold the corresponding term root is d4177b... and proposition id is 259217...
Axiom. (Inj1NE1) We take the following as an axiom:
∀x : set, Inj1 x ≠ 0
In Proofgold the corresponding term root is 5e3197... and proposition id is 09bd10...
Axiom. (Inj1NE2) We take the following as an axiom:
∀x : set, Inj1 x ∉ {0}
In Proofgold the corresponding term root is 9e94b1... and proposition id is 3c4dd0...
Definition. We define Inj0 to be λX ⇒ {Inj1 x|x ∈ X} of type set → set.
In Proofgold the corresponding term root is 814321... and object id is 7d54be...
Axiom. (Inj0I) We take the following as an axiom:
∀X x : set, x ∈ X → Inj1 x ∈ Inj0 X
In Proofgold the corresponding term root is 7fc2e9... and proposition id is 565378...
Axiom. (Inj0E) We take the following as an axiom:
∀X y : set, y ∈ Inj0 X → ∃x : set, x ∈ X ∧ y = Inj1 x
In Proofgold the corresponding term root is 416684... and proposition id is 855213...
Definition. We define Unj to be In_rec_i (λX f ⇒ {f x|x ∈ X ∖ {0}}) of type set → set.
In Proofgold the corresponding term root is f202c1... and object id is 2e1675...
Axiom. (Unj_eq) We take the following as an axiom:
∀X : set, Unj X = {Unj x|x ∈ X ∖ {0}}
In Proofgold the corresponding term root is 3b1aa6... and proposition id is b4c852...
Axiom. (Unj_Inj1_eq) We take the following as an axiom:
∀X : set, Unj (Inj1 X) = X
In Proofgold the corresponding term root is e2cdfc... and proposition id is ae00e1...
Axiom. (Inj1_inj) We take the following as an axiom:
∀X Y : set, Inj1 X = Inj1 Y → X = Y
In Proofgold the corresponding term root is ce8b66... and proposition id is 3e918a...
Axiom. (Unj_Inj0_eq) We take the following as an axiom:
∀X : set, Unj (Inj0 X) = X
In Proofgold the corresponding term root is f3e39c... and proposition id is 3808ad...
Axiom. (Inj0_inj) We take the following as an axiom:
∀X Y : set, Inj0 X = Inj0 Y → X = Y
In Proofgold the corresponding term root is 662f53... and proposition id is 29f945...
Axiom. (Inj0_0) We take the following as an axiom:
Inj0 0 = 0
In Proofgold the corresponding term root is 171f47... and proposition id is 57f5af...
Axiom. (Inj0_Inj1_neq) We take the following as an axiom:
∀X Y : set, Inj0 X ≠ Inj1 Y
In Proofgold the corresponding term root is 21bb03... and proposition id is 2b14d8...
Definition. We define setsum to be λX Y ⇒ {Inj0 x|x ∈ X} ∪ {Inj1 y|y ∈ Y} of type set → set → set.
In Proofgold the corresponding term root is afe37e... and object id is 5b7e09...
Notation. We use + as an infix operator with priority 450 and which associates to the left corresponding to applying term setsum.
Axiom. (Inj0_setsum) We take the following as an axiom:
∀X Y x : set, x ∈ X → Inj0 x ∈ X + Y
In Proofgold the corresponding term root is 1c6408... and proposition id is 246ac5...
Axiom. (Inj1_setsum) We take the following as an axiom:
∀X Y y : set, y ∈ Y → Inj1 y ∈ X + Y
In Proofgold the corresponding term root is d47a0f... and proposition id is 2b4f94...
Axiom. (setsum_Inj_inv) We take the following as an axiom:
∀X Y z : set, z ∈ X + Y → (∃x ∈ X, z = Inj0 x) ∨ (∃y ∈ Y, z = Inj1 y)
In Proofgold the corresponding term root is 645a6c... and proposition id is a36400...
Axiom. (Inj0_setsum_0L) We take the following as an axiom:
∀X : set, 0 + X = Inj0 X
In Proofgold the corresponding term root is 0be1e7... and proposition id is 36fabd...
Axiom. (Subq_1_Sing0) We take the following as an axiom:
1 ⊆ {0}
In Proofgold the corresponding term root is aeae9a... and proposition id is abab2d...
Axiom. (Inj1_setsum_1L) We take the following as an axiom:
∀X : set, 1 + X = Inj1 X
In Proofgold the corresponding term root is f8d721... and proposition id is 45b1c8...
Axiom. (nat_setsum1_ordsucc) We take the following as an axiom:
∀n : set, nat_p n → 1 + n = ordsucc n
In Proofgold the corresponding term root is 3be3cc... and proposition id is 8fbdda...
Axiom. (setsum_0_0) We take the following as an axiom:
0 + 0 = 0
In Proofgold the corresponding term root is 5dcaeb... and proposition id is 4f3651...
Axiom. (setsum_1_0_1) We take the following as an axiom:
1 + 0 = 1
In Proofgold the corresponding term root is c2107f... and proposition id is e8609a...
Axiom. (setsum_1_1_2) We take the following as an axiom:
1 + 1 = 2
In Proofgold the corresponding term root is 9c89c0... and proposition id is ef3f41...
Beginning of Section pair_setsum
Let pair ≝ setsum
Definition. We define proj0 to be λZ ⇒ {Unj z|z ∈ Z, ∃x : set, Inj0 x = z} of type set → set.
In Proofgold the corresponding term root is 21a488... and object id is 9c5e4e...
Definition. We define proj1 to be λZ ⇒ {Unj z|z ∈ Z, ∃y : set, Inj1 y = z} of type set → set.
In Proofgold the corresponding term root is 7aba21... and object id is 7fd81e...
Axiom. (Inj0_pair_0_eq) We take the following as an axiom:
Inj0 = pair 0
In Proofgold the corresponding term root is 0fe601... and proposition id is 490c2a...
Axiom. (Inj1_pair_1_eq) We take the following as an axiom:
Inj1 = pair 1
In Proofgold the corresponding term root is 0bbde8... and proposition id is 8272d7...
Axiom. (pairI0) We take the following as an axiom:
∀X Y x, x ∈ X → pair 0 x ∈ pair X Y
In Proofgold the corresponding term root is 21a414... and proposition id is 34813b...
Axiom. (pairI1) We take the following as an axiom:
∀X Y y, y ∈ Y → pair 1 y ∈ pair X Y
In Proofgold the corresponding term root is bdaab5... and proposition id is b5248b...
Axiom. (pairE) We take the following as an axiom:
∀X Y z, z ∈ pair X Y → (∃x ∈ X, z = pair 0 x) ∨ (∃y ∈ Y, z = pair 1 y)
In Proofgold the corresponding term root is aac610... and proposition id is 0afdeb...
Axiom. (pairE0) We take the following as an axiom:
∀X Y x, pair 0 x ∈ pair X Y → x ∈ X
In Proofgold the corresponding term root is 042f30... and proposition id is f50b25...
Axiom. (pairE1) We take the following as an axiom:
∀X Y y, pair 1 y ∈ pair X Y → y ∈ Y
In Proofgold the corresponding term root is 505cfc... and proposition id is 30a181...
Axiom. (proj0I) We take the following as an axiom:
∀w u : set, pair 0 u ∈ w → u ∈ proj0 w
In Proofgold the corresponding term root is be55b9... and proposition id is 840c8d...
Axiom. (proj0E) We take the following as an axiom:
∀w u : set, u ∈ proj0 w → pair 0 u ∈ w
In Proofgold the corresponding term root is b9afa9... and proposition id is 5b7f58...
Axiom. (proj1I) We take the following as an axiom:
∀w u : set, pair 1 u ∈ w → u ∈ proj1 w
In Proofgold the corresponding term root is fbddb7... and proposition id is 595b3c...
Axiom. (proj1E) We take the following as an axiom:
∀w u : set, u ∈ proj1 w → pair 1 u ∈ w
In Proofgold the corresponding term root is 06e32e... and proposition id is c3c3e6...
Axiom. (proj0_pair_eq) We take the following as an axiom:
∀X Y : set, proj0 (pair X Y) = X
In Proofgold the corresponding term root is d546f3... and proposition id is 0c12fb...
Axiom. (proj1_pair_eq) We take the following as an axiom:
∀X Y : set, proj1 (pair X Y) = Y
In Proofgold the corresponding term root is 9f98a8... and proposition id is e0cb0f...
Definition. We define Sigma to be λX Y ⇒ ⋃x ∈ X{pair x y|y ∈ Y x} of type set → (set → set) → set.
In Proofgold the corresponding term root is 8acbb2... and object id is d64bcb...
Notation. We use ∑ x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using Sigma.
Axiom. (pair_Sigma) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀x ∈ X, ∀y ∈ Y x, pair x y ∈ ∑x ∈ X, Y x
In Proofgold the corresponding term root is 0d8645... and proposition id is 1456cb...
Axiom. (Sigma_eta_proj0_proj1) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀z ∈ (∑x ∈ X, Y x), pair (proj0 z) (proj1 z) = z ∧ proj0 z ∈ X ∧ proj1 z ∈ Y (proj0 z)
In Proofgold the corresponding term root is afe962... and proposition id is 77ba8e...
Axiom. (proj_Sigma_eta) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀z ∈ (∑x ∈ X, Y x), pair (proj0 z) (proj1 z) = z
In Proofgold the corresponding term root is 8b31cd... and proposition id is f30f76...
Axiom. (proj0_Sigma) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀z : set, z ∈ (∑x ∈ X, Y x) → proj0 z ∈ X
In Proofgold the corresponding term root is ae12a7... and proposition id is 506869...
Axiom. (proj1_Sigma) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀z : set, z ∈ (∑x ∈ X, Y x) → proj1 z ∈ Y (proj0 z)
In Proofgold the corresponding term root is 553db6... and proposition id is d79917...
Axiom. (pair_Sigma_E1) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀x y : set, pair x y ∈ (∑x ∈ X, Y x) → y ∈ Y x
In Proofgold the corresponding term root is c294a7... and proposition id is 81d8b0...
Axiom. (Sigma_E) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀z : set, z ∈ (∑x ∈ X, Y x) → ∃x ∈ X, ∃y ∈ Y x, z = pair x y
In Proofgold the corresponding term root is 5b1bd2... and proposition id is 8ecfab...
Definition. We define setprod to be λX Y : set ⇒ ∑x ∈ X, Y of type set → set → set.
In Proofgold the corresponding term root is fc0b60... and object id is 107b6b...
Notation. We use ⨯ as an infix operator with priority 440 and which associates to the left corresponding to applying term setprod.
Let lam : set → (set → set) → set ≝ Sigma
Definition. We define ap to be λf x ⇒ {proj1 z|z ∈ f, ∃y : set, z = pair x y} of type set → set → set.
In Proofgold the corresponding term root is c7aaa6... and object id is a4d82c...
Notation. When x is a set, a term x y is notation for ap x y.
Notation. λ x ∈ A ⇒ B is notation for the set Sigma A (λ x : set ⇒ B).
Notation. We now use n-tuple notation (a0,...,an-1) for n ≥ 2 for λ i ∈ n . if i = 0 then a0 else ... if i = n-2 then an-2 else an-1.
Axiom. (lamI) We take the following as an axiom:
∀X : set, ∀F : set → set, ∀x ∈ X, ∀y ∈ F x, pair x y ∈ λx ∈ X ⇒ F x
In Proofgold the corresponding term root is 0d8645... and proposition id is 1456cb...
Axiom. (lamE) We take the following as an axiom:
∀X : set, ∀F : set → set, ∀z : set, z ∈ (λx ∈ X ⇒ F x) → ∃x ∈ X, ∃y ∈ F x, z = pair x y
In Proofgold the corresponding term root is 5b1bd2... and proposition id is 8ecfab...
Axiom. (apI) We take the following as an axiom:
∀f x y, pair x y ∈ f → y ∈ f x
In Proofgold the corresponding term root is 64667c... and proposition id is 770816...
Axiom. (apE) We take the following as an axiom:
∀f x y, y ∈ f x → pair x y ∈ f
In Proofgold the corresponding term root is 85693a... and proposition id is c08565...
Axiom. (beta) We take the following as an axiom:
∀X : set, ∀F : set → set, ∀x : set, x ∈ X → (λx ∈ X ⇒ F x) x = F x
In Proofgold the corresponding term root is 95991d... and proposition id is b5182d...
Axiom. (proj0_ap_0) We take the following as an axiom:
∀u, proj0 u = u 0
In Proofgold the corresponding term root is 588f37... and proposition id is d4f351...
Axiom. (proj1_ap_1) We take the following as an axiom:
∀u, proj1 u = u 1
In Proofgold the corresponding term root is d116b3... and proposition id is 2328b0...
Axiom. (pair_ap_0) We take the following as an axiom:
∀x y : set, (pair x y) 0 = x
In Proofgold the corresponding term root is ac34b9... and proposition id is bb0477...
Axiom. (pair_ap_1) We take the following as an axiom:
∀x y : set, (pair x y) 1 = y
In Proofgold the corresponding term root is 2274fc... and proposition id is cce3d2...
Axiom. (ap0_Sigma) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀z : set, z ∈ (∑x ∈ X, Y x) → (z 0) ∈ X
In Proofgold the corresponding term root is 861a79... and proposition id is 1affcc...
Axiom. (ap1_Sigma) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀z : set, z ∈ (∑x ∈ X, Y x) → (z 1) ∈ (Y (z 0))
In Proofgold the corresponding term root is ad3bfe... and proposition id is 520af5...
Definition. We define pair_p to be λu : set ⇒ pair (u 0) (u 1) = u of type set → prop.
In Proofgold the corresponding term root is ade2bb... and object id is 5c8a35...
Axiom. (pair_p_I) We take the following as an axiom:
∀x y, pair_p (pair x y)
In Proofgold the corresponding term root is 06d9a2... and proposition id is 8f2fde...
Axiom. (Subq_2_UPair01) We take the following as an axiom:
2 ⊆ {0,1}
In Proofgold the corresponding term root is d90884... and proposition id is 94203e...
Axiom. (tuple_pair) We take the following as an axiom:
∀x y : set, pair x y = (x,y)
In Proofgold the corresponding term root is c122f6... and proposition id is 18198e...
Definition. We define Pi to be λX Y ⇒ {f ∈ 𝒫 (∑x ∈ X, ⋃ (Y x))|∀x ∈ X, f x ∈ Y x} of type set → (set → set) → set.
In Proofgold the corresponding term root is 40f1c3... and object id is a7b1b0...
Notation. We use ∏ x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using Pi.
Axiom. (PiI) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀f : set, (∀u ∈ f, pair_p u ∧ u 0 ∈ X) → (∀x ∈ X, f x ∈ Y x) → f ∈ ∏x ∈ X, Y x
In Proofgold the corresponding term root is 2b7ef4... and proposition id is 1f8f6f...
Axiom. (lam_Pi) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀F : set → set, (∀x ∈ X, F x ∈ Y x) → (λx ∈ X ⇒ F x) ∈ (∏x ∈ X, Y x)
In Proofgold the corresponding term root is c0b88f... and proposition id is 3733f8...
Axiom. (ap_Pi) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀f : set, ∀x : set, f ∈ (∏x ∈ X, Y x) → x ∈ X → f x ∈ Y x
In Proofgold the corresponding term root is 7c3617... and proposition id is cb962e...
Definition. We define setexp to be λX Y : set ⇒ ∏y ∈ Y, X of type set → set → set.
In Proofgold the corresponding term root is 1de7fc... and object id is 021ae0...
Notation. We use :^: as an infix operator with priority 430 and which associates to the left corresponding to applying term setexp.
Axiom. (pair_tuple_fun) We take the following as an axiom:
pair = (λx y ⇒ (x,y))
In Proofgold the corresponding term root is b02dfa... and proposition id is ed37d0...
Axiom. (lamI2) We take the following as an axiom:
∀X, ∀F : set → set, ∀x ∈ X, ∀y ∈ F x, (x,y) ∈ λx ∈ X ⇒ F x
In Proofgold the corresponding term root is d4a9d9... and proposition id is de381f...
Beginning of Section Tuples
Variable x0 x1 : set
Axiom. (tuple_2_0_eq) We take the following as an axiom:
(x0,x1) 0 = x0
In Proofgold the corresponding term root is 42d452... and proposition id is ad9037...
Axiom. (tuple_2_1_eq) We take the following as an axiom:
(x0,x1) 1 = x1
In Proofgold the corresponding term root is 596569... and proposition id is 2c0ad1...
End of Section Tuples
Axiom. (ReplEq_setprod_ext) We take the following as an axiom:
∀X Y, ∀F G : set → set → set, (∀x ∈ X, ∀y ∈ Y, F x y = G x y) → {F (w 0) (w 1)|w ∈ X ⨯ Y} = {G (w 0) (w 1)|w ∈ X ⨯ Y}
In Proofgold the corresponding term root is c486ab... and proposition id is f689a0...
Axiom. (tuple_2_Sigma) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀x ∈ X, ∀y ∈ Y x, (x,y) ∈ ∑x ∈ X, Y x
In Proofgold the corresponding term root is d4a9d9... and proposition id is de381f...
Axiom. (tuple_2_setprod) We take the following as an axiom:
∀X : set, ∀Y : set, ∀x ∈ X, ∀y ∈ Y, (x,y) ∈ X ⨯ Y
In Proofgold the corresponding term root is e907b8... and proposition id is 1f9d7f...
End of Section pair_setsum
Notation. We use ∑ x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using Sigma.
Notation. We use ⨯ as an infix operator with priority 440 and which associates to the left corresponding to applying term setprod.
Notation. We use ∏ x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using Pi.
Notation. We use :^: as an infix operator with priority 430 and which associates to the left corresponding to applying term setexp.
Definition. We define DescrR_i_io_1 to be λR ⇒ Eps_i (λx ⇒ (∃y : set → prop, R x y) ∧ (∀y z : set → prop, R x y → R x z → y = z)) of type (set → (set → prop) → prop) → set.
In Proofgold the corresponding term root is 1d3fd4... and object id is 82aecc...
Definition. We define DescrR_i_io_2 to be λR ⇒ Descr_Vo1 (λy ⇒ R (DescrR_i_io_1 R) y) of type (set → (set → prop) → prop) → set → prop.
In Proofgold the corresponding term root is 768eb2... and object id is 3f82bc...
Theorem. (DescrR_i_io_12) The following is provable:
∀R : set → (set → prop) → prop, (∃x, (∃y : set → prop, R x y) ∧ (∀y z : set → prop, R x y → R x z → y = z)) → R (DescrR_i_io_1 R) (DescrR_i_io_2 R)
In Proofgold the corresponding term root is a4fae2... and proposition id is da4f02...
Proof:
Let R be given.
Assume H1: ∃x, (∃y : set → prop, R x y) ∧ (∀y z : set → prop, R x y → R x z → y = z).
We prove the intermediate claim L1: (∃y : set → prop, R (DescrR_i_io_1 R) y) ∧ (∀y z : set → prop, R (DescrR_i_io_1 R) y → R (DescrR_i_io_1 R) z → y = z).
An exact proof term for the current goal is (Eps_i_ex (λx ⇒ (∃y : set → prop, R x y) ∧ (∀y z : set → prop, R x y → R x z → y = z)) H1).
Apply L1 to the current goal.
Assume H2 H3.
An exact proof term for the current goal is Descr_Vo1_prop (λy ⇒ R (DescrR_i_io_1 R) y) H2 H3.
∎
Definition. We define PNoEq_ to be λalpha p q ⇒ ∀beta ∈ alpha, p beta ↔ q beta of type set → (set → prop) → (set → prop) → prop.
In Proofgold the corresponding term root is d7d959... and object id is 144b65...
Theorem. (PNoEq_ref_) The following is provable:
∀alpha, ∀p : set → prop, PNoEq_ alpha p p
In Proofgold the corresponding term root is c27ebb... and proposition id is df4cf6...
Proof:
Let alpha, p and beta be given.
Assume H2.
Apply iff_refl to the current goal.
∎
Theorem. (PNoEq_sym_) The following is provable:
∀alpha, ∀p q : set → prop, PNoEq_ alpha p q → PNoEq_ alpha q p
In Proofgold the corresponding term root is b813f3... and proposition id is bfda0b...
Proof:
Let alpha, p and q be given.
Assume H1.
Let beta be given.
Assume H2.
Apply iff_sym to the current goal.
An exact proof term for the current goal is H1 beta H2.
∎
Theorem. (PNoEq_tra_) The following is provable:
∀alpha, ∀p q r : set → prop, PNoEq_ alpha p q → PNoEq_ alpha q r → PNoEq_ alpha p r
In Proofgold the corresponding term root is dded4c... and proposition id is fc92f3...
Proof:
Let alpha, p, q and r be given.
Assume H1 H2.
Let beta be given.
Assume H3.
Apply iff_trans (p beta) (q beta) to the current goal.
An exact proof term for the current goal is H1 beta H3.
An exact proof term for the current goal is H2 beta H3.
∎
Theorem. (PNoEq_antimon_) The following is provable:
∀p q : set → prop, ∀alpha, ordinal alpha → ∀beta ∈ alpha, PNoEq_ alpha p q → PNoEq_ beta p q
In Proofgold the corresponding term root is 8868e6... and proposition id is 094ae2...
Proof:
Let p, q and alpha be given.
Assume Ha.
Let beta be given.
Assume Hb H1.
Let gamma be given.
Assume H2: gamma ∈ beta.
We will prove p gamma ↔ q gamma.
Apply H1 to the current goal.
We will prove gamma ∈ alpha.
Apply Ha to the current goal.
Assume Ha1 _.
An exact proof term for the current goal is Ha1 beta Hb gamma H2.
∎
Definition. We define PNoLt_ to be λalpha p q ⇒ ∃beta ∈ alpha, PNoEq_ beta p q ∧ ¬ p beta ∧ q beta of type set → (set → prop) → (set → prop) → prop.
In Proofgold the corresponding term root is 34de68... and object id is c95964...
Theorem. (PNoLt_E_) The following is provable:
∀alpha, ∀p q : set → prop, PNoLt_ alpha p q → ∀R : prop, (∀beta, beta ∈ alpha → PNoEq_ beta p q → ¬ p beta → q beta → R) → R
In Proofgold the corresponding term root is 9ba543... and proposition id is 45aec8...
Proof:
Let alpha, p and q be given.
Assume H1.
Let R be given.
Assume H2.
Apply H1 to the current goal.
Let beta be given.
Assume H3.
Apply H3 to the current goal.
Assume H4: beta ∈ alpha.
Assume H5.
Apply H5 to the current goal.
Assume H5.
Apply H5 to the current goal.
Assume H6 H7 H8.
An exact proof term for the current goal is H2 beta H4 H6 H7 H8.
∎
Theorem. (PNoLt_irref_) The following is provable:
∀alpha, ∀p : set → prop, ¬ PNoLt_ alpha p p
In Proofgold the corresponding term root is fcb502... and proposition id is 987dff...
Proof:
Let alpha and p be given.
Assume H1.
Apply H1 to the current goal.
Let beta be given.
Assume H2.
Apply H2 to the current goal.
Assume _ H3.
Apply H3 to the current goal.
Assume H3.
Apply H3 to the current goal.
Assume _ H4 H5.
An exact proof term for the current goal is H4 H5.
∎
Theorem. (PNoLt_mon_) The following is provable:
∀p q : set → prop, ∀alpha, ordinal alpha → ∀beta ∈ alpha, PNoLt_ beta p q → PNoLt_ alpha p q
In Proofgold the corresponding term root is b1c3cf... and proposition id is d8d0f0...
Proof:
Let p, q and alpha be given.
Assume Ha.
Let beta be given.
Assume Hb H1.
Apply H1 to the current goal.
Let gamma be given.
Assume H2.
Apply H2 to the current goal.
Assume H2: gamma ∈ beta.
Assume H3.
We will prove ∃beta ∈ alpha, PNoEq_ beta p q ∧ ¬ p beta ∧ q beta.
We use gamma to witness the existential quantifier.
Apply andI to the current goal.
We will prove gamma ∈ alpha.
Apply Ha to the current goal.
Assume Ha1 _.
An exact proof term for the current goal is Ha1 beta Hb gamma H2.
An exact proof term for the current goal is H3.
∎
Theorem. (PNoLt_trichotomy_or_) The following is provable:
∀p q : set → prop, ∀alpha, ordinal alpha → PNoLt_ alpha p q ∨ PNoEq_ alpha p q ∨ PNoLt_ alpha q p
In Proofgold the corresponding term root is 664408... and proposition id is 8d3824...
Proof:
Let p and q be given.
Apply ordinal_ind to the current goal.
Let alpha be given.
Assume Ha.
Assume IH: ∀beta ∈ alpha, PNoLt_ beta p q ∨ PNoEq_ beta p q ∨ PNoLt_ beta q p.
Apply xm (PNoEq_ alpha p q) to the current goal.
Assume H1: PNoEq_ alpha p q.
Apply orIL to the current goal.
Apply orIR to the current goal.
An exact proof term for the current goal is H1.
Assume H1: ¬ PNoEq_ alpha p q.
We prove the intermediate claim L1: ∃beta, ¬ (beta ∈ alpha → (p beta ↔ q beta)).
An exact proof term for the current goal is not_all_ex_demorgan_i (λbeta ⇒ beta ∈ alpha → (p beta ↔ q beta)) H1.
Apply L1 to the current goal.
Let beta be given.
Assume H2: ¬ (beta ∈ alpha → (p beta ↔ q beta)).
We prove the intermediate claim L2: beta ∈ alpha ∧ ¬ (p beta ↔ q beta).
Apply xm (beta ∈ alpha) to the current goal.
Assume H3: beta ∈ alpha.
Apply xm (p beta ↔ q beta) to the current goal.
Assume H4: p beta ↔ q beta.
We will prove False.
Apply H2 to the current goal.
Assume _.
An exact proof term for the current goal is H4.
Assume H4: ¬ (p beta ↔ q beta).
Apply andI to the current goal.
An exact proof term for the current goal is H3.
An exact proof term for the current goal is H4.
Assume H3: beta ∉ alpha.
We will prove False.
Apply H2 to the current goal.
Assume H4.
We will prove False.
An exact proof term for the current goal is H3 H4.
Apply L2 to the current goal.
Assume H3: beta ∈ alpha.
Assume H4: ¬ (p beta ↔ q beta).
Apply IH beta H3 to the current goal.
Assume H5.
Apply H5 to the current goal.
Assume H5: PNoLt_ beta p q.
Apply orIL to the current goal.
Apply orIL to the current goal.
An exact proof term for the current goal is PNoLt_mon_ p q alpha Ha beta H3 H5.
Assume H5: PNoEq_ beta p q.
Apply xm (p beta) to the current goal.
Assume H6: p beta.
Apply xm (q beta) to the current goal.
Assume H7: q beta.
We will prove False.
Apply H4 to the current goal.
Apply iffI to the current goal.
Assume _.
An exact proof term for the current goal is H7.
Assume _.
An exact proof term for the current goal is H6.
Assume H7: ¬ q beta.
Apply orIR to the current goal.
We will prove ∃beta ∈ alpha, PNoEq_ beta q p ∧ ¬ q beta ∧ p beta.
We use beta to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H3.
Apply and3I to the current goal.
Apply PNoEq_sym_ to the current goal.
An exact proof term for the current goal is H5.
An exact proof term for the current goal is H7.
An exact proof term for the current goal is H6.
Assume H6: ¬ p beta.
Apply xm (q beta) to the current goal.
Assume H7: q beta.
Apply orIL to the current goal.
Apply orIL to the current goal.
We will prove ∃beta ∈ alpha, PNoEq_ beta p q ∧ ¬ p beta ∧ q beta.
We use beta to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H3.
Apply and3I to the current goal.
An exact proof term for the current goal is H5.
An exact proof term for the current goal is H6.
An exact proof term for the current goal is H7.
Assume H7: ¬ q beta.
We will prove False.
Apply H4 to the current goal.
Apply iffI to the current goal.
Assume H8.
We will prove False.
An exact proof term for the current goal is H6 H8.
Assume H8.
We will prove False.
An exact proof term for the current goal is H7 H8.
Assume H5: PNoLt_ beta q p.
Apply orIR to the current goal.
An exact proof term for the current goal is PNoLt_mon_ q p alpha Ha beta H3 H5.
∎
Theorem. (PNoLt_tra_) The following is provable:
∀alpha, ordinal alpha → ∀p q r : set → prop, PNoLt_ alpha p q → PNoLt_ alpha q r → PNoLt_ alpha p r
In Proofgold the corresponding term root is 3d7d91... and proposition id is 44767a...
Proof:
Let alpha be given.
Assume Ha.
Let p, q and r be given.
Assume Hpq Hqr.
We will prove ∃beta ∈ alpha, PNoEq_ beta p r ∧ ¬ p beta ∧ r beta.
Apply PNoLt_E_ alpha p q Hpq to the current goal.
Let beta be given.
Assume Hbeta1: beta ∈ alpha.
Assume Hbeta2: PNoEq_ beta p q.
Assume Hbeta3: ¬ p beta.
Assume Hbeta4: q beta.
Apply PNoLt_E_ alpha q r Hqr to the current goal.
Let gamma be given.
Assume Hgamma1: gamma ∈ alpha.
Assume Hgamma2: PNoEq_ gamma q r.
Assume Hgamma3: ¬ q gamma.
Assume Hgamma4: r gamma.
We prove the intermediate claim Lbeta: ordinal beta.
An exact proof term for the current goal is ordinal_Hered alpha Ha beta Hbeta1.
We prove the intermediate claim Lgamma: ordinal gamma.
An exact proof term for the current goal is ordinal_Hered alpha Ha gamma Hgamma1.
Apply ordinal_trichotomy_or beta gamma Lbeta Lgamma to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1: beta ∈ gamma.
We use beta to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hbeta1.
Apply and3I to the current goal.
We will prove PNoEq_ beta p r.
Apply PNoEq_tra_ beta p q r Hbeta2 to the current goal.
We will prove PNoEq_ beta q r.
An exact proof term for the current goal is PNoEq_antimon_ q r gamma Lgamma beta H1 Hgamma2.
We will prove ¬ p beta.
An exact proof term for the current goal is Hbeta3.
We will prove r beta.
Apply Hgamma2 beta H1 to the current goal.
Assume H2 _.
An exact proof term for the current goal is H2 Hbeta4.
Assume H1: beta = gamma.
We use beta to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hbeta1.
Apply and3I to the current goal.
We will prove PNoEq_ beta p r.
Apply PNoEq_tra_ beta p q r Hbeta2 to the current goal.
We will prove PNoEq_ beta q r.
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is Hgamma2.
We will prove ¬ p beta.
An exact proof term for the current goal is Hbeta3.
We will prove r beta.
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is Hgamma4.
Assume H1: gamma ∈ beta.
We use gamma to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hgamma1.
Apply and3I to the current goal.
We will prove PNoEq_ gamma p r.
Apply PNoEq_tra_ gamma p q r to the current goal.
We will prove PNoEq_ gamma p q.
An exact proof term for the current goal is PNoEq_antimon_ p q beta Lbeta gamma H1 Hbeta2.
An exact proof term for the current goal is Hgamma2.
We will prove ¬ p gamma.
Assume H2: p gamma.
Apply Hbeta2 gamma H1 to the current goal.
Assume H3 _.
Apply Hgamma3 to the current goal.
We will prove q gamma.
An exact proof term for the current goal is H3 H2.
We will prove r gamma.
An exact proof term for the current goal is Hgamma4.
∎
Definition. We define PNoLt to be λalpha p beta q ⇒ PNoLt_ (alpha ∩ beta) p q ∨ alpha ∈ beta ∧ PNoEq_ alpha p q ∧ q alpha ∨ beta ∈ alpha ∧ PNoEq_ beta p q ∧ ¬ p beta of type set → (set → prop) → set → (set → prop) → prop.
In Proofgold the corresponding term root is 8f57a0... and object id is f2094c...
Theorem. (PNoLtI1) The following is provable:
∀alpha beta, ∀p q : set → prop, PNoLt_ (alpha ∩ beta) p q → PNoLt alpha p beta q
In Proofgold the corresponding term root is c5735c... and proposition id is ecbc71...
Proof:
Let alpha, beta, p and q be given.
Assume H1.
We will prove PNoLt_ (alpha ∩ beta) p q ∨ alpha ∈ beta ∧ PNoEq_ alpha p q ∧ q alpha ∨ beta ∈ alpha ∧ PNoEq_ beta p q ∧ ¬ p beta.
Apply or3I1 to the current goal.
An exact proof term for the current goal is H1.
∎
Theorem. (PNoLtI2) The following is provable:
∀alpha beta, ∀p q : set → prop, alpha ∈ beta → PNoEq_ alpha p q → q alpha → PNoLt alpha p beta q
In Proofgold the corresponding term root is 419b53... and proposition id is 030093...
Proof:
Let alpha, beta, p and q be given.
Assume H1 H2 H3.
We will prove PNoLt_ (alpha ∩ beta) p q ∨ alpha ∈ beta ∧ PNoEq_ alpha p q ∧ q alpha ∨ beta ∈ alpha ∧ PNoEq_ beta p q ∧ ¬ p beta.
Apply or3I2 to the current goal.
Apply and3I to the current goal.
An exact proof term for the current goal is H1.
An exact proof term for the current goal is H2.
An exact proof term for the current goal is H3.
∎
Theorem. (PNoLtI3) The following is provable:
∀alpha beta, ∀p q : set → prop, beta ∈ alpha → PNoEq_ beta p q → ¬ p beta → PNoLt alpha p beta q
In Proofgold the corresponding term root is c392cb... and proposition id is 410442...
Proof:
Let alpha, beta, p and q be given.
Assume H1 H2 H3.
We will prove PNoLt_ (alpha ∩ beta) p q ∨ alpha ∈ beta ∧ PNoEq_ alpha p q ∧ q alpha ∨ beta ∈ alpha ∧ PNoEq_ beta p q ∧ ¬ p beta.
Apply or3I3 to the current goal.
Apply and3I to the current goal.
An exact proof term for the current goal is H1.
An exact proof term for the current goal is H2.
An exact proof term for the current goal is H3.
∎
Theorem. (PNoLtE) The following is provable:
∀alpha beta, ∀p q : set → prop, PNoLt alpha p beta q → ∀R : prop, (PNoLt_ (alpha ∩ beta) p q → R) → (alpha ∈ beta → PNoEq_ alpha p q → q alpha → R) → (beta ∈ alpha → PNoEq_ beta p q → ¬ p beta → R) → R
In Proofgold the corresponding term root is f7e6e3... and proposition id is af36ce...
Proof:
Let alpha, beta, p and q be given.
Assume H1.
Let R be given.
Assume HC1 HC2 HC3.
Apply H1 to the current goal.
Assume H1.
Apply H1 to the current goal.
An exact proof term for the current goal is HC1.
Assume H1.
Apply H1 to the current goal.
Assume H1.
Apply H1 to the current goal.
An exact proof term for the current goal is HC2.
Assume H1.
Apply H1 to the current goal.
Assume H1.
Apply H1 to the current goal.
An exact proof term for the current goal is HC3.
∎
Theorem. (PNoLt_irref) The following is provable:
∀alpha, ∀p : set → prop, ¬ PNoLt alpha p alpha p
In Proofgold the corresponding term root is ff1a80... and proposition id is d4c379...
Proof:
Let alpha and p be given.
Assume H1.
Apply PNoLtE alpha alpha p p H1 to the current goal.
Assume H1: PNoLt_ (alpha ∩ alpha) p p.
An exact proof term for the current goal is PNoLt_irref_ (alpha ∩ alpha) p H1.
Assume H1: alpha ∈ alpha.
We will prove False.
An exact proof term for the current goal is In_irref alpha H1.
Assume H1: alpha ∈ alpha.
We will prove False.
An exact proof term for the current goal is In_irref alpha H1.
∎
Theorem. (PNoLt_trichotomy_or) The following is provable:
∀alpha beta, ∀p q : set → prop, ordinal alpha → ordinal beta → PNoLt alpha p beta q ∨ alpha = beta ∧ PNoEq_ alpha p q ∨ PNoLt beta q alpha p
In Proofgold the corresponding term root is 4f39e4... and proposition id is 90b387...
Proof:
Let alpha, beta, p and q be given.
Assume Ha Hb.
Apply Ha to the current goal.
Assume Ha1 _.
Apply Hb to the current goal.
Assume Hb1 _.
We prove the intermediate claim Lab: ordinal (alpha ∩ beta).
An exact proof term for the current goal is ordinal_binintersect alpha beta Ha Hb.
Apply PNoLt_trichotomy_or_ p q (alpha ∩ beta) Lab to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1: PNoLt_ (alpha ∩ beta) p q.
Apply or3I1 to the current goal.
Apply PNoLtI1 to the current goal.
An exact proof term for the current goal is H1.
Assume H1: PNoEq_ (alpha ∩ beta) p q.
Apply ordinal_trichotomy_or alpha beta Ha Hb to the current goal.
Assume H2.
Apply H2 to the current goal.
Assume H2: alpha ∈ beta.
We prove the intermediate claim L1: alpha ∩ beta = alpha.
An exact proof term for the current goal is binintersect_Subq_eq_1 alpha beta (Hb1 alpha H2).
We prove the intermediate claim L2: PNoEq_ alpha p q.
rewrite the current goal using L1 (from right to left).
An exact proof term for the current goal is H1.
Apply xm (q alpha) to the current goal.
Assume H3: q alpha.
Apply or3I1 to the current goal.
Apply PNoLtI2 to the current goal.
An exact proof term for the current goal is H2.
We will prove PNoEq_ alpha p q.
An exact proof term for the current goal is L2.
An exact proof term for the current goal is H3.
Assume H3: ¬ q alpha.
Apply or3I3 to the current goal.
Apply PNoLtI3 to the current goal.
An exact proof term for the current goal is H2.
We will prove PNoEq_ alpha q p.
Apply PNoEq_sym_ to the current goal.
An exact proof term for the current goal is L2.
An exact proof term for the current goal is H3.
Assume H2: alpha = beta.
We prove the intermediate claim L1: alpha ∩ beta = alpha.
rewrite the current goal using H2 (from right to left).
An exact proof term for the current goal is binintersect_Subq_eq_1 alpha alpha (Subq_ref alpha).
We prove the intermediate claim L2: PNoEq_ alpha p q.
rewrite the current goal using L1 (from right to left).
An exact proof term for the current goal is H1.
Apply or3I2 to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is H2.
We will prove PNoEq_ alpha p q.
An exact proof term for the current goal is L2.
Assume H2: beta ∈ alpha.
We prove the intermediate claim L1: alpha ∩ beta = beta.
rewrite the current goal using binintersect_com (from left to right).
An exact proof term for the current goal is binintersect_Subq_eq_1 beta alpha (Ha1 beta H2).
We prove the intermediate claim L2: PNoEq_ beta p q.
rewrite the current goal using L1 (from right to left).
An exact proof term for the current goal is H1.
Apply xm (p beta) to the current goal.
Assume H3: p beta.
Apply or3I3 to the current goal.
Apply PNoLtI2 to the current goal.
An exact proof term for the current goal is H2.
We will prove PNoEq_ beta q p.
Apply PNoEq_sym_ to the current goal.
An exact proof term for the current goal is L2.
An exact proof term for the current goal is H3.
Assume H3: ¬ p beta.
Apply or3I1 to the current goal.
Apply PNoLtI3 to the current goal.
An exact proof term for the current goal is H2.
We will prove PNoEq_ beta p q.
An exact proof term for the current goal is L2.
An exact proof term for the current goal is H3.
Assume H1: PNoLt_ (alpha ∩ beta) q p.
Apply or3I3 to the current goal.
Apply PNoLtI1 to the current goal.
rewrite the current goal using binintersect_com (from left to right).
An exact proof term for the current goal is H1.
∎
Theorem. (PNoLtEq_tra) The following is provable:
∀alpha beta, ordinal alpha → ordinal beta → ∀p q r : set → prop, PNoLt alpha p beta q → PNoEq_ beta q r → PNoLt alpha p beta r
In Proofgold the corresponding term root is 2e082a... and proposition id is 2f2a82...
Proof:
Let alpha and beta be given.
Assume Ha Hb.
Let p, q and r be given.
Assume Hpq Hqr.
Apply PNoLtE alpha beta p q Hpq to the current goal.
Assume Hpq1: PNoLt_ (alpha ∩ beta) p q.
Apply Hpq1 to the current goal.
Let delta be given.
Assume Hpq2.
Apply Hpq2 to the current goal.
Assume Hd: delta ∈ alpha ∩ beta.
Apply binintersectE alpha beta delta Hd to the current goal.
Assume Hd1 Hd2.
Assume Hpq3.
Apply Hpq3 to the current goal.
Assume Hpq3.
Apply Hpq3 to the current goal.
Assume Hpq3: PNoEq_ delta p q.
Assume Hpq4: ¬ p delta.
Assume Hpq5: q delta.
We will prove PNoLt alpha p beta r.
Apply PNoLtI1 to the current goal.
We will prove ∃delta ∈ alpha ∩ beta, PNoEq_ delta p r ∧ ¬ p delta ∧ r delta.
We use delta to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hd.
Apply and3I to the current goal.
We will prove PNoEq_ delta p r.
Apply PNoEq_tra_ delta p q r to the current goal.
We will prove PNoEq_ delta p q.
An exact proof term for the current goal is Hpq3.
We will prove PNoEq_ delta q r.
Apply PNoEq_antimon_ q r beta Hb delta Hd2 to the current goal.
We will prove PNoEq_ beta q r.
An exact proof term for the current goal is Hqr.
We will prove ¬ p delta.
An exact proof term for the current goal is Hpq4.
We will prove r delta.
An exact proof term for the current goal is iffEL (q delta) (r delta) (Hqr delta Hd2) Hpq5.
Assume Hpq1: alpha ∈ beta.
Assume Hpq2: PNoEq_ alpha p q.
Assume Hpq3: q alpha.
We will prove PNoLt alpha p beta r.
Apply PNoLtI2 to the current goal.
We will prove alpha ∈ beta.
An exact proof term for the current goal is Hpq1.
We will prove PNoEq_ alpha p r.
Apply PNoEq_tra_ alpha p q r to the current goal.
An exact proof term for the current goal is Hpq2.
We will prove PNoEq_ alpha q r.
Apply PNoEq_antimon_ q r beta Hb alpha Hpq1 to the current goal.
An exact proof term for the current goal is Hqr.
We will prove r alpha.
An exact proof term for the current goal is iffEL (q alpha) (r alpha) (Hqr alpha Hpq1) Hpq3.
Assume Hpq1: beta ∈ alpha.
Assume Hpq2: PNoEq_ beta p q.
Assume Hpq3: ¬ p beta.
We will prove PNoLt alpha p beta r.
Apply PNoLtI3 to the current goal.
We will prove beta ∈ alpha.
An exact proof term for the current goal is Hpq1.
We will prove PNoEq_ beta p r.
Apply PNoEq_tra_ beta p q r to the current goal.
An exact proof term for the current goal is Hpq2.
An exact proof term for the current goal is Hqr.
We will prove ¬ p beta.
An exact proof term for the current goal is Hpq3.
∎
Theorem. (PNoEqLt_tra) The following is provable:
∀alpha beta, ordinal alpha → ordinal beta → ∀p q r : set → prop, PNoEq_ alpha p q → PNoLt alpha q beta r → PNoLt alpha p beta r
In Proofgold the corresponding term root is fe144b... and proposition id is f07654...
Proof:
Let alpha and beta be given.
Assume Ha Hb.
Let p, q and r be given.
Assume Hpq Hqr.
Apply PNoLtE alpha beta q r Hqr to the current goal.
Assume Hqr1: PNoLt_ (alpha ∩ beta) q r.
Apply Hqr1 to the current goal.
Let delta be given.
Assume Hqr2.
Apply Hqr2 to the current goal.
Assume Hd: delta ∈ alpha ∩ beta.
Apply binintersectE alpha beta delta Hd to the current goal.
Assume Hd1 Hd2.
Assume Hqr3.
Apply Hqr3 to the current goal.
Assume Hqr3.
Apply Hqr3 to the current goal.
Assume Hqr3: PNoEq_ delta q r.
Assume Hqr4: ¬ q delta.
Assume Hqr5: r delta.
We will prove PNoLt alpha p beta r.
Apply PNoLtI1 to the current goal.
We will prove ∃delta ∈ alpha ∩ beta, PNoEq_ delta p r ∧ ¬ p delta ∧ r delta.
We use delta to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hd.
Apply and3I to the current goal.
We will prove PNoEq_ delta p r.
Apply PNoEq_tra_ delta p q r to the current goal.
We will prove PNoEq_ delta p q.
Apply PNoEq_antimon_ p q alpha Ha delta Hd1 to the current goal.
We will prove PNoEq_ alpha p q.
An exact proof term for the current goal is Hpq.
We will prove PNoEq_ delta q r.
An exact proof term for the current goal is Hqr3.
We will prove ¬ p delta.
Assume H1: p delta.
Apply Hqr4 to the current goal.
We will prove q delta.
An exact proof term for the current goal is iffEL (p delta) (q delta) (Hpq delta Hd1) H1.
We will prove r delta.
An exact proof term for the current goal is Hqr5.
Assume Hqr1: alpha ∈ beta.
Assume Hqr2: PNoEq_ alpha q r.
Assume Hqr3: r alpha.
We will prove PNoLt alpha p beta r.
Apply PNoLtI2 to the current goal.
We will prove alpha ∈ beta.
An exact proof term for the current goal is Hqr1.
We will prove PNoEq_ alpha p r.
Apply PNoEq_tra_ alpha p q r to the current goal.
An exact proof term for the current goal is Hpq.
An exact proof term for the current goal is Hqr2.
We will prove r alpha.
An exact proof term for the current goal is Hqr3.
Assume Hqr1: beta ∈ alpha.
Assume Hqr2: PNoEq_ beta q r.
Assume Hqr3: ¬ q beta.
We will prove PNoLt alpha p beta r.
Apply PNoLtI3 to the current goal.
We will prove beta ∈ alpha.
An exact proof term for the current goal is Hqr1.
We will prove PNoEq_ beta p r.
Apply PNoEq_tra_ beta p q r to the current goal.
Apply PNoEq_antimon_ p q alpha Ha beta Hqr1 to the current goal.
An exact proof term for the current goal is Hpq.
An exact proof term for the current goal is Hqr2.
We will prove ¬ p beta.
Assume H1: p beta.
Apply Hqr3 to the current goal.
An exact proof term for the current goal is iffEL (p beta) (q beta) (Hpq beta Hqr1) H1.
∎
Theorem. (PNoLt_tra) The following is provable:
∀alpha beta gamma, ordinal alpha → ordinal beta → ordinal gamma → ∀p q r : set → prop, PNoLt alpha p beta q → PNoLt beta q gamma r → PNoLt alpha p gamma r
In Proofgold the corresponding term root is b72127... and proposition id is 8eff85...
Proof:
Let alpha, beta and gamma be given.
Assume Ha Hb Hc.
Apply Ha to the current goal.
Assume Ha1 _.
Apply Hc to the current goal.
Assume Hc1 _.
Let p, q and r be given.
Assume Hpq Hqr.
Apply PNoLtE alpha beta p q Hpq to the current goal.
Assume Hpq1: PNoLt_ (alpha ∩ beta) p q.
Apply Hpq1 to the current goal.
Let delta be given.
Assume Hpq2.
Apply Hpq2 to the current goal.
Assume Hd: delta ∈ alpha ∩ beta.
Apply binintersectE alpha beta delta Hd to the current goal.
Assume Hd1 Hd2.
Assume Hpq3.
Apply Hpq3 to the current goal.
Assume Hpq3.
Apply Hpq3 to the current goal.
Assume Hpq3: PNoEq_ delta p q.
Assume Hpq4: ¬ p delta.
Assume Hpq5: q delta.
We prove the intermediate claim Ld: ordinal delta.
An exact proof term for the current goal is ordinal_Hered beta Hb delta Hd2.
Apply PNoLtE beta gamma q r Hqr to the current goal.
Assume Hqr1: PNoLt_ (beta ∩ gamma) q r.
Apply Hqr1 to the current goal.
Let eps be given.
Assume Hqr2.
Apply Hqr2 to the current goal.
Assume He: eps ∈ beta ∩ gamma.
Apply binintersectE beta gamma eps He to the current goal.
Assume He1 He2.
Assume Hqr3.
Apply Hqr3 to the current goal.
Assume Hqr3.
Apply Hqr3 to the current goal.
Assume Hqr3: PNoEq_ eps q r.
Assume Hqr4: ¬ q eps.
Assume Hqr5: r eps.
We prove the intermediate claim Le: ordinal eps.
An exact proof term for the current goal is ordinal_Hered beta Hb eps He1.
We will prove PNoLt alpha p gamma r.
Apply PNoLtI1 to the current goal.
We will prove ∃delta ∈ alpha ∩ gamma, PNoEq_ delta p r ∧ ¬ p delta ∧ r delta.
Apply ordinal_trichotomy_or delta eps Ld Le to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1: delta ∈ eps.
We use delta to witness the existential quantifier.
Apply andI to the current goal.
We will prove delta ∈ alpha ∩ gamma.
Apply binintersectI to the current goal.
An exact proof term for the current goal is Hd1.
We will prove delta ∈ gamma.
An exact proof term for the current goal is Hc1 eps He2 delta H1.
Apply and3I to the current goal.
We will prove PNoEq_ delta p r.
Apply PNoEq_tra_ delta p q r to the current goal.
We will prove PNoEq_ delta p q.
An exact proof term for the current goal is Hpq3.
We will prove PNoEq_ delta q r.
Apply PNoEq_antimon_ q r eps Le delta H1 to the current goal.
We will prove PNoEq_ eps q r.
An exact proof term for the current goal is Hqr3.
We will prove ¬ p delta.
An exact proof term for the current goal is Hpq4.
We will prove r delta.
An exact proof term for the current goal is iffEL (q delta) (r delta) (Hqr3 delta H1) Hpq5.
Assume H1: delta = eps.
We use delta to witness the existential quantifier.
Apply andI to the current goal.
We will prove delta ∈ alpha ∩ gamma.
Apply binintersectI to the current goal.
An exact proof term for the current goal is Hd1.
We will prove delta ∈ gamma.
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is He2.
Apply and3I to the current goal.
We will prove PNoEq_ delta p r.
Apply PNoEq_tra_ delta p q r to the current goal.
We will prove PNoEq_ delta p q.
An exact proof term for the current goal is Hpq3.
We will prove PNoEq_ delta q r.
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is Hqr3.
We will prove ¬ p delta.
An exact proof term for the current goal is Hpq4.
We will prove r delta.
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is Hqr5.
Assume H1: eps ∈ delta.
We use eps to witness the existential quantifier.
Apply andI to the current goal.
We will prove eps ∈ alpha ∩ gamma.
Apply binintersectI to the current goal.
We will prove eps ∈ alpha.
An exact proof term for the current goal is Ha1 delta Hd1 eps H1.
An exact proof term for the current goal is He2.
Apply and3I to the current goal.
We will prove PNoEq_ eps p r.
Apply PNoEq_tra_ eps p q r to the current goal.
We will prove PNoEq_ eps p q.
Apply PNoEq_antimon_ p q delta Ld eps H1 to the current goal.
We will prove PNoEq_ delta p q.
An exact proof term for the current goal is Hpq3.
We will prove PNoEq_ eps q r.
An exact proof term for the current goal is Hqr3.
We will prove ¬ p eps.
Assume H2: p eps.
Apply Hqr4 to the current goal.
An exact proof term for the current goal is iffEL (p eps) (q eps) (Hpq3 eps H1) H2.
We will prove r eps.
An exact proof term for the current goal is Hqr5.
Assume Hqr1: beta ∈ gamma.
Assume Hqr2: PNoEq_ beta q r.
Assume Hqr3: r beta.
Apply PNoLtI1 to the current goal.
We will prove ∃delta ∈ alpha ∩ gamma, PNoEq_ delta p r ∧ ¬ p delta ∧ r delta.
We use delta to witness the existential quantifier.
Apply andI to the current goal.
We will prove delta ∈ alpha ∩ gamma.
Apply binintersectI to the current goal.
An exact proof term for the current goal is Hd1.
We will prove delta ∈ gamma.
An exact proof term for the current goal is Hc1 beta Hqr1 delta Hd2.
Apply and3I to the current goal.
We will prove PNoEq_ delta p r.
Apply PNoEq_tra_ delta p q r to the current goal.
We will prove PNoEq_ delta p q.
An exact proof term for the current goal is Hpq3.
We will prove PNoEq_ delta q r.
Apply PNoEq_antimon_ q r beta Hb delta Hd2 to the current goal.
We will prove PNoEq_ beta q r.
An exact proof term for the current goal is Hqr2.
We will prove ¬ p delta.
An exact proof term for the current goal is Hpq4.
We will prove r delta.
An exact proof term for the current goal is iffEL (q delta) (r delta) (Hqr2 delta Hd2) Hpq5.
Assume Hqr1: gamma ∈ beta.
Assume Hqr2: PNoEq_ gamma q r.
Assume Hqr3: ¬ q gamma.
Apply ordinal_trichotomy_or delta gamma Ld Hc to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1: delta ∈ gamma.
We will prove PNoLt alpha p gamma r.
Apply PNoLtI1 to the current goal.
We will prove ∃delta ∈ alpha ∩ gamma, PNoEq_ delta p r ∧ ¬ p delta ∧ r delta.
We use delta to witness the existential quantifier.
Apply andI to the current goal.
We will prove delta ∈ alpha ∩ gamma.
Apply binintersectI to the current goal.
An exact proof term for the current goal is Hd1.
We will prove delta ∈ gamma.
An exact proof term for the current goal is H1.
Apply and3I to the current goal.
We will prove PNoEq_ delta p r.
Apply PNoEq_tra_ delta p q r to the current goal.
We will prove PNoEq_ delta p q.
An exact proof term for the current goal is Hpq3.
We will prove PNoEq_ delta q r.
Apply PNoEq_antimon_ q r gamma Hc delta H1 to the current goal.
We will prove PNoEq_ gamma q r.
An exact proof term for the current goal is Hqr2.
We will prove ¬ p delta.
An exact proof term for the current goal is Hpq4.
We will prove r delta.
An exact proof term for the current goal is iffEL (q delta) (r delta) (Hqr2 delta H1) Hpq5.
Assume H1: delta = gamma.
Apply PNoLtI3 to the current goal.
We will prove gamma ∈ alpha.
rewrite the current goal using H1 (from right to left).
An exact proof term for the current goal is Hd1.
We will prove PNoEq_ gamma p r.
Apply PNoEq_tra_ gamma p q r to the current goal.
We will prove PNoEq_ gamma p q.
rewrite the current goal using H1 (from right to left).
An exact proof term for the current goal is Hpq3.
We will prove PNoEq_ gamma q r.
An exact proof term for the current goal is Hqr2.
We will prove ¬ p gamma.
rewrite the current goal using H1 (from right to left).
An exact proof term for the current goal is Hpq4.
Assume H1: gamma ∈ delta.
Apply PNoLtI3 to the current goal.
We will prove gamma ∈ alpha.
An exact proof term for the current goal is Ha1 delta Hd1 gamma H1.
We will prove PNoEq_ gamma p r.
Apply PNoEq_tra_ gamma p q r to the current goal.
We will prove PNoEq_ gamma p q.
Apply PNoEq_antimon_ p q delta Ld gamma H1 to the current goal.
An exact proof term for the current goal is Hpq3.
We will prove PNoEq_ gamma q r.
An exact proof term for the current goal is Hqr2.
We will prove ¬ p gamma.
Assume H2: p gamma.
Apply Hqr3 to the current goal.
We will prove q gamma.
An exact proof term for the current goal is iffEL (p gamma) (q gamma) (Hpq3 gamma H1) H2.
Assume Hpq1: alpha ∈ beta.
Assume Hpq2: PNoEq_ alpha p q.
Assume Hpq3: q alpha.
Apply PNoLtE beta gamma q r Hqr to the current goal.
Assume Hqr1: PNoLt_ (beta ∩ gamma) q r.
Apply Hqr1 to the current goal.
Let eps be given.
Assume Hqr2.
Apply Hqr2 to the current goal.
Assume He: eps ∈ beta ∩ gamma.
Apply binintersectE beta gamma eps He to the current goal.
Assume He1 He2.
Assume Hqr3.
Apply Hqr3 to the current goal.
Assume Hqr3.
Apply Hqr3 to the current goal.
Assume Hqr3: PNoEq_ eps q r.
Assume Hqr4: ¬ q eps.
Assume Hqr5: r eps.
We prove the intermediate claim Le: ordinal eps.
An exact proof term for the current goal is ordinal_Hered beta Hb eps He1.
Apply ordinal_trichotomy_or alpha eps Ha Le to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1: alpha ∈ eps.
We will prove PNoLt alpha p gamma r.
Apply PNoLtI2 to the current goal.
We will prove alpha ∈ gamma.
An exact proof term for the current goal is Hc1 eps He2 alpha H1.
We will prove PNoEq_ alpha p r.
Apply PNoEq_tra_ alpha p q r to the current goal.
We will prove PNoEq_ alpha p q.
An exact proof term for the current goal is Hpq2.
We will prove PNoEq_ alpha q r.
Apply PNoEq_antimon_ q r eps Le alpha H1 to the current goal.
We will prove PNoEq_ eps q r.
An exact proof term for the current goal is Hqr3.
We will prove r alpha.
An exact proof term for the current goal is iffEL (q alpha) (r alpha) (Hqr3 alpha H1) Hpq3.
Assume H1: alpha = eps.
We will prove PNoLt alpha p gamma r.
Apply PNoLtI2 to the current goal.
We will prove alpha ∈ gamma.
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is He2.
We will prove PNoEq_ alpha p r.
Apply PNoEq_tra_ alpha p q r to the current goal.
We will prove PNoEq_ alpha p q.
An exact proof term for the current goal is Hpq2.
We will prove PNoEq_ alpha q r.
rewrite the current goal using H1 (from left to right).
We will prove PNoEq_ eps q r.
An exact proof term for the current goal is Hqr3.
We will prove r alpha.
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is Hqr5.
Assume H1: eps ∈ alpha.
We will prove PNoLt alpha p gamma r.
Apply PNoLtI1 to the current goal.
We will prove ∃delta ∈ alpha ∩ gamma, PNoEq_ delta p r ∧ ¬ p delta ∧ r delta.
We use eps to witness the existential quantifier.
Apply andI to the current goal.
We will prove eps ∈ alpha ∩ gamma.
Apply binintersectI to the current goal.
An exact proof term for the current goal is H1.
An exact proof term for the current goal is He2.
Apply and3I to the current goal.
We will prove PNoEq_ eps p r.
Apply PNoEq_tra_ eps p q r to the current goal.
We will prove PNoEq_ eps p q.
Apply PNoEq_antimon_ p q alpha Ha eps H1 to the current goal.
We will prove PNoEq_ alpha p q.
An exact proof term for the current goal is Hpq2.
We will prove PNoEq_ eps q r.
An exact proof term for the current goal is Hqr3.
We will prove ¬ p eps.
Assume H2: p eps.
Apply Hqr4 to the current goal.
We will prove q eps.
An exact proof term for the current goal is iffEL (p eps) (q eps) (Hpq2 eps H1) H2.
We will prove r eps.
An exact proof term for the current goal is Hqr5.
Assume Hqr1: beta ∈ gamma.
Assume Hqr2: PNoEq_ beta q r.
Assume Hqr3: r beta.
Apply PNoLtI2 to the current goal.
We will prove alpha ∈ gamma.
An exact proof term for the current goal is Hc1 beta Hqr1 alpha Hpq1.
We will prove PNoEq_ alpha p r.
Apply PNoEq_tra_ alpha p q r to the current goal.
An exact proof term for the current goal is Hpq2.
Apply PNoEq_antimon_ q r beta Hb alpha Hpq1 to the current goal.
An exact proof term for the current goal is Hqr2.
We will prove r alpha.
An exact proof term for the current goal is iffEL (q alpha) (r alpha) (Hqr2 alpha Hpq1) Hpq3.
Assume Hqr1: gamma ∈ beta.
Assume Hqr2: PNoEq_ gamma q r.
Assume Hqr3: ¬ q gamma.
We will prove PNoLt alpha p gamma r.
Apply ordinal_trichotomy_or alpha gamma Ha Hc to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1: alpha ∈ gamma.
Apply PNoLtI2 to the current goal.
We will prove alpha ∈ gamma.
An exact proof term for the current goal is H1.
We will prove PNoEq_ alpha p r.
Apply PNoEq_tra_ alpha p q r to the current goal.
An exact proof term for the current goal is Hpq2.
Apply PNoEq_antimon_ q r gamma Hc alpha H1 to the current goal.
An exact proof term for the current goal is Hqr2.
We will prove r alpha.
An exact proof term for the current goal is iffEL (q alpha) (r alpha) (Hqr2 alpha H1) Hpq3.
Assume H1: alpha = gamma.
We will prove False.
Apply Hqr3 to the current goal.
rewrite the current goal using H1 (from right to left).
An exact proof term for the current goal is Hpq3.
Assume H1: gamma ∈ alpha.
Apply PNoLtI3 to the current goal.
We will prove gamma ∈ alpha.
An exact proof term for the current goal is H1.
We will prove PNoEq_ gamma p r.
Apply PNoEq_tra_ gamma p q r to the current goal.
Apply PNoEq_antimon_ p q alpha Ha gamma H1 to the current goal.
An exact proof term for the current goal is Hpq2.
An exact proof term for the current goal is Hqr2.
We will prove ¬ p gamma.
Assume H2: p gamma.
Apply Hqr3 to the current goal.
We will prove q gamma.
An exact proof term for the current goal is iffEL (p gamma) (q gamma) (Hpq2 gamma H1) H2.
Assume Hpq1: beta ∈ alpha.
Assume Hpq2: PNoEq_ beta p q.
Assume Hpq3: ¬ p beta.
Apply PNoLtE beta gamma q r Hqr to the current goal.
Assume Hqr1: PNoLt_ (beta ∩ gamma) q r.
Apply Hqr1 to the current goal.
Let eps be given.
Assume Hqr2.
Apply Hqr2 to the current goal.
Assume He: eps ∈ beta ∩ gamma.
Apply binintersectE beta gamma eps He to the current goal.
Assume He1 He2.
Assume Hqr3.
Apply Hqr3 to the current goal.
Assume Hqr3.
Apply Hqr3 to the current goal.
Assume Hqr3: PNoEq_ eps q r.
Assume Hqr4: ¬ q eps.
Assume Hqr5: r eps.
We will prove PNoLt alpha p gamma r.
Apply PNoLtI1 to the current goal.
We will prove ∃delta ∈ alpha ∩ gamma, PNoEq_ delta p r ∧ ¬ p delta ∧ r delta.
We use eps to witness the existential quantifier.
Apply andI to the current goal.
We will prove eps ∈ alpha ∩ gamma.
Apply binintersectI to the current goal.
We will prove eps ∈ alpha.
An exact proof term for the current goal is Ha1 beta Hpq1 eps He1.
An exact proof term for the current goal is He2.
Apply and3I to the current goal.
We will prove PNoEq_ eps p r.
Apply PNoEq_tra_ eps p q r to the current goal.
We will prove PNoEq_ eps p q.
Apply PNoEq_antimon_ p q beta Hb eps He1 to the current goal.
An exact proof term for the current goal is Hpq2.
An exact proof term for the current goal is Hqr3.
We will prove ¬ p eps.
Assume H1: p eps.
Apply Hqr4 to the current goal.
We will prove q eps.
An exact proof term for the current goal is iffEL (p eps) (q eps) (Hpq2 eps He1) H1.
We will prove r eps.
An exact proof term for the current goal is Hqr5.
Assume Hqr1: beta ∈ gamma.
Assume Hqr2: PNoEq_ beta q r.
Assume Hqr3: r beta.
Apply PNoLtI1 to the current goal.
We will prove ∃delta ∈ alpha ∩ gamma, PNoEq_ delta p r ∧ ¬ p delta ∧ r delta.
We use beta to witness the existential quantifier.
Apply andI to the current goal.
Apply binintersectI to the current goal.
An exact proof term for the current goal is Hpq1.
An exact proof term for the current goal is Hqr1.
Apply and3I to the current goal.
Apply PNoEq_tra_ beta p q r to the current goal.
An exact proof term for the current goal is Hpq2.
An exact proof term for the current goal is Hqr2.
We will prove ¬ p beta.
An exact proof term for the current goal is Hpq3.
We will prove r beta.
An exact proof term for the current goal is Hqr3.
Assume Hqr1: gamma ∈ beta.
Assume Hqr2: PNoEq_ gamma q r.
Assume Hqr3: ¬ q gamma.
Apply PNoLtI3 to the current goal.
We will prove gamma ∈ alpha.
An exact proof term for the current goal is Ha1 beta Hpq1 gamma Hqr1.
We will prove PNoEq_ gamma p r.
Apply PNoEq_tra_ gamma p q r to the current goal.
We will prove PNoEq_ gamma p q.
Apply PNoEq_antimon_ p q beta Hb gamma Hqr1 to the current goal.
An exact proof term for the current goal is Hpq2.
An exact proof term for the current goal is Hqr2.
We will prove ¬ p gamma.
Assume H1: p gamma.
Apply Hqr3 to the current goal.
We will prove q gamma.
An exact proof term for the current goal is iffEL (p gamma) (q gamma) (Hpq2 gamma Hqr1) H1.
∎
Definition. We define PNoLe to be λalpha p beta q ⇒ PNoLt alpha p beta q ∨ alpha = beta ∧ PNoEq_ alpha p q of type set → (set → prop) → set → (set → prop) → prop.
In Proofgold the corresponding term root is ac6311... and object id is 770cf7...
Theorem. (PNoLeI1) The following is provable:
∀alpha beta, ∀p q : set → prop, PNoLt alpha p beta q → PNoLe alpha p beta q
In Proofgold the corresponding term root is 1f0528... and proposition id is 674a2c...
Proof:
Let alpha, beta, p and q be given.
Assume H1.
We will prove PNoLt alpha p beta q ∨ alpha = beta ∧ PNoEq_ alpha p q.
Apply orIL to the current goal.
An exact proof term for the current goal is H1.
∎
Theorem. (PNoLeI2) The following is provable:
∀alpha, ∀p q : set → prop, PNoEq_ alpha p q → PNoLe alpha p alpha q
In Proofgold the corresponding term root is b45332... and proposition id is 0b2157...
Proof:
Let alpha, p and q be given.
Assume H1.
We will prove PNoLt alpha p alpha q ∨ alpha = alpha ∧ PNoEq_ alpha p q.
Apply orIR to the current goal.
Apply andI to the current goal.
Use reflexivity.
An exact proof term for the current goal is H1.
∎
Theorem. (PNoLe_ref) The following is provable:
∀alpha, ∀p : set → prop, PNoLe alpha p alpha p
In Proofgold the corresponding term root is 1b91bd... and proposition id is 613386...
Proof:
Let alpha and p be given.
Apply PNoLeI2 to the current goal.
Apply PNoEq_ref_ to the current goal.
∎
Theorem. (PNoLe_antisym) The following is provable:
∀alpha beta, ordinal alpha → ordinal beta → ∀p q : set → prop, PNoLe alpha p beta q → PNoLe beta q alpha p → alpha = beta ∧ PNoEq_ alpha p q
In Proofgold the corresponding term root is 934d7a... and proposition id is 4e3594...
Proof:
Let alpha and beta be given.
Assume Ha Hb.
Let p and q be given.
Assume H1: PNoLt alpha p beta q ∨ alpha = beta ∧ PNoEq_ alpha p q.
Assume H2: PNoLt beta q alpha p ∨ beta = alpha ∧ PNoEq_ beta q p.
Apply H1 to the current goal.
Assume H1: PNoLt alpha p beta q.
We will prove False.
Apply H2 to the current goal.
Assume H2: PNoLt beta q alpha p.
Apply PNoLt_irref alpha p to the current goal.
Apply PNoLt_tra alpha beta alpha Ha Hb Ha p q p to the current goal.
An exact proof term for the current goal is H1.
An exact proof term for the current goal is H2.
Assume H2.
Apply H2 to the current goal.
Assume H2a: beta = alpha.
Assume H2b: PNoEq_ beta q p.
Apply PNoLtE alpha beta p q H1 to the current goal.
Assume Hpq1: PNoLt_ (alpha ∩ beta) p q.
Apply Hpq1 to the current goal.
Let delta be given.
Assume Hpq2.
Apply Hpq2 to the current goal.
Assume Hd: delta ∈ alpha ∩ beta.
Apply binintersectE alpha beta delta Hd to the current goal.
Assume Hd1 Hd2.
Assume Hpq3.
Apply Hpq3 to the current goal.
Assume Hpq3.
Apply Hpq3 to the current goal.
Assume Hpq3: PNoEq_ delta p q.
Assume Hpq4: ¬ p delta.
Assume Hpq5: q delta.
Apply Hpq4 to the current goal.
An exact proof term for the current goal is iffEL (q delta) (p delta) (H2b delta Hd2) Hpq5.
Assume Hpq1: alpha ∈ beta.
Assume Hpq2: PNoEq_ alpha p q.
Assume Hpq3: q alpha.
Apply In_irref alpha to the current goal.
rewrite the current goal using H2a (from right to left) at position 2.
An exact proof term for the current goal is Hpq1.
Assume Hpq1: beta ∈ alpha.
Assume Hpq2: PNoEq_ beta p q.
Assume Hpq3: ¬ p beta.
Apply In_irref alpha to the current goal.
rewrite the current goal using H2a (from right to left) at position 1.
An exact proof term for the current goal is Hpq1.
Assume H1.
An exact proof term for the current goal is H1.
∎
Theorem. (PNoLtLe_tra) The following is provable:
∀alpha beta gamma, ordinal alpha → ordinal beta → ordinal gamma → ∀p q r : set → prop, PNoLt alpha p beta q → PNoLe beta q gamma r → PNoLt alpha p gamma r
In Proofgold the corresponding term root is 156586... and proposition id is 09246b...
Proof:
Let alpha, beta and gamma be given.
Assume Ha Hb Hc.
Let p, q and r be given.
Assume H1: PNoLt alpha p beta q.
Assume H2: PNoLt beta q gamma r ∨ beta = gamma ∧ PNoEq_ beta q r.
Apply H2 to the current goal.
Assume H2: PNoLt beta q gamma r.
An exact proof term for the current goal is PNoLt_tra alpha beta gamma Ha Hb Hc p q r H1 H2.
Assume H2.
Apply H2 to the current goal.
Assume H2a: beta = gamma.
Assume H2b: PNoEq_ beta q r.
We will prove PNoLt alpha p gamma r.
rewrite the current goal using H2a (from right to left).
We will prove PNoLt alpha p beta r.
An exact proof term for the current goal is PNoLtEq_tra alpha beta Ha Hb p q r H1 H2b.
∎
Theorem. (PNoLeLt_tra) The following is provable:
∀alpha beta gamma, ordinal alpha → ordinal beta → ordinal gamma → ∀p q r : set → prop, PNoLe alpha p beta q → PNoLt beta q gamma r → PNoLt alpha p gamma r
In Proofgold the corresponding term root is a260ca... and proposition id is ad6971...
Proof:
Let alpha, beta and gamma be given.
Assume Ha Hb Hc.
Let p, q and r be given.
Assume H1: PNoLt alpha p beta q ∨ alpha = beta ∧ PNoEq_ alpha p q.
Assume H2: PNoLt beta q gamma r.
Apply H1 to the current goal.
Assume H1: PNoLt alpha p beta q.
An exact proof term for the current goal is PNoLt_tra alpha beta gamma Ha Hb Hc p q r H1 H2.
Assume H1.
Apply H1 to the current goal.
Assume H1a: alpha = beta.
Assume H1b: PNoEq_ alpha p q.
We will prove PNoLt alpha p gamma r.
rewrite the current goal using H1a (from left to right).
We will prove PNoLt beta p gamma r.
Apply PNoEqLt_tra beta gamma Hb Hc p q r to the current goal.
We will prove PNoEq_ beta p q.
rewrite the current goal using H1a (from right to left).
An exact proof term for the current goal is H1b.
An exact proof term for the current goal is H2.
∎
Theorem. (PNoEqLe_tra) The following is provable:
∀alpha beta, ordinal alpha → ordinal beta → ∀p q r : set → prop, PNoEq_ alpha p q → PNoLe alpha q beta r → PNoLe alpha p beta r
In Proofgold the corresponding term root is 7d3ff8... and proposition id is 002ebf...
Proof:
Let alpha and beta be given.
Assume Ha Hb.
Let p, q and r be given.
Assume Hpq.
Assume Hqr: PNoLt alpha q beta r ∨ alpha = beta ∧ PNoEq_ alpha q r.
We will prove PNoLt alpha p beta r ∨ alpha = beta ∧ PNoEq_ alpha p r.
Apply Hqr to the current goal.
Assume Hqr1.
Apply orIL to the current goal.
An exact proof term for the current goal is PNoEqLt_tra alpha beta Ha Hb p q r Hpq Hqr1.
Assume Hqr.
Apply Hqr to the current goal.
Assume Hqr1: alpha = beta.
Assume Hqr2: PNoEq_ alpha q r.
Apply orIR to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hqr1.
An exact proof term for the current goal is PNoEq_tra_ alpha p q r Hpq Hqr2.
∎
Theorem. (PNoLe_tra) The following is provable:
∀alpha beta gamma, ordinal alpha → ordinal beta → ordinal gamma → ∀p q r : set → prop, PNoLe alpha p beta q → PNoLe beta q gamma r → PNoLe alpha p gamma r
In Proofgold the corresponding term root is 70b92b... and proposition id is 4b557d...
Proof:
Let alpha, beta and gamma be given.
Assume Ha Hb Hc.
Let p, q and r be given.
Assume H1: PNoLt alpha p beta q ∨ alpha = beta ∧ PNoEq_ alpha p q.
Assume H2: PNoLe beta q gamma r.
Apply H1 to the current goal.
Assume H1: PNoLt alpha p beta q.
We will prove PNoLt alpha p gamma r ∨ alpha = gamma ∧ PNoEq_ alpha p r.
Apply orIL to the current goal.
An exact proof term for the current goal is PNoLtLe_tra alpha beta gamma Ha Hb Hc p q r H1 H2.
Assume H1.
Apply H1 to the current goal.
Assume H1a: alpha = beta.
Assume H1b: PNoEq_ alpha p q.
We will prove PNoLe alpha p gamma r.
rewrite the current goal using H1a (from left to right).
We will prove PNoLe beta p gamma r.
We prove the intermediate claim L1: PNoEq_ beta p q.
rewrite the current goal using H1a (from right to left).
An exact proof term for the current goal is H1b.
An exact proof term for the current goal is PNoEqLe_tra beta gamma Hb Hc p q r L1 H2.
∎
Definition. We define PNo_downc to be λL alpha p ⇒ ∃beta, ordinal beta ∧ ∃q : set → prop, L beta q ∧ PNoLe alpha p beta q of type (set → (set → prop) → prop) → set → (set → prop) → prop.
In Proofgold the corresponding term root is 93dab1... and object id is f6c962...
Definition. We define PNo_upc to be λR alpha p ⇒ ∃beta, ordinal beta ∧ ∃q : set → prop, R beta q ∧ PNoLe beta q alpha p of type (set → (set → prop) → prop) → set → (set → prop) → prop.
In Proofgold the corresponding term root is 543712... and object id is b97935...
Theorem. (PNoLe_downc) The following is provable:
∀L : set → (set → prop) → prop, ∀alpha beta, ∀p q : set → prop, ordinal alpha → ordinal beta → PNo_downc L alpha p → PNoLe beta q alpha p → PNo_downc L beta q
In Proofgold the corresponding term root is 6b1f0d... and proposition id is cd130e...
Proof:
Let L, alpha, beta, p and q be given.
Assume Ha Hb.
Assume H1: PNo_downc L alpha p.
Assume H2: PNoLe beta q alpha p.
We will prove PNo_downc L beta q.
Apply H1 to the current goal.
Let gamma be given.
Assume H3.
Apply H3 to the current goal.
Assume Hc: ordinal gamma.
Assume H3.
Apply H3 to the current goal.
Let r be given.
Assume H3.
Apply H3 to the current goal.
Assume H3: L gamma r.
Assume H4: PNoLe alpha p gamma r.
We will prove ∃delta, ordinal delta ∧ ∃r : set → prop, L delta r ∧ PNoLe beta q delta r.
We use gamma to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hc.
We use r to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H3.
An exact proof term for the current goal is PNoLe_tra beta alpha gamma Hb Ha Hc q p r H2 H4.
∎
Theorem. (PNo_downc_ref) The following is provable:
∀L : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p : set → prop, L alpha p → PNo_downc L alpha p
In Proofgold the corresponding term root is 347aa9... and proposition id is 69dfcb...
Proof:
Let L and alpha be given.
Assume Ha.
Let p be given.
Assume H1: L alpha p.
We will prove ∃beta, ordinal beta ∧ ∃q : set → prop, L beta q ∧ PNoLe alpha p beta q.
We use alpha to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Ha.
We use p to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H1.
Apply PNoLe_ref to the current goal.
∎
Theorem. (PNo_upc_ref) The following is provable:
∀R : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p : set → prop, R alpha p → PNo_upc R alpha p
In Proofgold the corresponding term root is 403942... and proposition id is c4bf71...
Proof:
Let R and alpha be given.
Assume Ha.
Let p be given.
Assume H1: R alpha p.
We will prove ∃beta, ordinal beta ∧ ∃q : set → prop, R beta q ∧ PNoLe beta q alpha p.
We use alpha to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Ha.
We use p to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H1.
Apply PNoLe_ref to the current goal.
∎
Theorem. (PNoLe_upc) The following is provable:
∀R : set → (set → prop) → prop, ∀alpha beta, ∀p q : set → prop, ordinal alpha → ordinal beta → PNo_upc R alpha p → PNoLe alpha p beta q → PNo_upc R beta q
In Proofgold the corresponding term root is 111b74... and proposition id is eb9ed5...
Proof:
Let R, alpha, beta, p and q be given.
Assume Ha Hb.
Assume H1: PNo_upc R alpha p.
Assume H2: PNoLe alpha p beta q.
We will prove PNo_upc R beta q.
Apply H1 to the current goal.
Let gamma be given.
Assume H3.
Apply H3 to the current goal.
Assume Hc: ordinal gamma.
Assume H3.
Apply H3 to the current goal.
Let r be given.
Assume H3.
Apply H3 to the current goal.
Assume H3: R gamma r.
Assume H4: PNoLe gamma r alpha p.
We will prove ∃delta, ordinal delta ∧ ∃r : set → prop, R delta r ∧ PNoLe delta r beta q.
We use gamma to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hc.
We use r to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H3.
An exact proof term for the current goal is PNoLe_tra gamma alpha beta Hc Ha Hb r p q H4 H2.
∎
Definition. We define PNoLt_pwise to be λL R ⇒ ∀gamma, ordinal gamma → ∀p : set → prop, L gamma p → ∀delta, ordinal delta → ∀q : set → prop, R delta q → PNoLt gamma p delta q of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → prop.
In Proofgold the corresponding term root is ae448b... and object id is 123808...
Theorem. (PNoLt_pwise_downc_upc) The following is provable:
∀L R : set → (set → prop) → prop, PNoLt_pwise L R → PNoLt_pwise (PNo_downc L) (PNo_upc R)
In Proofgold the corresponding term root is 2b8e3b... and proposition id is 2f244c...
Proof:
Let L and R be given.
Assume HLR.
We will prove PNoLt_pwise (PNo_downc L) (PNo_upc R).
Let gamma be given.
Assume Hc.
Let p be given.
Assume Hp.
Let delta be given.
Assume Hd.
Let q be given.
Assume Hq.
Apply Hp to the current goal.
Let alpha be given.
Assume H1.
Apply H1 to the current goal.
Assume H2: ordinal alpha.
Assume H3.
Apply H3 to the current goal.
Let p2 be given.
Assume H3.
Apply H3 to the current goal.
Assume H4: L alpha p2.
Assume H5: PNoLe gamma p alpha p2.
Apply Hq to the current goal.
Let beta be given.
Assume H6.
Apply H6 to the current goal.
Assume H7: ordinal beta.
Assume H8.
Apply H8 to the current goal.
Let q2 be given.
Assume H9.
Apply H9 to the current goal.
Assume H10: R beta q2.
Assume H11: PNoLe beta q2 delta q.
We prove the intermediate claim L1: PNoLt gamma p delta q.
Apply PNoLeLt_tra gamma alpha delta Hc H2 Hd p p2 q H5 to the current goal.
We will prove PNoLt alpha p2 delta q.
Apply PNoLtLe_tra alpha beta delta H2 H7 Hd p2 q2 q (HLR alpha H2 p2 H4 beta H7 q2 H10) to the current goal.
We will prove PNoLe beta q2 delta q.
An exact proof term for the current goal is H11.
Apply PNoLt_trichotomy_or delta gamma q p Hd Hc to the current goal.
Assume H12.
Apply H12 to the current goal.
Assume H12: PNoLt delta q gamma p.
Apply PNoLt_irref gamma p to the current goal.
We will prove PNoLt gamma p gamma p.
Apply PNoLt_tra gamma delta gamma Hc Hd Hc p q p L1 to the current goal.
An exact proof term for the current goal is H12.
Assume H12: delta = gamma ∧ PNoEq_ delta q p.
Apply PNoLt_irref delta q to the current goal.
We will prove PNoLt delta q delta q.
Apply PNoLeLt_tra delta gamma delta Hd Hc Hd q p q to the current goal.
We will prove PNoLe delta q gamma p.
We will prove PNoLt delta q gamma p ∨ delta = gamma ∧ PNoEq_ delta q p.
Apply orIR to the current goal.
An exact proof term for the current goal is H12.
We will prove PNoLt gamma p delta q.
An exact proof term for the current goal is L1.
Assume H12: PNoLt gamma p delta q.
An exact proof term for the current goal is H12.
∎
Definition. We define PNo_rel_strict_upperbd to be λL alpha p ⇒ ∀beta ∈ alpha, ∀q : set → prop, PNo_downc L beta q → PNoLt beta q alpha p of type (set → (set → prop) → prop) → set → (set → prop) → prop.
In Proofgold the corresponding term root is dc1665... and object id is 3e1663...
Definition. We define PNo_rel_strict_lowerbd to be λR alpha p ⇒ ∀beta ∈ alpha, ∀q : set → prop, PNo_upc R beta q → PNoLt alpha p beta q of type (set → (set → prop) → prop) → set → (set → prop) → prop.
In Proofgold the corresponding term root is e5a4b6... and object id is ff3150...
Definition. We define PNo_rel_strict_imv to be λL R alpha p ⇒ PNo_rel_strict_upperbd L alpha p ∧ PNo_rel_strict_lowerbd R alpha p of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → set → (set → prop) → prop.
In Proofgold the corresponding term root is 64ce99... and object id is 5b35fb...
Theorem. (PNoEq_rel_strict_upperbd) The following is provable:
∀L : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p q : set → prop, PNoEq_ alpha p q → PNo_rel_strict_upperbd L alpha p → PNo_rel_strict_upperbd L alpha q
In Proofgold the corresponding term root is bb65cf... and proposition id is db4b82...
Proof:
Let L and alpha be given.
Assume Ha.
Let p and q be given.
Assume Hpq: PNoEq_ alpha p q.
Assume H1: PNo_rel_strict_upperbd L alpha p.
We will prove PNo_rel_strict_upperbd L alpha q.
Let beta be given.
Assume Hb: beta ∈ alpha.
Let r be given.
Assume H2: PNo_downc L beta r.
We prove the intermediate claim Lb: ordinal beta.
An exact proof term for the current goal is ordinal_Hered alpha Ha beta Hb.
We will prove PNoLt beta r alpha q.
Apply PNoLtEq_tra beta alpha Lb Ha r p q to the current goal.
We will prove PNoLt beta r alpha p.
An exact proof term for the current goal is H1 beta Hb r H2.
We will prove PNoEq_ alpha p q.
An exact proof term for the current goal is Hpq.
∎
Theorem. (PNo_rel_strict_upperbd_antimon) The following is provable:
∀L : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p : set → prop, ∀beta ∈ alpha, PNo_rel_strict_upperbd L alpha p → PNo_rel_strict_upperbd L beta p
In Proofgold the corresponding term root is 9986af... and proposition id is ed53da...
Proof:
Let L and alpha be given.
Assume Ha.
Let p and beta be given.
Assume Hb.
Apply Ha to the current goal.
Assume Ha1 _.
We prove the intermediate claim Lb: ordinal beta.
An exact proof term for the current goal is ordinal_Hered alpha Ha beta Hb.
We prove the intermediate claim Lbt: TransSet beta.
Apply Lb to the current goal.
Assume H2 _.
An exact proof term for the current goal is H2.
Assume H1: ∀gamma ∈ alpha, ∀q : set → prop, PNo_downc L gamma q → PNoLt gamma q alpha p.
We will prove ∀gamma ∈ beta, ∀q : set → prop, PNo_downc L gamma q → PNoLt gamma q beta p.
Let gamma be given.
Assume Hc.
Let q be given.
Assume H4.
We will prove PNoLt gamma q beta p.
We prove the intermediate claim Lca: gamma ∈ alpha.
An exact proof term for the current goal is Ha1 beta Hb gamma Hc.
We prove the intermediate claim L1: PNoLt gamma q alpha p.
Apply H1 to the current goal.
We will prove gamma ∈ alpha.
An exact proof term for the current goal is Lca.
We will prove PNo_downc L gamma q.
An exact proof term for the current goal is H4.
Apply PNoLtE gamma alpha q p L1 to the current goal.
Assume H5: PNoLt_ (gamma ∩ alpha) q p.
We prove the intermediate claim L2: gamma ∩ alpha = gamma.
Apply binintersect_Subq_eq_1 to the current goal.
An exact proof term for the current goal is Ha1 gamma Lca.
We prove the intermediate claim L3: gamma ∩ beta = gamma.
Apply binintersect_Subq_eq_1 to the current goal.
An exact proof term for the current goal is Lbt gamma Hc.
Apply PNoLtI1 to the current goal.
rewrite the current goal using L3 (from left to right).
rewrite the current goal using L2 (from right to left).
An exact proof term for the current goal is H5.
Assume H5: gamma ∈ alpha.
Assume H6: PNoEq_ gamma q p.
Assume H7: p gamma.
Apply PNoLtI2 to the current goal.
We will prove gamma ∈ beta.
An exact proof term for the current goal is Hc.
We will prove PNoEq_ gamma q p.
An exact proof term for the current goal is H6.
We will prove p gamma.
An exact proof term for the current goal is H7.
Assume H5: alpha ∈ gamma.
We will prove False.
An exact proof term for the current goal is In_no2cycle alpha gamma H5 Lca.
∎
Theorem. (PNoEq_rel_strict_lowerbd) The following is provable:
∀R : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p q : set → prop, PNoEq_ alpha p q → PNo_rel_strict_lowerbd R alpha p → PNo_rel_strict_lowerbd R alpha q
In Proofgold the corresponding term root is 76080e... and proposition id is 614e58...
Proof:
Let R and alpha be given.
Assume Ha.
Let p and q be given.
Assume Hpq: PNoEq_ alpha p q.
Assume H1: PNo_rel_strict_lowerbd R alpha p.
We will prove PNo_rel_strict_lowerbd R alpha q.
Let beta be given.
Assume Hb: beta ∈ alpha.
Let r be given.
Assume H2: PNo_upc R beta r.
We prove the intermediate claim Lb: ordinal beta.
An exact proof term for the current goal is ordinal_Hered alpha Ha beta Hb.
We will prove PNoLt alpha q beta r.
Apply PNoEqLt_tra alpha beta Ha Lb q p r to the current goal.
We will prove PNoEq_ alpha q p.
Apply PNoEq_sym_ to the current goal.
An exact proof term for the current goal is Hpq.
We will prove PNoLt alpha p beta r.
An exact proof term for the current goal is H1 beta Hb r H2.
∎
Theorem. (PNo_rel_strict_lowerbd_antimon) The following is provable:
∀R : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p : set → prop, ∀beta ∈ alpha, PNo_rel_strict_lowerbd R alpha p → PNo_rel_strict_lowerbd R beta p
In Proofgold the corresponding term root is 27f253... and proposition id is 344b63...
Proof:
Let R and alpha be given.
Assume Ha.
Let p and beta be given.
Assume Hb.
Apply Ha to the current goal.
Assume Ha1 _.
We prove the intermediate claim Lb: ordinal beta.
An exact proof term for the current goal is ordinal_Hered alpha Ha beta Hb.
We prove the intermediate claim Lbt: TransSet beta.
Apply Lb to the current goal.
Assume H2 _.
An exact proof term for the current goal is H2.
Assume H1: ∀gamma ∈ alpha, ∀q : set → prop, PNo_upc R gamma q → PNoLt alpha p gamma q.
We will prove ∀gamma ∈ beta, ∀q : set → prop, PNo_upc R gamma q → PNoLt beta p gamma q.
Let gamma be given.
Assume Hc.
Let q be given.
Assume H4.
We will prove PNoLt beta p gamma q.
We prove the intermediate claim Lca: gamma ∈ alpha.
An exact proof term for the current goal is Ha1 beta Hb gamma Hc.
We prove the intermediate claim L1: PNoLt alpha p gamma q.
Apply H1 to the current goal.
We will prove gamma ∈ alpha.
An exact proof term for the current goal is Lca.
We will prove PNo_upc R gamma q.
An exact proof term for the current goal is H4.
Apply PNoLtE alpha gamma p q L1 to the current goal.
Assume H5: PNoLt_ (alpha ∩ gamma) p q.
We prove the intermediate claim L2: alpha ∩ gamma = gamma.
rewrite the current goal using binintersect_com (from left to right).
Apply binintersect_Subq_eq_1 to the current goal.
An exact proof term for the current goal is Ha1 gamma Lca.
We prove the intermediate claim L3: beta ∩ gamma = gamma.
rewrite the current goal using binintersect_com (from left to right).
Apply binintersect_Subq_eq_1 to the current goal.
An exact proof term for the current goal is Lbt gamma Hc.
Apply PNoLtI1 to the current goal.
rewrite the current goal using L3 (from left to right).
rewrite the current goal using L2 (from right to left).
An exact proof term for the current goal is H5.
Assume H5: alpha ∈ gamma.
We will prove False.
An exact proof term for the current goal is In_no2cycle alpha gamma H5 Lca.
Assume H5: gamma ∈ alpha.
Assume H6: PNoEq_ gamma p q.
Assume H7: ¬ p gamma.
Apply PNoLtI3 to the current goal.
We will prove gamma ∈ beta.
An exact proof term for the current goal is Hc.
We will prove PNoEq_ gamma p q.
An exact proof term for the current goal is H6.
We will prove ¬ p gamma.
An exact proof term for the current goal is H7.
∎
Theorem. (PNoEq_rel_strict_imv) The following is provable:
∀L R : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p q : set → prop, PNoEq_ alpha p q → PNo_rel_strict_imv L R alpha p → PNo_rel_strict_imv L R alpha q
In Proofgold the corresponding term root is e3f251... and proposition id is 7ae13d...
Proof:
Let L, R and alpha be given.
Assume Ha.
Let p and q be given.
Assume Hpq H1.
Apply H1 to the current goal.
Assume H2 H3.
We will prove PNo_rel_strict_upperbd L alpha q ∧ PNo_rel_strict_lowerbd R alpha q.
Apply andI to the current goal.
An exact proof term for the current goal is PNoEq_rel_strict_upperbd L alpha Ha p q Hpq H2.
An exact proof term for the current goal is PNoEq_rel_strict_lowerbd R alpha Ha p q Hpq H3.
∎
Theorem. (PNo_rel_strict_imv_antimon) The following is provable:
∀L R : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p : set → prop, ∀beta ∈ alpha, PNo_rel_strict_imv L R alpha p → PNo_rel_strict_imv L R beta p
In Proofgold the corresponding term root is 2434dc... and proposition id is 87e0ce...
Proof:
Let L, R and alpha be given.
Assume Ha.
Let p and beta be given.
Assume Hb H1.
Apply H1 to the current goal.
Assume H2 H3.
We will prove PNo_rel_strict_upperbd L beta p ∧ PNo_rel_strict_lowerbd R beta p.
Apply andI to the current goal.
An exact proof term for the current goal is PNo_rel_strict_upperbd_antimon L alpha Ha p beta Hb H2.
An exact proof term for the current goal is PNo_rel_strict_lowerbd_antimon R alpha Ha p beta Hb H3.
∎
Definition. We define PNo_rel_strict_uniq_imv to be λL R alpha p ⇒ PNo_rel_strict_imv L R alpha p ∧ ∀q : set → prop, PNo_rel_strict_imv L R alpha q → PNoEq_ alpha p q of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → set → (set → prop) → prop.
In Proofgold the corresponding term root is 23c9d9... and object id is 56ed1b...
Definition. We define PNo_rel_strict_split_imv to be λL R alpha p ⇒ PNo_rel_strict_imv L R (ordsucc alpha) (λdelta ⇒ p delta ∧ delta ≠ alpha) ∧ PNo_rel_strict_imv L R (ordsucc alpha) (λdelta ⇒ p delta ∨ delta = alpha) of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → set → (set → prop) → prop.
In Proofgold the corresponding term root is 217d17... and object id is dd9cee...
Theorem. (PNo_extend0_eq) The following is provable:
∀alpha, ∀p : set → prop, PNoEq_ alpha p (λdelta ⇒ p delta ∧ delta ≠ alpha)
In Proofgold the corresponding term root is 2d441e... and proposition id is 5ed08e...
Proof:
Let alpha and p be given.
Set p0 to be the term λdelta ⇒ p delta ∧ delta ≠ alpha of type set → prop.
Let beta be given.
Assume Hb: beta ∈ alpha.
We will prove p beta ↔ p0 beta.
Apply iffI to the current goal.
Assume H1: p beta.
We will prove p beta ∧ beta ≠ alpha.
Apply andI to the current goal.
An exact proof term for the current goal is H1.
We will prove beta ≠ alpha.
Assume H2: beta = alpha.
Apply In_irref alpha to the current goal.
rewrite the current goal using H2 (from right to left) at position 1.
An exact proof term for the current goal is Hb.
Assume H1: p0 beta.
Apply H1 to the current goal.
Assume H2 _.
An exact proof term for the current goal is H2.
∎
Theorem. (PNo_extend1_eq) The following is provable:
∀alpha, ∀p : set → prop, PNoEq_ alpha p (λdelta ⇒ p delta ∨ delta = alpha)
In Proofgold the corresponding term root is 8eb99c... and proposition id is 4cac1a...
Proof:
Let alpha and p be given.
Set p1 to be the term λdelta ⇒ p delta ∨ delta = alpha of type set → prop.
Let beta be given.
Assume Hb: beta ∈ alpha.
We will prove p beta ↔ p1 beta.
Apply iffI to the current goal.
Assume H1: p beta.
We will prove p beta ∨ beta = alpha.
Apply orIL to the current goal.
An exact proof term for the current goal is H1.
Assume H1: p1 beta.
Apply H1 to the current goal.
Assume H2: p beta.
An exact proof term for the current goal is H2.
Assume H2: beta = alpha.
We will prove False.
Apply In_irref alpha to the current goal.
rewrite the current goal using H2 (from right to left) at position 1.
An exact proof term for the current goal is Hb.
∎
Theorem. (PNo_rel_imv_ex) The following is provable:
∀L R : set → (set → prop) → prop, PNoLt_pwise L R → ∀alpha, ordinal alpha → (∃p : set → prop, PNo_rel_strict_uniq_imv L R alpha p) ∨ (∃tau ∈ alpha, ∃p : set → prop, PNo_rel_strict_split_imv L R tau p)
In Proofgold the corresponding term root is 3e3224... and proposition id is 749b63...
Proof:
Let L and R be given.
Assume HLR.
We prove the intermediate claim LLR: PNoLt_pwise (PNo_downc L) (PNo_upc R).
An exact proof term for the current goal is PNoLt_pwise_downc_upc L R HLR.
Apply ordinal_ind to the current goal.
Let alpha be given.
Assume Ha.
Apply Ha to the current goal.
Assume Ha1 _.
Assume IH: ∀gamma ∈ alpha, (∃p : set → prop, PNo_rel_strict_uniq_imv L R gamma p) ∨ (∃tau ∈ gamma, ∃p : set → prop, PNo_rel_strict_split_imv L R tau p).
Apply dneg to the current goal.
Assume HNC: ¬ ((∃p : set → prop, PNo_rel_strict_uniq_imv L R alpha p) ∨ (∃tau ∈ alpha, ∃p : set → prop, PNo_rel_strict_split_imv L R tau p)).
Apply not_or_and_demorgan (∃p : set → prop, PNo_rel_strict_uniq_imv L R alpha p) (∃tau ∈ alpha, ∃p : set → prop, PNo_rel_strict_split_imv L R tau p) HNC to the current goal.
Assume HNC1: ¬ (∃p : set → prop, PNo_rel_strict_uniq_imv L R alpha p).
Assume HNC2: ¬ (∃tau ∈ alpha, ∃p : set → prop, PNo_rel_strict_split_imv L R tau p).
We prove the intermediate claim LIH: ∀gamma ∈ alpha, ∃p : set → prop, PNo_rel_strict_uniq_imv L R gamma p.
Let gamma be given.
Assume Hc: gamma ∈ alpha.
Apply IH gamma Hc to the current goal.
Assume H1.
An exact proof term for the current goal is H1.
Assume H1: ∃tau ∈ gamma, ∃p : set → prop, PNo_rel_strict_split_imv L R tau p.
Apply H1 to the current goal.
Let tau be given.
Assume H2.
Apply H2 to the current goal.
Assume Ht: tau ∈ gamma.
Assume H2.
Apply H2 to the current goal.
Let p be given.
Assume H3: PNo_rel_strict_split_imv L R tau p.
Apply HNC2 to the current goal.
We use tau to witness the existential quantifier.
Apply andI to the current goal.
We will prove tau ∈ alpha.
An exact proof term for the current goal is Ha1 gamma Hc tau Ht.
We use p to witness the existential quantifier.
We will prove PNo_rel_strict_split_imv L R tau p.
An exact proof term for the current goal is H3.
Apply ordinal_lim_or_succ alpha Ha to the current goal.
Assume H1: ∀beta ∈ alpha, ordsucc beta ∈ alpha.
Set pl to be the term λdelta ⇒ ∀p : set → prop, PNo_rel_strict_imv L R (ordsucc delta) p → p delta of type set → prop.
We prove the intermediate claim Lpl1: ∀gamma, ordinal gamma → gamma ∈ alpha → PNo_rel_strict_uniq_imv L R gamma pl.
Apply ordinal_ind to the current goal.
Let gamma be given.
Assume Hc: ordinal gamma.
Assume IH2: ∀delta ∈ gamma, delta ∈ alpha → PNo_rel_strict_uniq_imv L R delta pl.
Assume Hc1: gamma ∈ alpha.
Apply LIH gamma Hc1 to the current goal.
Let p be given.
Assume Hp.
Apply Hp to the current goal.
Assume Hp1: PNo_rel_strict_imv L R gamma p.
Apply Hp1 to the current goal.
Assume Hp1a Hp1b.
Assume Hp2: ∀q : set → prop, PNo_rel_strict_imv L R gamma q → PNoEq_ gamma p q.
We prove the intermediate claim Lplpe: PNoEq_ gamma pl p.
Let delta be given.
Assume Hd: delta ∈ gamma.
Apply ordinal_ordsucc_In_eq gamma delta Hc Hd to the current goal.
Assume Hsd: ordsucc delta ∈ gamma.
We prove the intermediate claim Lsda: ordsucc delta ∈ alpha.
An exact proof term for the current goal is Ha1 gamma Hc1 (ordsucc delta) Hsd.
Apply IH2 (ordsucc delta) Hsd Lsda to the current goal.
Assume Hpl1: PNo_rel_strict_imv L R (ordsucc delta) pl.
Assume Hpl2: ∀q : set → prop, PNo_rel_strict_imv L R (ordsucc delta) q → PNoEq_ (ordsucc delta) pl q.
We will prove pl delta ↔ p delta.
Apply Hpl2 p to the current goal.
We will prove PNo_rel_strict_imv L R (ordsucc delta) p.
An exact proof term for the current goal is PNo_rel_strict_imv_antimon L R gamma Hc p (ordsucc delta) Hsd Hp1.
We will prove delta ∈ ordsucc delta.
Apply ordsuccI2 to the current goal.
Assume Hsd: gamma = ordsucc delta.
We will prove pl delta ↔ p delta.
Apply iffI to the current goal.
Assume H2: pl delta.
We will prove p delta.
Apply H2 p to the current goal.
We will prove PNo_rel_strict_imv L R (ordsucc delta) p.
rewrite the current goal using Hsd (from right to left).
An exact proof term for the current goal is Hp1.
Assume H2: p delta.
Let q be given.
rewrite the current goal using Hsd (from right to left).
Assume Hq: PNo_rel_strict_imv L R gamma q.
We will prove q delta.
An exact proof term for the current goal is iffEL (p delta) (q delta) (Hp2 q Hq delta Hd) H2.
We will prove PNo_rel_strict_uniq_imv L R gamma pl.
We will prove PNo_rel_strict_imv L R gamma pl ∧ ∀q : set → prop, PNo_rel_strict_imv L R gamma q → PNoEq_ gamma pl q.
Apply andI to the current goal.
We will prove PNo_rel_strict_imv L R gamma pl.
We will prove PNo_rel_strict_upperbd L gamma pl ∧ PNo_rel_strict_lowerbd R gamma pl.
Apply andI to the current goal.
We will prove PNo_rel_strict_upperbd L gamma pl.
Let beta be given.
Assume Hb: beta ∈ gamma.
Let q be given.
Assume Hq: PNo_downc L beta q.
We prove the intermediate claim Lb: ordinal beta.
An exact proof term for the current goal is ordinal_Hered gamma Hc beta Hb.
We will prove PNoLt beta q gamma pl.
Apply PNoLtEq_tra beta gamma Lb Hc q p pl to the current goal.
We will prove PNoLt beta q gamma p.
An exact proof term for the current goal is Hp1a beta Hb q Hq.
We will prove PNoEq_ gamma p pl.
Apply PNoEq_sym_ to the current goal.
An exact proof term for the current goal is Lplpe.
We will prove PNo_rel_strict_lowerbd R gamma pl.
Let beta be given.
Assume Hb: beta ∈ gamma.
Let q be given.
Assume Hq: PNo_upc R beta q.
We prove the intermediate claim Lb: ordinal beta.
An exact proof term for the current goal is ordinal_Hered gamma Hc beta Hb.
We will prove PNoLt gamma pl beta q.
Apply PNoEqLt_tra gamma beta Hc Lb pl p q to the current goal.
We will prove PNoEq_ gamma pl p.
An exact proof term for the current goal is Lplpe.
We will prove PNoLt gamma p beta q.
An exact proof term for the current goal is Hp1b beta Hb q Hq.
We will prove ∀q : set → prop, PNo_rel_strict_imv L R gamma q → PNoEq_ gamma pl q.
Let q be given.
Assume Hq: PNo_rel_strict_imv L R gamma q.
We will prove PNoEq_ gamma pl q.
Apply PNoEq_tra_ gamma pl p q to the current goal.
We will prove PNoEq_ gamma pl p.
An exact proof term for the current goal is Lplpe.
We will prove PNoEq_ gamma p q.
An exact proof term for the current goal is Hp2 q Hq.
We prove the intermediate claim Lpl2: ∀gamma ∈ alpha, PNo_rel_strict_uniq_imv L R gamma pl.
Let gamma be given.
Assume Hc: gamma ∈ alpha.
We prove the intermediate claim Lc: ordinal gamma.
An exact proof term for the current goal is ordinal_Hered alpha Ha gamma Hc.
An exact proof term for the current goal is Lpl1 gamma Lc Hc.
Apply HNC1 to the current goal.
We use pl to witness the existential quantifier.
We will prove PNo_rel_strict_uniq_imv L R alpha pl.
We will prove PNo_rel_strict_imv L R alpha pl ∧ ∀q : set → prop, PNo_rel_strict_imv L R alpha q → PNoEq_ alpha pl q.
Apply andI to the current goal.
We will prove PNo_rel_strict_imv L R alpha pl.
We will prove PNo_rel_strict_upperbd L alpha pl ∧ PNo_rel_strict_lowerbd R alpha pl.
Apply andI to the current goal.
We will prove PNo_rel_strict_upperbd L alpha pl.
Let beta be given.
Assume Hb: beta ∈ alpha.
Let q be given.
Assume Hq: PNo_downc L beta q.
We prove the intermediate claim Lb: ordinal beta.
An exact proof term for the current goal is ordinal_Hered alpha Ha beta Hb.
We prove the intermediate claim Lsb: ordinal (ordsucc beta).
An exact proof term for the current goal is ordinal_ordsucc beta Lb.
We will prove PNoLt beta q alpha pl.
Apply PNoLt_trichotomy_or beta alpha q pl Lb Ha to the current goal.
Assume H2.
Apply H2 to the current goal.
Assume H2: PNoLt beta q alpha pl.
An exact proof term for the current goal is H2.
Assume H2.
Apply H2 to the current goal.
Assume H2: beta = alpha.
We will prove False.
Apply In_irref alpha to the current goal.
rewrite the current goal using H2 (from right to left) at position 1.
An exact proof term for the current goal is Hb.
Assume H2: PNoLt alpha pl beta q.
Apply PNoLtE alpha beta pl q H2 to the current goal.
Assume H3: PNoLt_ (alpha ∩ beta) pl q.
Apply H3 to the current goal.
Let gamma be given.
Assume H4.
Apply H4 to the current goal.
Assume Hc: gamma ∈ alpha ∩ beta.
Apply binintersectE alpha beta gamma Hc to the current goal.
Assume Hc1 Hc2.
Assume H5.
Apply H5 to the current goal.
Assume H5.
Apply H5 to the current goal.
Assume H5: PNoEq_ gamma pl q.
Assume H6: ¬ pl gamma.
Assume H7: q gamma.
We prove the intermediate claim Lc: ordinal gamma.
An exact proof term for the current goal is ordinal_Hered beta Lb gamma Hc2.
We prove the intermediate claim Lsc: ordinal (ordsucc gamma).
An exact proof term for the current goal is ordinal_ordsucc gamma Lc.
We will prove False.
Apply H6 to the current goal.
We will prove pl gamma.
Let p be given.
Assume Hp: PNo_rel_strict_imv L R (ordsucc gamma) p.
We will prove p gamma.
Apply Hp to the current goal.
Assume Hp1 Hp2.
We prove the intermediate claim Lqp: PNoLt gamma q (ordsucc gamma) p.
Apply Hp1 gamma (ordsuccI2 gamma) q to the current goal.
We will prove PNo_downc L gamma q.
Apply PNoLe_downc L beta gamma q q Lb Lc to the current goal.
We will prove PNo_downc L beta q.
An exact proof term for the current goal is Hq.
We will prove PNoLe gamma q beta q.
Apply PNoLeI1 to the current goal.
We will prove PNoLt gamma q beta q.
Apply PNoLtI2 to the current goal.
We will prove gamma ∈ beta.
An exact proof term for the current goal is Hc2.
We will prove PNoEq_ gamma q q.
Apply PNoEq_ref_ to the current goal.
We will prove q gamma.
An exact proof term for the current goal is H7.
Apply PNoLtE gamma (ordsucc gamma) q p Lqp to the current goal.
Assume H6: PNoLt_ (gamma ∩ ordsucc gamma) q p.
Apply H6 to the current goal.
Let delta be given.
Assume H7.
Apply H7 to the current goal.
Assume Hd: delta ∈ gamma ∩ ordsucc gamma.
Apply binintersectE gamma (ordsucc gamma) delta Hd to the current goal.
Assume Hd1 Hd2.
Assume H7.
Apply H7 to the current goal.
Assume H7.
Apply H7 to the current goal.
Assume H7: PNoEq_ delta q p.
Assume H8: ¬ q delta.
Assume H9: p delta.
We prove the intermediate claim Ld: ordinal delta.
An exact proof term for the current goal is ordinal_Hered gamma Lc delta Hd1.
We prove the intermediate claim Lda: delta ∈ alpha.
An exact proof term for the current goal is Ha1 gamma Hc1 delta Hd1.
We prove the intermediate claim Lsda: ordsucc delta ∈ alpha.
An exact proof term for the current goal is H1 delta Lda.
We prove the intermediate claim Lpld: pl delta.
Apply Lpl2 (ordsucc delta) Lsda to the current goal.
Assume _.
Assume Hpl3: ∀q : set → prop, PNo_rel_strict_imv L R (ordsucc delta) q → PNoEq_ (ordsucc delta) pl q.
We prove the intermediate claim Lpld1: PNoEq_ (ordsucc delta) pl p.
Apply Hpl3 p to the current goal.
We will prove PNo_rel_strict_imv L R (ordsucc delta) p.
Apply PNo_rel_strict_imv_antimon L R (ordsucc gamma) Lsc p to the current goal.
We will prove ordsucc delta ∈ ordsucc gamma.
Apply ordinal_ordsucc_In to the current goal.
An exact proof term for the current goal is Lc.
We will prove delta ∈ gamma.
An exact proof term for the current goal is Hd1.
An exact proof term for the current goal is Hp.
An exact proof term for the current goal is iffER (pl delta) (p delta) (Lpld1 delta (ordsuccI2 delta)) H9.
We prove the intermediate claim Lnpld: ¬ pl delta.
Assume H10: pl delta.
Apply H8 to the current goal.
An exact proof term for the current goal is iffEL (pl delta) (q delta) (H5 delta Hd1) H10.
We will prove False.
An exact proof term for the current goal is Lnpld Lpld.
Assume H6: gamma ∈ ordsucc gamma.
Assume H7: PNoEq_ gamma q p.
Assume H8: p gamma.
An exact proof term for the current goal is H8.
Assume H6: ordsucc gamma ∈ gamma.
We will prove False.
An exact proof term for the current goal is In_no2cycle gamma (ordsucc gamma) (ordsuccI2 gamma) H6.
Assume H3: alpha ∈ beta.
We will prove False.
An exact proof term for the current goal is In_no2cycle beta alpha Hb H3.
Assume H3: beta ∈ alpha.
Assume H4: PNoEq_ beta pl q.
Assume H5: ¬ pl beta.
We will prove False.
Apply H5 to the current goal.
We will prove pl beta.
Let p be given.
Assume Hp: PNo_rel_strict_imv L R (ordsucc beta) p.
We will prove p beta.
Apply Hp to the current goal.
Assume Hp1 Hp2.
We prove the intermediate claim Lqp: PNoLt beta q (ordsucc beta) p.
An exact proof term for the current goal is Hp1 beta (ordsuccI2 beta) q Hq.
Apply PNoLtE beta (ordsucc beta) q p Lqp to the current goal.
Assume H6: PNoLt_ (beta ∩ ordsucc beta) q p.
Apply H6 to the current goal.
Let delta be given.
Assume H7.
Apply H7 to the current goal.
Assume Hd: delta ∈ beta ∩ ordsucc beta.
Apply binintersectE beta (ordsucc beta) delta Hd to the current goal.
Assume Hd1 Hd2.
Assume H7.
Apply H7 to the current goal.
Assume H7.
Apply H7 to the current goal.
Assume H7: PNoEq_ delta q p.
Assume H8: ¬ q delta.
Assume H9: p delta.
We prove the intermediate claim Ld: ordinal delta.
An exact proof term for the current goal is ordinal_Hered beta Lb delta Hd1.
We prove the intermediate claim Lda: delta ∈ alpha.
An exact proof term for the current goal is Ha1 beta Hb delta Hd1.
We prove the intermediate claim Lsda: ordsucc delta ∈ alpha.
An exact proof term for the current goal is H1 delta Lda.
We prove the intermediate claim Lpld: pl delta.
Apply Lpl2 (ordsucc delta) Lsda to the current goal.
Assume _.
Assume Hpl3: ∀q : set → prop, PNo_rel_strict_imv L R (ordsucc delta) q → PNoEq_ (ordsucc delta) pl q.
We prove the intermediate claim Lpld1: PNoEq_ (ordsucc delta) pl p.
Apply Hpl3 p to the current goal.
We will prove PNo_rel_strict_imv L R (ordsucc delta) p.
Apply PNo_rel_strict_imv_antimon L R (ordsucc beta) Lsb p to the current goal.
We will prove ordsucc delta ∈ ordsucc beta.
Apply ordinal_ordsucc_In to the current goal.
An exact proof term for the current goal is Lb.
We will prove delta ∈ beta.
An exact proof term for the current goal is Hd1.
An exact proof term for the current goal is Hp.
An exact proof term for the current goal is iffER (pl delta) (p delta) (Lpld1 delta (ordsuccI2 delta)) H9.
We prove the intermediate claim Lnpld: ¬ pl delta.
Assume H10: pl delta.
Apply H8 to the current goal.
An exact proof term for the current goal is iffEL (pl delta) (q delta) (H4 delta Hd1) H10.
We will prove False.
An exact proof term for the current goal is Lnpld Lpld.
Assume H6: beta ∈ ordsucc beta.
Assume H7: PNoEq_ beta q p.
Assume H8: p beta.
An exact proof term for the current goal is H8.
Assume H6: ordsucc beta ∈ beta.
We will prove False.
An exact proof term for the current goal is In_no2cycle beta (ordsucc beta) (ordsuccI2 beta) H6.
We will prove PNo_rel_strict_lowerbd R alpha pl.
Let beta be given.
Assume Hb: beta ∈ alpha.
Let q be given.
Assume Hq: PNo_upc R beta q.
We prove the intermediate claim Lb: ordinal beta.
An exact proof term for the current goal is ordinal_Hered alpha Ha beta Hb.
We prove the intermediate claim Lsb: ordinal (ordsucc beta).
An exact proof term for the current goal is ordinal_ordsucc beta Lb.
We prove the intermediate claim Lsba: ordsucc beta ∈ alpha.
An exact proof term for the current goal is H1 beta Hb.
We will prove PNoLt alpha pl beta q.
Apply PNoLt_trichotomy_or alpha beta pl q Ha Lb to the current goal.
Assume H2.
Apply H2 to the current goal.
Assume H2: PNoLt alpha pl beta q.
An exact proof term for the current goal is H2.
Assume H2.
Apply H2 to the current goal.
Assume H2: alpha = beta.
We will prove False.
Apply In_irref alpha to the current goal.
rewrite the current goal using H2 (from left to right) at position 1.
An exact proof term for the current goal is Hb.
Assume H2: PNoLt beta q alpha pl.
Apply PNoLtE beta alpha q pl H2 to the current goal.
Assume H3: PNoLt_ (beta ∩ alpha) q pl.
Apply H3 to the current goal.
Let gamma be given.
Assume H4.
Apply H4 to the current goal.
Assume Hc: gamma ∈ beta ∩ alpha.
Apply binintersectE beta alpha gamma Hc to the current goal.
Assume Hc2 Hc1.
Assume H5.
Apply H5 to the current goal.
Assume H5.
Apply H5 to the current goal.
Assume H5: PNoEq_ gamma q pl.
Assume H6: ¬ q gamma.
Assume H7: pl gamma.
We prove the intermediate claim Lc: ordinal gamma.
An exact proof term for the current goal is ordinal_Hered beta Lb gamma Hc2.
We prove the intermediate claim Lsc: ordinal (ordsucc gamma).
An exact proof term for the current goal is ordinal_ordsucc gamma Lc.
We prove the intermediate claim Lsca: ordsucc gamma ∈ alpha.
An exact proof term for the current goal is H1 gamma Hc1.
We will prove False.
Apply Lpl2 (ordsucc gamma) Lsca to the current goal.
Assume Hpl2: PNo_rel_strict_imv L R (ordsucc gamma) pl.
Assume _.
Apply Hpl2 to the current goal.
Assume _.
Assume Hpl2b: PNo_rel_strict_lowerbd R (ordsucc gamma) pl.
We prove the intermediate claim Lplq: PNoLt (ordsucc gamma) pl gamma q.
Apply Hpl2b gamma (ordsuccI2 gamma) q to the current goal.
We will prove PNo_upc R gamma q.
Apply PNoLe_upc R beta gamma q q Lb Lc to the current goal.
We will prove PNo_upc R beta q.
An exact proof term for the current goal is Hq.
We will prove PNoLe beta q gamma q.
Apply PNoLeI1 beta gamma q q to the current goal.
We will prove PNoLt beta q gamma q.
Apply PNoLtI3 to the current goal.
We will prove gamma ∈ beta.
An exact proof term for the current goal is Hc2.
We will prove PNoEq_ gamma q q.
Apply PNoEq_ref_ to the current goal.
We will prove ¬ q gamma.
An exact proof term for the current goal is H6.
We prove the intermediate claim Lqpl: PNoLt gamma q (ordsucc gamma) pl.
Apply PNoLtI2 to the current goal.
We will prove gamma ∈ ordsucc gamma.
Apply ordsuccI2 to the current goal.
We will prove PNoEq_ gamma q pl.
An exact proof term for the current goal is H5.
We will prove pl gamma.
An exact proof term for the current goal is H7.
We will prove False.
Apply PNoLt_irref gamma q to the current goal.
An exact proof term for the current goal is PNoLt_tra gamma (ordsucc gamma) gamma Lc Lsc Lc q pl q Lqpl Lplq.
Assume H3: beta ∈ alpha.
Assume H4: PNoEq_ beta q pl.
Assume H5: pl beta.
Apply Lpl2 (ordsucc beta) Lsba to the current goal.
Assume Hpl2: PNo_rel_strict_imv L R (ordsucc beta) pl.
Assume _.
Apply Hpl2 to the current goal.
Assume _.
Assume Hpl2b: PNo_rel_strict_lowerbd R (ordsucc beta) pl.
We prove the intermediate claim Lplq: PNoLt (ordsucc beta) pl beta q.
Apply Hpl2b beta (ordsuccI2 beta) q to the current goal.
We will prove PNo_upc R beta q.
An exact proof term for the current goal is Hq.
We prove the intermediate claim Lqpl: PNoLt beta q (ordsucc beta) pl.
Apply PNoLtI2 to the current goal.
We will prove beta ∈ ordsucc beta.
Apply ordsuccI2 to the current goal.
We will prove PNoEq_ beta q pl.
An exact proof term for the current goal is H4.
We will prove pl beta.
An exact proof term for the current goal is H5.
We will prove False.
Apply PNoLt_irref beta q to the current goal.
An exact proof term for the current goal is PNoLt_tra beta (ordsucc beta) beta Lb Lsb Lb q pl q Lqpl Lplq.
Assume H3: alpha ∈ beta.
We will prove False.
An exact proof term for the current goal is In_no2cycle beta alpha Hb H3.
We will prove ∀q : set → prop, PNo_rel_strict_imv L R alpha q → PNoEq_ alpha pl q.
Let q be given.
Assume Hq: PNo_rel_strict_imv L R alpha q.
Let gamma be given.
Assume Hc: gamma ∈ alpha.
We will prove pl gamma ↔ q gamma.
We prove the intermediate claim Lsca: ordsucc gamma ∈ alpha.
An exact proof term for the current goal is H1 gamma Hc.
Apply Lpl2 (ordsucc gamma) Lsca to the current goal.
Assume _.
Assume Hpl3: ∀q : set → prop, PNo_rel_strict_imv L R (ordsucc gamma) q → PNoEq_ (ordsucc gamma) pl q.
Apply Hpl3 to the current goal.
We will prove PNo_rel_strict_imv L R (ordsucc gamma) q.
An exact proof term for the current goal is PNo_rel_strict_imv_antimon L R alpha Ha q (ordsucc gamma) Lsca Hq.
We will prove gamma ∈ ordsucc gamma.
Apply ordsuccI2 to the current goal.
Assume H1: ∃beta ∈ alpha, alpha = ordsucc beta.
Apply H1 to the current goal.
Let beta be given.
Assume H1.
Apply H1 to the current goal.
Assume Hb: beta ∈ alpha.
Assume Hab: alpha = ordsucc beta.
We prove the intermediate claim Lb: ordinal beta.
An exact proof term for the current goal is ordinal_Hered alpha Ha beta Hb.
We prove the intermediate claim Lsb: ordinal (ordsucc beta).
rewrite the current goal using Hab (from right to left).
An exact proof term for the current goal is Ha.
We prove the intermediate claim Lbsb1: beta ∩ ordsucc beta = beta.
Apply binintersect_Subq_eq_1 to the current goal.
Apply ordsuccI1 to the current goal.
We prove the intermediate claim Lbsb2: ordsucc beta ∩ beta = beta.
rewrite the current goal using binintersect_com (from left to right).
An exact proof term for the current goal is Lbsb1.
Apply LIH beta Hb to the current goal.
Let p be given.
Assume Hp: PNo_rel_strict_uniq_imv L R beta p.
Apply Hp to the current goal.
Assume Hp0: PNo_rel_strict_imv L R beta p.
Apply Hp0 to the current goal.
Assume Hp1: ∀gamma ∈ beta, ∀q : set → prop, PNo_downc L gamma q → PNoLt gamma q beta p.
Assume Hp2: ∀gamma ∈ beta, ∀q : set → prop, PNo_upc R gamma q → PNoLt beta p gamma q.
Assume Hp3: ∀q : set → prop, PNo_rel_strict_imv L R beta q → PNoEq_ beta p q.
Set p0 to be the term λdelta ⇒ p delta ∧ delta ≠ beta of type set → prop.
Set p1 to be the term λdelta ⇒ p delta ∨ delta = beta of type set → prop.
We prove the intermediate claim Lp0e: PNoEq_ beta p0 p.
Let gamma be given.
Assume Hc: gamma ∈ beta.
We will prove p0 gamma ↔ p gamma.
Apply iffI to the current goal.
Assume H2: p gamma ∧ gamma ≠ beta.
We will prove p gamma.
Apply H2 to the current goal.
Assume H2 _.
An exact proof term for the current goal is H2.
Assume H2: p gamma.
We will prove p gamma ∧ gamma ≠ beta.
Apply andI to the current goal.
An exact proof term for the current goal is H2.
Assume H3: gamma = beta.
Apply In_irref beta to the current goal.
rewrite the current goal using H3 (from right to left) at position 1.
An exact proof term for the current goal is Hc.
We prove the intermediate claim Lp0b: ¬ p0 beta.
Assume H2: p beta ∧ beta ≠ beta.
Apply H2 to the current goal.
Assume _ H2.
Apply H2 to the current goal.
Use reflexivity.
We prove the intermediate claim Lp0p: PNoLt (ordsucc beta) p0 beta p.
Apply PNoLtI3 to the current goal.
We will prove beta ∈ ordsucc beta.
Apply ordsuccI2 to the current goal.
We will prove PNoEq_ beta p0 p.
An exact proof term for the current goal is Lp0e.
We will prove ¬ p0 beta.
An exact proof term for the current goal is Lp0b.
We prove the intermediate claim Lp1e: PNoEq_ beta p p1.
Let gamma be given.
Assume Hc: gamma ∈ beta.
We will prove p gamma ↔ p1 gamma.
Apply iffI to the current goal.
Assume H2: p gamma.
We will prove p gamma ∨ gamma = beta.
Apply orIL to the current goal.
An exact proof term for the current goal is H2.
Assume H2: p gamma ∨ gamma = beta.
We will prove p gamma.
Apply H2 to the current goal.
Assume H3: p gamma.
An exact proof term for the current goal is H3.
Assume H3: gamma = beta.
We will prove False.
Apply In_irref beta to the current goal.
rewrite the current goal using H3 (from right to left) at position 1.
An exact proof term for the current goal is Hc.
We prove the intermediate claim Lp1b: p1 beta.
We will prove p beta ∨ beta = beta.
Apply orIR to the current goal.
Use reflexivity.
We prove the intermediate claim Lpp1: PNoLt beta p (ordsucc beta) p1.
Apply PNoLtI2 to the current goal.
We will prove beta ∈ ordsucc beta.
Apply ordsuccI2 to the current goal.
We will prove PNoEq_ beta p p1.
An exact proof term for the current goal is Lp1e.
We will prove p1 beta.
An exact proof term for the current goal is Lp1b.
We prove the intermediate claim Lnotboth: ¬ (PNo_rel_strict_imv L R alpha p0 ∧ PNo_rel_strict_imv L R alpha p1).
rewrite the current goal using Hab (from left to right).
Assume H2.
Apply HNC2 to the current goal.
We use beta to witness the existential quantifier.
Apply andI to the current goal.
We will prove beta ∈ alpha.
An exact proof term for the current goal is Hb.
We use p to witness the existential quantifier.
We will prove PNo_rel_strict_split_imv L R beta p.
An exact proof term for the current goal is H2.
We prove the intermediate claim Lcases: (∀q : set → prop, PNo_downc L beta q → ¬ PNoEq_ beta p q) ∨ (∀q : set → prop, PNo_upc R beta q → ¬ PNoEq_ beta p q).
rewrite the current goal using eq_or_nand (from left to right).
Assume H2.
Apply H2 to the current goal.
Assume H2: ¬ (∀q : set → prop, PNo_downc L beta q → ¬ PNoEq_ beta p q).
Assume H3: ¬ (∀q : set → prop, PNo_upc R beta q → ¬ PNoEq_ beta p q).
Apply H2 to the current goal.
Let q0 be given.
Assume H4: PNo_downc L beta q0.
Assume H5: PNoEq_ beta p q0.
Apply H3 to the current goal.
Let q1 be given.
Assume H6: PNo_upc R beta q1.
Assume H7: PNoEq_ beta p q1.
We prove the intermediate claim L2: PNoLt beta q0 beta q1.
An exact proof term for the current goal is LLR beta Lb q0 H4 beta Lb q1 H6.
Apply PNoLt_irref beta q0 to the current goal.
Apply PNoLtLe_tra beta beta beta Lb Lb Lb q0 q1 q0 L2 to the current goal.
We will prove PNoLe beta q1 beta q0.
We will prove PNoLt beta q1 beta q0 ∨ beta = beta ∧ PNoEq_ beta q1 q0.
Apply orIR to the current goal.
Apply andI to the current goal.
Use reflexivity.
We will prove PNoEq_ beta q1 q0.
Apply PNoEq_tra_ beta q1 p q0 to the current goal.
We will prove PNoEq_ beta q1 p.
Apply PNoEq_sym_ to the current goal.
An exact proof term for the current goal is H7.
We will prove PNoEq_ beta p q0.
An exact proof term for the current goal is H5.
We will prove False.
Apply Lcases to the current goal.
Assume H2: ∀q : set → prop, PNo_downc L beta q → ¬ PNoEq_ beta p q.
We prove the intermediate claim Lp0imv: PNo_rel_strict_imv L R (ordsucc beta) p0.
We will prove PNo_rel_strict_upperbd L (ordsucc beta) p0 ∧ PNo_rel_strict_lowerbd R (ordsucc beta) p0.
Apply andI to the current goal.
Let gamma be given.
Assume Hc: gamma ∈ ordsucc beta.
Let q be given.
Assume H3: PNo_downc L gamma q.
We prove the intermediate claim Lc: ordinal gamma.
An exact proof term for the current goal is ordinal_Hered (ordsucc beta) Lsb gamma Hc.
We will prove PNoLt gamma q (ordsucc beta) p0.
Apply ordsuccE beta gamma Hc to the current goal.
Assume H4: gamma ∈ beta.
We prove the intermediate claim L1: PNoLt gamma q beta p.
An exact proof term for the current goal is Hp1 gamma H4 q H3.
Apply PNoLtE gamma beta q p L1 to the current goal.
Assume H5: PNoLt_ (gamma ∩ beta) q p.
Apply H5 to the current goal.
Let delta be given.
Assume H6.
Apply H6 to the current goal.
Assume Hd: delta ∈ gamma ∩ beta.
Assume H6.
Apply H6 to the current goal.
Assume H6.
Apply H6 to the current goal.
Assume H6: PNoEq_ delta q p.
Assume H7: ¬ q delta.
Assume H8: p delta.
Apply binintersectE gamma beta delta Hd to the current goal.
Assume Hd1: delta ∈ gamma.
Assume Hd2: delta ∈ beta.
We will prove PNoLt gamma q (ordsucc beta) p0.
Apply PNoLtI1 to the current goal.
We will prove PNoLt_ (gamma ∩ ordsucc beta) q p0.
We will prove ∃beta ∈ gamma ∩ ordsucc beta, PNoEq_ beta q p0 ∧ ¬ q beta ∧ p0 beta.
We use delta to witness the existential quantifier.
Apply andI to the current goal.
We will prove delta ∈ gamma ∩ ordsucc beta.
Apply binintersectI to the current goal.
An exact proof term for the current goal is Hd1.
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is Hd2.
Apply and3I to the current goal.
We will prove PNoEq_ delta q p0.
Apply PNoEq_tra_ delta q p p0 to the current goal.
An exact proof term for the current goal is H6.
Apply PNoEq_sym_ to the current goal.
Apply PNoEq_antimon_ p0 p beta Lb delta Hd2 to the current goal.
An exact proof term for the current goal is Lp0e.
We will prove ¬ q delta.
An exact proof term for the current goal is H7.
We will prove p0 delta.
We will prove p delta ∧ delta ≠ beta.
Apply andI to the current goal.
An exact proof term for the current goal is H8.
Assume H9: delta = beta.
Apply In_irref beta to the current goal.
rewrite the current goal using H9 (from right to left) at position 1.
An exact proof term for the current goal is Hd2.
Assume H5: gamma ∈ beta.
Assume H6: PNoEq_ gamma q p.
Assume H7: p gamma.
We will prove PNoLt gamma q (ordsucc beta) p0.
Apply PNoLtI2 to the current goal.
We will prove gamma ∈ ordsucc beta.
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is H5.
We will prove PNoEq_ gamma q p0.
Apply PNoEq_tra_ gamma q p p0 to the current goal.
We will prove PNoEq_ gamma q p.
An exact proof term for the current goal is H6.
We will prove PNoEq_ gamma p p0.
Apply PNoEq_sym_ to the current goal.
Apply PNoEq_antimon_ p0 p beta Lb gamma H5 to the current goal.
An exact proof term for the current goal is Lp0e.
We will prove p0 gamma.
We will prove p gamma ∧ gamma ≠ beta.
Apply andI to the current goal.
An exact proof term for the current goal is H7.
Assume H8: gamma = beta.
Apply In_irref gamma to the current goal.
rewrite the current goal using H8 (from left to right) at position 2.
An exact proof term for the current goal is H5.
Assume H5: beta ∈ gamma.
We will prove False.
An exact proof term for the current goal is In_no2cycle gamma beta H4 H5.
Assume H4: gamma = beta.
rewrite the current goal using H4 (from left to right).
We will prove PNoLt beta q (ordsucc beta) p0.
Apply PNoLt_trichotomy_or beta (ordsucc beta) q p0 Lb Lsb to the current goal.
Assume H5.
Apply H5 to the current goal.
Assume H5.
An exact proof term for the current goal is H5.
Assume H5.
Apply H5 to the current goal.
Assume H5: beta = ordsucc beta.
We will prove False.
Apply In_irref beta to the current goal.
rewrite the current goal using H5 (from left to right) at position 2.
Apply ordsuccI2 to the current goal.
Assume H5: PNoLt (ordsucc beta) p0 beta q.
Apply PNoLtE (ordsucc beta) beta p0 q H5 to the current goal.
rewrite the current goal using Lbsb2 (from left to right).
Assume H6: PNoLt_ beta p0 q.
Apply H6 to the current goal.
Let delta be given.
Assume H7.
Apply H7 to the current goal.
Assume Hd: delta ∈ beta.
Assume H7.
Apply H7 to the current goal.
Assume H7.
Apply H7 to the current goal.
Assume H7: PNoEq_ delta p0 q.
Assume H8: ¬ p0 delta.
Assume H9: q delta.
We prove the intermediate claim Ld: ordinal delta.
An exact proof term for the current goal is ordinal_Hered beta Lb delta Hd.
We prove the intermediate claim L2: PNoLt beta p delta q.
Apply PNoLtI3 to the current goal.
We will prove delta ∈ beta.
An exact proof term for the current goal is Hd.
We will prove PNoEq_ delta p q.
Apply PNoEq_tra_ delta p p0 q to the current goal.
We will prove PNoEq_ delta p p0.
Apply PNoEq_sym_ to the current goal.
Apply PNoEq_antimon_ p0 p beta Lb delta Hd to the current goal.
An exact proof term for the current goal is Lp0e.
We will prove PNoEq_ delta p0 q.
An exact proof term for the current goal is H7.
We will prove ¬ p delta.
Assume H10: p delta.
Apply H8 to the current goal.
We will prove p delta ∧ delta ≠ beta.
Apply andI to the current goal.
An exact proof term for the current goal is H10.
Assume H11: delta = beta.
Apply In_irref beta to the current goal.
rewrite the current goal using H11 (from right to left) at position 1.
An exact proof term for the current goal is Hd.
We prove the intermediate claim L3: PNoLt delta q beta p.
Apply Hp1 delta Hd q to the current goal.
We will prove PNo_downc L delta q.
Apply PNoLe_downc L gamma delta q q Lc Ld H3 to the current goal.
We will prove PNoLe delta q gamma q.
Apply PNoLeI1 to the current goal.
We will prove PNoLt delta q gamma q.
Apply PNoLtI2 to the current goal.
We will prove delta ∈ gamma.
rewrite the current goal using H4 (from left to right).
An exact proof term for the current goal is Hd.
We will prove PNoEq_ delta q q.
Apply PNoEq_ref_ to the current goal.
We will prove q delta.
An exact proof term for the current goal is H9.
Apply PNoLt_irref delta q to the current goal.
We will prove PNoLt delta q delta q.
An exact proof term for the current goal is PNoLt_tra delta beta delta Ld Lb Ld q p q L3 L2.
Assume H6: ordsucc beta ∈ beta.
We will prove False.
Apply In_no2cycle (ordsucc beta) beta H6 to the current goal.
Apply ordsuccI2 to the current goal.
Assume H6: beta ∈ ordsucc beta.
Assume H7: PNoEq_ beta p0 q.
We will prove False.
Apply H2 q to the current goal.
We will prove PNo_downc L beta q.
rewrite the current goal using H4 (from right to left).
An exact proof term for the current goal is H3.
We will prove PNoEq_ beta p q.
Apply PNoEq_tra_ beta p p0 q to the current goal.
Apply PNoEq_sym_ to the current goal.
An exact proof term for the current goal is Lp0e.
An exact proof term for the current goal is H7.
Let gamma be given.
Assume Hc: gamma ∈ ordsucc beta.
Let q be given.
Assume H3: PNo_upc R gamma q.
We prove the intermediate claim Lc: ordinal gamma.
An exact proof term for the current goal is ordinal_Hered (ordsucc beta) Lsb gamma Hc.
We will prove PNoLt (ordsucc beta) p0 gamma q.
Apply ordsuccE beta gamma Hc to the current goal.
Assume H4: gamma ∈ beta.
Apply PNoLt_tra (ordsucc beta) beta gamma Lsb Lb Lc p0 p q Lp0p to the current goal.
We will prove PNoLt beta p gamma q.
Apply Hp2 gamma H4 q to the current goal.
We will prove PNo_upc R gamma q.
An exact proof term for the current goal is H3.
Assume H4: gamma = beta.
rewrite the current goal using H4 (from left to right).
We will prove PNoLt (ordsucc beta) p0 beta q.
Apply PNoLt_trichotomy_or beta (ordsucc beta) q p0 Lb Lsb to the current goal.
Assume H5.
Apply H5 to the current goal.
Assume H5: PNoLt beta q (ordsucc beta) p0.
Apply PNoLtE beta (ordsucc beta) q p0 H5 to the current goal.
rewrite the current goal using Lbsb1 (from left to right).
Assume H6: PNoLt_ beta q p0.
Apply H6 to the current goal.
Let delta be given.
Assume H7.
Apply H7 to the current goal.
Assume H8: delta ∈ beta.
Assume H9.
Apply H9 to the current goal.
Assume H9.
Apply H9 to the current goal.
Assume H9: PNoEq_ delta q p0.
Assume H10: ¬ q delta.
Assume H11: p0 delta.
We will prove False.
We prove the intermediate claim Ld: ordinal delta.
An exact proof term for the current goal is ordinal_Hered beta Lb delta H8.
We prove the intermediate claim L4: PNoLt beta p delta q.
Apply Hp2 delta H8 q to the current goal.
We will prove PNo_upc R delta q.
Apply PNoLe_upc R gamma delta q q Lc Ld H3 to the current goal.
We will prove PNoLe gamma q delta q.
Apply PNoLeI1 to the current goal.
We will prove PNoLt gamma q delta q.
Apply PNoLtI3 to the current goal.
We will prove delta ∈ gamma.
rewrite the current goal using H4 (from left to right).
An exact proof term for the current goal is H8.
We will prove PNoEq_ delta q q.
Apply PNoEq_ref_ to the current goal.
We will prove ¬ q delta.
An exact proof term for the current goal is H10.
We prove the intermediate claim L5: PNoLt delta q beta p.
Apply PNoLtI2 to the current goal.
We will prove delta ∈ beta.
An exact proof term for the current goal is H8.
We will prove PNoEq_ delta q p.
Apply PNoEq_tra_ delta q p0 p to the current goal.
An exact proof term for the current goal is H9.
We will prove PNoEq_ delta p0 p.
Apply PNoEq_antimon_ p0 p beta Lb delta H8 to the current goal.
An exact proof term for the current goal is Lp0e.
We will prove p delta.
Apply H11 to the current goal.
Assume H12 _.
An exact proof term for the current goal is H12.
Apply PNoLt_irref beta p to the current goal.
An exact proof term for the current goal is PNoLt_tra beta delta beta Lb Ld Lb p q p L4 L5.
Assume H6: beta ∈ ordsucc beta.
Assume H7: PNoEq_ beta q p0.
Assume H8: p beta ∧ beta ≠ beta.
We will prove False.
Apply H8 to the current goal.
Assume _ H9.
Apply H9 to the current goal.
Use reflexivity.
Assume H6: ordsucc beta ∈ beta.
We will prove False.
Apply In_no2cycle (ordsucc beta) beta H6 to the current goal.
Apply ordsuccI2 to the current goal.
Assume H5.
Apply H5 to the current goal.
Assume H5: beta = ordsucc beta.
We will prove False.
Apply In_irref beta to the current goal.
rewrite the current goal using H5 (from left to right) at position 2.
Apply ordsuccI2 to the current goal.
Assume H5: PNoLt (ordsucc beta) p0 beta q.
An exact proof term for the current goal is H5.
Apply HNC1 to the current goal.
We use p0 to witness the existential quantifier.
rewrite the current goal using Hab (from left to right).
We will prove PNo_rel_strict_uniq_imv L R (ordsucc beta) p0.
We will prove PNo_rel_strict_imv L R (ordsucc beta) p0 ∧ ∀q : set → prop, PNo_rel_strict_imv L R (ordsucc beta) q → PNoEq_ (ordsucc beta) p0 q.
Apply andI to the current goal.
An exact proof term for the current goal is Lp0imv.
Let q be given.
Assume Hq: PNo_rel_strict_imv L R (ordsucc beta) q.
We will prove PNoEq_ (ordsucc beta) p0 q.
We prove the intermediate claim Lqb: PNo_rel_strict_imv L R beta q.
An exact proof term for the current goal is PNo_rel_strict_imv_antimon L R (ordsucc beta) Lsb q beta (ordsuccI2 beta) Hq.
We prove the intermediate claim Lpqe: PNoEq_ beta p q.
An exact proof term for the current goal is Hp3 q Lqb.
Apply xm (q beta) to the current goal.
Assume Hq1: q beta.
We will prove False.
Apply Lnotboth to the current goal.
rewrite the current goal using Hab (from left to right).
Apply andI to the current goal.
We will prove PNo_rel_strict_imv L R (ordsucc beta) p0.
An exact proof term for the current goal is Lp0imv.
We will prove PNo_rel_strict_imv L R (ordsucc beta) p1.
Apply PNoEq_rel_strict_imv L R (ordsucc beta) Lsb q p1 to the current goal.
We will prove PNoEq_ (ordsucc beta) q p1.
Let gamma be given.
Assume Hc: gamma ∈ ordsucc beta.
Apply ordsuccE beta gamma Hc to the current goal.
Assume H3: gamma ∈ beta.
We prove the intermediate claim Lpqce: p gamma ↔ q gamma.
An exact proof term for the current goal is Lpqe gamma H3.
Apply Lpqce to the current goal.
Assume Hpqc Hqpc.
We will prove q gamma ↔ p1 gamma.
Apply iffI to the current goal.
Assume H4: q gamma.
We will prove p gamma ∨ gamma = beta.
Apply orIL to the current goal.
An exact proof term for the current goal is Hqpc H4.
Assume H4: p gamma ∨ gamma = beta.
Apply H4 to the current goal.
An exact proof term for the current goal is Hpqc.
Assume H5: gamma = beta.
We will prove False.
Apply In_irref beta to the current goal.
rewrite the current goal using H5 (from right to left) at position 1.
An exact proof term for the current goal is H3.
Assume H3: gamma = beta.
We will prove q gamma ↔ p1 gamma.
Apply iffI to the current goal.
Assume _.
We will prove p gamma ∨ gamma = beta.
Apply orIR to the current goal.
An exact proof term for the current goal is H3.
Assume _.
We will prove q gamma.
rewrite the current goal using H3 (from left to right).
An exact proof term for the current goal is Hq1.
We will prove PNo_rel_strict_imv L R (ordsucc beta) q.
An exact proof term for the current goal is Hq.
Assume Hq0: ¬ q beta.
We will prove PNoEq_ (ordsucc beta) p0 q.
Let gamma be given.
Assume Hc: gamma ∈ ordsucc beta.
Apply ordsuccE beta gamma Hc to the current goal.
Assume H3: gamma ∈ beta.
We prove the intermediate claim Lpqce: p gamma ↔ q gamma.
An exact proof term for the current goal is Lpqe gamma H3.
Apply Lpqce to the current goal.
Assume Hpqc Hqpc.
We will prove p0 gamma ↔ q gamma.
Apply iffI to the current goal.
Assume H4: p gamma ∧ gamma ≠ beta.
Apply H4 to the current goal.
Assume H5: p gamma.
Assume _.
An exact proof term for the current goal is Hpqc H5.
Assume H4: q gamma.
We will prove p gamma ∧ gamma ≠ beta.
Apply andI to the current goal.
We will prove p gamma.
An exact proof term for the current goal is Hqpc H4.
We will prove gamma ≠ beta.
Assume H5: gamma = beta.
Apply In_irref beta to the current goal.
rewrite the current goal using H5 (from right to left) at position 1.
An exact proof term for the current goal is H3.
Assume H3: gamma = beta.
We will prove p0 gamma ↔ q gamma.
Apply iffI to the current goal.
Assume H4: p gamma ∧ gamma ≠ beta.
Apply H4 to the current goal.
Assume _ H5.
We will prove False.
An exact proof term for the current goal is H5 H3.
Assume H4: q gamma.
We will prove False.
Apply Hq0 to the current goal.
We will prove q beta.
rewrite the current goal using H3 (from right to left).
An exact proof term for the current goal is H4.
Assume H2: ∀q : set → prop, PNo_upc R beta q → ¬ PNoEq_ beta p q.
We prove the intermediate claim Lp1imv: PNo_rel_strict_imv L R (ordsucc beta) p1.
We will prove PNo_rel_strict_upperbd L (ordsucc beta) p1 ∧ PNo_rel_strict_lowerbd R (ordsucc beta) p1.
Apply andI to the current goal.
Let gamma be given.
Assume Hc: gamma ∈ ordsucc beta.
Let q be given.
Assume H3: PNo_downc L gamma q.
We prove the intermediate claim Lc: ordinal gamma.
An exact proof term for the current goal is ordinal_Hered (ordsucc beta) Lsb gamma Hc.
We will prove PNoLt gamma q (ordsucc beta) p1.
Apply ordsuccE beta gamma Hc to the current goal.
Assume H4: gamma ∈ beta.
Apply PNoLt_tra gamma beta (ordsucc beta) Lc Lb Lsb q p p1 to the current goal.
We will prove PNoLt gamma q beta p.
Apply Hp1 gamma H4 q to the current goal.
We will prove PNo_downc L gamma q.
An exact proof term for the current goal is H3.
An exact proof term for the current goal is Lpp1.
Assume H4: gamma = beta.
rewrite the current goal using H4 (from left to right).
We will prove PNoLt beta q (ordsucc beta) p1.
Apply PNoLt_trichotomy_or beta (ordsucc beta) q p1 Lb Lsb to the current goal.
Assume H5.
Apply H5 to the current goal.
Assume H5: PNoLt beta q (ordsucc beta) p1.
An exact proof term for the current goal is H5.
Assume H5.
Apply H5 to the current goal.
Assume H5: beta = ordsucc beta.
We will prove False.
Apply In_irref beta to the current goal.
rewrite the current goal using H5 (from left to right) at position 2.
Apply ordsuccI2 to the current goal.
Assume H5: PNoLt (ordsucc beta) p1 beta q.
Apply PNoLtE (ordsucc beta) beta p1 q H5 to the current goal.
rewrite the current goal using Lbsb2 (from left to right).
Assume H6: PNoLt_ beta p1 q.
Apply H6 to the current goal.
Let delta be given.
Assume H7.
Apply H7 to the current goal.
Assume H8: delta ∈ beta.
Assume H9.
Apply H9 to the current goal.
Assume H9.
Apply H9 to the current goal.
Assume H9: PNoEq_ delta p1 q.
Assume H10: ¬ p1 delta.
Assume H11: q delta.
We will prove False.
We prove the intermediate claim Ld: ordinal delta.
An exact proof term for the current goal is ordinal_Hered beta Lb delta H8.
We prove the intermediate claim L4: PNoLt delta q beta p.
Apply Hp1 delta H8 q to the current goal.
We will prove PNo_downc L delta q.
Apply PNoLe_downc L gamma delta q q Lc Ld H3 to the current goal.
We will prove PNoLe delta q gamma q.
Apply PNoLeI1 to the current goal.
We will prove PNoLt delta q gamma q.
Apply PNoLtI2 to the current goal.
We will prove delta ∈ gamma.
rewrite the current goal using H4 (from left to right).
An exact proof term for the current goal is H8.
We will prove PNoEq_ delta q q.
Apply PNoEq_ref_ to the current goal.
We will prove q delta.
An exact proof term for the current goal is H11.
We prove the intermediate claim L5: PNoLt beta p delta q.
Apply PNoLtI3 to the current goal.
We will prove delta ∈ beta.
An exact proof term for the current goal is H8.
We will prove PNoEq_ delta p q.
Apply PNoEq_tra_ delta p p1 q to the current goal.
We will prove PNoEq_ delta p p1.
Apply PNoEq_antimon_ p p1 beta Lb delta H8 to the current goal.
An exact proof term for the current goal is Lp1e.
An exact proof term for the current goal is H9.
We will prove ¬ p delta.
Assume H12: p delta.
Apply H10 to the current goal.
We will prove p delta ∨ delta = beta.
Apply orIL to the current goal.
An exact proof term for the current goal is H12.
Apply PNoLt_irref beta p to the current goal.
An exact proof term for the current goal is PNoLt_tra beta delta beta Lb Ld Lb p q p L5 L4.
Assume H6: ordsucc beta ∈ beta.
We will prove False.
Apply In_no2cycle (ordsucc beta) beta H6 to the current goal.
Apply ordsuccI2 to the current goal.
Assume H6: beta ∈ ordsucc beta.
Assume H7: PNoEq_ beta p1 q.
Assume H8: ¬ p1 beta.
We will prove False.
Apply H8 to the current goal.
We will prove p beta ∨ beta = beta.
Apply orIR to the current goal.
Use reflexivity.
Let gamma be given.
Assume Hc: gamma ∈ ordsucc beta.
Let q be given.
Assume H3: PNo_upc R gamma q.
We prove the intermediate claim Lc: ordinal gamma.
An exact proof term for the current goal is ordinal_Hered (ordsucc beta) Lsb gamma Hc.
We will prove PNoLt (ordsucc beta) p1 gamma q.
Apply ordsuccE beta gamma Hc to the current goal.
Assume H4: gamma ∈ beta.
We prove the intermediate claim L1: PNoLt beta p gamma q.
An exact proof term for the current goal is Hp2 gamma H4 q H3.
Apply PNoLtE beta gamma p q L1 to the current goal.
Assume H5: PNoLt_ (beta ∩ gamma) p q.
Apply H5 to the current goal.
Let delta be given.
Assume H6.
Apply H6 to the current goal.
Assume Hd: delta ∈ beta ∩ gamma.
Assume H6.
Apply H6 to the current goal.
Assume H6.
Apply H6 to the current goal.
Assume H6: PNoEq_ delta p q.
Assume H7: ¬ p delta.
Assume H8: q delta.
Apply binintersectE beta gamma delta Hd to the current goal.
Assume Hd2: delta ∈ beta.
Assume Hd1: delta ∈ gamma.
We will prove PNoLt (ordsucc beta) p1 gamma q.
Apply PNoLtI1 to the current goal.
We will prove PNoLt_ (ordsucc beta ∩ gamma) p1 q.
We will prove ∃beta ∈ ordsucc beta ∩ gamma, PNoEq_ beta p1 q ∧ ¬ p1 beta ∧ q beta.
We use delta to witness the existential quantifier.
Apply andI to the current goal.
We will prove delta ∈ ordsucc beta ∩ gamma.
Apply binintersectI to the current goal.
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is Hd2.
An exact proof term for the current goal is Hd1.
Apply and3I to the current goal.
We will prove PNoEq_ delta p1 q.
Apply PNoEq_tra_ delta p1 p q to the current goal.
Apply PNoEq_antimon_ p1 p beta Lb delta Hd2 to the current goal.
Apply PNoEq_sym_ to the current goal.
An exact proof term for the current goal is Lp1e.
An exact proof term for the current goal is H6.
We will prove ¬ p1 delta.
Assume H9: p delta ∨ delta = beta.
We will prove False.
Apply H9 to the current goal.
An exact proof term for the current goal is H7.
Assume H10: delta = beta.
Apply In_irref beta to the current goal.
rewrite the current goal using H10 (from right to left) at position 1.
An exact proof term for the current goal is Hd2.
We will prove q delta.
An exact proof term for the current goal is H8.
Assume H5: beta ∈ gamma.
We will prove False.
An exact proof term for the current goal is In_no2cycle gamma beta H4 H5.
Assume H5: gamma ∈ beta.
Assume H6: PNoEq_ gamma p q.
Assume H7: ¬ p gamma.
We will prove PNoLt (ordsucc beta) p1 gamma q.
Apply PNoLtI3 to the current goal.
We will prove gamma ∈ ordsucc beta.
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is H5.
We will prove PNoEq_ gamma p1 q.
Apply PNoEq_tra_ gamma p1 p q to the current goal.
We will prove PNoEq_ gamma p1 p.
Apply PNoEq_antimon_ p1 p beta Lb gamma H5 to the current goal.
Apply PNoEq_sym_ to the current goal.
An exact proof term for the current goal is Lp1e.
We will prove PNoEq_ gamma p q.
An exact proof term for the current goal is H6.
We will prove ¬ p1 gamma.
Assume H8: p gamma ∨ gamma = beta.
Apply H8 to the current goal.
An exact proof term for the current goal is H7.
Assume H9: gamma = beta.
Apply In_irref beta to the current goal.
rewrite the current goal using H9 (from right to left) at position 1.
An exact proof term for the current goal is H5.
Assume H4: gamma = beta.
rewrite the current goal using H4 (from left to right).
We will prove PNoLt (ordsucc beta) p1 beta q.
Apply PNoLt_trichotomy_or beta (ordsucc beta) q p1 Lb Lsb to the current goal.
Assume H5.
Apply H5 to the current goal.
Assume H5: PNoLt beta q (ordsucc beta) p1.
Apply PNoLtE beta (ordsucc beta) q p1 H5 to the current goal.
rewrite the current goal using Lbsb1 (from left to right).
Assume H6: PNoLt_ beta q p1.
Apply H6 to the current goal.
Let delta be given.
Assume H7.
Apply H7 to the current goal.
Assume Hd: delta ∈ beta.
Assume H7.
Apply H7 to the current goal.
Assume H7.
Apply H7 to the current goal.
Assume H7: PNoEq_ delta q p1.
Assume H8: ¬ q delta.
Assume H9: p1 delta.
We prove the intermediate claim Ld: ordinal delta.
An exact proof term for the current goal is ordinal_Hered beta Lb delta Hd.
We prove the intermediate claim L2: PNoLt delta q beta p.
Apply PNoLtI2 to the current goal.
We will prove delta ∈ beta.
An exact proof term for the current goal is Hd.
We will prove PNoEq_ delta q p.
Apply PNoEq_tra_ delta q p1 p to the current goal.
We will prove PNoEq_ delta q p1.
An exact proof term for the current goal is H7.
We will prove PNoEq_ delta p1 p.
Apply PNoEq_antimon_ p1 p beta Lb delta Hd to the current goal.
Apply PNoEq_sym_ to the current goal.
An exact proof term for the current goal is Lp1e.
We will prove p delta.
Apply H9 to the current goal.
Assume H10: p delta.
An exact proof term for the current goal is H10.
Assume H10: delta = beta.
We will prove False.
Apply In_irref beta to the current goal.
rewrite the current goal using H10 (from right to left) at position 1.
An exact proof term for the current goal is Hd.
We prove the intermediate claim L3: PNoLt beta p delta q.
Apply Hp2 delta Hd q to the current goal.
We will prove PNo_upc R delta q.
Apply PNoLe_upc R gamma delta q q Lc Ld H3 to the current goal.
We will prove PNoLe gamma q delta q.
Apply PNoLeI1 to the current goal.
We will prove PNoLt gamma q delta q.
Apply PNoLtI3 to the current goal.
We will prove delta ∈ gamma.
rewrite the current goal using H4 (from left to right).
An exact proof term for the current goal is Hd.
We will prove PNoEq_ delta q q.
Apply PNoEq_ref_ to the current goal.
We will prove ¬ q delta.
An exact proof term for the current goal is H8.
Apply PNoLt_irref delta q to the current goal.
We will prove PNoLt delta q delta q.
An exact proof term for the current goal is PNoLt_tra delta beta delta Ld Lb Ld q p q L2 L3.
Assume H6: beta ∈ ordsucc beta.
Assume H7: PNoEq_ beta q p1.
We will prove False.
Apply H2 q to the current goal.
We will prove PNo_upc R beta q.
rewrite the current goal using H4 (from right to left).
An exact proof term for the current goal is H3.
We will prove PNoEq_ beta p q.
Apply PNoEq_tra_ beta p p1 q to the current goal.
An exact proof term for the current goal is Lp1e.
Apply PNoEq_sym_ to the current goal.
An exact proof term for the current goal is H7.
Assume H6: ordsucc beta ∈ beta.
We will prove False.
Apply In_no2cycle (ordsucc beta) beta H6 to the current goal.
Apply ordsuccI2 to the current goal.
Assume H5.
Apply H5 to the current goal.
Assume H5: beta = ordsucc beta.
We will prove False.
Apply In_irref beta to the current goal.
rewrite the current goal using H5 (from left to right) at position 2.
Apply ordsuccI2 to the current goal.
Assume H5.
An exact proof term for the current goal is H5.
Apply HNC1 to the current goal.
We use p1 to witness the existential quantifier.
rewrite the current goal using Hab (from left to right).
We will prove PNo_rel_strict_uniq_imv L R (ordsucc beta) p1.
We will prove PNo_rel_strict_imv L R (ordsucc beta) p1 ∧ ∀q : set → prop, PNo_rel_strict_imv L R (ordsucc beta) q → PNoEq_ (ordsucc beta) p1 q.
Apply andI to the current goal.
An exact proof term for the current goal is Lp1imv.
Let q be given.
Assume Hq: PNo_rel_strict_imv L R (ordsucc beta) q.
We will prove PNoEq_ (ordsucc beta) p1 q.
We prove the intermediate claim Lqb: PNo_rel_strict_imv L R beta q.
An exact proof term for the current goal is PNo_rel_strict_imv_antimon L R (ordsucc beta) Lsb q beta (ordsuccI2 beta) Hq.
We prove the intermediate claim Lpqe: PNoEq_ beta p q.
An exact proof term for the current goal is Hp3 q Lqb.
Apply xm (q beta) to the current goal.
Assume Hq1: q beta.
We will prove PNoEq_ (ordsucc beta) p1 q.
Let gamma be given.
Assume Hc: gamma ∈ ordsucc beta.
Apply ordsuccE beta gamma Hc to the current goal.
Assume H3: gamma ∈ beta.
We prove the intermediate claim Lpqce: p gamma ↔ q gamma.
An exact proof term for the current goal is Lpqe gamma H3.
Apply Lpqce to the current goal.
Assume Hpqc Hqpc.
We will prove p1 gamma ↔ q gamma.
Apply iffI to the current goal.
Assume H4: p gamma ∨ gamma = beta.
Apply H4 to the current goal.
Assume H5: p gamma.
An exact proof term for the current goal is Hpqc H5.
Assume H5: gamma = beta.
We will prove False.
Apply In_irref beta to the current goal.
rewrite the current goal using H5 (from right to left) at position 1.
An exact proof term for the current goal is H3.
Assume H4: q gamma.
We will prove p gamma ∨ gamma = beta.
Apply orIL to the current goal.
We will prove p gamma.
An exact proof term for the current goal is Hqpc H4.
Assume H3: gamma = beta.
We will prove p1 gamma ↔ q gamma.
Apply iffI to the current goal.
Assume _.
We will prove q gamma.
rewrite the current goal using H3 (from left to right).
We will prove q beta.
An exact proof term for the current goal is Hq1.
Assume H4: q gamma.
We will prove p gamma ∨ gamma = beta.
Apply orIR to the current goal.
An exact proof term for the current goal is H3.
Assume Hq0: ¬ q beta.
We will prove False.
Apply Lnotboth to the current goal.
rewrite the current goal using Hab (from left to right).
Apply andI to the current goal.
We will prove PNo_rel_strict_imv L R (ordsucc beta) p0.
Apply PNoEq_rel_strict_imv L R (ordsucc beta) Lsb q p0 to the current goal.
We will prove PNoEq_ (ordsucc beta) q p0.
Let gamma be given.
Assume Hc: gamma ∈ ordsucc beta.
Apply ordsuccE beta gamma Hc to the current goal.
Assume H3: gamma ∈ beta.
We prove the intermediate claim Lpqce: p gamma ↔ q gamma.
An exact proof term for the current goal is Lpqe gamma H3.
Apply Lpqce to the current goal.
Assume Hpqc Hqpc.
We will prove q gamma ↔ p0 gamma.
Apply iffI to the current goal.
Assume H4: q gamma.
We will prove p gamma ∧ gamma ≠ beta.
Apply andI to the current goal.
We will prove p gamma.
An exact proof term for the current goal is Hqpc H4.
We will prove gamma ≠ beta.
Assume H5: gamma = beta.
Apply In_irref beta to the current goal.
rewrite the current goal using H5 (from right to left) at position 1.
An exact proof term for the current goal is H3.
Assume H4: p gamma ∧ gamma ≠ beta.
Apply H4 to the current goal.
Assume H5 _.
An exact proof term for the current goal is Hpqc H5.
Assume H3: gamma = beta.
We will prove q gamma ↔ p0 gamma.
Apply iffI to the current goal.
Assume H4: q gamma.
We will prove False.
Apply Hq0 to the current goal.
rewrite the current goal using H3 (from right to left).
An exact proof term for the current goal is H4.
Assume H4: p0 gamma.
Apply H4 to the current goal.
Assume _ H5.
We will prove False.
Apply H5 to the current goal.
An exact proof term for the current goal is H3.
We will prove PNo_rel_strict_imv L R (ordsucc beta) q.
An exact proof term for the current goal is Hq.
We will prove PNo_rel_strict_imv L R (ordsucc beta) p1.
An exact proof term for the current goal is Lp1imv.
∎
Definition. We define PNo_lenbdd to be λalpha L ⇒ ∀beta, ∀p : set → prop, L beta p → beta ∈ alpha of type set → (set → (set → prop) → prop) → prop.
In Proofgold the corresponding term root is 009fa7... and object id is a452a6...
Theorem. (PNo_lenbdd_strict_imv_extend0) The following is provable:
∀L R : set → (set → prop) → prop, ∀alpha, ordinal alpha → PNo_lenbdd alpha L → PNo_lenbdd alpha R → ∀p : set → prop, PNo_rel_strict_imv L R alpha p → PNo_rel_strict_imv L R (ordsucc alpha) (λdelta ⇒ p delta ∧ delta ≠ alpha)
In Proofgold the corresponding term root is 17a114... and proposition id is 69327e...
Proof:
Let L and R be given.
Let alpha be given.
Assume Ha.
Apply Ha to the current goal.
Assume Ha1 _.
Assume HaL HaR.
Let p be given.
Assume Hp1: PNo_rel_strict_imv L R alpha p.
Apply Hp1 to the current goal.
Assume Hp1a Hp1b.
Set p0 to be the term λdelta ⇒ p delta ∧ delta ≠ alpha of type set → prop.
We prove the intermediate claim Lsa: ordinal (ordsucc alpha).
An exact proof term for the current goal is ordinal_ordsucc alpha Ha.
We prove the intermediate claim Lpp0e: PNoEq_ alpha p p0.
An exact proof term for the current goal is PNo_extend0_eq alpha p.
We will prove PNo_rel_strict_upperbd L (ordsucc alpha) p0 ∧ PNo_rel_strict_lowerbd R (ordsucc alpha) p0.
Apply andI to the current goal.
We will prove PNo_rel_strict_upperbd L (ordsucc alpha) p0.
Let gamma be given.
Assume Hc: gamma ∈ ordsucc alpha.
Let q be given.
Assume Hq: PNo_downc L gamma q.
We prove the intermediate claim Lc: ordinal gamma.
An exact proof term for the current goal is ordinal_Hered (ordsucc alpha) Lsa gamma Hc.
We will prove PNoLt gamma q (ordsucc alpha) p0.
Apply Hq to the current goal.
Let delta be given.
Assume Hq1.
Apply Hq1 to the current goal.
Assume Hd: ordinal delta.
Assume Hq1.
Apply Hq1 to the current goal.
Let r be given.
Assume Hq1.
Apply Hq1 to the current goal.
Assume Hr: L delta r.
Assume Hqr: PNoLe gamma q delta r.
Apply PNoLeLt_tra gamma delta (ordsucc alpha) Lc Hd Lsa q r p0 Hqr to the current goal.
We will prove PNoLt delta r (ordsucc alpha) p0.
We prove the intermediate claim Lda: delta ∈ alpha.
An exact proof term for the current goal is HaL delta r Hr.
We prove the intermediate claim Ldsa: delta ∈ ordsucc alpha.
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is Lda.
We prove the intermediate claim Ldr: PNo_downc L delta r.
An exact proof term for the current goal is PNo_downc_ref L delta Hd r Hr.
We prove the intermediate claim Lrp: PNoLt delta r alpha p.
An exact proof term for the current goal is Hp1a delta Lda r Ldr.
Apply PNoLt_trichotomy_or delta (ordsucc alpha) r p0 Hd Lsa to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1.
An exact proof term for the current goal is H1.
Assume H1.
Apply H1 to the current goal.
Assume H2: delta = ordsucc alpha.
We will prove False.
Apply In_irref delta to the current goal.
rewrite the current goal using H2 (from left to right) at position 2.
An exact proof term for the current goal is Ldsa.
Assume H1: PNoLt (ordsucc alpha) p0 delta r.
We will prove False.
Apply PNoLt_irref delta r to the current goal.
Apply PNoLt_tra delta alpha delta Hd Ha Hd r p r Lrp to the current goal.
We will prove PNoLt alpha p delta r.
Apply PNoLtE (ordsucc alpha) delta p0 r H1 to the current goal.
Assume H2: PNoLt_ (ordsucc alpha ∩ delta) p0 r.
Apply H2 to the current goal.
Let eps be given.
Assume H3.
Apply H3 to the current goal.
Assume He: eps ∈ ordsucc alpha ∩ delta.
Apply binintersectE (ordsucc alpha) delta eps He to the current goal.
Assume He1 He2.
We prove the intermediate claim Lea: eps ∈ alpha.
An exact proof term for the current goal is Ha1 delta Lda eps He2.
Assume H3.
Apply H3 to the current goal.
Assume H3.
Apply H3 to the current goal.
Assume H3: PNoEq_ eps p0 r.
Assume H4: ¬ p0 eps.
Assume H5: r eps.
Apply PNoLtI1 to the current goal.
We will prove PNoLt_ (alpha ∩ delta) p r.
We will prove ∃beta ∈ alpha ∩ delta, PNoEq_ beta p r ∧ ¬ p beta ∧ r beta.
We use eps to witness the existential quantifier.
Apply andI to the current goal.
We will prove eps ∈ alpha ∩ delta.
Apply binintersectI to the current goal.
An exact proof term for the current goal is Lea.
An exact proof term for the current goal is He2.
Apply and3I to the current goal.
We will prove PNoEq_ eps p r.
Apply PNoEq_tra_ eps p p0 r to the current goal.
Apply PNoEq_antimon_ p p0 alpha Ha eps Lea to the current goal.
An exact proof term for the current goal is Lpp0e.
An exact proof term for the current goal is H3.
We will prove ¬ p eps.
Assume H5: p eps.
Apply H4 to the current goal.
We will prove p eps ∧ eps ≠ alpha.
Apply andI to the current goal.
An exact proof term for the current goal is H5.
We will prove eps ≠ alpha.
Assume H6: eps = alpha.
Apply In_irref alpha to the current goal.
rewrite the current goal using H6 (from right to left) at position 1.
An exact proof term for the current goal is Lea.
We will prove r eps.
An exact proof term for the current goal is H5.
Assume H2: ordsucc alpha ∈ delta.
We will prove False.
An exact proof term for the current goal is In_no2cycle delta (ordsucc alpha) Ldsa H2.
Assume H2: delta ∈ ordsucc alpha.
Assume H3: PNoEq_ delta p0 r.
Assume H4: ¬ p0 delta.
Apply PNoLtI3 alpha delta p r Lda to the current goal.
We will prove PNoEq_ delta p r.
Apply PNoEq_tra_ delta p p0 r to the current goal.
Apply PNoEq_antimon_ p p0 alpha Ha delta Lda to the current goal.
An exact proof term for the current goal is Lpp0e.
An exact proof term for the current goal is H3.
We will prove ¬ p delta.
Assume H5: p delta.
Apply H4 to the current goal.
We will prove p delta ∧ delta ≠ alpha.
Apply andI to the current goal.
An exact proof term for the current goal is H5.
We will prove delta ≠ alpha.
Assume H6: delta = alpha.
Apply In_irref alpha to the current goal.
rewrite the current goal using H6 (from right to left) at position 1.
An exact proof term for the current goal is Lda.
We will prove PNo_rel_strict_lowerbd R (ordsucc alpha) p0.
Let gamma be given.
Assume Hc: gamma ∈ ordsucc alpha.
Let q be given.
Assume Hq: PNo_upc R gamma q.
We prove the intermediate claim Lc: ordinal gamma.
An exact proof term for the current goal is ordinal_Hered (ordsucc alpha) Lsa gamma Hc.
We will prove PNoLt (ordsucc alpha) p0 gamma q.
Apply PNoLt_tra (ordsucc alpha) alpha gamma Lsa Ha Lc p0 p q to the current goal.
We will prove PNoLt (ordsucc alpha) p0 alpha p.
Apply PNoLtI3 to the current goal.
We will prove alpha ∈ ordsucc alpha.
Apply ordsuccI2 to the current goal.
We will prove PNoEq_ alpha p0 p.
Apply PNoEq_sym_ to the current goal.
An exact proof term for the current goal is Lpp0e.
We will prove ¬ p0 alpha.
Assume H2: p0 alpha.
Apply H2 to the current goal.
Assume H3: p alpha.
Assume H4: alpha ≠ alpha.
Apply H4 to the current goal.
Use reflexivity.
We will prove PNoLt alpha p gamma q.
Apply Hq to the current goal.
Let delta be given.
Assume Hq1.
Apply Hq1 to the current goal.
Assume Hd: ordinal delta.
Assume Hq1.
Apply Hq1 to the current goal.
Let r be given.
Assume Hq1.
Apply Hq1 to the current goal.
Assume Hr: R delta r.
Assume Hrq: PNoLe delta r gamma q.
We prove the intermediate claim Ldr: PNo_upc R delta r.
An exact proof term for the current goal is PNo_upc_ref R delta Hd r Hr.
Apply (λH : PNoLt alpha p delta r ⇒ PNoLtLe_tra alpha delta gamma Ha Hd Lc p r q H Hrq) to the current goal.
We will prove PNoLt alpha p delta r.
An exact proof term for the current goal is Hp1b delta (HaR delta r Hr) r Ldr.
∎
Theorem. (PNo_lenbdd_strict_imv_extend1) The following is provable:
∀L R : set → (set → prop) → prop, ∀alpha, ordinal alpha → PNo_lenbdd alpha L → PNo_lenbdd alpha R → ∀p : set → prop, PNo_rel_strict_imv L R alpha p → PNo_rel_strict_imv L R (ordsucc alpha) (λdelta ⇒ p delta ∨ delta = alpha)
In Proofgold the corresponding term root is ad69ec... and proposition id is 5ff993...
Proof:
Let L and R be given.
Let alpha be given.
Assume Ha.
Apply Ha to the current goal.
Assume Ha1 _.
Assume HaL HaR.
Let p be given.
Assume Hp1: PNo_rel_strict_imv L R alpha p.
Apply Hp1 to the current goal.
Assume Hp1a Hp1b.
Set p1 to be the term λdelta ⇒ p delta ∨ delta = alpha of type set → prop.
We prove the intermediate claim Lsa: ordinal (ordsucc alpha).
An exact proof term for the current goal is ordinal_ordsucc alpha Ha.
We prove the intermediate claim Lpp1e: PNoEq_ alpha p p1.
An exact proof term for the current goal is PNo_extend1_eq alpha p.
We will prove PNo_rel_strict_upperbd L (ordsucc alpha) p1 ∧ PNo_rel_strict_lowerbd R (ordsucc alpha) p1.
Apply andI to the current goal.
We will prove PNo_rel_strict_upperbd L (ordsucc alpha) p1.
Let gamma be given.
Assume Hc: gamma ∈ ordsucc alpha.
Let q be given.
Assume Hq: PNo_downc L gamma q.
We prove the intermediate claim Lc: ordinal gamma.
An exact proof term for the current goal is ordinal_Hered (ordsucc alpha) Lsa gamma Hc.
We will prove PNoLt gamma q (ordsucc alpha) p1.
Apply PNoLt_tra gamma alpha (ordsucc alpha) Lc Ha Lsa q p p1 to the current goal.
We will prove PNoLt gamma q alpha p.
Apply Hq to the current goal.
Let delta be given.
Assume Hq1.
Apply Hq1 to the current goal.
Assume Hd: ordinal delta.
Assume Hq1.
Apply Hq1 to the current goal.
Let r be given.
Assume Hq1.
Apply Hq1 to the current goal.
Assume Hr: L delta r.
Assume Hqr: PNoLe gamma q delta r.
We prove the intermediate claim Ldr: PNo_downc L delta r.
We will prove ∃beta, ordinal beta ∧ ∃q : set → prop, L beta q ∧ PNoLe delta r beta q.
We use delta to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hd.
We use r to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hr.
Apply PNoLe_ref to the current goal.
Apply PNoLeLt_tra gamma delta alpha Lc Hd Ha q r p Hqr to the current goal.
We will prove PNoLt delta r alpha p.
An exact proof term for the current goal is Hp1a delta (HaL delta r Hr) r Ldr.
We will prove PNoLt alpha p (ordsucc alpha) p1.
Apply PNoLtI2 to the current goal.
We will prove alpha ∈ ordsucc alpha.
Apply ordsuccI2 to the current goal.
We will prove PNoEq_ alpha p p1.
An exact proof term for the current goal is Lpp1e.
We will prove p1 alpha.
We will prove p alpha ∨ alpha = alpha.
Apply orIR to the current goal.
Use reflexivity.
We will prove PNo_rel_strict_lowerbd R (ordsucc alpha) p1.
Let gamma be given.
Assume Hc: gamma ∈ ordsucc alpha.
Let q be given.
Assume Hq: PNo_upc R gamma q.
We prove the intermediate claim Lc: ordinal gamma.
An exact proof term for the current goal is ordinal_Hered (ordsucc alpha) Lsa gamma Hc.
We will prove PNoLt (ordsucc alpha) p1 gamma q.
Apply Hq to the current goal.
Let delta be given.
Assume Hq1.
Apply Hq1 to the current goal.
Assume Hd: ordinal delta.
Assume Hq1.
Apply Hq1 to the current goal.
Let r be given.
Assume Hq1.
Apply Hq1 to the current goal.
Assume Hr: R delta r.
Assume Hrq: PNoLe delta r gamma q.
Apply (λH : PNoLt (ordsucc alpha) p1 delta r ⇒ PNoLtLe_tra (ordsucc alpha) delta gamma Lsa Hd Lc p1 r q H Hrq) to the current goal.
We will prove PNoLt (ordsucc alpha) p1 delta r.
We prove the intermediate claim Lda: delta ∈ alpha.
An exact proof term for the current goal is HaR delta r Hr.
We prove the intermediate claim Ldsa: delta ∈ ordsucc alpha.
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is Lda.
We prove the intermediate claim Ldr: PNo_upc R delta r.
We will prove ∃beta, ordinal beta ∧ ∃q : set → prop, R beta q ∧ PNoLe beta q delta r.
We use delta to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hd.
We use r to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hr.
Apply PNoLe_ref to the current goal.
We prove the intermediate claim Lpr: PNoLt alpha p delta r.
An exact proof term for the current goal is Hp1b delta Lda r Ldr.
Apply PNoLt_trichotomy_or delta (ordsucc alpha) r p1 Hd Lsa to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1: PNoLt delta r (ordsucc alpha) p1.
We will prove False.
Apply PNoLt_irref alpha p to the current goal.
We will prove PNoLt alpha p alpha p.
Apply PNoLt_tra alpha delta alpha Ha Hd Ha p r p Lpr to the current goal.
We will prove PNoLt delta r alpha p.
Apply PNoLtE delta (ordsucc alpha) r p1 H1 to the current goal.
Assume H2: PNoLt_ (delta ∩ ordsucc alpha) r p1.
Apply H2 to the current goal.
Let eps be given.
Assume H3.
Apply H3 to the current goal.
Assume He: eps ∈ delta ∩ ordsucc alpha.
Apply binintersectE delta (ordsucc alpha) eps He to the current goal.
Assume He1 He2.
We prove the intermediate claim Lea: eps ∈ alpha.
An exact proof term for the current goal is Ha1 delta Lda eps He1.
Assume H3.
Apply H3 to the current goal.
Assume H3.
Apply H3 to the current goal.
Assume H3: PNoEq_ eps r p1.
Assume H4: ¬ r eps.
Assume H5: p1 eps.
Apply PNoLtI1 to the current goal.
We will prove PNoLt_ (delta ∩ alpha) r p.
We will prove ∃beta ∈ delta ∩ alpha, PNoEq_ beta r p ∧ ¬ r beta ∧ p beta.
We use eps to witness the existential quantifier.
Apply andI to the current goal.
We will prove eps ∈ delta ∩ alpha.
Apply binintersectI to the current goal.
An exact proof term for the current goal is He1.
An exact proof term for the current goal is Lea.
Apply and3I to the current goal.
We will prove PNoEq_ eps r p.
Apply PNoEq_tra_ eps r p1 p to the current goal.
An exact proof term for the current goal is H3.
Apply PNoEq_antimon_ p1 p alpha Ha eps Lea to the current goal.
Apply PNoEq_sym_ to the current goal.
An exact proof term for the current goal is Lpp1e.
We will prove ¬ r eps.
An exact proof term for the current goal is H4.
We will prove p eps.
Apply H5 to the current goal.
An exact proof term for the current goal is (λH ⇒ H).
Assume H6: eps = alpha.
We will prove False.
Apply In_irref alpha to the current goal.
rewrite the current goal using H6 (from right to left) at position 1.
An exact proof term for the current goal is Lea.
Assume H2: delta ∈ ordsucc alpha.
Assume H3: PNoEq_ delta r p1.
Assume H4: p1 delta.
Apply PNoLtI2 delta alpha r p Lda to the current goal.
We will prove PNoEq_ delta r p.
Apply PNoEq_tra_ delta r p1 p to the current goal.
An exact proof term for the current goal is H3.
Apply PNoEq_antimon_ p1 p alpha Ha delta Lda to the current goal.
Apply PNoEq_sym_ to the current goal.
An exact proof term for the current goal is Lpp1e.
We will prove p delta.
Apply H4 to the current goal.
An exact proof term for the current goal is (λH ⇒ H).
Assume H5: delta = alpha.
We will prove False.
Apply In_irref alpha to the current goal.
rewrite the current goal using H5 (from right to left) at position 1.
An exact proof term for the current goal is Lda.
Assume H2: ordsucc alpha ∈ delta.
We will prove False.
An exact proof term for the current goal is In_no2cycle delta (ordsucc alpha) Ldsa H2.
Assume H1.
Apply H1 to the current goal.
Assume H2: delta = ordsucc alpha.
We will prove False.
Apply In_irref delta to the current goal.
rewrite the current goal using H2 (from left to right) at position 2.
An exact proof term for the current goal is Ldsa.
Assume H1.
An exact proof term for the current goal is H1.
∎
Theorem. (PNo_lenbdd_strict_imv_split) The following is provable:
∀L R : set → (set → prop) → prop, ∀alpha, ordinal alpha → PNo_lenbdd alpha L → PNo_lenbdd alpha R → ∀p : set → prop, PNo_rel_strict_imv L R alpha p → PNo_rel_strict_split_imv L R alpha p
In Proofgold the corresponding term root is 76ae4f... and proposition id is f98998...
Proof:
Let L and R be given.
Let alpha be given.
Assume Ha.
Assume HaL HaR.
Let p be given.
Assume Hp1.
We will prove PNo_rel_strict_split_imv L R alpha p.
An exact proof term for the current goal is andI (PNo_rel_strict_imv L R (ordsucc alpha) (λdelta ⇒ p delta ∧ delta ≠ alpha)) (PNo_rel_strict_imv L R (ordsucc alpha) (λdelta ⇒ p delta ∨ delta = alpha)) (PNo_lenbdd_strict_imv_extend0 L R alpha Ha HaL HaR p Hp1) (PNo_lenbdd_strict_imv_extend1 L R alpha Ha HaL HaR p Hp1).
∎
Theorem. (PNo_rel_imv_bdd_ex) The following is provable:
∀L R : set → (set → prop) → prop, PNoLt_pwise L R → ∀alpha, ordinal alpha → PNo_lenbdd alpha L → PNo_lenbdd alpha R → ∃beta ∈ ordsucc alpha, ∃p : set → prop, PNo_rel_strict_split_imv L R beta p
In Proofgold the corresponding term root is 9a98e4... and proposition id is 25bcd2...
Proof:
Let L and R be given.
Assume HLR.
Let alpha be given.
Assume Ha.
Apply Ha to the current goal.
Assume Ha1 _.
Assume HaL HaR.
We prove the intermediate claim Lsa: ordinal (ordsucc alpha).
An exact proof term for the current goal is ordinal_ordsucc alpha Ha.
Apply PNo_rel_imv_ex L R HLR alpha Ha to the current goal.
Assume H2.
Apply H2 to the current goal.
Let p be given.
Assume Hp: PNo_rel_strict_uniq_imv L R alpha p.
Apply Hp to the current goal.
Assume Hp1: PNo_rel_strict_imv L R alpha p.
Apply Hp1 to the current goal.
Assume Hp1a Hp1b.
Assume Hp2: ∀q : set → prop, PNo_rel_strict_imv L R alpha q → PNoEq_ alpha p q.
We use alpha to witness the existential quantifier.
Apply andI to the current goal.
We will prove alpha ∈ ordsucc alpha.
Apply ordsuccI2 to the current goal.
We use p to witness the existential quantifier.
We will prove PNo_rel_strict_split_imv L R alpha p.
An exact proof term for the current goal is PNo_lenbdd_strict_imv_split L R alpha Ha HaL HaR p Hp1.
Assume H1.
Apply H1 to the current goal.
Let beta be given.
Assume H1.
Apply H1 to the current goal.
Assume Hb: beta ∈ alpha.
Assume H1.
We use beta to witness the existential quantifier.
Apply andI to the current goal.
We will prove beta ∈ ordsucc alpha.
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is Hb.
An exact proof term for the current goal is H1.
∎
Definition. We define PNo_strict_upperbd to be λL alpha p ⇒ ∀beta, ordinal beta → ∀q : set → prop, L beta q → PNoLt beta q alpha p of type (set → (set → prop) → prop) → set → (set → prop) → prop.
In Proofgold the corresponding term root is 6913bd... and object id is 3723ab...
Definition. We define PNo_strict_lowerbd to be λR alpha p ⇒ ∀beta, ordinal beta → ∀q : set → prop, R beta q → PNoLt alpha p beta q of type (set → (set → prop) → prop) → set → (set → prop) → prop.
In Proofgold the corresponding term root is 87fac4... and object id is 3606d4...
Definition. We define PNo_strict_imv to be λL R alpha p ⇒ PNo_strict_upperbd L alpha p ∧ PNo_strict_lowerbd R alpha p of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → set → (set → prop) → prop.
In Proofgold the corresponding term root is ee97f6... and object id is bc6c55...
Theorem. (PNoEq_strict_upperbd) The following is provable:
∀L : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p q : set → prop, PNoEq_ alpha p q → PNo_strict_upperbd L alpha p → PNo_strict_upperbd L alpha q
In Proofgold the corresponding term root is 9b7b8e... and proposition id is f28b04...
Proof:
Let L and alpha be given.
Assume Ha.
Let p and q be given.
Assume Hpq: PNoEq_ alpha p q.
Assume H1: PNo_strict_upperbd L alpha p.
We will prove PNo_strict_upperbd L alpha q.
Let beta be given.
Assume Hb: ordinal beta.
Let r be given.
Assume H2: L beta r.
We will prove PNoLt beta r alpha q.
Apply PNoLtEq_tra beta alpha Hb Ha r p q to the current goal.
We will prove PNoLt beta r alpha p.
An exact proof term for the current goal is H1 beta Hb r H2.
We will prove PNoEq_ alpha p q.
An exact proof term for the current goal is Hpq.
∎
Theorem. (PNoEq_strict_lowerbd) The following is provable:
∀R : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p q : set → prop, PNoEq_ alpha p q → PNo_strict_lowerbd R alpha p → PNo_strict_lowerbd R alpha q
In Proofgold the corresponding term root is 4db3f9... and proposition id is 67fa73...
Proof:
Let R and alpha be given.
Assume Ha.
Let p and q be given.
Assume Hpq: PNoEq_ alpha p q.
Assume H1: PNo_strict_lowerbd R alpha p.
We will prove PNo_strict_lowerbd R alpha q.
Let beta be given.
Assume Hb: ordinal beta.
Let r be given.
Assume H2: R beta r.
We will prove PNoLt alpha q beta r.
Apply PNoEqLt_tra alpha beta Ha Hb q p r to the current goal.
We will prove PNoEq_ alpha q p.
Apply PNoEq_sym_ to the current goal.
An exact proof term for the current goal is Hpq.
We will prove PNoLt alpha p beta r.
An exact proof term for the current goal is H1 beta Hb r H2.
∎
Theorem. (PNoEq_strict_imv) The following is provable:
∀L R : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p q : set → prop, PNoEq_ alpha p q → PNo_strict_imv L R alpha p → PNo_strict_imv L R alpha q
In Proofgold the corresponding term root is 1ec352... and proposition id is 5f582f...
Proof:
Let L, R and alpha be given.
Assume Ha.
Let p and q be given.
Assume Hpq H1.
Apply H1 to the current goal.
Assume H2 H3.
We will prove PNo_strict_upperbd L alpha q ∧ PNo_strict_lowerbd R alpha q.
Apply andI to the current goal.
An exact proof term for the current goal is PNoEq_strict_upperbd L alpha Ha p q Hpq H2.
An exact proof term for the current goal is PNoEq_strict_lowerbd R alpha Ha p q Hpq H3.
∎
Theorem. (PNo_strict_upperbd_imp_rel_strict_upperbd) The following is provable:
∀L : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀beta ∈ ordsucc alpha, ∀p : set → prop, PNo_strict_upperbd L alpha p → PNo_rel_strict_upperbd L beta p
In Proofgold the corresponding term root is 2898f0... and proposition id is 3cdd3b...
Proof:
Let L and alpha be given.
Assume Ha: ordinal alpha.
Let beta be given.
Assume Hb: beta ∈ ordsucc alpha.
Let p be given.
Assume H1: PNo_strict_upperbd L alpha p.
Let gamma be given.
Assume Hc: gamma ∈ beta.
Let q be given.
Assume Hq: PNo_downc L gamma q.
Apply Ha to the current goal.
Assume Ha1 _.
We prove the intermediate claim Lsa: ordinal (ordsucc alpha).
An exact proof term for the current goal is ordinal_ordsucc alpha Ha.
We prove the intermediate claim Lb: ordinal beta.
An exact proof term for the current goal is ordinal_Hered (ordsucc alpha) Lsa beta Hb.
We prove the intermediate claim Lb1: TransSet beta.
Apply Lb to the current goal.
Assume H _.
An exact proof term for the current goal is H.
We prove the intermediate claim Lc: ordinal gamma.
An exact proof term for the current goal is ordinal_Hered beta Lb gamma Hc.
We prove the intermediate claim Lcb: gamma ⊆ beta.
An exact proof term for the current goal is Lb1 gamma Hc.
We will prove PNoLt gamma q beta p.
Apply Hq to the current goal.
Let delta be given.
Assume H2.
Apply H2 to the current goal.
Assume Hd: ordinal delta.
Assume H2.
Apply H2 to the current goal.
Let r be given.
Assume H2.
Apply H2 to the current goal.
Assume H2: L delta r.
Assume H3: PNoLe gamma q delta r.
We prove the intermediate claim L1: PNoLt delta r alpha p.
An exact proof term for the current goal is H1 delta Hd r H2.
We prove the intermediate claim L2: PNoLt gamma q alpha p.
An exact proof term for the current goal is PNoLeLt_tra gamma delta alpha Lc Hd Ha q r p H3 L1.
We prove the intermediate claim Lca: gamma ∈ alpha.
Apply ordsuccE alpha beta Hb to the current goal.
Assume Hb1: beta ∈ alpha.
An exact proof term for the current goal is Ha1 beta Hb1 gamma Hc.
Assume Hb1: beta = alpha.
rewrite the current goal using Hb1 (from right to left).
An exact proof term for the current goal is Hc.
We prove the intermediate claim Lca2: gamma ⊆ alpha.
An exact proof term for the current goal is Ha1 gamma Lca.
We will prove PNoLt gamma q beta p.
Apply PNoLt_trichotomy_or gamma beta q p Lc Lb to the current goal.
Assume H4.
Apply H4 to the current goal.
Assume H4.
An exact proof term for the current goal is H4.
Assume H4.
Apply H4 to the current goal.
Assume H4: gamma = beta.
We will prove False.
Apply In_irref beta to the current goal.
rewrite the current goal using H4 (from right to left) at position 1.
An exact proof term for the current goal is Hc.
Assume H4: PNoLt beta p gamma q.
We will prove False.
Apply PNoLtE beta gamma p q H4 to the current goal.
rewrite the current goal using binintersect_com (from left to right).
rewrite the current goal using binintersect_Subq_eq_1 gamma beta Lcb (from left to right).
Assume H5: PNoLt_ gamma p q.
Apply H5 to the current goal.
Apply PNoLt_irref alpha p to the current goal.
Apply PNoLt_tra alpha gamma alpha Ha Lc Ha p q p to the current goal.
We will prove PNoLt alpha p gamma q.
Apply PNoLtI1 to the current goal.
We will prove PNoLt_ (alpha ∩ gamma) p q.
rewrite the current goal using binintersect_com (from left to right).
rewrite the current goal using binintersect_Subq_eq_1 gamma alpha Lca2 (from left to right).
We will prove PNoLt_ gamma p q.
An exact proof term for the current goal is H5.
We will prove PNoLt gamma q alpha p.
An exact proof term for the current goal is L2.
Assume H5: beta ∈ gamma.
We will prove False.
An exact proof term for the current goal is In_no2cycle beta gamma H5 Hc.
Assume H5: gamma ∈ beta.
Assume H6: PNoEq_ gamma p q.
Assume H7: ¬ p gamma.
Apply PNoLt_irref alpha p to the current goal.
Apply PNoLt_tra alpha gamma alpha Ha Lc Ha p q p to the current goal.
We will prove PNoLt alpha p gamma q.
Apply PNoLtI3 to the current goal.
We will prove gamma ∈ alpha.
An exact proof term for the current goal is Lca.
We will prove PNoEq_ gamma p q.
An exact proof term for the current goal is H6.
We will prove ¬ p gamma.
An exact proof term for the current goal is H7.
We will prove PNoLt gamma q alpha p.
An exact proof term for the current goal is L2.
∎
Theorem. (PNo_strict_lowerbd_imp_rel_strict_lowerbd) The following is provable:
∀R : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀beta ∈ ordsucc alpha, ∀p : set → prop, PNo_strict_lowerbd R alpha p → PNo_rel_strict_lowerbd R beta p
In Proofgold the corresponding term root is 442af5... and proposition id is 04acc2...
Proof:
Let R and alpha be given.
Assume Ha: ordinal alpha.
Let beta be given.
Assume Hb: beta ∈ ordsucc alpha.
Let p be given.
Assume H1: PNo_strict_lowerbd R alpha p.
Let gamma be given.
Assume Hc: gamma ∈ beta.
Let q be given.
Assume Hq: PNo_upc R gamma q.
Apply Ha to the current goal.
Assume Ha1 _.
We prove the intermediate claim Lsa: ordinal (ordsucc alpha).
An exact proof term for the current goal is ordinal_ordsucc alpha Ha.
We prove the intermediate claim Lb: ordinal beta.
An exact proof term for the current goal is ordinal_Hered (ordsucc alpha) Lsa beta Hb.
We prove the intermediate claim Lb1: TransSet beta.
Apply Lb to the current goal.
Assume H _.
An exact proof term for the current goal is H.
We prove the intermediate claim Lc: ordinal gamma.
An exact proof term for the current goal is ordinal_Hered beta Lb gamma Hc.
We prove the intermediate claim Lcb: gamma ⊆ beta.
An exact proof term for the current goal is Lb1 gamma Hc.
We will prove PNoLt beta p gamma q.
Apply Hq to the current goal.
Let delta be given.
Assume H2.
Apply H2 to the current goal.
Assume Hd: ordinal delta.
Assume H2.
Apply H2 to the current goal.
Let r be given.
Assume H2.
Apply H2 to the current goal.
Assume H2: R delta r.
Assume H3: PNoLe delta r gamma q.
We prove the intermediate claim L1: PNoLt alpha p delta r.
An exact proof term for the current goal is H1 delta Hd r H2.
We prove the intermediate claim L2: PNoLt alpha p gamma q.
An exact proof term for the current goal is PNoLtLe_tra alpha delta gamma Ha Hd Lc p r q L1 H3.
We prove the intermediate claim Lca: gamma ∈ alpha.
Apply ordsuccE alpha beta Hb to the current goal.
Assume Hb1: beta ∈ alpha.
An exact proof term for the current goal is Ha1 beta Hb1 gamma Hc.
Assume Hb1: beta = alpha.
rewrite the current goal using Hb1 (from right to left).
An exact proof term for the current goal is Hc.
We prove the intermediate claim Lca2: gamma ⊆ alpha.
An exact proof term for the current goal is Ha1 gamma Lca.
We will prove PNoLt beta p gamma q.
Apply PNoLt_trichotomy_or gamma beta q p Lc Lb to the current goal.
Assume H4.
Apply H4 to the current goal.
Assume H4: PNoLt gamma q beta p.
We will prove False.
Apply PNoLtE gamma beta q p H4 to the current goal.
rewrite the current goal using binintersect_Subq_eq_1 gamma beta Lcb (from left to right).
Assume H5: PNoLt_ gamma q p.
Apply H5 to the current goal.
Apply PNoLt_irref alpha p to the current goal.
Apply PNoLt_tra alpha gamma alpha Ha Lc Ha p q p to the current goal.
We will prove PNoLt alpha p gamma q.
An exact proof term for the current goal is L2.
We will prove PNoLt gamma q alpha p.
Apply PNoLtI1 to the current goal.
We will prove PNoLt_ (gamma ∩ alpha) q p.
rewrite the current goal using binintersect_Subq_eq_1 gamma alpha Lca2 (from left to right).
We will prove PNoLt_ gamma q p.
An exact proof term for the current goal is H5.
Assume H5: gamma ∈ beta.
Assume H6: PNoEq_ gamma q p.
Assume H7: p gamma.
Apply PNoLt_irref alpha p to the current goal.
Apply PNoLt_tra alpha gamma alpha Ha Lc Ha p q p to the current goal.
We will prove PNoLt alpha p gamma q.
An exact proof term for the current goal is L2.
We will prove PNoLt gamma q alpha p.
Apply PNoLtI2 to the current goal.
We will prove gamma ∈ alpha.
An exact proof term for the current goal is Lca.
We will prove PNoEq_ gamma q p.
An exact proof term for the current goal is H6.
We will prove p gamma.
An exact proof term for the current goal is H7.
Assume H5: beta ∈ gamma.
We will prove False.
An exact proof term for the current goal is In_no2cycle beta gamma H5 Hc.
Assume H4.
Apply H4 to the current goal.
Assume H4: gamma = beta.
We will prove False.
Apply In_irref beta to the current goal.
rewrite the current goal using H4 (from right to left) at position 1.
An exact proof term for the current goal is Hc.
Assume H4.
An exact proof term for the current goal is H4.
∎
Theorem. (PNo_strict_imv_imp_rel_strict_imv) The following is provable:
∀L R : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀beta ∈ ordsucc alpha, ∀p : set → prop, PNo_strict_imv L R alpha p → PNo_rel_strict_imv L R beta p
In Proofgold the corresponding term root is f4fc71... and proposition id is 46a6aa...
Proof:
Let L, R and alpha be given.
Assume Ha: ordinal alpha.
Let beta be given.
Assume Hb: beta ∈ ordsucc alpha.
Let p be given.
Assume H1: PNo_strict_imv L R alpha p.
Apply H1 to the current goal.
Assume H2: PNo_strict_upperbd L alpha p.
Assume H3: PNo_strict_lowerbd R alpha p.
We will prove PNo_rel_strict_imv L R beta p.
We will prove PNo_rel_strict_upperbd L beta p ∧ PNo_rel_strict_lowerbd R beta p.
Apply andI to the current goal.
An exact proof term for the current goal is PNo_strict_upperbd_imp_rel_strict_upperbd L alpha Ha beta Hb p H2.
An exact proof term for the current goal is PNo_strict_lowerbd_imp_rel_strict_lowerbd R alpha Ha beta Hb p H3.
∎
Theorem. (PNo_rel_split_imv_imp_strict_imv) The following is provable:
∀L R : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p : set → prop, PNo_rel_strict_split_imv L R alpha p → PNo_strict_imv L R alpha p
In Proofgold the corresponding term root is 72be36... and proposition id is adfdb0...
Proof:
Let L and R be given.
Let alpha be given.
Assume Ha: ordinal alpha.
Let p be given.
Assume Hp: PNo_rel_strict_split_imv L R alpha p.
We prove the intermediate claim Lsa: ordinal (ordsucc alpha).
An exact proof term for the current goal is ordinal_ordsucc alpha Ha.
Set p0 to be the term λdelta ⇒ p delta ∧ delta ≠ alpha of type set → prop.
Set p1 to be the term λdelta ⇒ p delta ∨ delta = alpha of type set → prop.
Apply Hp to the current goal.
Assume Hp0: PNo_rel_strict_imv L R (ordsucc alpha) p0.
Assume Hp1: PNo_rel_strict_imv L R (ordsucc alpha) p1.
Apply Hp0 to the current goal.
Assume Hp0a: PNo_rel_strict_upperbd L (ordsucc alpha) p0.
Assume Hp0b: PNo_rel_strict_lowerbd R (ordsucc alpha) p0.
Apply Hp1 to the current goal.
Assume Hp1a: PNo_rel_strict_upperbd L (ordsucc alpha) p1.
Assume Hp1b: PNo_rel_strict_lowerbd R (ordsucc alpha) p1.
We prove the intermediate claim Lnp0a: ¬ p0 alpha.
Assume H10.
Apply H10 to the current goal.
Assume H11: p alpha.
Assume H12: alpha ≠ alpha.
Apply H12 to the current goal.
Use reflexivity.
We prove the intermediate claim Lp1a: p1 alpha.
We will prove p alpha ∨ alpha = alpha.
Apply orIR to the current goal.
Use reflexivity.
We prove the intermediate claim Lap0p: PNoLt (ordsucc alpha) p0 alpha p.
Apply PNoLtI3 to the current goal.
Apply ordsuccI2 to the current goal.
We will prove PNoEq_ alpha p0 p.
Apply PNoEq_sym_ to the current goal.
Apply PNo_extend0_eq to the current goal.
We will prove ¬ p0 alpha.
An exact proof term for the current goal is Lnp0a.
We prove the intermediate claim Lapp1: PNoLt alpha p (ordsucc alpha) p1.
Apply PNoLtI2 to the current goal.
Apply ordsuccI2 to the current goal.
We will prove PNoEq_ alpha p p1.
Apply PNo_extend1_eq to the current goal.
We will prove p1 alpha.
An exact proof term for the current goal is Lp1a.
We will prove PNo_strict_upperbd L alpha p ∧ PNo_strict_lowerbd R alpha p.
Apply andI to the current goal.
Let beta be given.
Assume Hb: ordinal beta.
Let q be given.
Assume Hq: L beta q.
We will prove PNoLt beta q alpha p.
We prove the intermediate claim L4: PNo_downc L beta q.
Apply PNo_downc_ref L beta Hb to the current goal.
An exact proof term for the current goal is Hq.
We prove the intermediate claim L5: beta ∈ ordsucc alpha → PNoLt beta q alpha p.
Assume H10: beta ∈ ordsucc alpha.
Apply PNoLt_tra beta (ordsucc alpha) alpha Hb Lsa Ha q p0 p to the current goal.
We will prove PNoLt beta q (ordsucc alpha) p0.
Apply Hp0a beta H10 q to the current goal.
We will prove PNo_downc L beta q.
An exact proof term for the current goal is L4.
An exact proof term for the current goal is Lap0p.
We prove the intermediate claim L6: ∀gamma ∈ ordsucc alpha, gamma ∈ beta → PNoEq_ gamma p q → q gamma → p0 gamma.
Let gamma be given.
Assume Hc1: gamma ∈ ordsucc alpha.
Assume Hc2: gamma ∈ beta.
Assume H10: PNoEq_ gamma p q.
Assume H11: q gamma.
Apply dneg to the current goal.
Assume HNC: ¬ p0 gamma.
We prove the intermediate claim Lc: ordinal gamma.
An exact proof term for the current goal is ordinal_Hered beta Hb gamma Hc2.
We prove the intermediate claim L6a: PNoLt gamma q beta q.
Apply PNoLtI2 to the current goal.
An exact proof term for the current goal is Hc2.
We will prove PNoEq_ gamma q q.
Apply PNoEq_ref_ to the current goal.
We will prove q gamma.
An exact proof term for the current goal is H11.
We prove the intermediate claim L6b: PNo_downc L gamma q.
We will prove ∃delta, ordinal delta ∧ ∃r : set → prop, L delta r ∧ PNoLe gamma q delta r.
We use beta to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hb.
We use q to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hq.
Apply PNoLeI1 to the current goal.
An exact proof term for the current goal is L6a.
We prove the intermediate claim L6c: PNoLt gamma q (ordsucc alpha) p0.
An exact proof term for the current goal is Hp0a gamma Hc1 q L6b.
We prove the intermediate claim L6d: PNoLt (ordsucc alpha) p0 gamma q.
Apply PNoLtI3 to the current goal.
An exact proof term for the current goal is Hc1.
We will prove PNoEq_ gamma p0 q.
Apply PNoEq_tra_ gamma p0 p q to the current goal.
Apply PNoEq_sym_ to the current goal.
We will prove PNoEq_ gamma p p0.
Apply ordsuccE alpha gamma Hc1 to the current goal.
Assume H12: gamma ∈ alpha.
Apply PNoEq_antimon_ p p0 alpha Ha gamma H12 to the current goal.
We will prove PNoEq_ alpha p p0.
An exact proof term for the current goal is PNo_extend0_eq alpha p.
Assume H12: gamma = alpha.
rewrite the current goal using H12 (from left to right).
We will prove PNoEq_ alpha p p0.
An exact proof term for the current goal is PNo_extend0_eq alpha p.
An exact proof term for the current goal is H10.
We will prove ¬ p0 gamma.
An exact proof term for the current goal is HNC.
Apply PNoLt_irref gamma q to the current goal.
An exact proof term for the current goal is PNoLt_tra gamma (ordsucc alpha) gamma Lc Lsa Lc q p0 q L6c L6d.
Apply PNoLt_trichotomy_or alpha beta p q Ha Hb to the current goal.
Assume H10.
Apply H10 to the current goal.
Assume H10: PNoLt alpha p beta q.
Apply PNoLtE alpha beta p q H10 to the current goal.
Assume H11: PNoLt_ (alpha ∩ beta) p q.
Apply H11 to the current goal.
Let gamma be given.
Assume H12.
Apply H12 to the current goal.
Assume Hc: gamma ∈ alpha ∩ beta.
Assume H12.
Apply H12 to the current goal.
Assume H12.
Apply H12 to the current goal.
Assume H12: PNoEq_ gamma p q.
Assume H13: ¬ p gamma.
Assume H14: q gamma.
We will prove False.
Apply binintersectE alpha beta gamma Hc to the current goal.
Assume Hc1: gamma ∈ alpha.
Assume Hc2: gamma ∈ beta.
Apply L6 gamma (ordsuccI1 alpha gamma Hc1) Hc2 H12 H14 to the current goal.
Assume H15: p gamma.
Assume _.
Apply H13 to the current goal.
An exact proof term for the current goal is H15.
Assume H11: alpha ∈ beta.
Assume H12: PNoEq_ alpha p q.
Assume H13: q alpha.
We will prove False.
Apply Lnp0a to the current goal.
We will prove p0 alpha.
An exact proof term for the current goal is L6 alpha (ordsuccI2 alpha) H11 H12 H13.
Assume H11: beta ∈ alpha.
Assume _ _.
Apply L5 to the current goal.
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is H11.
Assume H10.
Apply H10 to the current goal.
Assume H10a: alpha = beta.
Assume H10b: PNoEq_ alpha p q.
Apply L5 to the current goal.
We will prove beta ∈ ordsucc alpha.
rewrite the current goal using H10a (from right to left).
Apply ordsuccI2 to the current goal.
Assume H10: PNoLt beta q alpha p.
An exact proof term for the current goal is H10.
Let beta be given.
Assume Hb: ordinal beta.
Let q be given.
Assume Hq: R beta q.
We will prove PNoLt alpha p beta q.
We prove the intermediate claim L4: PNo_upc R beta q.
Apply PNo_upc_ref R beta Hb to the current goal.
An exact proof term for the current goal is Hq.
We prove the intermediate claim L5: beta ∈ ordsucc alpha → PNoLt alpha p beta q.
Assume H10: beta ∈ ordsucc alpha.
Apply PNoLt_tra alpha (ordsucc alpha) beta Ha Lsa Hb p p1 q to the current goal.
An exact proof term for the current goal is Lapp1.
We will prove PNoLt (ordsucc alpha) p1 beta q.
Apply Hp1b beta H10 q to the current goal.
We will prove PNo_upc R beta q.
An exact proof term for the current goal is L4.
We prove the intermediate claim L6: ∀gamma ∈ ordsucc alpha, gamma ∈ beta → PNoEq_ gamma q p → p1 gamma → q gamma.
Let gamma be given.
Assume Hc1: gamma ∈ ordsucc alpha.
Assume Hc2: gamma ∈ beta.
Assume H10: PNoEq_ gamma q p.
Assume H11: p1 gamma.
Apply dneg to the current goal.
Assume HNC: ¬ q gamma.
We prove the intermediate claim Lc: ordinal gamma.
An exact proof term for the current goal is ordinal_Hered beta Hb gamma Hc2.
We prove the intermediate claim L6a: PNoLt beta q gamma q.
Apply PNoLtI3 to the current goal.
An exact proof term for the current goal is Hc2.
We will prove PNoEq_ gamma q q.
Apply PNoEq_ref_ to the current goal.
We will prove ¬ q gamma.
An exact proof term for the current goal is HNC.
We prove the intermediate claim L6b: PNo_upc R gamma q.
We will prove ∃delta, ordinal delta ∧ ∃r : set → prop, R delta r ∧ PNoLe delta r gamma q.
We use beta to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hb.
We use q to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hq.
Apply PNoLeI1 to the current goal.
An exact proof term for the current goal is L6a.
We prove the intermediate claim L6c: PNoLt (ordsucc alpha) p1 gamma q.
An exact proof term for the current goal is Hp1b gamma Hc1 q L6b.
We prove the intermediate claim L6d: PNoLt gamma q (ordsucc alpha) p1.
Apply PNoLtI2 to the current goal.
An exact proof term for the current goal is Hc1.
We will prove PNoEq_ gamma q p1.
Apply PNoEq_tra_ gamma q p p1 to the current goal.
An exact proof term for the current goal is H10.
We will prove PNoEq_ gamma p p1.
Apply ordsuccE alpha gamma Hc1 to the current goal.
Assume H12: gamma ∈ alpha.
Apply PNoEq_antimon_ p p1 alpha Ha gamma H12 to the current goal.
We will prove PNoEq_ alpha p p1.
An exact proof term for the current goal is PNo_extend1_eq alpha p.
Assume H12: gamma = alpha.
rewrite the current goal using H12 (from left to right).
We will prove PNoEq_ alpha p p1.
An exact proof term for the current goal is PNo_extend1_eq alpha p.
We will prove p1 gamma.
An exact proof term for the current goal is H11.
Apply PNoLt_irref gamma q to the current goal.
An exact proof term for the current goal is PNoLt_tra gamma (ordsucc alpha) gamma Lc Lsa Lc q p1 q L6d L6c.
Apply PNoLt_trichotomy_or alpha beta p q Ha Hb to the current goal.
Assume H10.
Apply H10 to the current goal.
Assume H10.
An exact proof term for the current goal is H10.
Assume H10.
Apply H10 to the current goal.
Assume H10a: alpha = beta.
Assume H10b: PNoEq_ alpha p q.
Apply L5 to the current goal.
We will prove beta ∈ ordsucc alpha.
rewrite the current goal using H10a (from right to left).
Apply ordsuccI2 to the current goal.
Assume H10: PNoLt beta q alpha p.
Apply PNoLtE beta alpha q p H10 to the current goal.
Assume H11: PNoLt_ (beta ∩ alpha) q p.
Apply H11 to the current goal.
Let gamma be given.
Assume H12.
Apply H12 to the current goal.
Assume Hc: gamma ∈ beta ∩ alpha.
Assume H12.
Apply H12 to the current goal.
Assume H12.
Apply H12 to the current goal.
Assume H12: PNoEq_ gamma q p.
Assume H13: ¬ q gamma.
Assume H14: p gamma.
We will prove False.
Apply binintersectE beta alpha gamma Hc to the current goal.
Assume Hc2: gamma ∈ beta.
Assume Hc1: gamma ∈ alpha.
Apply H13 to the current goal.
Apply L6 gamma (ordsuccI1 alpha gamma Hc1) Hc2 H12 to the current goal.
We will prove p1 gamma.
We will prove p gamma ∨ gamma = alpha.
Apply orIL to the current goal.
An exact proof term for the current goal is H14.
Assume H11: beta ∈ alpha.
Assume _ _.
Apply L5 to the current goal.
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is H11.
Assume H11: alpha ∈ beta.
Assume H12: PNoEq_ alpha q p.
Assume H13: ¬ q alpha.
We will prove False.
Apply H13 to the current goal.
An exact proof term for the current goal is L6 alpha (ordsuccI2 alpha) H11 H12 Lp1a.
∎
Theorem. (PNo_lenbdd_strict_imv_ex) The following is provable:
∀L R : set → (set → prop) → prop, PNoLt_pwise L R → ∀alpha, ordinal alpha → PNo_lenbdd alpha L → PNo_lenbdd alpha R → ∃beta ∈ ordsucc alpha, ∃p : set → prop, PNo_strict_imv L R beta p
In Proofgold the corresponding term root is 9485d6... and proposition id is a864a5...
Proof:
Let L and R be given.
Assume HLR.
Let alpha be given.
Assume Ha.
Assume HaL HaR.
Apply PNo_rel_imv_bdd_ex L R HLR alpha Ha HaL HaR to the current goal.
Let beta be given.
Assume H1.
Apply H1 to the current goal.
Assume Hb: beta ∈ ordsucc alpha.
Assume H1.
Apply H1 to the current goal.
Let p be given.
Assume Hp: PNo_rel_strict_split_imv L R beta p.
We prove the intermediate claim Lsa: ordinal (ordsucc alpha).
An exact proof term for the current goal is ordinal_ordsucc alpha Ha.
We prove the intermediate claim Lb: ordinal beta.
An exact proof term for the current goal is ordinal_Hered (ordsucc alpha) Lsa beta Hb.
We use beta to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hb.
We use p to witness the existential quantifier.
We will prove PNo_strict_imv L R beta p.
An exact proof term for the current goal is PNo_rel_split_imv_imp_strict_imv L R beta Lb p Hp.
∎
Definition. We define PNo_least_rep to be λL R beta p ⇒ ordinal beta ∧ PNo_strict_imv L R beta p ∧ ∀gamma ∈ beta, ∀q : set → prop, ¬ PNo_strict_imv L R gamma q of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → set → (set → prop) → prop.
In Proofgold the corresponding term root is 0711e2... and object id is e4c707...
Definition. We define PNo_least_rep2 to be λL R beta p ⇒ PNo_least_rep L R beta p ∧ ∀x, x ∉ beta → ¬ p x of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → set → (set → prop) → prop.
In Proofgold the corresponding term root is 1f6dc5... and object id is 09d320...
Theorem. (PNo_strict_imv_pred_eq) The following is provable:
∀L R : set → (set → prop) → prop, PNoLt_pwise L R → ∀alpha, ordinal alpha → ∀p q : set → prop, PNo_least_rep L R alpha p → PNo_strict_imv L R alpha q → ∀beta ∈ alpha, p beta ↔ q beta
In Proofgold the corresponding term root is 5e7822... and proposition id is 72e14d...
Proof:
Let L and R be given.
Assume HLR.
Let alpha be given.
Assume Ha.
Let p and q be given.
Assume Hp.
Assume Hq.
Apply Ha to the current goal.
Assume Ha1 _.
Apply Hp to the current goal.
Assume Hp1.
Apply Hp1 to the current goal.
Assume _.
Assume Hp1: PNo_strict_imv L R alpha p.
Assume Hp2: ∀beta ∈ alpha, ∀r : set → prop, ¬ PNo_strict_imv L R beta r.
Apply Hp1 to the current goal.
Assume Hp1a: PNo_strict_upperbd L alpha p.
Assume Hp1b: PNo_strict_lowerbd R alpha p.
Apply Hq to the current goal.
Assume Hq1: PNo_strict_upperbd L alpha q.
Assume Hq2: PNo_strict_lowerbd R alpha q.
We prove the intermediate claim L1: ∀beta, ordinal beta → beta ∈ alpha → (p beta ↔ q beta).
Apply ordinal_ind to the current goal.
Let beta be given.
Assume Hb1: ordinal beta.
Assume IH: ∀gamma ∈ beta, gamma ∈ alpha → (p gamma ↔ q gamma).
Assume Hb2: beta ∈ alpha.
We prove the intermediate claim Lbpq: PNoEq_ beta p q.
Let gamma be given.
Assume Hc: gamma ∈ beta.
An exact proof term for the current goal is IH gamma Hc (Ha1 beta Hb2 gamma Hc).
We will prove p beta ↔ q beta.
Apply iffI to the current goal.
Assume H1: p beta.
We will prove q beta.
Apply dneg to the current goal.
Assume H2: ¬ q beta.
We prove the intermediate claim Lqp: PNoLt beta q alpha p.
Apply PNoLtI2 to the current goal.
We will prove beta ∈ alpha.
An exact proof term for the current goal is Hb2.
We will prove PNoEq_ beta q p.
Apply PNoEq_sym_ to the current goal.
An exact proof term for the current goal is Lbpq.
We will prove p beta.
An exact proof term for the current goal is H1.
We prove the intermediate claim Lqq: PNoLt alpha q beta q.
Apply PNoLtI3 to the current goal.
We will prove beta ∈ alpha.
An exact proof term for the current goal is Hb2.
We will prove PNoEq_ beta q q.
Apply PNoEq_ref_ to the current goal.
We will prove ¬ q beta.
An exact proof term for the current goal is H2.
Apply Hp2 beta Hb2 q to the current goal.
We will prove PNo_strict_imv L R beta q.
We will prove PNo_strict_upperbd L beta q ∧ PNo_strict_lowerbd R beta q.
Apply andI to the current goal.
Let gamma be given.
Assume Hc: ordinal gamma.
Let r be given.
Assume Hr: L gamma r.
We will prove PNoLt gamma r beta q.
Apply PNoLt_tra gamma alpha beta Hc Ha Hb1 r q q to the current goal.
We will prove PNoLt gamma r alpha q.
An exact proof term for the current goal is Hq1 gamma Hc r Hr.
We will prove PNoLt alpha q beta q.
An exact proof term for the current goal is Lqq.
Let gamma be given.
Assume Hc: ordinal gamma.
Let r be given.
Assume Hr: R gamma r.
We will prove PNoLt beta q gamma r.
Apply PNoLt_tra beta alpha gamma Hb1 Ha Hc q p r to the current goal.
We will prove PNoLt beta q alpha p.
An exact proof term for the current goal is Lqp.
We will prove PNoLt alpha p gamma r.
An exact proof term for the current goal is Hp1b gamma Hc r Hr.
Assume H1: q beta.
We will prove p beta.
Apply dneg to the current goal.
Assume H2: ¬ p beta.
We prove the intermediate claim Lpq: PNoLt alpha p beta q.
Apply PNoLtI3 to the current goal.
We will prove beta ∈ alpha.
An exact proof term for the current goal is Hb2.
We will prove PNoEq_ beta p q.
An exact proof term for the current goal is Lbpq.
We will prove ¬ p beta.
An exact proof term for the current goal is H2.
We prove the intermediate claim Lqq: PNoLt beta q alpha q.
Apply PNoLtI2 to the current goal.
We will prove beta ∈ alpha.
An exact proof term for the current goal is Hb2.
We will prove PNoEq_ beta q q.
Apply PNoEq_ref_ to the current goal.
We will prove q beta.
An exact proof term for the current goal is H1.
Apply Hp2 beta Hb2 q to the current goal.
We will prove PNo_strict_imv L R beta q.
We will prove PNo_strict_upperbd L beta q ∧ PNo_strict_lowerbd R beta q.
Apply andI to the current goal.
Let gamma be given.
Assume Hc: ordinal gamma.
Let r be given.
Assume Hr: L gamma r.
We will prove PNoLt gamma r beta q.
Apply PNoLt_tra gamma alpha beta Hc Ha Hb1 r p q to the current goal.
We will prove PNoLt gamma r alpha p.
An exact proof term for the current goal is Hp1a gamma Hc r Hr.
We will prove PNoLt alpha p beta q.
An exact proof term for the current goal is Lpq.
Let gamma be given.
Assume Hc: ordinal gamma.
Let r be given.
Assume Hr: R gamma r.
We will prove PNoLt beta q gamma r.
Apply PNoLt_tra beta alpha gamma Hb1 Ha Hc q q r to the current goal.
We will prove PNoLt beta q alpha q.
An exact proof term for the current goal is Lqq.
We will prove PNoLt alpha q gamma r.
An exact proof term for the current goal is Hq2 gamma Hc r Hr.
Let beta be given.
Assume Hb: beta ∈ alpha.
An exact proof term for the current goal is L1 beta (ordinal_Hered alpha Ha beta Hb) Hb.
∎
Theorem. (PNo_lenbdd_least_rep2_exuniq2) The following is provable:
∀L R : set → (set → prop) → prop, PNoLt_pwise L R → ∀alpha, ordinal alpha → PNo_lenbdd alpha L → PNo_lenbdd alpha R → ∃beta, (∃p : set → prop, PNo_least_rep2 L R beta p) ∧ (∀p q : set → prop, PNo_least_rep2 L R beta p → PNo_least_rep2 L R beta q → p = q)
In Proofgold the corresponding term root is 5060a9... and proposition id is 8b62c5...
Proof:
Let L and R be given.
Assume HLR.
Let alpha be given.
Assume Ha HaL HaR.
We prove the intermediate claim L1: ∃beta, ordinal beta ∧ (∃p : set → prop, PNo_strict_imv L R beta p) ∧ ∀gamma ∈ beta, ¬ (∃p : set → prop, PNo_strict_imv L R gamma p).
Apply least_ordinal_ex (λbeta ⇒ ∃p : set → prop, PNo_strict_imv L R beta p) to the current goal.
We will prove ∃beta, ordinal beta ∧ ∃p : set → prop, PNo_strict_imv L R beta p.
Apply PNo_lenbdd_strict_imv_ex L R HLR alpha Ha HaL HaR to the current goal.
Let beta be given.
Assume H1.
Apply H1 to the current goal.
Assume Hb: beta ∈ ordsucc alpha.
Assume H1.
Apply H1 to the current goal.
Let p be given.
Assume Hp: PNo_strict_imv L R beta p.
We prove the intermediate claim Lsa: ordinal (ordsucc alpha).
An exact proof term for the current goal is ordinal_ordsucc alpha Ha.
We use beta to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is ordinal_Hered (ordsucc alpha) Lsa beta Hb.
We use p to witness the existential quantifier.
An exact proof term for the current goal is Hp.
Apply L1 to the current goal.
Let beta be given.
Assume H1.
Apply H1 to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1: ordinal beta.
Assume H2: ∃p : set → prop, PNo_strict_imv L R beta p.
Assume H3: ∀gamma ∈ beta, ¬ ∃p : set → prop, PNo_strict_imv L R gamma p.
Apply H2 to the current goal.
Let p be given.
Assume Hp: PNo_strict_imv L R beta p.
We use beta to witness the existential quantifier.
Apply andI to the current goal.
We use (λx ⇒ x ∈ beta ∧ p x) to witness the existential quantifier.
We will prove PNo_least_rep L R beta (λx ⇒ x ∈ beta ∧ p x) ∧ ∀x, x ∉ beta → ¬ (x ∈ beta ∧ p x).
Apply andI to the current goal.
We will prove ordinal beta ∧ PNo_strict_imv L R beta (λx ⇒ x ∈ beta ∧ p x) ∧ ∀gamma ∈ beta, ∀q : set → prop, ¬ PNo_strict_imv L R gamma q.
Apply and3I to the current goal.
An exact proof term for the current goal is H1.
Apply PNoEq_strict_imv L R beta H1 p (λx ⇒ x ∈ beta ∧ p x) to the current goal.
We will prove PNoEq_ beta p (λx ⇒ x ∈ beta ∧ p x).
Let x be given.
Assume Hx: x ∈ beta.
We will prove p x ↔ x ∈ beta ∧ p x.
Apply iffI to the current goal.
Assume H4.
Apply andI to the current goal.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is H4.
Assume H4.
Apply H4 to the current goal.
Assume _ H5.
An exact proof term for the current goal is H5.
An exact proof term for the current goal is Hp.
Let gamma be given.
Assume Hc: gamma ∈ beta.
Let q be given.
Assume H4: PNo_strict_imv L R gamma q.
We will prove False.
Apply H3 gamma Hc to the current goal.
We will prove ∃p : set → prop, PNo_strict_imv L R gamma p.
We use q to witness the existential quantifier.
We will prove PNo_strict_imv L R gamma q.
An exact proof term for the current goal is H4.
We will prove ∀x, x ∉ beta → ¬ (x ∈ beta ∧ p x).
Let x be given.
Assume Hx.
Assume H4.
Apply H4 to the current goal.
Assume H5 _.
An exact proof term for the current goal is Hx H5.
Let q and r be given.
Assume Hq: PNo_least_rep2 L R beta q.
Assume Hr: PNo_least_rep2 L R beta r.
Apply Hq to the current goal.
Assume Hq1 Hq2.
Apply Hr to the current goal.
Assume Hr1 Hr2.
We will prove q = r.
Apply pred_ext to the current goal.
Let x be given.
Apply xm (x ∈ beta) to the current goal.
Assume H4: x ∈ beta.
We will prove q x ↔ r x.
Apply Hr1 to the current goal.
Assume Hr1a.
Apply Hr1a to the current goal.
Assume _.
Assume Hr1a: PNo_strict_imv L R beta r.
Assume _.
An exact proof term for the current goal is PNo_strict_imv_pred_eq L R HLR beta H1 q r Hq1 Hr1a x H4.
Assume H4: x ∉ beta.
Apply iffI to the current goal.
Assume H5: q x.
We will prove False.
Apply Hq2 x H4 to the current goal.
An exact proof term for the current goal is H5.
Assume H5: r x.
We will prove False.
Apply Hr2 x H4 to the current goal.
An exact proof term for the current goal is H5.
∎
Definition. We define PNo_bd to be λL R ⇒ DescrR_i_io_1 (PNo_least_rep2 L R) of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → set.
In Proofgold the corresponding term root is ed76e7... and object id is aa75ef...
Definition. We define PNo_pred to be λL R ⇒ DescrR_i_io_2 (PNo_least_rep2 L R) of type (set → (set → prop) → prop) → (set → (set → prop) → prop) → set → prop.
In Proofgold the corresponding term root is b2d51d... and object id is 2efd18...
Theorem. (PNo_bd_pred_lem) The following is provable:
∀L R : set → (set → prop) → prop, PNoLt_pwise L R → ∀alpha, ordinal alpha → PNo_lenbdd alpha L → PNo_lenbdd alpha R → PNo_least_rep2 L R (PNo_bd L R) (PNo_pred L R)
In Proofgold the corresponding term root is 749b8f... and proposition id is 5de4a3...
Proof:
Let L and R be given.
Assume HLR.
Let alpha be given.
Assume Ha HaL HaR.
An exact proof term for the current goal is DescrR_i_io_12 (PNo_least_rep2 L R) (PNo_lenbdd_least_rep2_exuniq2 L R HLR alpha Ha HaL HaR).
∎
Theorem. (PNo_bd_pred) The following is provable:
∀L R : set → (set → prop) → prop, PNoLt_pwise L R → ∀alpha, ordinal alpha → PNo_lenbdd alpha L → PNo_lenbdd alpha R → PNo_least_rep L R (PNo_bd L R) (PNo_pred L R)
In Proofgold the corresponding term root is 42224b... and proposition id is 3309f6...
Proof:
Let L and R be given.
Assume HLR.
Let alpha be given.
Assume Ha HaL HaR.
Apply PNo_bd_pred_lem L R HLR alpha Ha HaL HaR to the current goal.
Assume H _.
An exact proof term for the current goal is H.
∎
Theorem. (PNo_bd_In) The following is provable:
∀L R : set → (set → prop) → prop, PNoLt_pwise L R → ∀alpha, ordinal alpha → PNo_lenbdd alpha L → PNo_lenbdd alpha R → PNo_bd L R ∈ ordsucc alpha
In Proofgold the corresponding term root is ad857b... and proposition id is 4719e1...
Proof:
Let L and R be given.
Assume HLR.
Let alpha be given.
Assume Ha HaL HaR.
Apply PNo_bd_pred L R HLR alpha Ha HaL HaR to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1: ordinal (PNo_bd L R).
Assume H2: PNo_strict_imv L R (PNo_bd L R) (PNo_pred L R).
Assume H3: ∀gamma ∈ PNo_bd L R, ∀q : set → prop, ¬ PNo_strict_imv L R gamma q.
Apply PNo_lenbdd_strict_imv_ex L R HLR alpha Ha HaL HaR to the current goal.
Let beta be given.
Assume H4.
Apply H4 to the current goal.
Assume Hb: beta ∈ ordsucc alpha.
Assume H4.
Apply H4 to the current goal.
Let p be given.
Assume Hp: PNo_strict_imv L R beta p.
We prove the intermediate claim Lsa: ordinal (ordsucc alpha).
An exact proof term for the current goal is ordinal_ordsucc alpha Ha.
Apply ordinal_In_Or_Subq (PNo_bd L R) (ordsucc alpha) H1 Lsa to the current goal.
Assume H4: PNo_bd L R ∈ ordsucc alpha.
An exact proof term for the current goal is H4.
Assume H4: ordsucc alpha ⊆ PNo_bd L R.
We will prove False.
We prove the intermediate claim Lb: beta ∈ PNo_bd L R.
Apply H4 to the current goal.
An exact proof term for the current goal is Hb.
Apply H3 beta Lb p to the current goal.
An exact proof term for the current goal is Hp.
∎