P. 169 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 16801-16900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	2exp16 16801	Two to the sixteenth power is 65536. (Contributed by Mario Carneiro, 20-Apr-2015.)
⊢ (2↑;16) = ;;;;65536
Theorem	3exp3 16802	Three to the third power is 27. (Contributed by Mario Carneiro, 20-Apr-2015.)
⊢ (3↑3) = ;27
Theorem	2expltfac 16803	The factorial grows faster than two to the power 𝑁. (Contributed by Mario Carneiro, 15-Sep-2016.)
⊢ (𝑁 ∈ (ℤ≥‘4) → (2↑𝑁) < (!‘𝑁))
6.2.18  Cyclical shifts of words (cont.)
Theorem	cshwsidrepsw 16804	If cyclically shifting a word of length being a prime number by a number of positions which is not divisible by the prime number results in the word itself, the word is a "repeated symbol word". (Contributed by AV, 18-May-2018.) (Revised by AV, 10-Nov-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) → ((𝐿 ∈ ℤ ∧ (𝐿 mod (♯‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊) → 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊))))
Theorem	cshwsidrepswmod0 16805	If cyclically shifting a word of length being a prime number results in the word itself, the shift must be either by 0 (modulo the length of the word) or the word must be a "repeated symbol word". (Contributed by AV, 18-May-2018.) (Revised by AV, 10-Nov-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ ∧ 𝐿 ∈ ℤ) → ((𝑊 cyclShift 𝐿) = 𝑊 → ((𝐿 mod (♯‘𝑊)) = 0 ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)))))
Theorem	cshwshashlem1 16806*	If cyclically shifting a word of length being a prime number not consisting of identical symbols by at least one position (and not by as many positions as the length of the word), the result will not be the word itself. (Contributed by AV, 19-May-2018.) (Revised by AV, 8-Jun-2018.) (Revised by AV, 10-Nov-2018.)
⊢ (𝜑 → (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ))    ⇒   ⊢ ((𝜑 ∧ ∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0) ∧ 𝐿 ∈ (1..^(♯‘𝑊))) → (𝑊 cyclShift 𝐿) ≠ 𝑊)
Theorem	cshwshashlem2 16807*	If cyclically shifting a word of length being a prime number and not of identical symbols by different numbers of positions, the resulting words are different. (Contributed by Alexander van der Vekens, 19-May-2018.) (Revised by Alexander van der Vekens, 8-Jun-2018.)
⊢ (𝜑 → (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ))    ⇒   ⊢ ((𝜑 ∧ ∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0)) → ((𝐿 ∈ (0..^(♯‘𝑊)) ∧ 𝐾 ∈ (0..^(♯‘𝑊)) ∧ 𝐾 < 𝐿) → (𝑊 cyclShift 𝐿) ≠ (𝑊 cyclShift 𝐾)))
Theorem	cshwshashlem3 16808*	If cyclically shifting a word of length being a prime number and not of identical symbols by different numbers of positions, the resulting words are different. (Contributed by Alexander van der Vekens, 19-May-2018.) (Revised by Alexander van der Vekens, 8-Jun-2018.)
⊢ (𝜑 → (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ))    ⇒   ⊢ ((𝜑 ∧ ∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0)) → ((𝐿 ∈ (0..^(♯‘𝑊)) ∧ 𝐾 ∈ (0..^(♯‘𝑊)) ∧ 𝐾 ≠ 𝐿) → (𝑊 cyclShift 𝐿) ≠ (𝑊 cyclShift 𝐾)))
Theorem	cshwsdisj 16809*	The singletons resulting by cyclically shifting a given word of length being a prime number and not consisting of identical symbols is a disjoint collection. (Contributed by Alexander van der Vekens, 19-May-2018.) (Revised by Alexander van der Vekens, 8-Jun-2018.)
⊢ (𝜑 → (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ))    ⇒   ⊢ ((𝜑 ∧ ∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0)) → Disj 𝑛 ∈ (0..^(♯‘𝑊)){(𝑊 cyclShift 𝑛)})
Theorem	cshwsiun 16810*	The set of (different!) words resulting by cyclically shifting a given word is an indexed union. (Contributed by AV, 19-May-2018.) (Revised by AV, 8-Jun-2018.) (Proof shortened by AV, 8-Nov-2018.)
⊢ 𝑀 = {𝑤 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(♯‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤}    ⇒   ⊢ (𝑊 ∈ Word 𝑉 → 𝑀 = ∪ 𝑛 ∈ (0..^(♯‘𝑊)){(𝑊 cyclShift 𝑛)})
Theorem	cshwsex 16811*	The class of (different!) words resulting by cyclically shifting a given word is a set. (Contributed by AV, 8-Jun-2018.) (Revised by AV, 8-Nov-2018.)
⊢ 𝑀 = {𝑤 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(♯‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤}    ⇒   ⊢ (𝑊 ∈ Word 𝑉 → 𝑀 ∈ V)
Theorem	cshws0 16812*	The size of the set of (different!) words resulting by cyclically shifting an empty word is 0. (Contributed by AV, 8-Nov-2018.)
⊢ 𝑀 = {𝑤 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(♯‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤}    ⇒   ⊢ (𝑊 = ∅ → (♯‘𝑀) = 0)
Theorem	cshwrepswhash1 16813*	The size of the set of (different!) words resulting by cyclically shifting a nonempty "repeated symbol word" is 1. (Contributed by AV, 18-May-2018.) (Revised by AV, 8-Nov-2018.)
⊢ 𝑀 = {𝑤 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(♯‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤}    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑊 = (𝐴 repeatS 𝑁)) → (♯‘𝑀) = 1)
Theorem	cshwshashnsame 16814*	If a word (not consisting of identical symbols) has a length being a prime number, the size of the set of (different!) words resulting by cyclically shifting the original word equals the length of the original word. (Contributed by AV, 19-May-2018.) (Revised by AV, 10-Nov-2018.)
⊢ 𝑀 = {𝑤 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(♯‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤}    ⇒   ⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) → (∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0) → (♯‘𝑀) = (♯‘𝑊)))
Theorem	cshwshash 16815*	If a word has a length being a prime number, the size of the set of (different!) words resulting by cyclically shifting the original word equals the length of the original word or 1. (Contributed by AV, 19-May-2018.) (Revised by AV, 10-Nov-2018.)
⊢ 𝑀 = {𝑤 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(♯‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤}    ⇒   ⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) → ((♯‘𝑀) = (♯‘𝑊) ∨ (♯‘𝑀) = 1))
6.2.19  Specific prime numbers
Theorem	prmlem0 16816*	Lemma for prmlem1 16818 and prmlem2 16830. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ ((¬ 2 ∥ 𝑀 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁))    &   ⊢ (𝐾 ∈ ℙ → ¬ 𝐾 ∥ 𝑁)    &   ⊢ (𝐾 + 2) = 𝑀    ⇒   ⊢ ((¬ 2 ∥ 𝐾 ∧ 𝑥 ∈ (ℤ≥‘𝐾)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁))
Theorem	prmlem1a 16817*	A quick proof skeleton to show that the numbers less than 25 are prime, by trial division. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑁 ∈ ℕ    &   ⊢ 1 < 𝑁    &   ⊢ ¬ 2 ∥ 𝑁    &   ⊢ ¬ 3 ∥ 𝑁    &   ⊢ ((¬ 2 ∥ 5 ∧ 𝑥 ∈ (ℤ≥‘5)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁))    ⇒   ⊢ 𝑁 ∈ ℙ
Theorem	prmlem1 16818	A quick proof skeleton to show that the numbers less than 25 are prime, by trial division. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑁 ∈ ℕ    &   ⊢ 1 < 𝑁    &   ⊢ ¬ 2 ∥ 𝑁    &   ⊢ ¬ 3 ∥ 𝑁    &   ⊢ 𝑁 < ;25    ⇒   ⊢ 𝑁 ∈ ℙ
Theorem	5prm 16819	5 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
⊢ 5 ∈ ℙ
Theorem	6nprm 16820	6 is not a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ ¬ 6 ∈ ℙ
Theorem	7prm 16821	7 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
⊢ 7 ∈ ℙ
Theorem	8nprm 16822	8 is not a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ ¬ 8 ∈ ℙ
Theorem	9nprm 16823	9 is not a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ ¬ 9 ∈ ℙ
Theorem	10nprm 16824	10 is not a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
⊢ ¬ ;10 ∈ ℙ
Theorem	11prm 16825	11 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
⊢ ;11 ∈ ℙ
Theorem	13prm 16826	13 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
⊢ ;13 ∈ ℙ
Theorem	17prm 16827	17 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
⊢ ;17 ∈ ℙ
Theorem	19prm 16828	19 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
⊢ ;19 ∈ ℙ
Theorem	23prm 16829	23 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
⊢ ;23 ∈ ℙ
Theorem	prmlem2 16830	Our last proving session got as far as 25 because we started with the two "bootstrap" primes 2 and 3, and the next prime is 5, so knowing that 2 and 3 are prime and 4 is not allows us to cover the numbers less than 5↑2 = 25. Additionally, nonprimes are "easy", so we can extend this range of known prime/nonprimes all the way until 29, which is the first prime larger than 25. Thus, in this lemma we extend another blanket out to 29↑2 = 841, from which we can prove even more primes. If we wanted, we could keep doing this, but the goal is Bertrand's postulate, and for that we only need a few large primes - we don't need to find them all, as we have been doing thus far. So after this blanket runs out, we'll have to switch to another method (see 1259prm 16846). As a side note, you can see the pattern of the primes in the indentation pattern of this lemma! (Contributed by Mario Carneiro, 18-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑁 < ;;841    &   ⊢ 1 < 𝑁    &   ⊢ ¬ 2 ∥ 𝑁    &   ⊢ ¬ 3 ∥ 𝑁    &   ⊢ ¬ 5 ∥ 𝑁    &   ⊢ ¬ 7 ∥ 𝑁    &   ⊢ ¬ ;11 ∥ 𝑁    &   ⊢ ¬ ;13 ∥ 𝑁    &   ⊢ ¬ ;17 ∥ 𝑁    &   ⊢ ¬ ;19 ∥ 𝑁    &   ⊢ ¬ ;23 ∥ 𝑁    ⇒   ⊢ 𝑁 ∈ ℙ
Theorem	37prm 16831	37 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
⊢ ;37 ∈ ℙ
Theorem	43prm 16832	43 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
⊢ ;43 ∈ ℙ
Theorem	83prm 16833	83 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
⊢ ;83 ∈ ℙ
Theorem	139prm 16834	139 is a prime number. (Contributed by Mario Carneiro, 19-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
⊢ ;;139 ∈ ℙ
Theorem	163prm 16835	163 is a prime number. (Contributed by Mario Carneiro, 19-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
⊢ ;;163 ∈ ℙ
Theorem	317prm 16836	317 is a prime number. (Contributed by Mario Carneiro, 19-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
⊢ ;;317 ∈ ℙ
Theorem	631prm 16837	631 is a prime number. (Contributed by Mario Carneiro, 1-Mar-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
⊢ ;;631 ∈ ℙ
Theorem	prmo4 16838	The primorial of 4. (Contributed by AV, 28-Aug-2020.)
⊢ (#p‘4) = 6
Theorem	prmo5 16839	The primorial of 5. (Contributed by AV, 28-Aug-2020.)
⊢ (#p‘5) = ;30
Theorem	prmo6 16840	The primorial of 6. (Contributed by AV, 28-Aug-2020.)
⊢ (#p‘6) = ;30
6.2.20  Very large primes
Theorem	1259lem1 16841	Lemma for 1259prm 16846. Calculate a power mod. In decimal, we calculate 2↑16 = 52𝑁 + 68≡68 and 2↑17≡68 · 2 = 136 in this lemma. (Contributed by Mario Carneiro, 22-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 16-Sep-2021.)
⊢ 𝑁 = ;;;1259    ⇒   ⊢ ((2↑;17) mod 𝑁) = (;;136 mod 𝑁)
Theorem	1259lem2 16842	Lemma for 1259prm 16846. Calculate a power mod. In decimal, we calculate 2↑34 = (2↑17)↑2≡136↑2≡14𝑁 + 870. (Contributed by Mario Carneiro, 22-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 15-Sep-2021.)
⊢ 𝑁 = ;;;1259    ⇒   ⊢ ((2↑;34) mod 𝑁) = (;;870 mod 𝑁)
Theorem	1259lem3 16843	Lemma for 1259prm 16846. Calculate a power mod. In decimal, we calculate 2↑38 = 2↑34 · 2↑4≡870 · 16 = 11𝑁 + 71 and 2↑76 = (2↑34)↑2≡71↑2 = 4𝑁 + 5≡5. (Contributed by Mario Carneiro, 22-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 16-Sep-2021.)
⊢ 𝑁 = ;;;1259    ⇒   ⊢ ((2↑;76) mod 𝑁) = (5 mod 𝑁)
Theorem	1259lem4 16844	Lemma for 1259prm 16846. Calculate a power mod. In decimal, we calculate 2↑306 = (2↑76)↑4 · 4≡5↑4 · 4 = 2𝑁 − 18, 2↑612 = (2↑306)↑2≡18↑2 = 324, 2↑629 = 2↑612 · 2↑17≡324 · 136 = 35𝑁 − 1 and finally 2↑(𝑁 − 1) = (2↑629)↑2≡1↑2 = 1. (Contributed by Mario Carneiro, 22-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 16-Sep-2021.)
⊢ 𝑁 = ;;;1259    ⇒   ⊢ ((2↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁)
Theorem	1259lem5 16845	Lemma for 1259prm 16846. Calculate the GCD of 2↑34 − 1≡869 with 𝑁 = 1259. (Contributed by Mario Carneiro, 22-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
⊢ 𝑁 = ;;;1259    ⇒   ⊢ (((2↑;34) − 1) gcd 𝑁) = 1
Theorem	1259prm 16846	1259 is a prime number. (Contributed by Mario Carneiro, 22-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
⊢ 𝑁 = ;;;1259    ⇒   ⊢ 𝑁 ∈ ℙ
Theorem	2503lem1 16847	Lemma for 2503prm 16850. Calculate a power mod. In decimal, we calculate 2↑18 = 512↑2 = 104𝑁 + 1832≡1832. (Contributed by Mario Carneiro, 3-Mar-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 16-Sep-2021.)
⊢ 𝑁 = ;;;2503    ⇒   ⊢ ((2↑;18) mod 𝑁) = (;;;1832 mod 𝑁)
Theorem	2503lem2 16848	Lemma for 2503prm 16850. Calculate a power mod. We calculate 2↑19 = 2↑18 · 2≡1832 · 2 = 𝑁 + 1161, 2↑38 = (2↑19)↑2≡1161↑2 = 538𝑁 + 1307, 2↑39 = 2↑38 · 2≡1307 · 2 = 𝑁 + 111, 2↑78 = (2↑39)↑2≡111↑2 = 5𝑁 − 194, 2↑156 = (2↑78)↑2≡194↑2 = 15𝑁 + 91, 2↑312 = (2↑156)↑2≡91↑2 = 3𝑁 + 772, 2↑624 = (2↑312)↑2≡772↑2 = 238𝑁 + 270, 2↑1248 = (2↑624)↑2≡270↑2 = 29𝑁 + 313, 2↑1251 = 2↑1248 · 8≡313 · 8 = 𝑁 + 1 and finally 2↑(𝑁 − 1) = (2↑1251)↑2≡1↑2 = 1. (Contributed by Mario Carneiro, 3-Mar-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 16-Sep-2021.)
⊢ 𝑁 = ;;;2503    ⇒   ⊢ ((2↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁)
Theorem	2503lem3 16849	Lemma for 2503prm 16850. Calculate the GCD of 2↑18 − 1≡1831 with 𝑁 = 2503. (Contributed by Mario Carneiro, 3-Mar-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 15-Sep-2021.)
⊢ 𝑁 = ;;;2503    ⇒   ⊢ (((2↑;18) − 1) gcd 𝑁) = 1
Theorem	2503prm 16850	2503 is a prime number. (Contributed by Mario Carneiro, 3-Mar-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
⊢ 𝑁 = ;;;2503    ⇒   ⊢ 𝑁 ∈ ℙ
Theorem	4001lem1 16851	Lemma for 4001prm 16855. Calculate a power mod. In decimal, we calculate 2↑12 = 4096 = 𝑁 + 95, 2↑24 = (2↑12)↑2≡95↑2 = 2𝑁 + 1023, 2↑25 = 2↑24 · 2≡1023 · 2 = 2046, 2↑50 = (2↑25)↑2≡2046↑2 = 1046𝑁 + 1070, 2↑100 = (2↑50)↑2≡1070↑2 = 286𝑁 + 614 and 2↑200 = (2↑100)↑2≡614↑2 = 94𝑁 + 902 ≡902. (Contributed by Mario Carneiro, 3-Mar-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 16-Sep-2021.)
⊢ 𝑁 = ;;;4001    ⇒   ⊢ ((2↑;;200) mod 𝑁) = (;;902 mod 𝑁)
Theorem	4001lem2 16852	Lemma for 4001prm 16855. Calculate a power mod. In decimal, we calculate 2↑400 = (2↑200)↑2≡902↑2 = 203𝑁 + 1401 and 2↑800 = (2↑400)↑2≡1401↑2 = 490𝑁 + 2311 ≡2311. (Contributed by Mario Carneiro, 3-Mar-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 16-Sep-2021.)
⊢ 𝑁 = ;;;4001    ⇒   ⊢ ((2↑;;800) mod 𝑁) = (;;;2311 mod 𝑁)
Theorem	4001lem3 16853	Lemma for 4001prm 16855. Calculate a power mod. In decimal, we calculate 2↑1000 = 2↑800 · 2↑200≡2311 · 902 = 521𝑁 + 1 and finally 2↑(𝑁 − 1) = (2↑1000)↑4≡1↑4 = 1. (Contributed by Mario Carneiro, 3-Mar-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 16-Sep-2021.)
⊢ 𝑁 = ;;;4001    ⇒   ⊢ ((2↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁)
Theorem	4001lem4 16854	Lemma for 4001prm 16855. Calculate the GCD of 2↑800 − 1≡2310 with 𝑁 = 4001. (Contributed by Mario Carneiro, 3-Mar-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 16-Sep-2021.)
⊢ 𝑁 = ;;;4001    ⇒   ⊢ (((2↑;;800) − 1) gcd 𝑁) = 1
Theorem	4001prm 16855	4001 is a prime number. (Contributed by Mario Carneiro, 3-Mar-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 16-Sep-2021.)
⊢ 𝑁 = ;;;4001    ⇒   ⊢ 𝑁 ∈ ℙ
PART 7  BASIC STRUCTURES
7.1  Extensible structures
7.1.1  Basic definitions An "extensible structure" (or "structure" in short, at least in this section) is used to define a specific group, ring, poset, and so on. An extensible structure can contain many components. For example, a group will have at least two components (base set and operation), although it can be further specialized by adding other components such as a multiplicative operation for rings (and still remain a group per our definition). Thus, every ring is also a group. This extensible structure approach allows theorems from more general structures (such as groups) to be reused for more specialized structures (such as rings) without having to reprove anything. Structures are common in mathematics, but in informal (natural language) proofs the details are assumed in ways that we must make explicit. An extensible structure is implemented as a function (a set of ordered pairs) on a finite (and not necessarily sequential) subset of ℕ. The function's argument is the index of a structure component (such as 1 for the base set of a group), and its value is the component (such as the base set). By convention, we normally avoid direct reference to the hard-coded numeric index and instead use structure component extractors such as ndxid 16907 and strfv 16914. Using extractors makes it easier to change numeric indices and also makes the components' purpose clearer. For example, as noted in ndxid 16907, we can refer to a specific poset with base set 𝐵 and order relation 𝐿 using the extensible structure {⟨(Base‘ndx), 𝐵⟩, ⟨(le‘ndx), 𝐿⟩} rather than {⟨1, 𝐵⟩, ⟨;10, 𝐿⟩}. See section header comment mmtheorems.html#cnx 16907 for more details on numeric indices versus the structure component extractors. There are many other possible ways to handle structures. We chose this extensible structure approach because this approach (1) results in simpler notation than other approaches we are aware of, and (2) is easier to do proofs with. We cannot use an approach that uses "hidden" arguments; Metamath does not support hidden arguments, and in any case we want nothing hidden. It would be possible to use a categorical approach (e.g., something vaguely similar to Lean's mathlib). However, instances (the chain of proofs that an 𝑋 is a 𝑌 via a bunch of forgetful functors) can cause serious performance problems for automated tooling, and the resulting proofs would be painful to look at directly (in the case of Lean, they are long past the level where people would find it acceptable to look at them directly). Metamath is working under much stricter conditions than this, and it has still managed to achieve about the same level of flexibility through this "extensible structure" approach. To create a substructure of a given extensible structure, you can simply use the multifunction restriction operator for extensible structures ↾s as defined in df-ress 16951. This can be used to turn statements about rings into statements about subrings, modules into submodules, etc. This definition knows nothing about individual structures and merely truncates the Base set while leaving operators alone. Individual kinds of structures will need to handle this behavior by ignoring operators' values outside the range (like Ring), defining a function using the base set and applying that (like TopGrp), or explicitly truncating the slot before use (like MetSp). For example, the unital ring of integers ℤring is defined in df-zring 20680 as simply ℤring = (ℂfld ↾s ℤ). This can be similarly done for all other subsets of ℂ, which has all the structure we can show applies to it, and this all comes "for free". Should we come up with some new structure in the future that we wish ℂ to inherit, then we change the definition of ℂfld, reprove all the slot extraction theorems, add a new one, and that's it. None of the other downstream theorems have to change. Note that the construct of df-prds 17167 addresses a different situation. It is not possible to have SubGroup and SubRing be the same thing because they produce different outputs on the same input. The subgroups of an extensible structure treated as a group are not the same as the subrings of that same structure. With df-prds 17167 it can actually reasonably perform the task, that is, being the product group given a family of groups, while also being the product ring given a family of rings. There is no contradiction here because the group part of a product ring is a product group. There is also a general theory of "substructure algebras", in the form of df-mre 17304 and df-acs 17307. SubGroup is a Moore collection, as is SubRing, SubRng and many other substructure collections. But it is not useful for picking out a particular collection of interest; SubRing and SubGroup still need to be defined and they are distinct --- nothing is going to select these definitions for us. Extensible structures only work well when they represent concrete categories, where there is a "base set", morphisms are functions, and subobjects are subsets with induced operations. In short, they primarily work well for "sets with (some) extra structure". Extensible structures may not suffice for more complicated situations. For example, in manifolds, ↾s would not work. That said, extensible structures are sufficient for many of the structures that set.mm currently considers, and offer a good compromise for a goal-oriented formalization.
7.1.1.1  Extensible structures as structures with components
Syntax	cstr 16856	Extend class notation with the class of structures with components numbered below 𝐴.
class Struct
Definition	df-struct 16857*	Define a structure with components in 𝑀...𝑁. This is not a requirement for groups, posets, etc., but it is a useful assumption for component extraction theorems. As mentioned in the section header, an "extensible structure should be implemented as a function (a set of ordered pairs)". The current definition, however, is less restrictive: it allows for classes which contain the empty set ∅ to be extensible structures. Because of 0nelfun 6459, such classes cannot be functions. Without the empty set, however, a structure must be a function, see structn0fun 16861: 𝐹 Struct 𝑋 → Fun (𝐹 ∖ {∅}). Allowing an extensible structure to contain the empty set ensures that expressions like {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} are structures without asserting or implying that 𝐴, 𝐵, 𝐶 and 𝐷 are sets (if 𝐴 or 𝐵 is a proper class, then ⟨𝐴, 𝐵⟩ = ∅, see opprc 4828). This is used critically in strle1 16868, strle2 16869, strle3 16870 and strleun 16867 to avoid sethood hypotheses on the "payload" sets: without this, ipsstr 17055 and theorems like it will have many sethood assumptions, and may not even be usable in the empty context. Instead, the sethood assumption is deferred until it is actually needed, e.g., ipsbase 17056, which requires that the base set be a set but not any of the other components. Usually, a concrete structure like ℂfld does not contain the empty set, and therefore is a function, see cnfldfun 20618. (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ Struct = {⟨𝑓, 𝑥⟩ ∣ (𝑥 ∈ ( ≤ ∩ (ℕ × ℕ)) ∧ Fun (𝑓 ∖ {∅}) ∧ dom 𝑓 ⊆ (...‘𝑥))}
Theorem	brstruct 16858	The structure relation is a relation. (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ Rel Struct
Theorem	isstruct2 16859	The property of being a structure with components in (1st ‘𝑋)...(2nd ‘𝑋). (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ (𝐹 Struct 𝑋 ↔ (𝑋 ∈ ( ≤ ∩ (ℕ × ℕ)) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)))
Theorem	structex 16860	A structure is a set. (Contributed by AV, 10-Nov-2021.)
⊢ (𝐺 Struct 𝑋 → 𝐺 ∈ V)
Theorem	structn0fun 16861	A structure without the empty set is a function. (Contributed by AV, 13-Nov-2021.)
⊢ (𝐹 Struct 𝑋 → Fun (𝐹 ∖ {∅}))
Theorem	isstruct 16862	The property of being a structure with components in 𝑀...𝑁. (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ (𝐹 Struct ⟨𝑀, 𝑁⟩ ↔ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (𝑀...𝑁)))
Theorem	structcnvcnv 16863	Two ways to express the relational part of a structure. (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ (𝐹 Struct 𝑋 → ◡◡𝐹 = (𝐹 ∖ {∅}))
Theorem	structfung 16864	The converse of the converse of a structure is a function. Closed form of structfun 16865. (Contributed by AV, 12-Nov-2021.)
⊢ (𝐹 Struct 𝑋 → Fun ◡◡𝐹)
Theorem	structfun 16865	Convert between two kinds of structure closure. (Contributed by Mario Carneiro, 29-Aug-2015.) (Proof shortened by AV, 12-Nov-2021.)
⊢ 𝐹 Struct 𝑋    ⇒   ⊢ Fun ◡◡𝐹
Theorem	structfn 16866	Convert between two kinds of structure closure. (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ 𝐹 Struct ⟨𝑀, 𝑁⟩    ⇒   ⊢ (Fun ◡◡𝐹 ∧ dom 𝐹 ⊆ (1...𝑁))
Theorem	strleun 16867	Combine two structures into one. (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ 𝐹 Struct ⟨𝐴, 𝐵⟩    &   ⊢ 𝐺 Struct ⟨𝐶, 𝐷⟩    &   ⊢ 𝐵 < 𝐶    ⇒   ⊢ (𝐹 ∪ 𝐺) Struct ⟨𝐴, 𝐷⟩
Theorem	strle1 16868	Make a structure from a singleton. (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ 𝐼 ∈ ℕ    &   ⊢ 𝐴 = 𝐼    ⇒   ⊢ {⟨𝐴, 𝑋⟩} Struct ⟨𝐼, 𝐼⟩
Theorem	strle2 16869	Make a structure from a pair. (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ 𝐼 ∈ ℕ    &   ⊢ 𝐴 = 𝐼    &   ⊢ 𝐼 < 𝐽    &   ⊢ 𝐽 ∈ ℕ    &   ⊢ 𝐵 = 𝐽    ⇒   ⊢ {⟨𝐴, 𝑋⟩, ⟨𝐵, 𝑌⟩} Struct ⟨𝐼, 𝐽⟩
Theorem	strle3 16870	Make a structure from a triple. (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ 𝐼 ∈ ℕ    &   ⊢ 𝐴 = 𝐼    &   ⊢ 𝐼 < 𝐽    &   ⊢ 𝐽 ∈ ℕ    &   ⊢ 𝐵 = 𝐽    &   ⊢ 𝐽 < 𝐾    &   ⊢ 𝐾 ∈ ℕ    &   ⊢ 𝐶 = 𝐾    ⇒   ⊢ {⟨𝐴, 𝑋⟩, ⟨𝐵, 𝑌⟩, ⟨𝐶, 𝑍⟩} Struct ⟨𝐼, 𝐾⟩
Theorem	sbcie2s 16871*	A special version of class substitution commonly used for structures. (Contributed by Thierry Arnoux, 14-Mar-2019.)
⊢ 𝐴 = (𝐸‘𝑊)    &   ⊢ 𝐵 = (𝐹‘𝑊)    &   ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝑤 = 𝑊 → ([(𝐸‘𝑤) / 𝑎][(𝐹‘𝑤) / 𝑏]𝜓 ↔ 𝜑))
Theorem	sbcie3s 16872*	A special version of class substitution commonly used for structures. (Contributed by Thierry Arnoux, 15-Mar-2019.)
⊢ 𝐴 = (𝐸‘𝑊)    &   ⊢ 𝐵 = (𝐹‘𝑊)    &   ⊢ 𝐶 = (𝐺‘𝑊)    &   ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝑤 = 𝑊 → ([(𝐸‘𝑤) / 𝑎][(𝐹‘𝑤) / 𝑏][(𝐺‘𝑤) / 𝑐]𝜓 ↔ 𝜑))
7.1.1.2  Substitution of components
Syntax	csts 16873	Set components of a structure.
class sSet
Definition	df-sets 16874*	Set a component of an extensible structure. This function is useful for taking an existing structure and "overriding" one of its components. For example, df-ress 16951 adjusts the base set to match its second argument, which has the effect of making subgroups, subspaces, subrings etc. from the original structures. Or df-mgp 19730, which takes a ring and overrides its addition operation with the multiplicative operation, so that we can consider the "multiplicative group" using group and monoid theorems, which expect the operation to be in the +g slot instead of the .r slot. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ sSet = (𝑠 ∈ V, 𝑒 ∈ V ↦ ((𝑠 ↾ (V ∖ dom {𝑒})) ∪ {𝑒}))
Theorem	reldmsets 16875	The structure override operator is a proper operator. (Contributed by Stefan O'Rear, 29-Jan-2015.)
⊢ Rel dom sSet
Theorem	setsvalg 16876	Value of the structure replacement function. (Contributed by Mario Carneiro, 30-Apr-2015.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑆 sSet 𝐴) = ((𝑆 ↾ (V ∖ dom {𝐴})) ∪ {𝐴}))
Theorem	setsval 16877	Value of the structure replacement function. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝑆 sSet ⟨𝐴, 𝐵⟩) = ((𝑆 ↾ (V ∖ {𝐴})) ∪ {⟨𝐴, 𝐵⟩}))
Theorem	fvsetsid 16878	The value of the structure replacement function for its first argument is its second argument. (Contributed by SO, 12-Jul-2018.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ∧ 𝑌 ∈ 𝑈) → ((𝐹 sSet ⟨𝑋, 𝑌⟩)‘𝑋) = 𝑌)
Theorem	fsets 16879	The structure replacement function is a function. (Contributed by SO, 12-Jul-2018.)
⊢ (((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (𝐹 sSet ⟨𝑋, 𝑌⟩):𝐴⟶𝐵)
Theorem	setsdm 16880	The domain of a structure with replacement is the domain of the original structure extended by the index of the replacement. (Contributed by AV, 7-Jun-2021.)
⊢ ((𝐺 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → dom (𝐺 sSet ⟨𝐼, 𝐸⟩) = (dom 𝐺 ∪ {𝐼}))
Theorem	setsfun 16881	A structure with replacement is a function if the original structure is a function. (Contributed by AV, 7-Jun-2021.)
⊢ (((𝐺 ∈ 𝑉 ∧ Fun 𝐺) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → Fun (𝐺 sSet ⟨𝐼, 𝐸⟩))
Theorem	setsfun0 16882	A structure with replacement without the empty set is a function if the original structure without the empty set is a function. This variant of setsfun 16881 is useful for proofs based on isstruct2 16859 which requires Fun (𝐹 ∖ {∅}) for 𝐹 to be an extensible structure. (Contributed by AV, 7-Jun-2021.)
⊢ (((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅})) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → Fun ((𝐺 sSet ⟨𝐼, 𝐸⟩) ∖ {∅}))
Theorem	setsn0fun 16883	The value of the structure replacement function (without the empty set) is a function if the structure (without the empty set) is a function. (Contributed by AV, 7-Jun-2021.) (Revised by AV, 16-Nov-2021.)
⊢ (𝜑 → 𝑆 Struct 𝑋)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑊)    ⇒   ⊢ (𝜑 → Fun ((𝑆 sSet ⟨𝐼, 𝐸⟩) ∖ {∅}))
Theorem	setsstruct2 16884	An extensible structure with a replaced slot is an extensible structure. (Contributed by AV, 14-Nov-2021.)
⊢ (((𝐺 Struct 𝑋 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ℕ) ∧ 𝑌 = ⟨if(𝐼 ≤ (1st ‘𝑋), 𝐼, (1st ‘𝑋)), if(𝐼 ≤ (2nd ‘𝑋), (2nd ‘𝑋), 𝐼)⟩) → (𝐺 sSet ⟨𝐼, 𝐸⟩) Struct 𝑌)
Theorem	setsexstruct2 16885*	An extensible structure with a replaced slot is an extensible structure. (Contributed by AV, 14-Nov-2021.)
⊢ ((𝐺 Struct 𝑋 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ℕ) → ∃𝑦(𝐺 sSet ⟨𝐼, 𝐸⟩) Struct 𝑦)
Theorem	setsstruct 16886	An extensible structure with a replaced slot is an extensible structure. (Contributed by AV, 9-Jun-2021.) (Revised by AV, 14-Nov-2021.)
⊢ ((𝐸 ∈ 𝑉 ∧ 𝐼 ∈ (ℤ≥‘𝑀) ∧ 𝐺 Struct ⟨𝑀, 𝑁⟩) → (𝐺 sSet ⟨𝐼, 𝐸⟩) Struct ⟨𝑀, if(𝐼 ≤ 𝑁, 𝑁, 𝐼)⟩)
Theorem	wunsets 16887	Closure of structure replacement in a weak universe. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝑆 sSet 𝐴) ∈ 𝑈)
Theorem	setsres 16888	The structure replacement function does not affect the value of 𝑆 away from 𝐴. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ (𝑆 ∈ 𝑉 → ((𝑆 sSet ⟨𝐴, 𝐵⟩) ↾ (V ∖ {𝐴})) = (𝑆 ↾ (V ∖ {𝐴})))
Theorem	setsabs 16889	Replacing the same components twice yields the same as the second setting only. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → ((𝑆 sSet ⟨𝐴, 𝐵⟩) sSet ⟨𝐴, 𝐶⟩) = (𝑆 sSet ⟨𝐴, 𝐶⟩))
Theorem	setscom 16890	Component-setting is commutative when the x-values are different. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋)) → ((𝑆 sSet ⟨𝐴, 𝐶⟩) sSet ⟨𝐵, 𝐷⟩) = ((𝑆 sSet ⟨𝐵, 𝐷⟩) sSet ⟨𝐴, 𝐶⟩))
7.1.1.3  Slots
Syntax	cslot 16891	Extend class notation with the slot function.
class Slot 𝐴
Definition	df-slot 16892*	Define the slot extractor for extensible structures. The class Slot 𝐴 is a function whose argument can be any set, although it is meaningful only if that set is a member of an extensible structure (such as a partially ordered set (df-poset 18040) or a group (df-grp 18589)). Note that Slot 𝐴 is implemented as "evaluation at 𝐴". That is, (Slot 𝐴‘𝑆) is defined to be (𝑆‘𝐴), where 𝐴 will typically be an index (which is implemented as a small natural number) of a component of an extensible structure 𝑆. Each extensible structure is a function defined on specific (natural number) "slots", and the function Slot 𝐴 extracts the structure's component as a function value at a particular slot (with index 𝐴). The special "structure" ndx, defined as the identity function restricted to ℕ, can be used to extract the number 𝐴 from a slot, since (Slot 𝐴‘ndx) = 𝐴 (see ndxarg 16906). This is typically used to refer to the number of a slot when defining structures without having to expose the detail of what that number is (for instance, we use the expression (Base‘ndx) in theorems and proofs instead of its hard-coded, numeric value 1), and discourage using the specific definition of slot extractors like Base = Slot 1 (see df-base 16922). Actually, these definitions are used in two basic theorems named *id (theorems of the form 𝐶 = Slot (𝐶‘ndx)) and *ndx (theorems of the form (𝐶‘ndx) = 𝑁) only (see, for example, baseid 16924 and basendx 16930), except additionally in the discouraged theorem baseval 16923 to demonstrate the representations of the value of the base set extractor. The *id theorems are implementation independent equivalents of the definitions by the means of ndxid 16907, but the *ndx theorems still depend on the hard-coded values of the indices. Therefore, the usage of these *ndx theorems is also discouraged (for more details see the section header comment mmtheorems.html#cnx 16907). Example: The group operation is the second component, i.e., the component in the second slot, of a group-like structure 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩} (see grpstr 17003). The slot extractor +g = Slot 2 (see df-plusg 16984) applied on the structure 𝐺 provides the group operation + = (+g‘𝐺). Expanding the defintions, we get + = (Slot 2‘𝐺) = (𝐺‘2) = (𝐺‘(+g‘ndx)) (for the last equation, see plusgndx 16997). The class Slot cannot be defined as (𝑥 ∈ V ↦ (𝑓 ∈ V ↦ (𝑓‘𝑥))) because each Slot 𝐴 is a function on the proper class V so is itself a proper class, and the values of functions are sets (fvex 6796). It is necessary to allow proper classes as values of Slot 𝐴 since for instance the class of all (base sets of) groups is proper. (Contributed by Mario Carneiro, 22-Sep-2015.)
⊢ Slot 𝐴 = (𝑥 ∈ V ↦ (𝑥‘𝐴))
Theorem	sloteq 16893	Equality theorem for the Slot construction. The converse holds if 𝐴 (or 𝐵) is a set. (Contributed by BJ, 27-Dec-2021.)
⊢ (𝐴 = 𝐵 → Slot 𝐴 = Slot 𝐵)
Theorem	slotfn 16894	A slot is a function on sets, treated as structures. (Contributed by Mario Carneiro, 22-Sep-2015.)
⊢ 𝐸 = Slot 𝑁    ⇒   ⊢ 𝐸 Fn V
Theorem	strfvnd 16895	Deduction version of strfvn 16896. (Contributed by Mario Carneiro, 15-Nov-2014.)
⊢ 𝐸 = Slot 𝑁    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐸‘𝑆) = (𝑆‘𝑁))
Theorem	strfvn 16896	Value of a structure component extractor 𝐸. Normally, 𝐸 is a defined constant symbol such as Base (df-base 16922) and 𝑁 is the index of the component. 𝑆 is a structure, i.e. a specific member of a class of structures such as Poset (df-poset 18040) where 𝑆 ∈ Poset. Hint: Do not substitute 𝑁 by a specific (positive) integer to be independent of a hard-coded index value. Often, (𝐸‘ndx) can be used instead of 𝑁. Alternatively, use strfv 16914 instead of strfvn 16896. (Contributed by NM, 9-Sep-2011.) (Revised by Mario Carneiro, 6-Oct-2013.) (New usage is discouraged.)
⊢ 𝑆 ∈ V    &   ⊢ 𝐸 = Slot 𝑁    ⇒   ⊢ (𝐸‘𝑆) = (𝑆‘𝑁)
Theorem	strfvss 16897	A structure component extractor produces a value which is contained in a set dependent on 𝑆, but not 𝐸. This is sometimes useful for showing sethood. (Contributed by Mario Carneiro, 15-Aug-2015.)
⊢ 𝐸 = Slot 𝑁    ⇒   ⊢ (𝐸‘𝑆) ⊆ ∪ ran 𝑆
Theorem	wunstr 16898	Closure of a structure index in a weak universe. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝐸 = Slot 𝑁    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐸‘𝑆) ∈ 𝑈)
Theorem	str0 16899	All components of the empty set are empty sets. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 7-Dec-2014.)
⊢ 𝐹 = Slot 𝐼    ⇒   ⊢ ∅ = (𝐹‘∅)
Theorem	strfvi 16900	Structure slot extractors cannot distinguish between proper classes and ∅, so they can be protected using the identity function. (Contributed by Stefan O'Rear, 21-Mar-2015.)
⊢ 𝐸 = Slot 𝑁    &   ⊢ 𝑋 = (𝐸‘𝑆)    ⇒   ⊢ 𝑋 = (𝐸‘( I ‘𝑆))