P. 355 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35401-35500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	derangen 35401*	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 35402*	The subfactorial is defined as the number of derangements (see derangval 35396) of the set (1...𝑁). (Contributed by Mario Carneiro, 21-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    &   ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))    ⇒   ⊢ (𝑁 ∈ ℕ0 → (𝑆‘𝑁) = (𝐷‘(1...𝑁)))
Theorem	derangen2 35403*	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 35404*	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 35405*	The subfactorial is less than the factorial. (Contributed by Mario Carneiro, 19-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    &   ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))    ⇒   ⊢ (𝑁 ∈ ℕ0 → (𝑆‘𝑁) ≤ (!‘𝑁))
Theorem	subfac0 35406*	The subfactorial at zero. (Contributed by Mario Carneiro, 19-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    &   ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))    ⇒   ⊢ (𝑆‘0) = 1
Theorem	subfac1 35407*	The subfactorial at one. (Contributed by Mario Carneiro, 19-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    &   ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))    ⇒   ⊢ (𝑆‘1) = 0
Theorem	subfacp1lem1 35408*	Lemma for subfacp1 35415. 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 35409*	Lemma for subfacp1 35415. 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 35410*	Lemma for subfacp1 35415. 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 35411*	Lemma for subfacp1 35415. In subfacp1lem6 35414 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 35412*	Lemma for subfacp1 35415. 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 35413*	Lemma for subfacp1 35415. In subfacp1lem6 35414 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 35414*	Lemma for subfacp1 35415. 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 35411), while the subset with (𝑓‘𝑀) ≠ 1 has size 𝑆(𝑁) (by subfacp1lem5 35413). 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 35415*	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 35406, subfac1 35407. (Contributed by Mario Carneiro, 23-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    &   ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))    ⇒   ⊢ (𝑁 ∈ ℕ → (𝑆‘(𝑁 + 1)) = (𝑁 · ((𝑆‘𝑁) + (𝑆‘(𝑁 − 1)))))
Theorem	subfacval2 35416*	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 35417*	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 35418*	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 35419*	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 35420*	Lemma for erdsze 35431. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ 𝑆 = {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)}    ⇒   ⊢ (𝑋 ∈ 𝑆 ↔ (𝑋 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑋) Isom < , 𝑂 (𝑋, (𝐹 “ 𝑋)) ∧ 𝐴 ∈ 𝑋))
Theorem	erdszelem2 35421*	Lemma for erdsze 35431. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ 𝑆 = {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)}    ⇒   ⊢ ((♯ “ 𝑆) ∈ Fin ∧ (♯ “ 𝑆) ⊆ ℕ)
Theorem	erdszelem3 35422*	Lemma for erdsze 35431. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ)    &   ⊢ 𝐾 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < ))    ⇒   ⊢ (𝐴 ∈ (1...𝑁) → (𝐾‘𝐴) = sup((♯ “ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)}), ℝ, < ))
Theorem	erdszelem4 35423*	Lemma for erdsze 35431. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ)    &   ⊢ 𝐾 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < ))    &   ⊢ 𝑂 Or ℝ    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ (1...𝑁)) → {𝐴} ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)})
Theorem	erdszelem5 35424*	Lemma for erdsze 35431. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ)    &   ⊢ 𝐾 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < ))    &   ⊢ 𝑂 Or ℝ    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ (1...𝑁)) → (𝐾‘𝐴) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)}))
Theorem	erdszelem6 35425*	Lemma for erdsze 35431. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ)    &   ⊢ 𝐾 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < ))    &   ⊢ 𝑂 Or ℝ    ⇒   ⊢ (𝜑 → 𝐾:(1...𝑁)⟶ℕ)
Theorem	erdszelem7 35426*	Lemma for erdsze 35431. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ)    &   ⊢ 𝐾 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < ))    &   ⊢ 𝑂 Or ℝ    &   ⊢ (𝜑 → 𝐴 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝑅 ∈ ℕ)    &   ⊢ (𝜑 → ¬ (𝐾‘𝐴) ∈ (1...(𝑅 − 1)))    ⇒   ⊢ (𝜑 → ∃𝑠 ∈ 𝒫 (1...𝑁)(𝑅 ≤ (♯‘𝑠) ∧ (𝐹 ↾ 𝑠) Isom < , 𝑂 (𝑠, (𝐹 “ 𝑠))))
Theorem	erdszelem8 35427*	Lemma for erdsze 35431. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ)    &   ⊢ 𝐾 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < ))    &   ⊢ 𝑂 Or ℝ    &   ⊢ (𝜑 → 𝐴 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝐵 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → ((𝐾‘𝐴) = (𝐾‘𝐵) → ¬ (𝐹‘𝐴)𝑂(𝐹‘𝐵)))
Theorem	erdszelem9 35428*	Lemma for erdsze 35431. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ)    &   ⊢ 𝐼 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , < (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < ))    &   ⊢ 𝐽 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , ◡ < (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < ))    &   ⊢ 𝑇 = (𝑛 ∈ (1...𝑁) ↦ ⟨(𝐼‘𝑛), (𝐽‘𝑛)⟩)    ⇒   ⊢ (𝜑 → 𝑇:(1...𝑁)–1-1→(ℕ × ℕ))
Theorem	erdszelem10 35429*	Lemma for erdsze 35431. (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 35430*	Lemma for erdsze 35431. (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 35431*	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 35432*	Lemma for erdsze2 35434. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ (𝜑 → 𝑅 ∈ ℕ)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:𝐴–1-1→ℝ)    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ 𝑁 = ((𝑅 − 1) · (𝑆 − 1))    &   ⊢ (𝜑 → 𝑁 < (♯‘𝐴))    ⇒   ⊢ (𝜑 → ∃𝑓(𝑓:(1...(𝑁 + 1))–1-1→𝐴 ∧ 𝑓 Isom < , < ((1...(𝑁 + 1)), ran 𝑓)))
Theorem	erdsze2lem2 35433*	Lemma for erdsze2 35434. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ (𝜑 → 𝑅 ∈ ℕ)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:𝐴–1-1→ℝ)    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ 𝑁 = ((𝑅 − 1) · (𝑆 − 1))    &   ⊢ (𝜑 → 𝑁 < (♯‘𝐴))    &   ⊢ (𝜑 → 𝐺:(1...(𝑁 + 1))–1-1→𝐴)    &   ⊢ (𝜑 → 𝐺 Isom < , < ((1...(𝑁 + 1)), ran 𝐺))    ⇒   ⊢ (𝜑 → ∃𝑠 ∈ 𝒫 𝐴((𝑅 ≤ (♯‘𝑠) ∧ (𝐹 ↾ 𝑠) Isom < , < (𝑠, (𝐹 “ 𝑠))) ∨ (𝑆 ≤ (♯‘𝑠) ∧ (𝐹 ↾ 𝑠) Isom < , ◡ < (𝑠, (𝐹 “ 𝑠)))))
Theorem	erdsze2 35434*	Generalize the statement of the Erdős-Szekeres theorem erdsze 35431 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 35435	Lemma for kur14 35445. (Contributed by Mario Carneiro, 17-Feb-2015.)
⊢ 𝐴 ⊆ 𝑋    &   ⊢ (𝑋 ∖ 𝐴) ∈ 𝑇    &   ⊢ (𝐾‘𝐴) ∈ 𝑇    ⇒   ⊢ (𝑁 = 𝐴 → (𝑁 ⊆ 𝑋 ∧ {(𝑋 ∖ 𝑁), (𝐾‘𝑁)} ⊆ 𝑇))
Theorem	kur14lem2 35436	Lemma for kur14 35445. Write interior in terms of closure and complement: 𝑖𝐴 = 𝑐𝑘𝑐𝐴 where 𝑐 is complement and 𝑘 is closure. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ 𝐽 ∈ Top    &   ⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (cls‘𝐽)    &   ⊢ 𝐼 = (int‘𝐽)    &   ⊢ 𝐴 ⊆ 𝑋    ⇒   ⊢ (𝐼‘𝐴) = (𝑋 ∖ (𝐾‘(𝑋 ∖ 𝐴)))
Theorem	kur14lem3 35437	Lemma for kur14 35445. A closure is a subset of the base set. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ 𝐽 ∈ Top    &   ⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (cls‘𝐽)    &   ⊢ 𝐼 = (int‘𝐽)    &   ⊢ 𝐴 ⊆ 𝑋    ⇒   ⊢ (𝐾‘𝐴) ⊆ 𝑋
Theorem	kur14lem4 35438	Lemma for kur14 35445. Complementation is an involution on the set of subsets of a topology. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ 𝐽 ∈ Top    &   ⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (cls‘𝐽)    &   ⊢ 𝐼 = (int‘𝐽)    &   ⊢ 𝐴 ⊆ 𝑋    ⇒   ⊢ (𝑋 ∖ (𝑋 ∖ 𝐴)) = 𝐴
Theorem	kur14lem5 35439	Lemma for kur14 35445. Closure is an idempotent operation in the set of subsets of a topology. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ 𝐽 ∈ Top    &   ⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (cls‘𝐽)    &   ⊢ 𝐼 = (int‘𝐽)    &   ⊢ 𝐴 ⊆ 𝑋    ⇒   ⊢ (𝐾‘(𝐾‘𝐴)) = (𝐾‘𝐴)
Theorem	kur14lem6 35440	Lemma for kur14 35445. If 𝑘 is the complementation operator and 𝑘 is the closure operator, this expresses the identity 𝑘𝑐𝑘𝐴 = 𝑘𝑐𝑘𝑐𝑘𝑐𝑘𝐴 for any subset 𝐴 of the topological space. This is the key result that lets us cut down long enough sequences of 𝑐𝑘𝑐𝑘... that arise when applying closure and complement repeatedly to 𝐴, and explains why we end up with a number as large as 14, yet no larger. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ 𝐽 ∈ Top    &   ⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (cls‘𝐽)    &   ⊢ 𝐼 = (int‘𝐽)    &   ⊢ 𝐴 ⊆ 𝑋    &   ⊢ 𝐵 = (𝑋 ∖ (𝐾‘𝐴))    ⇒   ⊢ (𝐾‘(𝐼‘(𝐾‘𝐵))) = (𝐾‘𝐵)
Theorem	kur14lem7 35441	Lemma for kur14 35445: main proof. The set 𝑇 here contains all the distinct combinations of 𝑘 and 𝑐 that can arise, and we prove here that applying 𝑘 or 𝑐 to any element of 𝑇 yields another element of 𝑇. In operator shorthand, we have 𝑇 = {𝐴, 𝑐𝐴, 𝑘𝐴 , 𝑐𝑘𝐴, 𝑘𝑐𝐴, 𝑐𝑘𝑐𝐴, 𝑘𝑐𝑘𝐴, 𝑐𝑘𝑐𝑘𝐴, 𝑘𝑐𝑘𝑐𝐴, 𝑐𝑘𝑐𝑘𝑐𝐴, 𝑘𝑐𝑘𝑐𝑘𝐴, 𝑐𝑘𝑐𝑘𝑐𝑘𝐴, 𝑘𝑐𝑘𝑐𝑘𝑐𝐴, 𝑐𝑘𝑐𝑘𝑐𝑘𝑐𝐴}. From the identities 𝑐𝑐𝐴 = 𝐴 and 𝑘𝑘𝐴 = 𝑘𝐴, we can reduce any operator combination containing two adjacent identical operators, which is why the list only contains alternating sequences. The reason the sequences don't keep going after a certain point is due to the identity 𝑘𝑐𝑘𝐴 = 𝑘𝑐𝑘𝑐𝑘𝑐𝑘𝐴, proved in kur14lem6 35440. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ 𝐽 ∈ Top    &   ⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (cls‘𝐽)    &   ⊢ 𝐼 = (int‘𝐽)    &   ⊢ 𝐴 ⊆ 𝑋    &   ⊢ 𝐵 = (𝑋 ∖ (𝐾‘𝐴))    &   ⊢ 𝐶 = (𝐾‘(𝑋 ∖ 𝐴))    &   ⊢ 𝐷 = (𝐼‘(𝐾‘𝐴))    &   ⊢ 𝑇 = ((({𝐴, (𝑋 ∖ 𝐴), (𝐾‘𝐴)} ∪ {𝐵, 𝐶, (𝐼‘𝐴)}) ∪ {(𝐾‘𝐵), 𝐷, (𝐾‘(𝐼‘𝐴))}) ∪ ({(𝐼‘𝐶), (𝐾‘𝐷), (𝐼‘(𝐾‘𝐵))} ∪ {(𝐾‘(𝐼‘𝐶)), (𝐼‘(𝐾‘(𝐼‘𝐴)))}))    ⇒   ⊢ (𝑁 ∈ 𝑇 → (𝑁 ⊆ 𝑋 ∧ {(𝑋 ∖ 𝑁), (𝐾‘𝑁)} ⊆ 𝑇))
Theorem	kur14lem8 35442	Lemma for kur14 35445. Show that the set 𝑇 contains at most 14 elements. (It could be less if some of the operators take the same value for a given set, but Kuratowski showed that this upper bound of 14 is tight in the sense that there exist topological spaces and subsets of these spaces for which all 14 generated sets are distinct, and indeed the real numbers form such a topological space.) (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ 𝐽 ∈ Top    &   ⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (cls‘𝐽)    &   ⊢ 𝐼 = (int‘𝐽)    &   ⊢ 𝐴 ⊆ 𝑋    &   ⊢ 𝐵 = (𝑋 ∖ (𝐾‘𝐴))    &   ⊢ 𝐶 = (𝐾‘(𝑋 ∖ 𝐴))    &   ⊢ 𝐷 = (𝐼‘(𝐾‘𝐴))    &   ⊢ 𝑇 = ((({𝐴, (𝑋 ∖ 𝐴), (𝐾‘𝐴)} ∪ {𝐵, 𝐶, (𝐼‘𝐴)}) ∪ {(𝐾‘𝐵), 𝐷, (𝐾‘(𝐼‘𝐴))}) ∪ ({(𝐼‘𝐶), (𝐾‘𝐷), (𝐼‘(𝐾‘𝐵))} ∪ {(𝐾‘(𝐼‘𝐶)), (𝐼‘(𝐾‘(𝐼‘𝐴)))}))    ⇒   ⊢ (𝑇 ∈ Fin ∧ (♯‘𝑇) ≤ ;14)
Theorem	kur14lem9 35443*	Lemma for kur14 35445. Since the set 𝑇 is closed under closure and complement, it contains the minimal set 𝑆 as a subset, so 𝑆 also has at most 14 elements. (Indeed 𝑆 = 𝑇, and it's not hard to prove this, but we don't need it for this proof.) (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ 𝐽 ∈ Top    &   ⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (cls‘𝐽)    &   ⊢ 𝐼 = (int‘𝐽)    &   ⊢ 𝐴 ⊆ 𝑋    &   ⊢ 𝐵 = (𝑋 ∖ (𝐾‘𝐴))    &   ⊢ 𝐶 = (𝐾‘(𝑋 ∖ 𝐴))    &   ⊢ 𝐷 = (𝐼‘(𝐾‘𝐴))    &   ⊢ 𝑇 = ((({𝐴, (𝑋 ∖ 𝐴), (𝐾‘𝐴)} ∪ {𝐵, 𝐶, (𝐼‘𝐴)}) ∪ {(𝐾‘𝐵), 𝐷, (𝐾‘(𝐼‘𝐴))}) ∪ ({(𝐼‘𝐶), (𝐾‘𝐷), (𝐼‘(𝐾‘𝐵))} ∪ {(𝐾‘(𝐼‘𝐶)), (𝐼‘(𝐾‘(𝐼‘𝐴)))}))    &   ⊢ 𝑆 = ∩ {𝑥 ∈ 𝒫 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 {(𝑋 ∖ 𝑦), (𝐾‘𝑦)} ⊆ 𝑥)}    ⇒   ⊢ (𝑆 ∈ Fin ∧ (♯‘𝑆) ≤ ;14)
Theorem	kur14lem10 35444*	Lemma for kur14 35445. Discharge the set 𝑇. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ 𝐽 ∈ Top    &   ⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (cls‘𝐽)    &   ⊢ 𝑆 = ∩ {𝑥 ∈ 𝒫 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 {(𝑋 ∖ 𝑦), (𝐾‘𝑦)} ⊆ 𝑥)}    &   ⊢ 𝐴 ⊆ 𝑋    ⇒   ⊢ (𝑆 ∈ Fin ∧ (♯‘𝑆) ≤ ;14)
Theorem	kur14 35445*	Kuratowski's closure-complement theorem. There are at most 14 sets which can be obtained by the application of the closure and complement operations to a set in a topological space. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (cls‘𝐽)    &   ⊢ 𝑆 = ∩ {𝑥 ∈ 𝒫 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 {(𝑋 ∖ 𝑦), (𝐾‘𝑦)} ⊆ 𝑥)}    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → (𝑆 ∈ Fin ∧ (♯‘𝑆) ≤ ;14))
21.6.6  Retracts and sections
Syntax	cretr 35446	Extend class notation with the retract relation.
class Retr
Definition	df-retr 35447*	Define the set of retractions on two topological spaces. We say that 𝑅 is a retraction from 𝐽 to 𝐾. or 𝑅 ∈ (𝐽 Retr 𝐾) iff there is an 𝑆 such that 𝑅:𝐽⟶𝐾, 𝑆:𝐾⟶𝐽 are continuous functions called the retraction and section respectively, and their composite 𝑅 ∘ 𝑆 is homotopic to the identity map. If a retraction exists, we say 𝐽 is a retract of 𝐾. (This terminology is borrowed from HoTT and appears to be nonstandard, although it has similaries to the concept of retract in the category of topological spaces and to a deformation retract in general topology.) Two topological spaces that are retracts of each other are called homotopy equivalent. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ Retr = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ {𝑟 ∈ (𝑗 Cn 𝑘) ∣ ∃𝑠 ∈ (𝑘 Cn 𝑗)((𝑟 ∘ 𝑠)(𝑗 Htpy 𝑗)( I ↾ ∪ 𝑗)) ≠ ∅})
21.6.7  Path-connected and simply connected spaces
Syntax	cpconn 35448	Extend class notation with the class of path-connected topologies.
class PConn
Syntax	csconn 35449	Extend class notation with the class of simply connected topologies.
class SConn
Definition	df-pconn 35450*	Define the class of path-connected topologies. A topology is path-connected if there is a path (a continuous function from the closed unit interval) that goes from 𝑥 to 𝑦 for any points 𝑥, 𝑦 in the space. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ PConn = {𝑗 ∈ Top ∣ ∀𝑥 ∈ ∪ 𝑗∀𝑦 ∈ ∪ 𝑗∃𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)}
Definition	df-sconn 35451*	Define the class of simply connected topologies. A topology is simply connected if it is path-connected and every loop (continuous path with identical start and endpoint) is contractible to a point (path-homotopic to a constant function). (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ SConn = {𝑗 ∈ PConn ∣ ∀𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = (𝑓‘1) → 𝑓( ≃ph‘𝑗)((0[,]1) × {(𝑓‘0)}))}
Theorem	ispconn 35452*	The property of being a path-connected topological space. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ PConn ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)))
Theorem	pconncn 35453*	The property of being a path-connected topological space. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ PConn ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝐴 ∧ (𝑓‘1) = 𝐵))
Theorem	pconntop 35454	A simply connected space is a topology. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ (𝐽 ∈ PConn → 𝐽 ∈ Top)
Theorem	issconn 35455*	The property of being a simply connected topological space. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ (𝐽 ∈ SConn ↔ (𝐽 ∈ PConn ∧ ∀𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = (𝑓‘1) → 𝑓( ≃ph‘𝐽)((0[,]1) × {(𝑓‘0)}))))
Theorem	sconnpconn 35456	A simply connected space is path-connected. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ (𝐽 ∈ SConn → 𝐽 ∈ PConn)
Theorem	sconntop 35457	A simply connected space is a topology. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ (𝐽 ∈ SConn → 𝐽 ∈ Top)
Theorem	sconnpht 35458	A closed path in a simply connected space is contractible to a point. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ ((𝐽 ∈ SConn ∧ 𝐹 ∈ (II Cn 𝐽) ∧ (𝐹‘0) = (𝐹‘1)) → 𝐹( ≃ph‘𝐽)((0[,]1) × {(𝐹‘0)}))
Theorem	cnpconn 35459	An image of a path-connected space is path-connected. (Contributed by Mario Carneiro, 24-Mar-2015.)
⊢ 𝑌 = ∪ 𝐾    ⇒   ⊢ ((𝐽 ∈ PConn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐾 ∈ PConn)
Theorem	pconnconn 35460	A path-connected space is connected. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ (𝐽 ∈ PConn → 𝐽 ∈ Conn)
Theorem	txpconn 35461	The topological product of two path-connected spaces is path-connected. (Contributed by Mario Carneiro, 12-Feb-2015.)
⊢ ((𝑅 ∈ PConn ∧ 𝑆 ∈ PConn) → (𝑅 ×t 𝑆) ∈ PConn)
Theorem	ptpconn 35462	The topological product of a collection of path-connected spaces is path-connected. The proof uses the axiom of choice. (Contributed by Mario Carneiro, 17-Feb-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶PConn) → (∏t‘𝐹) ∈ PConn)
Theorem	indispconn 35463	The indiscrete topology (or trivial topology) on any set is path-connected. (Contributed by Mario Carneiro, 7-Jul-2015.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ {∅, 𝐴} ∈ PConn
Theorem	connpconn 35464	A connected and locally path-connected space is path-connected. (Contributed by Mario Carneiro, 7-Jul-2015.)
⊢ ((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn) → 𝐽 ∈ PConn)
Theorem	qtoppconn 35465	A quotient of a path-connected space is path-connected. (Contributed by Mario Carneiro, 24-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ PConn ∧ 𝐹 Fn 𝑋) → (𝐽 qTop 𝐹) ∈ PConn)
Theorem	pconnpi1 35466	All fundamental groups in a path-connected space are isomorphic. (Contributed by Mario Carneiro, 12-Feb-2015.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝑃 = (𝐽 π1 𝐴)    &   ⊢ 𝑄 = (𝐽 π1 𝐵)    &   ⊢ 𝑆 = (Base‘𝑃)    &   ⊢ 𝑇 = (Base‘𝑄)    ⇒   ⊢ ((𝐽 ∈ PConn ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 𝑃 ≃𝑔 𝑄)
Theorem	sconnpht2 35467	Any two paths in a simply connected space with the same start and end point are path-homotopic. (Contributed by Mario Carneiro, 12-Feb-2015.)
⊢ (𝜑 → 𝐽 ∈ SConn)    &   ⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))    &   ⊢ (𝜑 → (𝐹‘0) = (𝐺‘0))    &   ⊢ (𝜑 → (𝐹‘1) = (𝐺‘1))    ⇒   ⊢ (𝜑 → 𝐹( ≃ph‘𝐽)𝐺)
Theorem	sconnpi1 35468	A path-connected topological space is simply connected iff its fundamental group is trivial. (Contributed by Mario Carneiro, 12-Feb-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ PConn ∧ 𝑌 ∈ 𝑋) → (𝐽 ∈ SConn ↔ (Base‘(𝐽 π1 𝑌)) ≈ 1o))
Theorem	txsconnlem 35469	Lemma for txsconn 35470. (Contributed by Mario Carneiro, 9-Mar-2015.)
⊢ (𝜑 → 𝑅 ∈ Top)    &   ⊢ (𝜑 → 𝑆 ∈ Top)    &   ⊢ (𝜑 → 𝐹 ∈ (II Cn (𝑅 ×t 𝑆)))    &   ⊢ 𝐴 = ((1st ↾ (∪ 𝑅 × ∪ 𝑆)) ∘ 𝐹)    &   ⊢ 𝐵 = ((2nd ↾ (∪ 𝑅 × ∪ 𝑆)) ∘ 𝐹)    &   ⊢ (𝜑 → 𝐺 ∈ (𝐴(PHtpy‘𝑅)((0[,]1) × {(𝐴‘0)})))    &   ⊢ (𝜑 → 𝐻 ∈ (𝐵(PHtpy‘𝑆)((0[,]1) × {(𝐵‘0)})))    ⇒   ⊢ (𝜑 → 𝐹( ≃ph‘(𝑅 ×t 𝑆))((0[,]1) × {(𝐹‘0)}))
Theorem	txsconn 35470	The topological product of two simply connected spaces is simply connected. (Contributed by Mario Carneiro, 12-Feb-2015.)
⊢ ((𝑅 ∈ SConn ∧ 𝑆 ∈ SConn) → (𝑅 ×t 𝑆) ∈ SConn)
Theorem	cvxpconn 35471*	A convex subset of the complex numbers is path-connected. (Contributed by Mario Carneiro, 12-Feb-2015.) Avoid ax-mulf 11116. (Revised by GG, 19-Apr-2025.)
⊢ (𝜑 → 𝑆 ⊆ ℂ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑡 ∈ (0[,]1))) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ 𝑆)    &   ⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝐾 = (𝐽 ↾t 𝑆)    ⇒   ⊢ (𝜑 → 𝐾 ∈ PConn)
Theorem	cvxsconn 35472*	A convex subset of the complex numbers is simply connected. (Contributed by Mario Carneiro, 12-Feb-2015.) Avoid ax-mulf 11116. (Revised by GG, 19-Apr-2025.)
⊢ (𝜑 → 𝑆 ⊆ ℂ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑡 ∈ (0[,]1))) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ 𝑆)    &   ⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝐾 = (𝐽 ↾t 𝑆)    ⇒   ⊢ (𝜑 → 𝐾 ∈ SConn)
Theorem	blsconn 35473	An open ball in the complex numbers is simply connected. (Contributed by Mario Carneiro, 12-Feb-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝑆 = (𝑃(ball‘(abs ∘ − ))𝑅)    &   ⊢ 𝐾 = (𝐽 ↾t 𝑆)    ⇒   ⊢ ((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*) → 𝐾 ∈ SConn)
Theorem	cnllysconn 35474	The topology of the complex numbers is locally simply connected. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ 𝐽 ∈ Locally SConn
Theorem	resconn 35475	A subset of ℝ is simply connected iff it is connected. (Contributed by Mario Carneiro, 9-Mar-2015.)
⊢ 𝐽 = ((topGen‘ran (,)) ↾t 𝐴)    ⇒   ⊢ (𝐴 ⊆ ℝ → (𝐽 ∈ SConn ↔ 𝐽 ∈ Conn))
Theorem	ioosconn 35476	An open interval is simply connected. (Contributed by Mario Carneiro, 9-Mar-2015.)
⊢ ((topGen‘ran (,)) ↾t (𝐴(,)𝐵)) ∈ SConn
Theorem	iccsconn 35477	A closed interval is simply connected. (Contributed by Mario Carneiro, 9-Mar-2015.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) ∈ SConn)
Theorem	retopsconn 35478	The real numbers are simply connected. (Contributed by Mario Carneiro, 9-Mar-2015.)
⊢ (topGen‘ran (,)) ∈ SConn
Theorem	iccllysconn 35479	A closed interval is locally simply connected. (Contributed by Mario Carneiro, 10-Mar-2015.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) ∈ Locally SConn)
Theorem	rellysconn 35480	The real numbers are locally simply connected. (Contributed by Mario Carneiro, 10-Mar-2015.)
⊢ (topGen‘ran (,)) ∈ Locally SConn
Theorem	iisconn 35481	The unit interval is simply connected. (Contributed by Mario Carneiro, 9-Mar-2015.)
⊢ II ∈ SConn
Theorem	iillysconn 35482	The unit interval is locally simply connected. (Contributed by Mario Carneiro, 10-Mar-2015.)
⊢ II ∈ Locally SConn
Theorem	iinllyconn 35483	The unit interval is locally connected. (Contributed by Mario Carneiro, 6-Jul-2015.)
⊢ II ∈ 𝑛-Locally Conn
21.6.8  Covering maps
Syntax	ccvm 35484	Extend class notation with the class of covering maps.
class CovMap
Definition	df-cvm 35485*	Define the class of covering maps on two topological spaces. A function 𝑓:𝑐⟶𝑗 is a covering map if it is continuous and for every point 𝑥 in the target space there is a neighborhood 𝑘 of 𝑥 and a decomposition 𝑠 of the preimage of 𝑘 as a disjoint union such that 𝑓 is a homeomorphism of each set 𝑢 ∈ 𝑠 onto 𝑘. (Contributed by Mario Carneiro, 13-Feb-2015.)
⊢ CovMap = (𝑐 ∈ Top, 𝑗 ∈ Top ↦ {𝑓 ∈ (𝑐 Cn 𝑗) ∣ ∀𝑥 ∈ ∪ 𝑗∃𝑘 ∈ 𝑗 (𝑥 ∈ 𝑘 ∧ ∃𝑠 ∈ (𝒫 𝑐 ∖ {∅})(∪ 𝑠 = (◡𝑓 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝑓 ↾ 𝑢) ∈ ((𝑐 ↾t 𝑢)Homeo(𝑗 ↾t 𝑘)))))})
Theorem	fncvm 35486	Lemma for covering maps. (Contributed by Mario Carneiro, 13-Feb-2015.)
⊢ CovMap Fn (Top × Top)
Theorem	cvmscbv 35487*	Change bound variables in the set of even coverings. (Contributed by Mario Carneiro, 17-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    ⇒   ⊢ 𝑆 = (𝑎 ∈ 𝐽 ↦ {𝑏 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑏 = (◡𝐹 “ 𝑎) ∧ ∀𝑐 ∈ 𝑏 (∀𝑑 ∈ (𝑏 ∖ {𝑐})(𝑐 ∩ 𝑑) = ∅ ∧ (𝐹 ↾ 𝑐) ∈ ((𝐶 ↾t 𝑐)Homeo(𝐽 ↾t 𝑎))))})
Theorem	iscvm 35488*	The property of being a covering map. (Contributed by Mario Carneiro, 13-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    &   ⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) ↔ ((𝐶 ∈ Top ∧ 𝐽 ∈ Top ∧ 𝐹 ∈ (𝐶 Cn 𝐽)) ∧ ∀𝑥 ∈ 𝑋 ∃𝑘 ∈ 𝐽 (𝑥 ∈ 𝑘 ∧ (𝑆‘𝑘) ≠ ∅)))
Theorem	cvmtop1 35489	Reverse closure for a covering map. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top)
Theorem	cvmtop2 35490	Reverse closure for a covering map. (Contributed by Mario Carneiro, 13-Feb-2015.)
⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐽 ∈ Top)
Theorem	cvmcn 35491	A covering map is a continuous function. (Contributed by Mario Carneiro, 13-Feb-2015.)
⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽))
Theorem	cvmcov 35492*	Property of a covering map. In order to make the covering property more manageable, we define here the set 𝑆(𝑘) of all even coverings of an open set 𝑘 in the range. Then the covering property states that every point has a neighborhood which has an even covering. (Contributed by Mario Carneiro, 13-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    &   ⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑃 ∈ 𝑋) → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝑆‘𝑥) ≠ ∅))
Theorem	cvmsrcl 35493*	Reverse closure for an even covering. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    ⇒   ⊢ (𝑇 ∈ (𝑆‘𝑈) → 𝑈 ∈ 𝐽)
Theorem	cvmsi 35494*	One direction of cvmsval 35495. (Contributed by Mario Carneiro, 13-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    ⇒   ⊢ (𝑇 ∈ (𝑆‘𝑈) → (𝑈 ∈ 𝐽 ∧ (𝑇 ⊆ 𝐶 ∧ 𝑇 ≠ ∅) ∧ (∪ 𝑇 = (◡𝐹 “ 𝑈) ∧ ∀𝑢 ∈ 𝑇 (∀𝑣 ∈ (𝑇 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑈))))))
Theorem	cvmsval 35495*	Elementhood in the set 𝑆 of all even coverings of an open set in 𝐽. 𝑆 is an even covering of 𝑈 if it is a nonempty collection of disjoint open sets in 𝐶 whose union is the preimage of 𝑈, such that each set 𝑢 ∈ 𝑆 is homeomorphic under 𝐹 to 𝑈. (Contributed by Mario Carneiro, 13-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    ⇒   ⊢ (𝐶 ∈ 𝑉 → (𝑇 ∈ (𝑆‘𝑈) ↔ (𝑈 ∈ 𝐽 ∧ (𝑇 ⊆ 𝐶 ∧ 𝑇 ≠ ∅) ∧ (∪ 𝑇 = (◡𝐹 “ 𝑈) ∧ ∀𝑢 ∈ 𝑇 (∀𝑣 ∈ (𝑇 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑈)))))))
Theorem	cvmsss 35496*	An even covering is a subset of the topology of the domain (i.e. a collection of open sets). (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    ⇒   ⊢ (𝑇 ∈ (𝑆‘𝑈) → 𝑇 ⊆ 𝐶)
Theorem	cvmsn0 35497*	An even covering is nonempty. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    ⇒   ⊢ (𝑇 ∈ (𝑆‘𝑈) → 𝑇 ≠ ∅)
Theorem	cvmsuni 35498*	An even covering of 𝑈 has union equal to the preimage of 𝑈 by 𝐹. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    ⇒   ⊢ (𝑇 ∈ (𝑆‘𝑈) → ∪ 𝑇 = (◡𝐹 “ 𝑈))
Theorem	cvmsdisj 35499*	An even covering of 𝑈 is a disjoint union. (Contributed by Mario Carneiro, 13-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    ⇒   ⊢ ((𝑇 ∈ (𝑆‘𝑈) ∧ 𝐴 ∈ 𝑇 ∧ 𝐵 ∈ 𝑇) → (𝐴 = 𝐵 ∨ (𝐴 ∩ 𝐵) = ∅))
Theorem	cvmshmeo 35500*	Every element of an even covering of 𝑈 is homeomorphic to 𝑈 via 𝐹. (Contributed by Mario Carneiro, 13-Feb-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾t 𝑢)Homeo(𝐽 ↾t 𝑘))))})    ⇒   ⊢ ((𝑇 ∈ (𝑆‘𝑈) ∧ 𝐴 ∈ 𝑇) → (𝐹 ↾ 𝐴) ∈ ((𝐶 ↾t 𝐴)Homeo(𝐽 ↾t 𝑈)))