P. 51 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 5001-5100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ssopab2 5001	Equivalence of ordered pair abstraction subclass and implication. (Contributed by NM, 27-Dec-1996.) (Revised by Mario Carneiro, 19-May-2013.)
⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) → {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝜓})
Theorem	ssopab2b 5002	Equivalence of ordered pair abstraction subclass and implication. (Contributed by NM, 27-Dec-1996.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
⊢ ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝜓} ↔ ∀𝑥∀𝑦(𝜑 → 𝜓))
Theorem	ssopab2i 5003	Inference of ordered pair abstraction subclass from implication. (Contributed by NM, 5-Apr-1995.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝜓}
Theorem	ssopab2dv 5004*	Inference of ordered pair abstraction subclass from implication. (Contributed by NM, 19-Jan-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝜒})
Theorem	eqopab2b 5005	Equivalence of ordered pair abstraction equality and biconditional. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ ({⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓} ↔ ∀𝑥∀𝑦(𝜑 ↔ 𝜓))
Theorem	opabn0 5006	Nonempty ordered pair class abstraction. (Contributed by NM, 10-Oct-2007.)
⊢ ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ≠ ∅ ↔ ∃𝑥∃𝑦𝜑)
Theorem	opab0 5007	Empty ordered pair class abstraction. (Contributed by AV, 29-Oct-2021.)
⊢ ({⟨𝑥, 𝑦⟩ ∣ 𝜑} = ∅ ↔ ∀𝑥∀𝑦 ¬ 𝜑)
Theorem	csbopab 5008*	Move substitution into a class abstraction. Version of csbopabgALT 5009 without a sethood antecedent but depending on more axioms. (Contributed by NM, 6-Aug-2007.) (Revised by NM, 23-Aug-2018.)
⊢ ⦋𝐴 / 𝑥⦌{⟨𝑦, 𝑧⟩ ∣ 𝜑} = {⟨𝑦, 𝑧⟩ ∣ [𝐴 / 𝑥]𝜑}
Theorem	csbopabgALT 5009*	Move substitution into a class abstraction. Version of csbopab 5008 with a sethood antecedent but depending on fewer axioms. (Contributed by NM, 6-Aug-2007.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌{⟨𝑦, 𝑧⟩ ∣ 𝜑} = {⟨𝑦, 𝑧⟩ ∣ [𝐴 / 𝑥]𝜑})
Theorem	csbmpt12 5010*	Move substitution into a maps-to notation. (Contributed by AV, 26-Sep-2019.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝑦 ∈ 𝑌 ↦ 𝑍) = (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝑌 ↦ ⦋𝐴 / 𝑥⦌𝑍))
Theorem	csbmpt2 5011*	Move substitution into the second part of a maps-to notation. (Contributed by AV, 26-Sep-2019.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝑦 ∈ 𝑌 ↦ 𝑍) = (𝑦 ∈ 𝑌 ↦ ⦋𝐴 / 𝑥⦌𝑍))
Theorem	iunopab 5012*	Move indexed union inside an ordered-pair abstraction. (Contributed by Stefan O'Rear, 20-Feb-2015.)
⊢ ∪ 𝑧 ∈ 𝐴 {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 𝜑}
Theorem	elopabr 5013*	Membership in a class abstraction of pairs, defined by a binary relation. (Contributed by AV, 16-Feb-2021.)
⊢ (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝑥𝑅𝑦} → 𝐴 ∈ 𝑅)
Theorem	elopabran 5014*	Membership in a class abstraction of pairs, defined by a restricted binary relation. (Contributed by AV, 16-Feb-2021.)
⊢ (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑅𝑦 ∧ 𝜓)} → 𝐴 ∈ 𝑅)
Theorem	rbropapd 5015*	Properties of a pair in an extended binary relation. (Contributed by Alexander van der Vekens, 30-Oct-2017.)
⊢ (𝜑 → 𝑀 = {⟨𝑓, 𝑝⟩ ∣ (𝑓𝑊𝑝 ∧ 𝜓)})    &   ⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ((𝐹 ∈ 𝑋 ∧ 𝑃 ∈ 𝑌) → (𝐹𝑀𝑃 ↔ (𝐹𝑊𝑃 ∧ 𝜒))))
Theorem	rbropap 5016*	Properties of a pair in a restricted binary relation 𝑀 expressed as an ordered-pair class abstraction: 𝑀 is the binary relation 𝑊 restricted by the condition 𝜓. (Contributed by AV, 31-Jan-2021.)
⊢ (𝜑 → 𝑀 = {⟨𝑓, 𝑝⟩ ∣ (𝑓𝑊𝑝 ∧ 𝜓)})    &   ⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝐹 ∈ 𝑋 ∧ 𝑃 ∈ 𝑌) → (𝐹𝑀𝑃 ↔ (𝐹𝑊𝑃 ∧ 𝜒)))
Theorem	2rbropap 5017*	Properties of a pair in a restricted binary relation 𝑀 expressed as an ordered-pair class abstraction: 𝑀 is the binary relation 𝑊 restricted by the conditions 𝜓 and 𝜏. (Contributed by AV, 31-Jan-2021.)
⊢ (𝜑 → 𝑀 = {⟨𝑓, 𝑝⟩ ∣ (𝑓𝑊𝑝 ∧ 𝜓 ∧ 𝜏)})    &   ⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (𝜓 ↔ 𝜒))    &   ⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (𝜏 ↔ 𝜃))    ⇒   ⊢ ((𝜑 ∧ 𝐹 ∈ 𝑋 ∧ 𝑃 ∈ 𝑌) → (𝐹𝑀𝑃 ↔ (𝐹𝑊𝑃 ∧ 𝜒 ∧ 𝜃)))
2.3.5  Power class of union and intersection
Theorem	pwin 5018	The power class of the intersection of two classes is the intersection of their power classes. Exercise 4.12(j) of [Mendelson] p. 235. (Contributed by NM, 23-Nov-2003.)
⊢ 𝒫 (𝐴 ∩ 𝐵) = (𝒫 𝐴 ∩ 𝒫 𝐵)
Theorem	pwunss 5019	The power class of the union of two classes includes the union of their power classes. Exercise 4.12(k) of [Mendelson] p. 235. (Contributed by NM, 23-Nov-2003.)
⊢ (𝒫 𝐴 ∪ 𝒫 𝐵) ⊆ 𝒫 (𝐴 ∪ 𝐵)
Theorem	pwssun 5020	The power class of the union of two classes is a subset of the union of their power classes, iff one class is a subclass of the other. Exercise 4.12(l) of [Mendelson] p. 235. (Contributed by NM, 23-Nov-2003.)
⊢ ((𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴) ↔ 𝒫 (𝐴 ∪ 𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵))
Theorem	pwundif 5021	Break up the power class of a union into a union of smaller classes. (Contributed by NM, 25-Mar-2007.) (Proof shortened by Thierry Arnoux, 20-Dec-2016.)
⊢ 𝒫 (𝐴 ∪ 𝐵) = ((𝒫 (𝐴 ∪ 𝐵) ∖ 𝒫 𝐴) ∪ 𝒫 𝐴)
Theorem	pwun 5022	The power class of the union of two classes equals the union of their power classes, iff one class is a subclass of the other. Part of Exercise 7(b) of [Enderton] p. 28. (Contributed by NM, 23-Nov-2003.)
⊢ ((𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴) ↔ 𝒫 (𝐴 ∪ 𝐵) = (𝒫 𝐴 ∪ 𝒫 𝐵))
2.3.6  The identity relation
Syntax	cid 5023	Extend the definition of a class to include the identity relation.
class I
Definition	df-id 5024*	Define the identity relation. Definition 9.15 of [Quine] p. 64. For example, 5 I 5 and ¬ 4 I 5 (ex-id 27291). (Contributed by NM, 13-Aug-1995.)
⊢ I = {⟨𝑥, 𝑦⟩ ∣ 𝑥 = 𝑦}
Theorem	dfid3 5025	A stronger version of df-id 5024 that doesn't require 𝑥 and 𝑦 to be distinct. Ordinarily, we wouldn't use this as a definition, since non-distinct dummy variables would make soundness verification more difficult (as the proof here shows). The proof can be instructive in showing how distinct variable requirements may be eliminated, a task that is not necessarily obvious. (Contributed by NM, 5-Feb-2008.) (Revised by Mario Carneiro, 18-Nov-2016.)
⊢ I = {⟨𝑥, 𝑦⟩ ∣ 𝑥 = 𝑦}
Theorem	dfid4 5026	The identity function using maps-to notation. (Contributed by Scott Fenton, 15-Dec-2017.)
⊢ I = (𝑥 ∈ V ↦ 𝑥)
Theorem	dfid2 5027	Alternate definition of the identity relation. (Contributed by NM, 15-Mar-2007.)
⊢ I = {⟨𝑥, 𝑥⟩ ∣ 𝑥 = 𝑥}
2.3.7  The membership (or epsilon) relation
Syntax	cep 5028	Extend class notation to include the membership/epsilon relation.
class E
Definition	df-eprel 5029*	Define the membership relation, or epsilon relation. Similar to Definition 6.22 of [TakeutiZaring] p. 30. The epsilon relation and set membership are the same, that is, (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵) when 𝐵 is a set by epelg 5030. Thus, 5 E {1, 5} (ex-eprel 27290). (Contributed by NM, 13-Aug-1995.)
⊢ E = {⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ 𝑦}
Theorem	epelg 5030	The epsilon relation and membership are the same. General version of epel 5032. (Contributed by Scott Fenton, 27-Mar-2011.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵))
Theorem	epelc 5031	The epsilon relationship and the membership relation are the same. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵)
Theorem	epel 5032	The epsilon relation and the membership relation are the same. (Contributed by NM, 13-Aug-1995.)
⊢ (𝑥 E 𝑦 ↔ 𝑥 ∈ 𝑦)
2.3.8  Partial and complete ordering
Syntax	wpo 5033	Extend wff notation to include the strict partial ordering predicate. Read: ' 𝑅 is a partial order on 𝐴.'
wff 𝑅 Po 𝐴
Syntax	wor 5034	Extend wff notation to include the strict complete ordering predicate. Read: ' 𝑅 orders 𝐴.'
wff 𝑅 Or 𝐴
Definition	df-po 5035*	Define the strict partial order predicate. Definition of [Enderton] p. 168. The expression 𝑅 Po 𝐴 means 𝑅 is a partial order on 𝐴. For example, < Po ℝ is true, while ≤ Po ℝ is false (ex-po 27292). (Contributed by NM, 16-Mar-1997.)
⊢ (𝑅 Po 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
Definition	df-so 5036*	Define the strict complete (linear) order predicate. The expression 𝑅 Or 𝐴 is true if relationship 𝑅 orders 𝐴. For example, < Or ℝ is true (ltso 10118). Equivalent to Definition 6.19(1) of [TakeutiZaring] p. 29. (Contributed by NM, 21-Jan-1996.)
⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
Theorem	poss 5037	Subset theorem for the partial ordering predicate. (Contributed by NM, 27-Mar-1997.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
⊢ (𝐴 ⊆ 𝐵 → (𝑅 Po 𝐵 → 𝑅 Po 𝐴))
Theorem	poeq1 5038	Equality theorem for partial ordering predicate. (Contributed by NM, 27-Mar-1997.)
⊢ (𝑅 = 𝑆 → (𝑅 Po 𝐴 ↔ 𝑆 Po 𝐴))
Theorem	poeq2 5039	Equality theorem for partial ordering predicate. (Contributed by NM, 27-Mar-1997.)
⊢ (𝐴 = 𝐵 → (𝑅 Po 𝐴 ↔ 𝑅 Po 𝐵))
Theorem	nfpo 5040	Bound-variable hypothesis builder for partial orders. (Contributed by Stefan O'Rear, 20-Jan-2015.)
⊢ Ⅎ𝑥𝑅    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥 𝑅 Po 𝐴
Theorem	nfso 5041	Bound-variable hypothesis builder for total orders. (Contributed by Stefan O'Rear, 20-Jan-2015.)
⊢ Ⅎ𝑥𝑅    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥 𝑅 Or 𝐴
Theorem	pocl 5042	Properties of partial order relation in class notation. (Contributed by NM, 27-Mar-1997.)
⊢ (𝑅 Po 𝐴 → ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴) → (¬ 𝐵𝑅𝐵 ∧ ((𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷) → 𝐵𝑅𝐷))))
Theorem	ispod 5043*	Sufficient conditions for a partial order. (Contributed by NM, 9-Jul-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ¬ 𝑥𝑅𝑥)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))    ⇒   ⊢ (𝜑 → 𝑅 Po 𝐴)
Theorem	swopolem 5044*	Perform the substitutions into the strict weak ordering law. (Contributed by Mario Carneiro, 31-Dec-2014.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦)))    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴)) → (𝑋𝑅𝑌 → (𝑋𝑅𝑍 ∨ 𝑍𝑅𝑌)))
Theorem	swopo 5045*	A strict weak order is a partial order. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑦𝑅𝑧 → ¬ 𝑧𝑅𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦)))    ⇒   ⊢ (𝜑 → 𝑅 Po 𝐴)
Theorem	poirr 5046	A partial order relation is irreflexive. (Contributed by NM, 27-Mar-1997.)
⊢ ((𝑅 Po 𝐴 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵𝑅𝐵)
Theorem	potr 5047	A partial order relation is a transitive relation. (Contributed by NM, 27-Mar-1997.)
⊢ ((𝑅 Po 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷) → 𝐵𝑅𝐷))
Theorem	po2nr 5048	A partial order relation has no 2-cycle loops. (Contributed by NM, 27-Mar-1997.)
⊢ ((𝑅 Po 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐵))
Theorem	po3nr 5049	A partial order relation has no 3-cycle loops. (Contributed by NM, 27-Mar-1997.)
⊢ ((𝑅 Po 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷 ∧ 𝐷𝑅𝐵))
Theorem	po0 5050	Any relation is a partial ordering of the empty set. (Contributed by NM, 28-Mar-1997.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ 𝑅 Po ∅
Theorem	pofun 5051*	A function preserves a partial order relation. (Contributed by Jeff Madsen, 18-Jun-2011.)
⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ 𝑋𝑅𝑌}    &   ⊢ (𝑥 = 𝑦 → 𝑋 = 𝑌)    ⇒   ⊢ ((𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵) → 𝑆 Po 𝐴)
Theorem	sopo 5052	A strict linear order is a strict partial order. (Contributed by NM, 28-Mar-1997.)
⊢ (𝑅 Or 𝐴 → 𝑅 Po 𝐴)
Theorem	soss 5053	Subset theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (𝐴 ⊆ 𝐵 → (𝑅 Or 𝐵 → 𝑅 Or 𝐴))
Theorem	soeq1 5054	Equality theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.)
⊢ (𝑅 = 𝑆 → (𝑅 Or 𝐴 ↔ 𝑆 Or 𝐴))
Theorem	soeq2 5055	Equality theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.)
⊢ (𝐴 = 𝐵 → (𝑅 Or 𝐴 ↔ 𝑅 Or 𝐵))
Theorem	sonr 5056	A strict order relation is irreflexive. (Contributed by NM, 24-Nov-1995.)
⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵𝑅𝐵)
Theorem	sotr 5057	A strict order relation is a transitive relation. (Contributed by NM, 21-Jan-1996.)
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷) → 𝐵𝑅𝐷))
Theorem	solin 5058	A strict order relation is linear (satisfies trichotomy). (Contributed by NM, 21-Jan-1996.)
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵𝑅𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶𝑅𝐵))
Theorem	so2nr 5059	A strict order relation has no 2-cycle loops. (Contributed by NM, 21-Jan-1996.)
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐵))
Theorem	so3nr 5060	A strict order relation has no 3-cycle loops. (Contributed by NM, 21-Jan-1996.)
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷 ∧ 𝐷𝑅𝐵))
Theorem	sotric 5061	A strict order relation satisfies strict trichotomy. (Contributed by NM, 19-Feb-1996.)
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵𝑅𝐶 ↔ ¬ (𝐵 = 𝐶 ∨ 𝐶𝑅𝐵)))
Theorem	sotrieq 5062	Trichotomy law for strict order relation. (Contributed by NM, 9-Apr-1996.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵 = 𝐶 ↔ ¬ (𝐵𝑅𝐶 ∨ 𝐶𝑅𝐵)))
Theorem	sotrieq2 5063	Trichotomy law for strict order relation. (Contributed by NM, 5-May-1999.)
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵 = 𝐶 ↔ (¬ 𝐵𝑅𝐶 ∧ ¬ 𝐶𝑅𝐵)))
Theorem	sotr2 5064	A transitivity relation. (Read 𝐵 ≤ 𝐶 and 𝐶 < 𝐷 implies 𝐵 < 𝐷.) (Contributed by Mario Carneiro, 10-May-2013.)
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((¬ 𝐶𝑅𝐵 ∧ 𝐶𝑅𝐷) → 𝐵𝑅𝐷))
Theorem	issod 5065*	An irreflexive, transitive, linear relation is a strict ordering. (Contributed by NM, 21-Jan-1996.) (Revised by Mario Carneiro, 9-Jul-2014.)
⊢ (𝜑 → 𝑅 Po 𝐴)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))    ⇒   ⊢ (𝜑 → 𝑅 Or 𝐴)
Theorem	issoi 5066*	An irreflexive, transitive, linear relation is a strict ordering. (Contributed by NM, 21-Jan-1996.) (Revised by Mario Carneiro, 9-Jul-2014.)
⊢ (𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥)    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))    ⇒   ⊢ 𝑅 Or 𝐴
Theorem	isso2i 5067*	Deduce strict ordering from its properties. (Contributed by NM, 29-Jan-1996.) (Revised by Mario Carneiro, 9-Jul-2014.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥𝑅𝑦 ↔ ¬ (𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))    ⇒   ⊢ 𝑅 Or 𝐴
Theorem	so0 5068	Any relation is a strict ordering of the empty set. (Contributed by NM, 16-Mar-1997.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ 𝑅 Or ∅
Theorem	somo 5069*	A totally ordered set has at most one minimal element. (Contributed by Mario Carneiro, 24-Jun-2015.) (Revised by NM, 16-Jun-2017.)
⊢ (𝑅 Or 𝐴 → ∃*𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑦𝑅𝑥)
2.3.9  Founded and well-ordering relations
Syntax	wfr 5070	Extend wff notation to include the well-founded predicate. Read: ' 𝑅 is a well-founded relation on 𝐴.'
wff 𝑅 Fr 𝐴
Syntax	wse 5071	Extend wff notation to include the set-like predicate. Read: ' 𝑅 is set-like on 𝐴.'
wff 𝑅 Se 𝐴
Syntax	wwe 5072	Extend wff notation to include the well-ordering predicate. Read: ' 𝑅 well-orders 𝐴.'
wff 𝑅 We 𝐴
Definition	df-fr 5073*	Define the well-founded relation predicate. Definition 6.24(1) of [TakeutiZaring] p. 30. For alternate definitions, see dffr2 5079 and dffr3 5498. (Contributed by NM, 3-Apr-1994.)
⊢ (𝑅 Fr 𝐴 ↔ ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦))
Definition	df-se 5074*	Define the set-like predicate. (Contributed by Mario Carneiro, 19-Nov-2014.)
⊢ (𝑅 Se 𝐴 ↔ ∀𝑥 ∈ 𝐴 {𝑦 ∈ 𝐴 ∣ 𝑦𝑅𝑥} ∈ V)
Definition	df-we 5075	Define the well-ordering predicate. For an alternate definition, see dfwe2 6981. (Contributed by NM, 3-Apr-1994.)
⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴))
Theorem	fri 5076*	Property of well-founded relation (one direction of definition). (Contributed by NM, 18-Mar-1997.)
⊢ (((𝐵 ∈ 𝐶 ∧ 𝑅 Fr 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥)
Theorem	seex 5077*	The 𝑅-preimage of an element of the base set in a set-like relation is a set. (Contributed by Mario Carneiro, 19-Nov-2014.)
⊢ ((𝑅 Se 𝐴 ∧ 𝐵 ∈ 𝐴) → {𝑥 ∈ 𝐴 ∣ 𝑥𝑅𝐵} ∈ V)
Theorem	exse 5078	Any relation on a set is set-like on it. (Contributed by Mario Carneiro, 22-Jun-2015.)
⊢ (𝐴 ∈ 𝑉 → 𝑅 Se 𝐴)
Theorem	dffr2 5079*	Alternate definition of well-founded relation. Similar to Definition 6.21 of [TakeutiZaring] p. 30. (Contributed by NM, 17-Feb-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Proof shortened by Mario Carneiro, 23-Jun-2015.)
⊢ (𝑅 Fr 𝐴 ↔ ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 {𝑧 ∈ 𝑥 ∣ 𝑧𝑅𝑦} = ∅))
Theorem	frc 5080*	Property of well-founded relation (one direction of definition using class variables). (Contributed by NM, 17-Feb-2004.) (Revised by Mario Carneiro, 19-Nov-2014.)
⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝑅 Fr 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅) → ∃𝑥 ∈ 𝐵 {𝑦 ∈ 𝐵 ∣ 𝑦𝑅𝑥} = ∅)
Theorem	frss 5081	Subset theorem for the well-founded predicate. Exercise 1 of [TakeutiZaring] p. 31. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (𝐴 ⊆ 𝐵 → (𝑅 Fr 𝐵 → 𝑅 Fr 𝐴))
Theorem	sess1 5082	Subset theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.)
⊢ (𝑅 ⊆ 𝑆 → (𝑆 Se 𝐴 → 𝑅 Se 𝐴))
Theorem	sess2 5083	Subset theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.)
⊢ (𝐴 ⊆ 𝐵 → (𝑅 Se 𝐵 → 𝑅 Se 𝐴))
Theorem	freq1 5084	Equality theorem for the well-founded predicate. (Contributed by NM, 9-Mar-1997.)
⊢ (𝑅 = 𝑆 → (𝑅 Fr 𝐴 ↔ 𝑆 Fr 𝐴))
Theorem	freq2 5085	Equality theorem for the well-founded predicate. (Contributed by NM, 3-Apr-1994.)
⊢ (𝐴 = 𝐵 → (𝑅 Fr 𝐴 ↔ 𝑅 Fr 𝐵))
Theorem	seeq1 5086	Equality theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.)
⊢ (𝑅 = 𝑆 → (𝑅 Se 𝐴 ↔ 𝑆 Se 𝐴))
Theorem	seeq2 5087	Equality theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.)
⊢ (𝐴 = 𝐵 → (𝑅 Se 𝐴 ↔ 𝑅 Se 𝐵))
Theorem	nffr 5088	Bound-variable hypothesis builder for well-founded relations. (Contributed by Stefan O'Rear, 20-Jan-2015.) (Revised by Mario Carneiro, 14-Oct-2016.)
⊢ Ⅎ𝑥𝑅    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥 𝑅 Fr 𝐴
Theorem	nfse 5089	Bound-variable hypothesis builder for set-like relations. (Contributed by Mario Carneiro, 24-Jun-2015.) (Revised by Mario Carneiro, 14-Oct-2016.)
⊢ Ⅎ𝑥𝑅    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥 𝑅 Se 𝐴
Theorem	nfwe 5090	Bound-variable hypothesis builder for well-orderings. (Contributed by Stefan O'Rear, 20-Jan-2015.) (Revised by Mario Carneiro, 14-Oct-2016.)
⊢ Ⅎ𝑥𝑅    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥 𝑅 We 𝐴
Theorem	frirr 5091	A well-founded relation is irreflexive. Special case of Proposition 6.23 of [TakeutiZaring] p. 30. (Contributed by NM, 2-Jan-1994.) (Revised by Mario Carneiro, 22-Jun-2015.)
⊢ ((𝑅 Fr 𝐴 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵𝑅𝐵)
Theorem	fr2nr 5092	A well-founded relation has no 2-cycle loops. Special case of Proposition 6.23 of [TakeutiZaring] p. 30. (Contributed by NM, 30-May-1994.) (Revised by Mario Carneiro, 22-Jun-2015.)
⊢ ((𝑅 Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐵))
Theorem	fr0 5093	Any relation is well-founded on the empty set. (Contributed by NM, 17-Sep-1993.)
⊢ 𝑅 Fr ∅
Theorem	frminex 5094*	If an element of a well-founded set satisfies a property 𝜑, then there is a minimal element that satisfies 𝜑. (Contributed by Jeff Madsen, 18-Jun-2010.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝑅 Fr 𝐴 → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 (𝜑 ∧ ∀𝑦 ∈ 𝐴 (𝜓 → ¬ 𝑦𝑅𝑥))))
Theorem	efrirr 5095	Irreflexivity of the epsilon relation: a class founded by epsilon is not a member of itself. (Contributed by NM, 18-Apr-1994.) (Revised by Mario Carneiro, 22-Jun-2015.)
⊢ ( E Fr 𝐴 → ¬ 𝐴 ∈ 𝐴)
Theorem	efrn2lp 5096	A set founded by epsilon contains no 2-cycle loops. (Contributed by NM, 19-Apr-1994.)
⊢ (( E Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → ¬ (𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐵))
Theorem	epse 5097	The epsilon relation is set-like on any class. (This is the origin of the term "set-like": a set-like relation "acts like" the epsilon relation of sets and their elements.) (Contributed by Mario Carneiro, 22-Jun-2015.)
⊢ E Se 𝐴
Theorem	tz7.2 5098	Similar to Theorem 7.2 of [TakeutiZaring] p. 35, of except that the Axiom of Regularity is not required due to antecedent E Fr 𝐴. (Contributed by NM, 4-May-1994.)
⊢ ((Tr 𝐴 ∧ E Fr 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ 𝐴))
Theorem	dfepfr 5099*	An alternate way of saying that the epsilon relation is well-founded. (Contributed by NM, 17-Feb-2004.) (Revised by Mario Carneiro, 23-Jun-2015.)
⊢ ( E Fr 𝐴 ↔ ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 (𝑥 ∩ 𝑦) = ∅))
Theorem	epfrc 5100*	A subset of an epsilon-founded class has a minimal element. (Contributed by NM, 17-Feb-2004.) (Revised by David Abernethy, 22-Feb-2011.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (( E Fr 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅) → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅)