![]() |
Metamath
Proof Explorer Theorem List (p. 336 of 454) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | brimageg 33501 | Closed form of brimage 33500. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴Image𝑅𝐵 ↔ 𝐵 = (𝑅 “ 𝐴))) | ||
Theorem | funimage 33502 | Image𝐴 is a function. (Contributed by Scott Fenton, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ Fun Image𝐴 | ||
Theorem | fnimage 33503* | Image𝑅 is a function over the set-like portion of 𝑅. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ Image𝑅 Fn {𝑥 ∣ (𝑅 “ 𝑥) ∈ V} | ||
Theorem | imageval 33504* | The image functor in maps-to notation. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ Image𝑅 = (𝑥 ∈ V ↦ (𝑅 “ 𝑥)) | ||
Theorem | fvimage 33505 | Value of the image functor. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑅 “ 𝐴) ∈ 𝑊) → (Image𝑅‘𝐴) = (𝑅 “ 𝐴)) | ||
Theorem | brcart 33506 | Binary relation form of the cartesian product operator. (Contributed by Scott Fenton, 11-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉Cart𝐶 ↔ 𝐶 = (𝐴 × 𝐵)) | ||
Theorem | brdomain 33507 | Binary relation form of the domain function. (Contributed by Scott Fenton, 11-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴Domain𝐵 ↔ 𝐵 = dom 𝐴) | ||
Theorem | brrange 33508 | Binary relation form of the range function. (Contributed by Scott Fenton, 11-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴Range𝐵 ↔ 𝐵 = ran 𝐴) | ||
Theorem | brdomaing 33509 | Closed form of brdomain 33507. (Contributed by Scott Fenton, 2-May-2014.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴Domain𝐵 ↔ 𝐵 = dom 𝐴)) | ||
Theorem | brrangeg 33510 | Closed form of brrange 33508. (Contributed by Scott Fenton, 3-May-2014.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴Range𝐵 ↔ 𝐵 = ran 𝐴)) | ||
Theorem | brimg 33511 | Binary relation form of the Img function. (Contributed by Scott Fenton, 12-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉Img𝐶 ↔ 𝐶 = (𝐴 “ 𝐵)) | ||
Theorem | brapply 33512 | Binary relation form of the Apply function. (Contributed by Scott Fenton, 12-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉Apply𝐶 ↔ 𝐶 = (𝐴‘𝐵)) | ||
Theorem | brcup 33513 | Binary relation form of the Cup function. (Contributed by Scott Fenton, 14-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉Cup𝐶 ↔ 𝐶 = (𝐴 ∪ 𝐵)) | ||
Theorem | brcap 33514 | Binary relation form of the Cap function. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉Cap𝐶 ↔ 𝐶 = (𝐴 ∩ 𝐵)) | ||
Theorem | brsuccf 33515 | Binary relation form of the Succ function. (Contributed by Scott Fenton, 14-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴Succ𝐵 ↔ 𝐵 = suc 𝐴) | ||
Theorem | funpartlem 33516* | Lemma for funpartfun 33517. Show membership in the restriction. (Contributed by Scott Fenton, 4-Dec-2017.) |
⊢ (𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )) ↔ ∃𝑥(𝐹 “ {𝐴}) = {𝑥}) | ||
Theorem | funpartfun 33517 | The functional part of 𝐹 is a function. (Contributed by Scott Fenton, 16-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
⊢ Fun Funpart𝐹 | ||
Theorem | funpartss 33518 | The functional part of 𝐹 is a subset of 𝐹. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ Funpart𝐹 ⊆ 𝐹 | ||
Theorem | funpartfv 33519 | The function value of the functional part is identical to the original functional value. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (Funpart𝐹‘𝐴) = (𝐹‘𝐴) | ||
Theorem | fullfunfnv 33520 | The full functional part of 𝐹 is a function over V. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ FullFun𝐹 Fn V | ||
Theorem | fullfunfv 33521 | The function value of the full function of 𝐹 agrees with 𝐹. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (FullFun𝐹‘𝐴) = (𝐹‘𝐴) | ||
Theorem | brfullfun 33522 | A binary relation form condition for the full function. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴FullFun𝐹𝐵 ↔ 𝐵 = (𝐹‘𝐴)) | ||
Theorem | brrestrict 33523 | Binary relation form of the Restrict function. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉Restrict𝐶 ↔ 𝐶 = (𝐴 ↾ 𝐵)) | ||
Theorem | dfrecs2 33524 | A quantifier-free definition of recs. (Contributed by Scott Fenton, 17-Jul-2020.) |
⊢ recs(𝐹) = ∪ (( Funs ∩ (◡Domain “ On)) ∖ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (FullFun𝐹 ∘ Restrict)))) | ||
Theorem | dfrdg4 33525 | A quantifier-free definition of the recursive definition generator. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
⊢ rec(𝐹, 𝐴) = ∪ (( Funs ∩ (◡Domain “ On)) ∖ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))))) | ||
Theorem | dfint3 33526 | Quantifier-free definition of class intersection. (Contributed by Scott Fenton, 13-Apr-2018.) |
⊢ ∩ 𝐴 = (V ∖ (◡(V ∖ E ) “ 𝐴)) | ||
Theorem | imagesset 33527 | The Image functor applied to the converse of the subset relationship yields a subset of the subset relationship. (Contributed by Scott Fenton, 14-Apr-2018.) |
⊢ Image◡ SSet ⊆ SSet | ||
Theorem | brub 33528* | Binary relation form of the upper bound functor. (Contributed by Scott Fenton, 3-May-2018.) |
⊢ 𝑆 ∈ V & ⊢ 𝐴 ∈ V ⇒ ⊢ (𝑆UB𝑅𝐴 ↔ ∀𝑥 ∈ 𝑆 𝑥𝑅𝐴) | ||
Theorem | brlb 33529* | Binary relation form of the lower bound functor. (Contributed by Scott Fenton, 3-May-2018.) |
⊢ 𝑆 ∈ V & ⊢ 𝐴 ∈ V ⇒ ⊢ (𝑆LB𝑅𝐴 ↔ ∀𝑥 ∈ 𝑆 𝐴𝑅𝑥) | ||
Syntax | caltop 33530 | Declare the syntax for an alternate ordered pair. |
class ⟪𝐴, 𝐵⟫ | ||
Syntax | caltxp 33531 | Declare the syntax for an alternate Cartesian product. |
class (𝐴 ×× 𝐵) | ||
Definition | df-altop 33532 | An alternative definition of ordered pairs. This definition removes a hypothesis from its defining theorem (see altopth 33543), making it more convenient in some circumstances. (Contributed by Scott Fenton, 22-Mar-2012.) |
⊢ ⟪𝐴, 𝐵⟫ = {{𝐴}, {𝐴, {𝐵}}} | ||
Definition | df-altxp 33533* | Define Cartesian products of alternative ordered pairs. (Contributed by Scott Fenton, 23-Mar-2012.) |
⊢ (𝐴 ×× 𝐵) = {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = ⟪𝑥, 𝑦⟫} | ||
Theorem | altopex 33534 | Alternative ordered pairs always exist. (Contributed by Scott Fenton, 22-Mar-2012.) |
⊢ ⟪𝐴, 𝐵⟫ ∈ V | ||
Theorem | altopthsn 33535 | Two alternate ordered pairs are equal iff the singletons of their respective elements are equal. Note that this holds regardless of sethood of any of the elements. (Contributed by Scott Fenton, 16-Apr-2012.) |
⊢ (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ ({𝐴} = {𝐶} ∧ {𝐵} = {𝐷})) | ||
Theorem | altopeq12 33536 | Equality for alternate ordered pairs. (Contributed by Scott Fenton, 22-Mar-2012.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → ⟪𝐴, 𝐶⟫ = ⟪𝐵, 𝐷⟫) | ||
Theorem | altopeq1 33537 | Equality for alternate ordered pairs. (Contributed by Scott Fenton, 22-Mar-2012.) |
⊢ (𝐴 = 𝐵 → ⟪𝐴, 𝐶⟫ = ⟪𝐵, 𝐶⟫) | ||
Theorem | altopeq2 33538 | Equality for alternate ordered pairs. (Contributed by Scott Fenton, 22-Mar-2012.) |
⊢ (𝐴 = 𝐵 → ⟪𝐶, 𝐴⟫ = ⟪𝐶, 𝐵⟫) | ||
Theorem | altopth1 33539 | Equality of the first members of equal alternate ordered pairs, which holds regardless of the second members' sethood. (Contributed by Scott Fenton, 22-Mar-2012.) |
⊢ (𝐴 ∈ 𝑉 → (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ → 𝐴 = 𝐶)) | ||
Theorem | altopth2 33540 | Equality of the second members of equal alternate ordered pairs, which holds regardless of the first members' sethood. (Contributed by Scott Fenton, 22-Mar-2012.) |
⊢ (𝐵 ∈ 𝑉 → (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ → 𝐵 = 𝐷)) | ||
Theorem | altopthg 33541 | Alternate ordered pair theorem. (Contributed by Scott Fenton, 22-Mar-2012.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) | ||
Theorem | altopthbg 33542 | Alternate ordered pair theorem. (Contributed by Scott Fenton, 14-Apr-2012.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊) → (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) | ||
Theorem | altopth 33543 | The alternate ordered pair theorem. If two alternate ordered pairs are equal, their first elements are equal and their second elements are equal. Note that 𝐶 and 𝐷 are not required to be a set due to a peculiarity of our specific ordered pair definition, as opposed to the regular ordered pairs used here, which (as in opth 5333), requires 𝐷 to be a set. (Contributed by Scott Fenton, 23-Mar-2012.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
Theorem | altopthb 33544 | Alternate ordered pair theorem with different sethood requirements. See altopth 33543 for more comments. (Contributed by Scott Fenton, 14-Apr-2012.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
Theorem | altopthc 33545 | Alternate ordered pair theorem with different sethood requirements. See altopth 33543 for more comments. (Contributed by Scott Fenton, 14-Apr-2012.) |
⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
Theorem | altopthd 33546 | Alternate ordered pair theorem with different sethood requirements. See altopth 33543 for more comments. (Contributed by Scott Fenton, 14-Apr-2012.) |
⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
Theorem | altxpeq1 33547 | Equality for alternate Cartesian products. (Contributed by Scott Fenton, 24-Mar-2012.) |
⊢ (𝐴 = 𝐵 → (𝐴 ×× 𝐶) = (𝐵 ×× 𝐶)) | ||
Theorem | altxpeq2 33548 | Equality for alternate Cartesian products. (Contributed by Scott Fenton, 24-Mar-2012.) |
⊢ (𝐴 = 𝐵 → (𝐶 ×× 𝐴) = (𝐶 ×× 𝐵)) | ||
Theorem | elaltxp 33549* | Membership in alternate Cartesian products. (Contributed by Scott Fenton, 23-Mar-2012.) |
⊢ (𝑋 ∈ (𝐴 ×× 𝐵) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑋 = ⟪𝑥, 𝑦⟫) | ||
Theorem | altopelaltxp 33550 | Alternate ordered pair membership in a Cartesian product. Note that, unlike opelxp 5555, there is no sethood requirement here. (Contributed by Scott Fenton, 22-Mar-2012.) |
⊢ (⟪𝑋, 𝑌⟫ ∈ (𝐴 ×× 𝐵) ↔ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵)) | ||
Theorem | altxpsspw 33551 | An inclusion rule for alternate Cartesian products. (Contributed by Scott Fenton, 24-Mar-2012.) |
⊢ (𝐴 ×× 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝒫 𝐵) | ||
Theorem | altxpexg 33552 | The alternate Cartesian product of two sets is a set. (Contributed by Scott Fenton, 24-Mar-2012.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ×× 𝐵) ∈ V) | ||
Theorem | rankaltopb 33553 | Compute the rank of an alternate ordered pair. (Contributed by Scott Fenton, 18-Dec-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ ∪ (𝑅1 “ On)) → (rank‘⟪𝐴, 𝐵⟫) = suc suc ((rank‘𝐴) ∪ suc (rank‘𝐵))) | ||
Theorem | nfaltop 33554 | Bound-variable hypothesis builder for alternate ordered pairs. (Contributed by Scott Fenton, 25-Sep-2015.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥⟪𝐴, 𝐵⟫ | ||
Theorem | sbcaltop 33555* | Distribution of class substitution over alternate ordered pairs. (Contributed by Scott Fenton, 25-Sep-2015.) |
⊢ (𝐴 ∈ V → ⦋𝐴 / 𝑥⦌⟪𝐶, 𝐷⟫ = ⟪⦋𝐴 / 𝑥⦌𝐶, ⦋𝐴 / 𝑥⦌𝐷⟫) | ||
Syntax | cofs 33556 | Declare the syntax for the outer five segment configuration. |
class OuterFiveSeg | ||
Definition | df-ofs 33557* | The outer five segment configuration is an abbreviation for the conditions of the Five Segment Axiom (ax5seg 26732). See brofs 33579 and 5segofs 33580 for how it is used. Definition 2.10 of [Schwabhauser] p. 28. (Contributed by Scott Fenton, 21-Sep-2013.) |
⊢ OuterFiveSeg = {〈𝑝, 𝑞〉 ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑞 = 〈〈𝑥, 𝑦〉, 〈𝑧, 𝑤〉〉 ∧ ((𝑏 Btwn 〈𝑎, 𝑐〉 ∧ 𝑦 Btwn 〈𝑥, 𝑧〉) ∧ (〈𝑎, 𝑏〉Cgr〈𝑥, 𝑦〉 ∧ 〈𝑏, 𝑐〉Cgr〈𝑦, 𝑧〉) ∧ (〈𝑎, 𝑑〉Cgr〈𝑥, 𝑤〉 ∧ 〈𝑏, 𝑑〉Cgr〈𝑦, 𝑤〉)))} | ||
Theorem | cgrrflx2d 33558 | Deduction form of axcgrrflx 26708. (Contributed by Scott Fenton, 13-Oct-2013.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) ⇒ ⊢ (𝜑 → 〈𝐴, 𝐵〉Cgr〈𝐵, 𝐴〉) | ||
Theorem | cgrtr4d 33559 | Deduction form of axcgrtr 26709. (Contributed by Scott Fenton, 13-Oct-2013.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐸 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐹 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉) & ⊢ (𝜑 → 〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉) ⇒ ⊢ (𝜑 → 〈𝐶, 𝐷〉Cgr〈𝐸, 𝐹〉) | ||
Theorem | cgrtr4and 33560 | Deduction form of axcgrtr 26709. (Contributed by Scott Fenton, 13-Oct-2013.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐸 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐹 ∈ (𝔼‘𝑁)) & ⊢ ((𝜑 ∧ 𝜓) → 〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉) & ⊢ ((𝜑 ∧ 𝜓) → 〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 〈𝐶, 𝐷〉Cgr〈𝐸, 𝐹〉) | ||
Theorem | cgrrflx 33561 | Reflexivity law for congruence. Theorem 2.1 of [Schwabhauser] p. 27. (Contributed by Scott Fenton, 12-Jun-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → 〈𝐴, 𝐵〉Cgr〈𝐴, 𝐵〉) | ||
Theorem | cgrrflxd 33562 | Deduction form of cgrrflx 33561. (Contributed by Scott Fenton, 13-Oct-2013.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) ⇒ ⊢ (𝜑 → 〈𝐴, 𝐵〉Cgr〈𝐴, 𝐵〉) | ||
Theorem | cgrcomim 33563 | Congruence commutes on the two sides. Implication version. Theorem 2.2 of [Schwabhauser] p. 27. (Contributed by Scott Fenton, 12-Jun-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉 → 〈𝐶, 𝐷〉Cgr〈𝐴, 𝐵〉)) | ||
Theorem | cgrcom 33564 | Congruence commutes between the two sides. (Contributed by Scott Fenton, 12-Jun-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉 ↔ 〈𝐶, 𝐷〉Cgr〈𝐴, 𝐵〉)) | ||
Theorem | cgrcomand 33565 | Deduction form of cgrcom 33564. (Contributed by Scott Fenton, 13-Oct-2013.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁)) & ⊢ ((𝜑 ∧ 𝜓) → 〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 〈𝐶, 𝐷〉Cgr〈𝐴, 𝐵〉) | ||
Theorem | cgrtr 33566 | Transitivity law for congruence. Theorem 2.3 of [Schwabhauser] p. 27. (Contributed by Scott Fenton, 24-Sep-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → ((〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝐹〉) → 〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉)) | ||
Theorem | cgrtrand 33567 | Deduction form of cgrtr 33566. (Contributed by Scott Fenton, 13-Oct-2013.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐸 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐹 ∈ (𝔼‘𝑁)) & ⊢ ((𝜑 ∧ 𝜓) → 〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉) & ⊢ ((𝜑 ∧ 𝜓) → 〈𝐶, 𝐷〉Cgr〈𝐸, 𝐹〉) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉) | ||
Theorem | cgrtr3 33568 | Transitivity law for congruence. (Contributed by Scott Fenton, 7-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → ((〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝐹〉) → 〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉)) | ||
Theorem | cgrtr3and 33569 | Deduction form of cgrtr3 33568. (Contributed by Scott Fenton, 13-Oct-2013.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐸 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐹 ∈ (𝔼‘𝑁)) & ⊢ ((𝜑 ∧ 𝜓) → 〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉) & ⊢ ((𝜑 ∧ 𝜓) → 〈𝐶, 𝐷〉Cgr〈𝐸, 𝐹〉) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉) | ||
Theorem | cgrcoml 33570 | Congruence commutes on the left. Biconditional version of Theorem 2.4 of [Schwabhauser] p. 27. (Contributed by Scott Fenton, 12-Jun-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉 ↔ 〈𝐵, 𝐴〉Cgr〈𝐶, 𝐷〉)) | ||
Theorem | cgrcomr 33571 | Congruence commutes on the right. Biconditional version of Theorem 2.5 of [Schwabhauser] p. 27. (Contributed by Scott Fenton, 12-Jun-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉 ↔ 〈𝐴, 𝐵〉Cgr〈𝐷, 𝐶〉)) | ||
Theorem | cgrcomlr 33572 | Congruence commutes on both sides. (Contributed by Scott Fenton, 12-Jun-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉 ↔ 〈𝐵, 𝐴〉Cgr〈𝐷, 𝐶〉)) | ||
Theorem | cgrcomland 33573 | Deduction form of cgrcoml 33570. (Contributed by Scott Fenton, 14-Oct-2013.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁)) & ⊢ ((𝜑 ∧ 𝜓) → 〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 〈𝐵, 𝐴〉Cgr〈𝐶, 𝐷〉) | ||
Theorem | cgrcomrand 33574 | Deduction form of cgrcoml 33570. (Contributed by Scott Fenton, 14-Oct-2013.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁)) & ⊢ ((𝜑 ∧ 𝜓) → 〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 〈𝐴, 𝐵〉Cgr〈𝐷, 𝐶〉) | ||
Theorem | cgrcomlrand 33575 | Deduction form of cgrcomlr 33572. (Contributed by Scott Fenton, 14-Oct-2013.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁)) & ⊢ ((𝜑 ∧ 𝜓) → 〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 〈𝐵, 𝐴〉Cgr〈𝐷, 𝐶〉) | ||
Theorem | cgrtriv 33576 | Degenerate segments are congruent. Theorem 2.8 of [Schwabhauser] p. 28. (Contributed by Scott Fenton, 12-Jun-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → 〈𝐴, 𝐴〉Cgr〈𝐵, 𝐵〉) | ||
Theorem | cgrid2 33577 | Identity law for congruence. (Contributed by Scott Fenton, 12-Jun-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐴〉Cgr〈𝐵, 𝐶〉 → 𝐵 = 𝐶)) | ||
Theorem | cgrdegen 33578 | Two congruent segments are either both degenerate or both nondegenerate. (Contributed by Scott Fenton, 12-Jun-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉 → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷))) | ||
Theorem | brofs 33579 | Binary relation form of the outer five segment predicate. (Contributed by Scott Fenton, 21-Sep-2013.) |
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 OuterFiveSeg 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 ↔ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐵, 𝐷〉Cgr〈𝐹, 𝐻〉)))) | ||
Theorem | 5segofs 33580 | Rephrase ax5seg 26732 using the outer five segment predicate. Theorem 2.10 of [Schwabhauser] p. 28. (Contributed by Scott Fenton, 21-Sep-2013.) |
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → ((〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 OuterFiveSeg 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 ∧ 𝐴 ≠ 𝐵) → 〈𝐶, 𝐷〉Cgr〈𝐺, 𝐻〉)) | ||
Theorem | ofscom 33581 | The outer five segment predicate commutes. (Contributed by Scott Fenton, 26-Sep-2013.) |
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 OuterFiveSeg 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 ↔ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 OuterFiveSeg 〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉)) | ||
Theorem | cgrextend 33582 | Link congruence over a pair of line segments. Theorem 2.11 of [Schwabhauser] p. 29. (Contributed by Scott Fenton, 12-Jun-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐸 Btwn 〈𝐷, 𝐹〉) ∧ (〈𝐴, 𝐵〉Cgr〈𝐷, 𝐸〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐸, 𝐹〉)) → 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉)) | ||
Theorem | cgrextendand 33583 | Deduction form of cgrextend 33582. (Contributed by Scott Fenton, 14-Oct-2013.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐸 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐹 ∈ (𝔼‘𝑁)) & ⊢ ((𝜑 ∧ 𝜓) → 𝐵 Btwn 〈𝐴, 𝐶〉) & ⊢ ((𝜑 ∧ 𝜓) → 𝐸 Btwn 〈𝐷, 𝐹〉) & ⊢ ((𝜑 ∧ 𝜓) → 〈𝐴, 𝐵〉Cgr〈𝐷, 𝐸〉) & ⊢ ((𝜑 ∧ 𝜓) → 〈𝐵, 𝐶〉Cgr〈𝐸, 𝐹〉) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 〈𝐴, 𝐶〉Cgr〈𝐷, 𝐹〉) | ||
Theorem | segconeq 33584 | Two points that satisfy the conclusion of axsegcon 26721 are identical. Uniqueness portion of Theorem 2.12 of [Schwabhauser] p. 29. (Contributed by Scott Fenton, 12-Jun-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑋 ∈ (𝔼‘𝑁) ∧ 𝑌 ∈ (𝔼‘𝑁))) → ((𝑄 ≠ 𝐴 ∧ (𝐴 Btwn 〈𝑄, 𝑋〉 ∧ 〈𝐴, 𝑋〉Cgr〈𝐵, 𝐶〉) ∧ (𝐴 Btwn 〈𝑄, 𝑌〉 ∧ 〈𝐴, 𝑌〉Cgr〈𝐵, 𝐶〉)) → 𝑋 = 𝑌)) | ||
Theorem | segconeu 33585* | Existential uniqueness version of segconeq 33584. (Contributed by Scott Fenton, 19-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ 𝐶 ≠ 𝐷)) → ∃!𝑟 ∈ (𝔼‘𝑁)(𝐷 Btwn 〈𝐶, 𝑟〉 ∧ 〈𝐷, 𝑟〉Cgr〈𝐴, 𝐵〉)) | ||
Theorem | btwntriv2 33586 | Betweenness always holds for the second endpoint. Theorem 3.1 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 12-Jun-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → 𝐵 Btwn 〈𝐴, 𝐵〉) | ||
Theorem | btwncomim 33587 | Betweenness commutes. Implication version. Theorem 3.2 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 12-Jun-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐴 Btwn 〈𝐵, 𝐶〉 → 𝐴 Btwn 〈𝐶, 𝐵〉)) | ||
Theorem | btwncom 33588 | Betweenness commutes. (Contributed by Scott Fenton, 12-Jun-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐴 Btwn 〈𝐵, 𝐶〉 ↔ 𝐴 Btwn 〈𝐶, 𝐵〉)) | ||
Theorem | btwncomand 33589 | Deduction form of btwncom 33588. (Contributed by Scott Fenton, 14-Oct-2013.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁)) & ⊢ ((𝜑 ∧ 𝜓) → 𝐴 Btwn 〈𝐵, 𝐶〉) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝐴 Btwn 〈𝐶, 𝐵〉) | ||
Theorem | btwntriv1 33590 | Betweenness always holds for the first endpoint. Theorem 3.3 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 12-Jun-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → 𝐴 Btwn 〈𝐴, 𝐵〉) | ||
Theorem | btwnswapid 33591 | If you can swap the first two arguments of a betweenness statement, then those arguments are identical. Theorem 3.4 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 12-Jun-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → ((𝐴 Btwn 〈𝐵, 𝐶〉 ∧ 𝐵 Btwn 〈𝐴, 𝐶〉) → 𝐴 = 𝐵)) | ||
Theorem | btwnswapid2 33592 | If you can swap arguments one and three of a betweenness statement, then those arguments are identical. (Contributed by Scott Fenton, 7-Oct-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → ((𝐴 Btwn 〈𝐵, 𝐶〉 ∧ 𝐶 Btwn 〈𝐵, 𝐴〉) → 𝐴 = 𝐶)) | ||
Theorem | btwnintr 33593 | Inner transitivity law for betweenness. Left-hand side of Theorem 3.5 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 12-Jun-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn 〈𝐴, 𝐷〉 ∧ 𝐶 Btwn 〈𝐵, 𝐷〉) → 𝐵 Btwn 〈𝐴, 𝐶〉)) | ||
Theorem | btwnexch3 33594 | Exchange the first endpoint in betweenness. Left-hand side of Theorem 3.6 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 12-Jun-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐶 Btwn 〈𝐴, 𝐷〉) → 𝐶 Btwn 〈𝐵, 𝐷〉)) | ||
Theorem | btwnexch3and 33595 | Deduction form of btwnexch3 33594. (Contributed by Scott Fenton, 13-Oct-2013.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁)) & ⊢ ((𝜑 ∧ 𝜓) → 𝐵 Btwn 〈𝐴, 𝐶〉) & ⊢ ((𝜑 ∧ 𝜓) → 𝐶 Btwn 〈𝐴, 𝐷〉) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝐶 Btwn 〈𝐵, 𝐷〉) | ||
Theorem | btwnouttr2 33596 | Outer transitivity law for betweenness. Left-hand side of Theorem 3.1 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 12-Jun-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((𝐵 ≠ 𝐶 ∧ 𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐶 Btwn 〈𝐵, 𝐷〉) → 𝐶 Btwn 〈𝐴, 𝐷〉)) | ||
Theorem | btwnexch2 33597 | Exchange the outer point of two betweenness statements. Right-hand side of Theorem 3.5 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 14-Jun-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn 〈𝐴, 𝐷〉 ∧ 𝐶 Btwn 〈𝐵, 𝐷〉) → 𝐶 Btwn 〈𝐴, 𝐷〉)) | ||
Theorem | btwnouttr 33598 | Outer transitivity law for betweenness. Right-hand side of Theorem 3.7 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 14-Jun-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((𝐵 ≠ 𝐶 ∧ 𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐶 Btwn 〈𝐵, 𝐷〉) → 𝐵 Btwn 〈𝐴, 𝐷〉)) | ||
Theorem | btwnexch 33599 | Outer transitivity law for betweenness. Right-hand side of Theorem 3.6 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 24-Sep-2013.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐶 Btwn 〈𝐴, 𝐷〉) → 𝐵 Btwn 〈𝐴, 𝐷〉)) | ||
Theorem | btwnexchand 33600 | Deduction form of btwnexch 33599. (Contributed by Scott Fenton, 13-Oct-2013.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁)) & ⊢ ((𝜑 ∧ 𝜓) → 𝐵 Btwn 〈𝐴, 𝐶〉) & ⊢ ((𝜑 ∧ 𝜓) → 𝐶 Btwn 〈𝐴, 𝐷〉) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝐵 Btwn 〈𝐴, 𝐷〉) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |