P. 352 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35101-35200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	onvf1od 35101*	If 𝐺 is a global choice function, then 𝐹 is a bijection from the ordinals to the universe. This is the ZFC version of (1 → 2) in https://tinyurl.com/hamkins-gblac. (Contributed by BTernaryTau, 5-Dec-2025.)
⊢ (𝜑 → ∀𝑧(𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧))    &   ⊢ 𝑀 = ∩ {𝑥 ∈ On ∣ ∃𝑦 ∈ (𝑅1‘𝑥) ¬ 𝑦 ∈ ran 𝑤}    &   ⊢ 𝑁 = (𝐺‘((𝑅1‘𝑀) ∖ ran 𝑤))    &   ⊢ 𝐹 = recs((𝑤 ∈ V ↦ 𝑁))    ⇒   ⊢ (𝜑 → 𝐹:On–1-1-onto→V)
Theorem	vonf1owev 35102*	If 𝐹 is a bijection from the universe to the ordinals, then 𝑅 well-orders the universe. This is the ZFC version of (2 → 3) in https://tinyurl.com/hamkins-gblac. (Contributed by BTernaryTau, 6-Dec-2025.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝐹‘𝑥) ∈ (𝐹‘𝑦)}    ⇒   ⊢ (𝐹:V–1-1-onto→On → 𝑅 We V)
Theorem	wevgblacfn 35103*	If 𝑅 is a well-ordering of the universe, then 𝐺 is a global choice function. Here 𝐺 maps each set 𝑧 to its minimal element with respect to 𝑅 (except when 𝑧 is the empty set, in which case it is mapped to the empty set, though this is only done for convenience). This is the ZFC version of (3 → 1) in https://tinyurl.com/hamkins-gblac. (Contributed by BTernaryTau, 29-Jun-2025.)
⊢ 𝐺 = (𝑧 ∈ V ↦ ∪ {𝑦 ∈ 𝑧 ∣ ∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦})    ⇒   ⊢ (𝑅 We V → (𝐺 Fn V ∧ ∀𝑧(𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧)))
21.5.3  Real and complex numbers
Theorem	zltp1ne 35104	Integer ordering relation. (Contributed by BTernaryTau, 24-Sep-2023.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 + 1) < 𝐵 ↔ (𝐴 < 𝐵 ∧ 𝐵 ≠ (𝐴 + 1))))
Theorem	nnltp1ne 35105	Positive integer ordering relation. (Contributed by BTernaryTau, 24-Sep-2023.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((𝐴 + 1) < 𝐵 ↔ (𝐴 < 𝐵 ∧ 𝐵 ≠ (𝐴 + 1))))
Theorem	nn0ltp1ne 35106	Nonnegative integer ordering relation. (Contributed by BTernaryTau, 24-Sep-2023.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → ((𝐴 + 1) < 𝐵 ↔ (𝐴 < 𝐵 ∧ 𝐵 ≠ (𝐴 + 1))))
Theorem	0nn0m1nnn0 35107	A number is zero if and only if it's a nonnegative integer that becomes negative after subtracting 1. (Contributed by BTernaryTau, 30-Sep-2023.)
⊢ (𝑁 = 0 ↔ (𝑁 ∈ ℕ0 ∧ ¬ (𝑁 − 1) ∈ ℕ0))
Theorem	f1resfz0f1d 35108	If a function with a sequence of nonnegative integers (starting at 0) as its domain is one-to-one when 0 is removed, and if the range of that restriction does not contain the function's value at the removed integer, then the function is itself one-to-one. (Contributed by BTernaryTau, 4-Oct-2023.)
⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐹:(0...𝐾)⟶𝑉)    &   ⊢ (𝜑 → (𝐹 ↾ (1...𝐾)):(1...𝐾)–1-1→𝑉)    &   ⊢ (𝜑 → ((𝐹 “ {0}) ∩ (𝐹 “ (1...𝐾))) = ∅)    ⇒   ⊢ (𝜑 → 𝐹:(0...𝐾)–1-1→𝑉)
Theorem	fisshasheq 35109	A finite set is equal to its subset if they are the same size. (Contributed by BTernaryTau, 3-Oct-2023.)
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ⊆ 𝐵 ∧ (♯‘𝐴) = (♯‘𝐵)) → 𝐴 = 𝐵)
Theorem	revpfxsfxrev 35110	The reverse of a prefix of a word is equal to the same-length suffix of the reverse of that word. (Contributed by BTernaryTau, 2-Dec-2023.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → (reverse‘(𝑊 prefix 𝐿)) = ((reverse‘𝑊) substr ⟨((♯‘𝑊) − 𝐿), (♯‘𝑊)⟩))
Theorem	swrdrevpfx 35111	A subword expressed in terms of reverses and prefixes. (Contributed by BTernaryTau, 3-Dec-2023.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑊))) → (𝑊 substr ⟨𝐹, 𝐿⟩) = (reverse‘((reverse‘(𝑊 prefix 𝐿)) prefix (𝐿 − 𝐹))))
21.5.4  Graph theory
Theorem	lfuhgr 35112*	A hypergraph is loop-free if and only if every edge connects at least two vertices. (Contributed by BTernaryTau, 15-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ UHGraph → (𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)} ↔ ∀𝑥 ∈ (Edg‘𝐺)2 ≤ (♯‘𝑥)))
Theorem	lfuhgr2 35113*	A hypergraph is loop-free if and only if every edge is not a loop. (Contributed by BTernaryTau, 15-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ UHGraph → (𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)} ↔ ∀𝑥 ∈ (Edg‘𝐺)(♯‘𝑥) ≠ 1))
Theorem	lfuhgr3 35114*	A hypergraph is loop-free if and only if none of its edges connect to only one vertex. (Contributed by BTernaryTau, 15-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ UHGraph → (𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)} ↔ ¬ ∃𝑎{𝑎} ∈ (Edg‘𝐺)))
Theorem	cplgredgex 35115*	Any two (distinct) vertices in a complete graph are connected to each other by at least one edge. (Contributed by BTernaryTau, 2-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝐺 ∈ ComplGraph → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (𝑉 ∖ {𝐴})) → ∃𝑒 ∈ 𝐸 {𝐴, 𝐵} ⊆ 𝑒))
Theorem	cusgredgex 35116	Any two (distinct) vertices in a complete simple graph are connected to each other by an edge. (Contributed by BTernaryTau, 3-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝐺 ∈ ComplUSGraph → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (𝑉 ∖ {𝐴})) → {𝐴, 𝐵} ∈ 𝐸))
Theorem	cusgredgex2 35117	Any two distinct vertices in a complete simple graph are connected to each other by an edge. (Contributed by BTernaryTau, 4-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝐺 ∈ ComplUSGraph → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} ∈ 𝐸))
Theorem	pfxwlk 35118	A prefix of a walk is a walk. (Contributed by BTernaryTau, 2-Dec-2023.)
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝐿 ∈ (0...(♯‘𝐹))) → (𝐹 prefix 𝐿)(Walks‘𝐺)(𝑃 prefix (𝐿 + 1)))
Theorem	revwlk 35119	The reverse of a walk is a walk. (Contributed by BTernaryTau, 30-Nov-2023.)
⊢ (𝐹(Walks‘𝐺)𝑃 → (reverse‘𝐹)(Walks‘𝐺)(reverse‘𝑃))
Theorem	revwlkb 35120	Two words represent a walk if and only if their reverses also represent a walk. (Contributed by BTernaryTau, 4-Dec-2023.)
⊢ ((𝐹 ∈ Word 𝑊 ∧ 𝑃 ∈ Word 𝑈) → (𝐹(Walks‘𝐺)𝑃 ↔ (reverse‘𝐹)(Walks‘𝐺)(reverse‘𝑃)))
Theorem	swrdwlk 35121	Two matching subwords of a walk also represent a walk. (Contributed by BTernaryTau, 7-Dec-2023.)
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝐵 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝐹))) → (𝐹 substr ⟨𝐵, 𝐿⟩)(Walks‘𝐺)(𝑃 substr ⟨𝐵, (𝐿 + 1)⟩))
Theorem	pthhashvtx 35122	A graph containing a path has at least as many vertices as there are edges in the path. (Contributed by BTernaryTau, 5-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐹(Paths‘𝐺)𝑃 → (♯‘𝐹) ≤ (♯‘𝑉))
Theorem	spthcycl 35123	A walk is a trivial path if and only if it is both a simple path and a cycle. (Contributed by BTernaryTau, 8-Oct-2023.)
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 𝐹 = ∅) ↔ (𝐹(SPaths‘𝐺)𝑃 ∧ 𝐹(Cycles‘𝐺)𝑃))
Theorem	usgrgt2cycl 35124	A non-trivial cycle in a simple graph has a length greater than 2. (Contributed by BTernaryTau, 24-Sep-2023.)
⊢ ((𝐺 ∈ USGraph ∧ 𝐹(Cycles‘𝐺)𝑃 ∧ 𝐹 ≠ ∅) → 2 < (♯‘𝐹))
Theorem	usgrcyclgt2v 35125	A simple graph with a non-trivial cycle must have at least 3 vertices. (Contributed by BTernaryTau, 5-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝐹(Cycles‘𝐺)𝑃 ∧ 𝐹 ≠ ∅) → 2 < (♯‘𝑉))
Theorem	subgrwlk 35126	If a walk exists in a subgraph of a graph 𝐺, then that walk also exists in 𝐺. (Contributed by BTernaryTau, 22-Oct-2023.)
⊢ (𝑆 SubGraph 𝐺 → (𝐹(Walks‘𝑆)𝑃 → 𝐹(Walks‘𝐺)𝑃))
Theorem	subgrtrl 35127	If a trail exists in a subgraph of a graph 𝐺, then that trail also exists in 𝐺. (Contributed by BTernaryTau, 22-Oct-2023.)
⊢ (𝑆 SubGraph 𝐺 → (𝐹(Trails‘𝑆)𝑃 → 𝐹(Trails‘𝐺)𝑃))
Theorem	subgrpth 35128	If a path exists in a subgraph of a graph 𝐺, then that path also exists in 𝐺. (Contributed by BTernaryTau, 22-Oct-2023.)
⊢ (𝑆 SubGraph 𝐺 → (𝐹(Paths‘𝑆)𝑃 → 𝐹(Paths‘𝐺)𝑃))
Theorem	subgrcycl 35129	If a cycle exists in a subgraph of a graph 𝐺, then that cycle also exists in 𝐺. (Contributed by BTernaryTau, 23-Oct-2023.)
⊢ (𝑆 SubGraph 𝐺 → (𝐹(Cycles‘𝑆)𝑃 → 𝐹(Cycles‘𝐺)𝑃))
Theorem	cusgr3cyclex 35130*	Every complete simple graph with more than two vertices has a 3-cycle. (Contributed by BTernaryTau, 4-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ ComplUSGraph ∧ 2 < (♯‘𝑉)) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 3))
Theorem	loop1cycl 35131*	A hypergraph has a cycle of length one if and only if it has a loop. (Contributed by BTernaryTau, 13-Oct-2023.)
⊢ (𝐺 ∈ UHGraph → (∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = 𝐴) ↔ {𝐴} ∈ (Edg‘𝐺)))
Theorem	2cycld 35132	Construction of a 2-cycle from two given edges in a graph. (Contributed by BTernaryTau, 16-Oct-2023.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐶”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾”⟩    &   ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))    &   ⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶))    &   ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾)))    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝐽 ≠ 𝐾)    &   ⊢ (𝜑 → 𝐴 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐹(Cycles‘𝐺)𝑃)
Theorem	2cycl2d 35133	Construction of a 2-cycle from two given edges in a graph. (Contributed by BTernaryTau, 16-Oct-2023.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐴”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾”⟩    &   ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐴, 𝐵} ⊆ (𝐼‘𝐾)))    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝐽 ≠ 𝐾)    ⇒   ⊢ (𝜑 → 𝐹(Cycles‘𝐺)𝑃)
Theorem	umgr2cycllem 35134*	Lemma for umgr2cycl 35135. (Contributed by BTernaryTau, 17-Oct-2023.)
⊢ 𝐹 = ⟨“𝐽𝐾”⟩    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ UMGraph)    &   ⊢ (𝜑 → 𝐽 ∈ dom 𝐼)    &   ⊢ (𝜑 → 𝐽 ≠ 𝐾)    &   ⊢ (𝜑 → (𝐼‘𝐽) = (𝐼‘𝐾))    ⇒   ⊢ (𝜑 → ∃𝑝 𝐹(Cycles‘𝐺)𝑝)
Theorem	umgr2cycl 35135*	A multigraph with two distinct edges that connect the same vertices has a 2-cycle. (Contributed by BTernaryTau, 17-Oct-2023.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UMGraph ∧ ∃𝑗 ∈ dom 𝐼∃𝑘 ∈ dom 𝐼((𝐼‘𝑗) = (𝐼‘𝑘) ∧ 𝑗 ≠ 𝑘)) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 2))
21.5.4.1  Acyclic graphs
Syntax	cacycgr 35136	Extend class notation with acyclic graphs.
class AcyclicGraph
Definition	df-acycgr 35137*	Define the class of all acyclic graphs. A graph is called acyclic if it has no (non-trivial) cycles. (Contributed by BTernaryTau, 11-Oct-2023.)
⊢ AcyclicGraph = {𝑔 ∣ ¬ ∃𝑓∃𝑝(𝑓(Cycles‘𝑔)𝑝 ∧ 𝑓 ≠ ∅)}
Theorem	dfacycgr1 35138*	An alternate definition of the class of all acyclic graphs that requires all cycles to be trivial. (Contributed by BTernaryTau, 11-Oct-2023.)
⊢ AcyclicGraph = {𝑔 ∣ ∀𝑓∀𝑝(𝑓(Cycles‘𝑔)𝑝 → 𝑓 = ∅)}
Theorem	isacycgr 35139*	The property of being an acyclic graph. (Contributed by BTernaryTau, 11-Oct-2023.)
⊢ (𝐺 ∈ 𝑊 → (𝐺 ∈ AcyclicGraph ↔ ¬ ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ 𝑓 ≠ ∅)))
Theorem	isacycgr1 35140*	The property of being an acyclic graph. (Contributed by BTernaryTau, 11-Oct-2023.)
⊢ (𝐺 ∈ 𝑊 → (𝐺 ∈ AcyclicGraph ↔ ∀𝑓∀𝑝(𝑓(Cycles‘𝐺)𝑝 → 𝑓 = ∅)))
Theorem	acycgrcycl 35141	Any cycle in an acyclic graph is trivial (i.e. has one vertex and no edges). (Contributed by BTernaryTau, 12-Oct-2023.)
⊢ ((𝐺 ∈ AcyclicGraph ∧ 𝐹(Cycles‘𝐺)𝑃) → 𝐹 = ∅)
Theorem	acycgr0v 35142	A null graph (with no vertices) is an acyclic graph. (Contributed by BTernaryTau, 11-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑊 ∧ 𝑉 = ∅) → 𝐺 ∈ AcyclicGraph)
Theorem	acycgr1v 35143	A multigraph with one vertex is an acyclic graph. (Contributed by BTernaryTau, 12-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UMGraph ∧ (♯‘𝑉) = 1) → 𝐺 ∈ AcyclicGraph)
Theorem	acycgr2v 35144	A simple graph with two vertices is an acyclic graph. (Contributed by BTernaryTau, 12-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ (♯‘𝑉) = 2) → 𝐺 ∈ AcyclicGraph)
Theorem	prclisacycgr 35145*	A proper class (representing a null graph, see vtxvalprc 28979) has the property of an acyclic graph (see also acycgr0v 35142). (Contributed by BTernaryTau, 11-Oct-2023.) (New usage is discouraged.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (¬ 𝐺 ∈ V → ¬ ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ 𝑓 ≠ ∅))
Theorem	acycgrislfgr 35146*	An acyclic hypergraph is a loop-free hypergraph. (Contributed by BTernaryTau, 15-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ AcyclicGraph ∧ 𝐺 ∈ UHGraph) → 𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)})
Theorem	upgracycumgr 35147	An acyclic pseudograph is a multigraph. (Contributed by BTernaryTau, 15-Oct-2023.)
⊢ ((𝐺 ∈ UPGraph ∧ 𝐺 ∈ AcyclicGraph) → 𝐺 ∈ UMGraph)
Theorem	umgracycusgr 35148	An acyclic multigraph is a simple graph. (Contributed by BTernaryTau, 17-Oct-2023.)
⊢ ((𝐺 ∈ UMGraph ∧ 𝐺 ∈ AcyclicGraph) → 𝐺 ∈ USGraph)
Theorem	upgracycusgr 35149	An acyclic pseudograph is a simple graph. (Contributed by BTernaryTau, 17-Oct-2023.)
⊢ ((𝐺 ∈ UPGraph ∧ 𝐺 ∈ AcyclicGraph) → 𝐺 ∈ USGraph)
Theorem	cusgracyclt3v 35150	A complete simple graph is acyclic if and only if it has fewer than three vertices. (Contributed by BTernaryTau, 20-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐺 ∈ ComplUSGraph → (𝐺 ∈ AcyclicGraph ↔ (♯‘𝑉) < 3))
Theorem	pthacycspth 35151	A path in an acyclic graph is a simple path. (Contributed by BTernaryTau, 21-Oct-2023.)
⊢ ((𝐺 ∈ AcyclicGraph ∧ 𝐹(Paths‘𝐺)𝑃) → 𝐹(SPaths‘𝐺)𝑃)
Theorem	acycgrsubgr 35152	The subgraph of an acyclic graph is also acyclic. (Contributed by BTernaryTau, 23-Oct-2023.)
⊢ ((𝐺 ∈ AcyclicGraph ∧ 𝑆 SubGraph 𝐺) → 𝑆 ∈ AcyclicGraph)
21.6  Mathbox for Mario Carneiro
21.6.1  Predicate calculus with all distinct variables
Axiom	ax-7d 35153*	Distinct variable version of ax-11 2158. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
Axiom	ax-8d 35154*	Distinct variable version of ax-7 2008. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
Axiom	ax-9d1 35155	Distinct variable version of ax-6 1967, equal variables case. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑥
Axiom	ax-9d2 35156*	Distinct variable version of ax-6 1967, distinct variables case. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑦
Axiom	ax-10d 35157*	Distinct variable version of axc11n 2425. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
Axiom	ax-11d 35158*	Distinct variable version of ax-12 2178. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
21.6.2  Miscellaneous stuff
Theorem	quartfull 35159	The quartic equation, written out in full. This actually makes a fairly good Metamath stress test. Note that the length of this formula could be shortened significantly if the intermediate expressions were expanded and simplified, but it's not like this theorem will be used anyway. (Contributed by Mario Carneiro, 6-May-2015.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3)) ≠ 0)    &   ⊢ (𝜑 → -((((2 · (𝐵 − ((3 / 8) · (𝐴↑2)))) + (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3))) + ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))) / (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3)))) / 3) ≠ 0)    ⇒   ⊢ (𝜑 → ((((𝑋↑4) + (𝐴 · (𝑋↑3))) + ((𝐵 · (𝑋↑2)) + ((𝐶 · 𝑋) + 𝐷))) = 0 ↔ ((𝑋 = ((-(𝐴 / 4) − ((√‘-((((2 · (𝐵 − ((3 / 8) · (𝐴↑2)))) + (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3))) + ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))) / (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3)))) / 3)) / 2)) + (√‘((-(((√‘-((((2 · (𝐵 − ((3 / 8) · (𝐴↑2)))) + (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3))) + ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))) / (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3)))) / 3)) / 2)↑2) − ((𝐵 − ((3 / 8) · (𝐴↑2))) / 2)) + ((((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8)) / 4) / ((√‘-((((2 · (𝐵 − ((3 / 8) · (𝐴↑2)))) + (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3))) + ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))) / (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3)))) / 3)) / 2))))) ∨ 𝑋 = ((-(𝐴 / 4) − ((√‘-((((2 · (𝐵 − ((3 / 8) · (𝐴↑2)))) + (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3))) + ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))) / (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3)))) / 3)) / 2)) − (√‘((-(((√‘-((((2 · (𝐵 − ((3 / 8) · (𝐴↑2)))) + (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3))) + ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))) / (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3)))) / 3)) / 2)↑2) − ((𝐵 − ((3 / 8) · (𝐴↑2))) / 2)) + ((((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8)) / 4) / ((√‘-((((2 · (𝐵 − ((3 / 8) · (𝐴↑2)))) + (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3))) + ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))) / (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3)))) / 3)) / 2)))))) ∨ (𝑋 = ((-(𝐴 / 4) + ((√‘-((((2 · (𝐵 − ((3 / 8) · (𝐴↑2)))) + (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3))) + ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))) / (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3)))) / 3)) / 2)) + (√‘((-(((√‘-((((2 · (𝐵 − ((3 / 8) · (𝐴↑2)))) + (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3))) + ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))) / (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3)))) / 3)) / 2)↑2) − ((𝐵 − ((3 / 8) · (𝐴↑2))) / 2)) − ((((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8)) / 4) / ((√‘-((((2 · (𝐵 − ((3 / 8) · (𝐴↑2)))) + (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3))) + ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))) / (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3)))) / 3)) / 2))))) ∨ 𝑋 = ((-(𝐴 / 4) + ((√‘-((((2 · (𝐵 − ((3 / 8) · (𝐴↑2)))) + (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3))) + ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))) / (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3)))) / 3)) / 2)) − (√‘((-(((√‘-((((2 · (𝐵 − ((3 / 8) · (𝐴↑2)))) + (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3))) + ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))) / (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3)))) / 3)) / 2)↑2) − ((𝐵 − ((3 / 8) · (𝐴↑2))) / 2)) − ((((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8)) / 4) / ((√‘-((((2 · (𝐵 − ((3 / 8) · (𝐴↑2)))) + (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3))) + ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))) / (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3)))) / 3)) / 2)))))))))
21.6.3  Derangements and the Subfactorial
Theorem	deranglem 35160*	Lemma for derangements. (Contributed by Mario Carneiro, 19-Jan-2015.)
⊢ (𝐴 ∈ Fin → {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ 𝜑)} ∈ Fin)
Theorem	derangval 35161*	Define the derangement function, which counts the number of bijections from a set to itself such that no element is mapped to itself. (Contributed by Mario Carneiro, 19-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    ⇒   ⊢ (𝐴 ∈ Fin → (𝐷‘𝐴) = (♯‘{𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)}))
Theorem	derangf 35162*	The derangement number is a function from finite sets to nonnegative integers. (Contributed by Mario Carneiro, 19-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    ⇒   ⊢ 𝐷:Fin⟶ℕ0
Theorem	derang0 35163*	The derangement number of the empty set. (Contributed by Mario Carneiro, 19-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    ⇒   ⊢ (𝐷‘∅) = 1
Theorem	derangsn 35164*	The derangement number of a singleton. (Contributed by Mario Carneiro, 19-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝐷‘{𝐴}) = 0)
Theorem	derangenlem 35165*	One half of derangen 35166. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    ⇒   ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (𝐷‘𝐴) ≤ (𝐷‘𝐵))
Theorem	derangen 35166*	The derangement number is a cardinal invariant, i.e. it only depends on the size of a set and not on its contents. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    ⇒   ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (𝐷‘𝐴) = (𝐷‘𝐵))
Theorem	subfacval 35167*	The subfactorial is defined as the number of derangements (see derangval 35161) of the set (1...𝑁). (Contributed by Mario Carneiro, 21-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    &   ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))    ⇒   ⊢ (𝑁 ∈ ℕ0 → (𝑆‘𝑁) = (𝐷‘(1...𝑁)))
Theorem	derangen2 35168*	Write the derangement number in terms of the subfactorial. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    &   ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))    ⇒   ⊢ (𝐴 ∈ Fin → (𝐷‘𝐴) = (𝑆‘(♯‘𝐴)))
Theorem	subfacf 35169*	The subfactorial is a function from nonnegative integers to nonnegative integers. (Contributed by Mario Carneiro, 19-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    &   ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))    ⇒   ⊢ 𝑆:ℕ0⟶ℕ0
Theorem	subfaclefac 35170*	The subfactorial is less than the factorial. (Contributed by Mario Carneiro, 19-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    &   ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))    ⇒   ⊢ (𝑁 ∈ ℕ0 → (𝑆‘𝑁) ≤ (!‘𝑁))
Theorem	subfac0 35171*	The subfactorial at zero. (Contributed by Mario Carneiro, 19-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    &   ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))    ⇒   ⊢ (𝑆‘0) = 1
Theorem	subfac1 35172*	The subfactorial at one. (Contributed by Mario Carneiro, 19-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    &   ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))    ⇒   ⊢ (𝑆‘1) = 0
Theorem	subfacp1lem1 35173*	Lemma for subfacp1 35180. The set 𝐾 together with {1, 𝑀} partitions the set 1...(𝑁 + 1). (Contributed by Mario Carneiro, 23-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    &   ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))    &   ⊢ 𝐴 = {𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦)}    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ (2...(𝑁 + 1)))    &   ⊢ 𝑀 ∈ V    &   ⊢ 𝐾 = ((2...(𝑁 + 1)) ∖ {𝑀})    ⇒   ⊢ (𝜑 → ((𝐾 ∩ {1, 𝑀}) = ∅ ∧ (𝐾 ∪ {1, 𝑀}) = (1...(𝑁 + 1)) ∧ (♯‘𝐾) = (𝑁 − 1)))
Theorem	subfacp1lem2a 35174*	Lemma for subfacp1 35180. Properties of a bijection on 𝐾 augmented with the two-element flip to get a bijection on 𝐾 ∪ {1, 𝑀}. (Contributed by Mario Carneiro, 23-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    &   ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))    &   ⊢ 𝐴 = {𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦)}    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ (2...(𝑁 + 1)))    &   ⊢ 𝑀 ∈ V    &   ⊢ 𝐾 = ((2...(𝑁 + 1)) ∖ {𝑀})    &   ⊢ 𝐹 = (𝐺 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})    &   ⊢ (𝜑 → 𝐺:𝐾–1-1-onto→𝐾)    ⇒   ⊢ (𝜑 → (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ (𝐹‘1) = 𝑀 ∧ (𝐹‘𝑀) = 1))
Theorem	subfacp1lem2b 35175*	Lemma for subfacp1 35180. Properties of a bijection on 𝐾 augmented with the two-element flip to get a bijection on 𝐾 ∪ {1, 𝑀}. (Contributed by Mario Carneiro, 23-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    &   ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))    &   ⊢ 𝐴 = {𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦)}    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ (2...(𝑁 + 1)))    &   ⊢ 𝑀 ∈ V    &   ⊢ 𝐾 = ((2...(𝑁 + 1)) ∖ {𝑀})    &   ⊢ 𝐹 = (𝐺 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})    &   ⊢ (𝜑 → 𝐺:𝐾–1-1-onto→𝐾)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐾) → (𝐹‘𝑋) = (𝐺‘𝑋))
Theorem	subfacp1lem3 35176*	Lemma for subfacp1 35180. In subfacp1lem6 35179 we cut up the set of all derangements on 1...(𝑁 + 1) first according to the value at 1, and then by whether or not (𝑓‘(𝑓‘1)) = 1. In this lemma, we show that the subset of all 𝑁 + 1 derangements that satisfy this for fixed 𝑀 = (𝑓‘1) is in bijection with 𝑁 − 1 derangements, by simply dropping the 𝑥 = 1 and 𝑥 = 𝑀 points from the function to get a derangement on 𝐾 = (1...(𝑁 − 1)) ∖ {1, 𝑀}. (Contributed by Mario Carneiro, 23-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    &   ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))    &   ⊢ 𝐴 = {𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦)}    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ (2...(𝑁 + 1)))    &   ⊢ 𝑀 ∈ V    &   ⊢ 𝐾 = ((2...(𝑁 + 1)) ∖ {𝑀})    &   ⊢ 𝐵 = {𝑔 ∈ 𝐴 ∣ ((𝑔‘1) = 𝑀 ∧ (𝑔‘𝑀) = 1)}    &   ⊢ 𝐶 = {𝑓 ∣ (𝑓:𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑓‘𝑦) ≠ 𝑦)}    ⇒   ⊢ (𝜑 → (♯‘𝐵) = (𝑆‘(𝑁 − 1)))
Theorem	subfacp1lem4 35177*	Lemma for subfacp1 35180. The function 𝐹, which swaps 1 with 𝑀 and leaves all other elements alone, is a bijection of order 2, i.e. it is its own inverse. (Contributed by Mario Carneiro, 19-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    &   ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))    &   ⊢ 𝐴 = {𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦)}    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ (2...(𝑁 + 1)))    &   ⊢ 𝑀 ∈ V    &   ⊢ 𝐾 = ((2...(𝑁 + 1)) ∖ {𝑀})    &   ⊢ 𝐵 = {𝑔 ∈ 𝐴 ∣ ((𝑔‘1) = 𝑀 ∧ (𝑔‘𝑀) ≠ 1)}    &   ⊢ 𝐹 = (( I ↾ 𝐾) ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})    ⇒   ⊢ (𝜑 → ◡𝐹 = 𝐹)
Theorem	subfacp1lem5 35178*	Lemma for subfacp1 35180. In subfacp1lem6 35179 we cut up the set of all derangements on 1...(𝑁 + 1) first according to the value at 1, and then by whether or not (𝑓‘(𝑓‘1)) = 1. In this lemma, we show that the subset of all 𝑁 + 1 derangements with (𝑓‘(𝑓‘1)) ≠ 1 for fixed 𝑀 = (𝑓‘1) is in bijection with derangements of 2...(𝑁 + 1), because pre-composing with the function 𝐹 swaps 1 and 𝑀 and turns the function into a bijection with (𝑓‘1) = 1 and (𝑓‘𝑥) ≠ 𝑥 for all other 𝑥, so dropping the point at 1 yields a derangement on the 𝑁 remaining points. (Contributed by Mario Carneiro, 23-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    &   ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))    &   ⊢ 𝐴 = {𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦)}    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ (2...(𝑁 + 1)))    &   ⊢ 𝑀 ∈ V    &   ⊢ 𝐾 = ((2...(𝑁 + 1)) ∖ {𝑀})    &   ⊢ 𝐵 = {𝑔 ∈ 𝐴 ∣ ((𝑔‘1) = 𝑀 ∧ (𝑔‘𝑀) ≠ 1)}    &   ⊢ 𝐹 = (( I ↾ 𝐾) ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})    &   ⊢ 𝐶 = {𝑓 ∣ (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦)}    ⇒   ⊢ (𝜑 → (♯‘𝐵) = (𝑆‘𝑁))
Theorem	subfacp1lem6 35179*	Lemma for subfacp1 35180. By induction, we cut up the set of all derangements on 𝑁 + 1 according to the 𝑁 possible values of (𝑓‘1) (since (𝑓‘1) ≠ 1), and for each set for fixed 𝑀 = (𝑓‘1), the subset of derangements with (𝑓‘𝑀) = 1 has size 𝑆(𝑁 − 1) (by subfacp1lem3 35176), while the subset with (𝑓‘𝑀) ≠ 1 has size 𝑆(𝑁) (by subfacp1lem5 35178). Adding it all up yields the desired equation 𝑁(𝑆(𝑁) + 𝑆(𝑁 − 1)) for the number of derangements on 𝑁 + 1. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    &   ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))    &   ⊢ 𝐴 = {𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦)}    ⇒   ⊢ (𝑁 ∈ ℕ → (𝑆‘(𝑁 + 1)) = (𝑁 · ((𝑆‘𝑁) + (𝑆‘(𝑁 − 1)))))
Theorem	subfacp1 35180*	A two-term recurrence for the subfactorial. This theorem allows to forget the combinatorial definition of the derangement number in favor of the recursive definition provided by this theorem and subfac0 35171, subfac1 35172. (Contributed by Mario Carneiro, 23-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    &   ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))    ⇒   ⊢ (𝑁 ∈ ℕ → (𝑆‘(𝑁 + 1)) = (𝑁 · ((𝑆‘𝑁) + (𝑆‘(𝑁 − 1)))))
Theorem	subfacval2 35181*	A closed-form expression for the subfactorial. (Contributed by Mario Carneiro, 23-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    &   ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))    ⇒   ⊢ (𝑁 ∈ ℕ0 → (𝑆‘𝑁) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) / (!‘𝑘))))
Theorem	subfaclim 35182*	The subfactorial converges rapidly to 𝑁! / e. This is part of Metamath 100 proof #88. (Contributed by Mario Carneiro, 23-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    &   ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))    ⇒   ⊢ (𝑁 ∈ ℕ → (abs‘(((!‘𝑁) / e) − (𝑆‘𝑁))) < (1 / 𝑁))
Theorem	subfacval3 35183*	Another closed form expression for the subfactorial. The expression ⌊‘(𝑥 + 1 / 2) is a way of saying "rounded to the nearest integer". (Contributed by Mario Carneiro, 23-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    &   ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))    ⇒   ⊢ (𝑁 ∈ ℕ → (𝑆‘𝑁) = (⌊‘(((!‘𝑁) / e) + (1 / 2))))
Theorem	derangfmla 35184*	The derangements formula, which expresses the number of derangements of a finite nonempty set in terms of the factorial. The expression ⌊‘(𝑥 + 1 / 2) is a way of saying "rounded to the nearest integer". This is part of Metamath 100 proof #88. (Contributed by Mario Carneiro, 23-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    ⇒   ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → (𝐷‘𝐴) = (⌊‘(((!‘(♯‘𝐴)) / e) + (1 / 2))))
21.6.4  The Erdős-Szekeres theorem
Theorem	erdszelem1 35185*	Lemma for erdsze 35196. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ 𝑆 = {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)}    ⇒   ⊢ (𝑋 ∈ 𝑆 ↔ (𝑋 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑋) Isom < , 𝑂 (𝑋, (𝐹 “ 𝑋)) ∧ 𝐴 ∈ 𝑋))
Theorem	erdszelem2 35186*	Lemma for erdsze 35196. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ 𝑆 = {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)}    ⇒   ⊢ ((♯ “ 𝑆) ∈ Fin ∧ (♯ “ 𝑆) ⊆ ℕ)
Theorem	erdszelem3 35187*	Lemma for erdsze 35196. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ)    &   ⊢ 𝐾 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < ))    ⇒   ⊢ (𝐴 ∈ (1...𝑁) → (𝐾‘𝐴) = sup((♯ “ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)}), ℝ, < ))
Theorem	erdszelem4 35188*	Lemma for erdsze 35196. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ)    &   ⊢ 𝐾 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < ))    &   ⊢ 𝑂 Or ℝ    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ (1...𝑁)) → {𝐴} ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)})
Theorem	erdszelem5 35189*	Lemma for erdsze 35196. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ)    &   ⊢ 𝐾 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < ))    &   ⊢ 𝑂 Or ℝ    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ (1...𝑁)) → (𝐾‘𝐴) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)}))
Theorem	erdszelem6 35190*	Lemma for erdsze 35196. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ)    &   ⊢ 𝐾 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < ))    &   ⊢ 𝑂 Or ℝ    ⇒   ⊢ (𝜑 → 𝐾:(1...𝑁)⟶ℕ)
Theorem	erdszelem7 35191*	Lemma for erdsze 35196. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ)    &   ⊢ 𝐾 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < ))    &   ⊢ 𝑂 Or ℝ    &   ⊢ (𝜑 → 𝐴 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝑅 ∈ ℕ)    &   ⊢ (𝜑 → ¬ (𝐾‘𝐴) ∈ (1...(𝑅 − 1)))    ⇒   ⊢ (𝜑 → ∃𝑠 ∈ 𝒫 (1...𝑁)(𝑅 ≤ (♯‘𝑠) ∧ (𝐹 ↾ 𝑠) Isom < , 𝑂 (𝑠, (𝐹 “ 𝑠))))
Theorem	erdszelem8 35192*	Lemma for erdsze 35196. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ)    &   ⊢ 𝐾 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < ))    &   ⊢ 𝑂 Or ℝ    &   ⊢ (𝜑 → 𝐴 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝐵 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → ((𝐾‘𝐴) = (𝐾‘𝐵) → ¬ (𝐹‘𝐴)𝑂(𝐹‘𝐵)))
Theorem	erdszelem9 35193*	Lemma for erdsze 35196. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ)    &   ⊢ 𝐼 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , < (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < ))    &   ⊢ 𝐽 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , ◡ < (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < ))    &   ⊢ 𝑇 = (𝑛 ∈ (1...𝑁) ↦ ⟨(𝐼‘𝑛), (𝐽‘𝑛)⟩)    ⇒   ⊢ (𝜑 → 𝑇:(1...𝑁)–1-1→(ℕ × ℕ))
Theorem	erdszelem10 35194*	Lemma for erdsze 35196. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ)    &   ⊢ 𝐼 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , < (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < ))    &   ⊢ 𝐽 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , ◡ < (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < ))    &   ⊢ 𝑇 = (𝑛 ∈ (1...𝑁) ↦ ⟨(𝐼‘𝑛), (𝐽‘𝑛)⟩)    &   ⊢ (𝜑 → 𝑅 ∈ ℕ)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ)    &   ⊢ (𝜑 → ((𝑅 − 1) · (𝑆 − 1)) < 𝑁)    ⇒   ⊢ (𝜑 → ∃𝑚 ∈ (1...𝑁)(¬ (𝐼‘𝑚) ∈ (1...(𝑅 − 1)) ∨ ¬ (𝐽‘𝑚) ∈ (1...(𝑆 − 1))))
Theorem	erdszelem11 35195*	Lemma for erdsze 35196. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ)    &   ⊢ 𝐼 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , < (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < ))    &   ⊢ 𝐽 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , ◡ < (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < ))    &   ⊢ 𝑇 = (𝑛 ∈ (1...𝑁) ↦ ⟨(𝐼‘𝑛), (𝐽‘𝑛)⟩)    &   ⊢ (𝜑 → 𝑅 ∈ ℕ)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ)    &   ⊢ (𝜑 → ((𝑅 − 1) · (𝑆 − 1)) < 𝑁)    ⇒   ⊢ (𝜑 → ∃𝑠 ∈ 𝒫 (1...𝑁)((𝑅 ≤ (♯‘𝑠) ∧ (𝐹 ↾ 𝑠) Isom < , < (𝑠, (𝐹 “ 𝑠))) ∨ (𝑆 ≤ (♯‘𝑠) ∧ (𝐹 ↾ 𝑠) Isom < , ◡ < (𝑠, (𝐹 “ 𝑠)))))
Theorem	erdsze 35196*	The Erdős-Szekeres theorem. For any injective sequence 𝐹 on the reals of length at least (𝑅 − 1) · (𝑆 − 1) + 1, there is either a subsequence of length at least 𝑅 on which 𝐹 is increasing (i.e. a < , < order isomorphism) or a subsequence of length at least 𝑆 on which 𝐹 is decreasing (i.e. a < , ◡ < order isomorphism, recalling that ◡ < is the "greater than" relation). This is part of Metamath 100 proof #73. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ)    &   ⊢ (𝜑 → 𝑅 ∈ ℕ)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ)    &   ⊢ (𝜑 → ((𝑅 − 1) · (𝑆 − 1)) < 𝑁)    ⇒   ⊢ (𝜑 → ∃𝑠 ∈ 𝒫 (1...𝑁)((𝑅 ≤ (♯‘𝑠) ∧ (𝐹 ↾ 𝑠) Isom < , < (𝑠, (𝐹 “ 𝑠))) ∨ (𝑆 ≤ (♯‘𝑠) ∧ (𝐹 ↾ 𝑠) Isom < , ◡ < (𝑠, (𝐹 “ 𝑠)))))
Theorem	erdsze2lem1 35197*	Lemma for erdsze2 35199. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ (𝜑 → 𝑅 ∈ ℕ)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:𝐴–1-1→ℝ)    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ 𝑁 = ((𝑅 − 1) · (𝑆 − 1))    &   ⊢ (𝜑 → 𝑁 < (♯‘𝐴))    ⇒   ⊢ (𝜑 → ∃𝑓(𝑓:(1...(𝑁 + 1))–1-1→𝐴 ∧ 𝑓 Isom < , < ((1...(𝑁 + 1)), ran 𝑓)))
Theorem	erdsze2lem2 35198*	Lemma for erdsze2 35199. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ (𝜑 → 𝑅 ∈ ℕ)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:𝐴–1-1→ℝ)    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ 𝑁 = ((𝑅 − 1) · (𝑆 − 1))    &   ⊢ (𝜑 → 𝑁 < (♯‘𝐴))    &   ⊢ (𝜑 → 𝐺:(1...(𝑁 + 1))–1-1→𝐴)    &   ⊢ (𝜑 → 𝐺 Isom < , < ((1...(𝑁 + 1)), ran 𝐺))    ⇒   ⊢ (𝜑 → ∃𝑠 ∈ 𝒫 𝐴((𝑅 ≤ (♯‘𝑠) ∧ (𝐹 ↾ 𝑠) Isom < , < (𝑠, (𝐹 “ 𝑠))) ∨ (𝑆 ≤ (♯‘𝑠) ∧ (𝐹 ↾ 𝑠) Isom < , ◡ < (𝑠, (𝐹 “ 𝑠)))))
Theorem	erdsze2 35199*	Generalize the statement of the Erdős-Szekeres theorem erdsze 35196 to "sequences" indexed by an arbitrary subset of ℝ, which can be infinite. This is part of Metamath 100 proof #73. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ (𝜑 → 𝑅 ∈ ℕ)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:𝐴–1-1→ℝ)    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → ((𝑅 − 1) · (𝑆 − 1)) < (♯‘𝐴))    ⇒   ⊢ (𝜑 → ∃𝑠 ∈ 𝒫 𝐴((𝑅 ≤ (♯‘𝑠) ∧ (𝐹 ↾ 𝑠) Isom < , < (𝑠, (𝐹 “ 𝑠))) ∨ (𝑆 ≤ (♯‘𝑠) ∧ (𝐹 ↾ 𝑠) Isom < , ◡ < (𝑠, (𝐹 “ 𝑠)))))
21.6.5  The Kuratowski closure-complement theorem
Theorem	kur14lem1 35200	Lemma for kur14 35210. (Contributed by Mario Carneiro, 17-Feb-2015.)
⊢ 𝐴 ⊆ 𝑋    &   ⊢ (𝑋 ∖ 𝐴) ∈ 𝑇    &   ⊢ (𝐾‘𝐴) ∈ 𝑇    ⇒   ⊢ (𝑁 = 𝐴 → (𝑁 ⊆ 𝑋 ∧ {(𝑋 ∖ 𝑁), (𝐾‘𝑁)} ⊆ 𝑇))