Home | Metamath
Proof Explorer Theorem List (p. 136 of 424) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lsws4 13501 | The last symbol of a 4 letter word is its fourth symbol. (Contributed by AV, 8-Feb-2021.) |
⊢ (𝐷 ∈ 𝑉 → ( lastS ‘〈“𝐴𝐵𝐶𝐷”〉) = 𝐷) | ||
Theorem | s2prop 13502 | A length 2 word is an unordered pair of ordered pairs. (Contributed by Alexander van der Vekens, 14-Aug-2017.) |
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → 〈“𝐴𝐵”〉 = {〈0, 𝐴〉, 〈1, 𝐵〉}) | ||
Theorem | s2dmALT 13503 | Alternate version of s2dm 13485, having a shorter proof, but requiring that 𝐴 and 𝐵 are sets. (Contributed by AV, 9-Jan-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → dom 〈“𝐴𝐵”〉 = {0, 1}) | ||
Theorem | s3tpop 13504 | A length 3 word is an unordered triple of ordered pairs. (Contributed by AV, 23-Jan-2021.) |
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → 〈“𝐴𝐵𝐶”〉 = {〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}) | ||
Theorem | s4prop 13505 | A length 4 word is a union of two unordered pairs of ordered pairs. (Contributed by Alexander van der Vekens, 14-Aug-2017.) |
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → 〈“𝐴𝐵𝐶𝐷”〉 = ({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉, 〈3, 𝐷〉})) | ||
Theorem | s3fn 13506 | A length 3 word is a function with a triple as domain. (Contributed by Alexander van der Vekens, 5-Dec-2017.) (Revised by AV, 23-Jan-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → 〈“𝐴𝐵𝐶”〉 Fn {0, 1, 2}) | ||
Theorem | funcnvs1 13507 | The converse of a singleton word is a function. (Contributed by AV, 22-Jan-2021.) |
⊢ Fun ◡〈“𝐴”〉 | ||
Theorem | funcnvs2 13508 | The converse of a length 2 word is a function if its symbols are different sets. (Contributed by AV, 23-Jan-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) → Fun ◡〈“𝐴𝐵”〉) | ||
Theorem | funcnvs3 13509 | The converse of a length 3 word is a function if its symbols are different sets. (Contributed by Alexander van der Vekens, 31-Jan-2018.) (Revised by AV, 23-Jan-2021.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → Fun ◡〈“𝐴𝐵𝐶”〉) | ||
Theorem | funcnvs4 13510 | The converse of a length 4 word is a function if its symbols are different sets. (Contributed by AV, 10-Feb-2021.) |
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) ∧ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷)) → Fun ◡〈“𝐴𝐵𝐶𝐷”〉) | ||
Theorem | s2f1o 13511 | A length 2 word with mutually different symbols is a one-to-one function onto the set of the symbols. (Contributed by Alexander van der Vekens, 14-Aug-2017.) |
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵) → (𝐸 = 〈“𝐴𝐵”〉 → 𝐸:{0, 1}–1-1-onto→{𝐴, 𝐵})) | ||
Theorem | f1oun2prg 13512 | A union of unordered pairs of ordered pairs with different elements is a one-to-one onto function. (Contributed by Alexander van der Vekens, 14-Aug-2017.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → (((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷)) → ({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉, 〈3, 𝐷〉}):({0, 1} ∪ {2, 3})–1-1-onto→({𝐴, 𝐵} ∪ {𝐶, 𝐷}))) | ||
Theorem | s4f1o 13513 | A length 4 word with mutually different symbols is a one-to-one function onto the set of the symbols. (Contributed by Alexander van der Vekens, 14-Aug-2017.) |
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷)) → (𝐸 = 〈“𝐴𝐵𝐶𝐷”〉 → 𝐸:dom 𝐸–1-1-onto→({𝐴, 𝐵} ∪ {𝐶, 𝐷})))) | ||
Theorem | s4dom 13514 | The domain of a length 4 word is the union of two (disjunct) pairs. (Contributed by Alexander van der Vekens, 15-Aug-2017.) |
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (𝐸 = 〈“𝐴𝐵𝐶𝐷”〉 → dom 𝐸 = ({0, 1} ∪ {2, 3}))) | ||
Theorem | s2co 13515 | Mapping a doubleton word by a function. (Contributed by Mario Carneiro, 27-Feb-2016.) |
⊢ (𝜑 → 𝐹:𝑋⟶𝑌) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑋) ⇒ ⊢ (𝜑 → (𝐹 ∘ 〈“𝐴𝐵”〉) = 〈“(𝐹‘𝐴)(𝐹‘𝐵)”〉) | ||
Theorem | s3co 13516 | Mapping a length 3 string by a function. (Contributed by Mario Carneiro, 27-Feb-2016.) |
⊢ (𝜑 → 𝐹:𝑋⟶𝑌) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑋) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) ⇒ ⊢ (𝜑 → (𝐹 ∘ 〈“𝐴𝐵𝐶”〉) = 〈“(𝐹‘𝐴)(𝐹‘𝐵)(𝐹‘𝐶)”〉) | ||
Theorem | s0s1 13517 | Concatenation of fixed length strings. (This special case of ccatlid 13222 is provided to complete the pattern s0s1 13517, df-s2 13444, df-s3 13445, ...) (Contributed by Mario Carneiro, 28-Feb-2016.) |
⊢ 〈“𝐴”〉 = (∅ ++ 〈“𝐴”〉) | ||
Theorem | s1s2 13518 | Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶”〉 = (〈“𝐴”〉 ++ 〈“𝐵𝐶”〉) | ||
Theorem | s1s3 13519 | Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶𝐷”〉 = (〈“𝐴”〉 ++ 〈“𝐵𝐶𝐷”〉) | ||
Theorem | s1s4 13520 | Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶𝐷𝐸”〉 = (〈“𝐴”〉 ++ 〈“𝐵𝐶𝐷𝐸”〉) | ||
Theorem | s1s5 13521 | Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶𝐷𝐸𝐹”〉 = (〈“𝐴”〉 ++ 〈“𝐵𝐶𝐷𝐸𝐹”〉) | ||
Theorem | s1s6 13522 | Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”〉 = (〈“𝐴”〉 ++ 〈“𝐵𝐶𝐷𝐸𝐹𝐺”〉) | ||
Theorem | s1s7 13523 | Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”〉 = (〈“𝐴”〉 ++ 〈“𝐵𝐶𝐷𝐸𝐹𝐺𝐻”〉) | ||
Theorem | s2s2 13524 | Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶𝐷”〉 = (〈“𝐴𝐵”〉 ++ 〈“𝐶𝐷”〉) | ||
Theorem | s4s2 13525 | Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶𝐷𝐸𝐹”〉 = (〈“𝐴𝐵𝐶𝐷”〉 ++ 〈“𝐸𝐹”〉) | ||
Theorem | s4s3 13526 | Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”〉 = (〈“𝐴𝐵𝐶𝐷”〉 ++ 〈“𝐸𝐹𝐺”〉) | ||
Theorem | s4s4 13527 | Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”〉 = (〈“𝐴𝐵𝐶𝐷”〉 ++ 〈“𝐸𝐹𝐺𝐻”〉) | ||
Theorem | s3s4 13528 | Concatenation of fixed length strings. (Contributed by AV, 1-Mar-2021.) |
⊢ 〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”〉 = (〈“𝐴𝐵𝐶”〉 ++ 〈“𝐷𝐸𝐹𝐺”〉) | ||
Theorem | s2s5 13529 | Concatenation of fixed length strings. (Contributed by AV, 1-Mar-2021.) |
⊢ 〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”〉 = (〈“𝐴𝐵”〉 ++ 〈“𝐶𝐷𝐸𝐹𝐺”〉) | ||
Theorem | s5s2 13530 | Concatenation of fixed length strings. (Contributed by AV, 1-Mar-2021.) |
⊢ 〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”〉 = (〈“𝐴𝐵𝐶𝐷𝐸”〉 ++ 〈“𝐹𝐺”〉) | ||
Theorem | s2eq2s1eq 13531 | Two length 2 words are equal iff the corresponding singleton words consisting of their symbols are equal. (Contributed by Alexander van der Vekens, 24-Sep-2018.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → (〈“𝐴𝐵”〉 = 〈“𝐶𝐷”〉 ↔ (〈“𝐴”〉 = 〈“𝐶”〉 ∧ 〈“𝐵”〉 = 〈“𝐷”〉))) | ||
Theorem | s2eq2seq 13532 | Two length 2 words are equal iff the corresponding symbols are equal. (Contributed by AV, 20-Oct-2018.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → (〈“𝐴𝐵”〉 = 〈“𝐶𝐷”〉 ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) | ||
Theorem | swrds2 13533 | Extract two adjacent symbols from a word. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈ (0..^(#‘𝑊))) → (𝑊 substr 〈𝐼, (𝐼 + 2)〉) = 〈“(𝑊‘𝐼)(𝑊‘(𝐼 + 1))”〉) | ||
Theorem | wrdlen2i 13534 | Implications of a word of length 2. (Contributed by AV, 27-Jul-2018.) (Proof shortened by AV, 14-Oct-2018.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) → (𝑊 = {〈0, 𝑆〉, 〈1, 𝑇〉} → ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 2) ∧ ((𝑊‘0) = 𝑆 ∧ (𝑊‘1) = 𝑇)))) | ||
Theorem | wrd2pr2op 13535 | A word of length 2 represented as unordered pair of ordered pairs. (Contributed by AV, 20-Oct-2018.) (Proof shortened by AV, 26-Jan-2021.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 2) → 𝑊 = {〈0, (𝑊‘0)〉, 〈1, (𝑊‘1)〉}) | ||
Theorem | wrdlen2 13536 | A word of length 2. (Contributed by AV, 20-Oct-2018.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) → (𝑊 = {〈0, 𝑆〉, 〈1, 𝑇〉} ↔ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 2) ∧ ((𝑊‘0) = 𝑆 ∧ (𝑊‘1) = 𝑇)))) | ||
Theorem | wrdlen2s2 13537 | A word of length 2 as doubleton word. (Contributed by AV, 20-Oct-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 2) → 𝑊 = 〈“(𝑊‘0)(𝑊‘1)”〉) | ||
Theorem | wrdl2exs2 13538* | A word of length 2 is a doubleton word. (Contributed by AV, 25-Jan-2021.) |
⊢ ((𝑊 ∈ Word 𝑆 ∧ (#‘𝑊) = 2) → ∃𝑠 ∈ 𝑆 ∃𝑡 ∈ 𝑆 𝑊 = 〈“𝑠𝑡”〉) | ||
Theorem | wrd3tpop 13539 | A word of length 3 represented as triple of ordered pairs. (Contributed by AV, 26-Jan-2021.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 3) → 𝑊 = {〈0, (𝑊‘0)〉, 〈1, (𝑊‘1)〉, 〈2, (𝑊‘2)〉}) | ||
Theorem | wrdlen3s3 13540 | A word of length 3 as length 3 string. (Contributed by AV, 26-Jan-2021.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 3) → 𝑊 = 〈“(𝑊‘0)(𝑊‘1)(𝑊‘2)”〉) | ||
Theorem | repsw2 13541 | The "repeated symbol word" of length 2. (Contributed by AV, 6-Nov-2018.) |
⊢ (𝑆 ∈ 𝑉 → (𝑆 repeatS 2) = 〈“𝑆𝑆”〉) | ||
Theorem | repsw3 13542 | The "repeated symbol word" of length 3. (Contributed by AV, 6-Nov-2018.) |
⊢ (𝑆 ∈ 𝑉 → (𝑆 repeatS 3) = 〈“𝑆𝑆𝑆”〉) | ||
Theorem | swrd2lsw 13543 | Extract the last two symbols from a word. (Contributed by Alexander van der Vekens, 23-Sep-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 1 < (#‘𝑊)) → (𝑊 substr 〈((#‘𝑊) − 2), (#‘𝑊)〉) = 〈“(𝑊‘((#‘𝑊) − 2))( lastS ‘𝑊)”〉) | ||
Theorem | 2swrd2eqwrdeq 13544 | Two words of length at least 2 are equal if and only if they have the same prefix and the same two single symbols suffix. (Contributed by AV, 24-Sep-2018.) (Revised by Mario Carneiro/AV, 23-Oct-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (#‘𝑊)) → (𝑊 = 𝑈 ↔ ((#‘𝑊) = (#‘𝑈) ∧ ((𝑊 substr 〈0, ((#‘𝑊) − 2)〉) = (𝑈 substr 〈0, ((#‘𝑊) − 2)〉) ∧ (𝑊‘((#‘𝑊) − 2)) = (𝑈‘((#‘𝑊) − 2)) ∧ ( lastS ‘𝑊) = ( lastS ‘𝑈))))) | ||
Theorem | ccatw2s1ccatws2 13545 | The concatenation of a word with two singleton words equals the concatenation of the word with the doubleton word consisting of the symbols of the two singletons. (Contributed by Mario Carneiro/AV, 21-Oct-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) = (𝑊 ++ 〈“𝑋𝑌”〉)) | ||
Theorem | ccat2s1fvwALT 13546 | Alternate proof of ccat2s1fvw 13267 using words of length 2, see df-s2 13444. A symbol of the concatenation of a word with two single symbols corresponding to the symbol of the word. (Contributed by AV, 22-Sep-2018.) (Proof shortened by Mario Carneiro/AV, 21-Oct-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < (#‘𝑊)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘𝐼) = (𝑊‘𝐼)) | ||
Theorem | wwlktovf 13547* | Lemma 1 for wrd2f1tovbij 13551. (Contributed by Alexander van der Vekens, 27-Jul-2018.) |
⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)} & ⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {𝑃, 𝑛} ∈ 𝑋} & ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡‘1)) ⇒ ⊢ 𝐹:𝐷⟶𝑅 | ||
Theorem | wwlktovf1 13548* | Lemma 2 for wrd2f1tovbij 13551. (Contributed by Alexander van der Vekens, 27-Jul-2018.) |
⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)} & ⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {𝑃, 𝑛} ∈ 𝑋} & ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡‘1)) ⇒ ⊢ 𝐹:𝐷–1-1→𝑅 | ||
Theorem | wwlktovfo 13549* | Lemma 3 for wrd2f1tovbij 13551. (Contributed by Alexander van der Vekens, 27-Jul-2018.) |
⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)} & ⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {𝑃, 𝑛} ∈ 𝑋} & ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡‘1)) ⇒ ⊢ (𝑃 ∈ 𝑉 → 𝐹:𝐷–onto→𝑅) | ||
Theorem | wwlktovf1o 13550* | Lemma 4 for wrd2f1tovbij 13551. (Contributed by Alexander van der Vekens, 28-Jul-2018.) |
⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)} & ⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {𝑃, 𝑛} ∈ 𝑋} & ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡‘1)) ⇒ ⊢ (𝑃 ∈ 𝑉 → 𝐹:𝐷–1-1-onto→𝑅) | ||
Theorem | wrd2f1tovbij 13551* | There is a bijection between words of length two with a fixed first symbol contained in a pair and the symbols contained in a pair together with the fixed symbol. (Contributed by Alexander van der Vekens, 28-Jul-2018.) |
⊢ ((𝑉 ∈ 𝑌 ∧ 𝑃 ∈ 𝑉) → ∃𝑓 𝑓:{𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)}–1-1-onto→{𝑛 ∈ 𝑉 ∣ {𝑃, 𝑛} ∈ 𝑋}) | ||
Theorem | eqwrds3 13552 | A word is equal with a length 3 string iff it has length 3 and the same symbol at each position. (Contributed by AV, 12-May-2021.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑊 = 〈“𝐴𝐵𝐶”〉 ↔ ((#‘𝑊) = 3 ∧ ((𝑊‘0) = 𝐴 ∧ (𝑊‘1) = 𝐵 ∧ (𝑊‘2) = 𝐶)))) | ||
Theorem | wrdl3s3 13553* | A word of length 3 is a length 3 string. (Contributed by AV, 18-May-2021.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 3) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑊 = 〈“𝑎𝑏𝑐”〉) | ||
Theorem | s3sndisj 13554* | The singletons consisting of length 3 strings which have distinct third symbols are disjunct. (Contributed by AV, 17-May-2021.) |
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → Disj 𝑐 ∈ 𝑍 {〈“𝐴𝐵𝑐”〉}) | ||
Theorem | s3iunsndisj 13555* | The union of singletons consisting of length 3 strings which have distinct first and third symbols are disjunct. (Contributed by AV, 17-May-2021.) |
⊢ (𝐵 ∈ 𝑋 → Disj 𝑎 ∈ 𝑌 ∪ 𝑐 ∈ (𝑍 ∖ {𝑎}){〈“𝑎𝐵𝑐”〉}) | ||
Theorem | ofccat 13556 | Letterwise operations on word concatenations. (Contributed by Thierry Arnoux, 28-Sep-2018.) |
⊢ (𝜑 → 𝐸 ∈ Word 𝑆) & ⊢ (𝜑 → 𝐹 ∈ Word 𝑆) & ⊢ (𝜑 → 𝐺 ∈ Word 𝑇) & ⊢ (𝜑 → 𝐻 ∈ Word 𝑇) & ⊢ (𝜑 → (#‘𝐸) = (#‘𝐺)) & ⊢ (𝜑 → (#‘𝐹) = (#‘𝐻)) ⇒ ⊢ (𝜑 → ((𝐸 ++ 𝐹) ∘𝑓 𝑅(𝐺 ++ 𝐻)) = ((𝐸 ∘𝑓 𝑅𝐺) ++ (𝐹 ∘𝑓 𝑅𝐻))) | ||
Theorem | ofs1 13557 | Letterwise operations on a single letter word. (Contributed by Thierry Arnoux, 7-Oct-2018.) |
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇) → (〈“𝐴”〉 ∘𝑓 𝑅〈“𝐵”〉) = 〈“(𝐴𝑅𝐵)”〉) | ||
Theorem | ofs2 13558 | Letterwise operations on a double letter word. (Contributed by Thierry Arnoux, 7-Oct-2018.) |
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇)) → (〈“𝐴𝐵”〉 ∘𝑓 𝑅〈“𝐶𝐷”〉) = 〈“(𝐴𝑅𝐶)(𝐵𝑅𝐷)”〉) | ||
A relation, 𝑅, has the reflexive property if 𝐴𝑅𝐴 holds whenever 𝐴 is an element which could be related by the the relation, namely elements of its domain and range. Eliminating dummy variables we see that a segment of the identity relation must be a subset of the relation or ( I ↾ (ran 𝑅 ∪ dom 𝑅)) ⊆ 𝑅. See issref 5428. A relation, 𝑅, has the transitive property if 𝐴𝑅𝐶 holds whenever there exists an intermediate value 𝐵 such that both 𝐴𝑅𝐵 and 𝐵𝑅𝐶 hold. This can be expressed without dummy variables as (𝑅 ∘ 𝑅) ⊆ 𝑅. See cotr 5427. The transitive closure of a relation, (t+‘𝑅), is the smallest superset of the relation which has the transitive property. Likewise the reflexive-transitive closure, (t*‘𝑅), is the smallest superset which has both the reflexive and transitive properties. Not to be confused with the transitive closure of a set, trcl 8487, which is a closure relative to a different transitive property, df-tr 4681. | ||
Theorem | coss12d 13559 | Subset deduction for composition of two classes. (Contributed by RP, 24-Dec-2019.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐶 ⊆ 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐷)) | ||
Theorem | trrelssd 13560 | The composition of subclasses of a transitive relation is a subclass of that relation. (Contributed by RP, 24-Dec-2019.) |
⊢ (𝜑 → (𝑅 ∘ 𝑅) ⊆ 𝑅) & ⊢ (𝜑 → 𝑆 ⊆ 𝑅) & ⊢ (𝜑 → 𝑇 ⊆ 𝑅) ⇒ ⊢ (𝜑 → (𝑆 ∘ 𝑇) ⊆ 𝑅) | ||
Theorem | xpcogend 13561 | The most interesting case of the composition of two cross products. (Contributed by RP, 24-Dec-2019.) |
⊢ (𝜑 → (𝐵 ∩ 𝐶) ≠ ∅) ⇒ ⊢ (𝜑 → ((𝐶 × 𝐷) ∘ (𝐴 × 𝐵)) = (𝐴 × 𝐷)) | ||
Theorem | xpcoidgend 13562 | If two classes are not disjoint, then the composition of their cross-product with itself is idempotent. (Contributed by RP, 24-Dec-2019.) |
⊢ (𝜑 → (𝐴 ∩ 𝐵) ≠ ∅) ⇒ ⊢ (𝜑 → ((𝐴 × 𝐵) ∘ (𝐴 × 𝐵)) = (𝐴 × 𝐵)) | ||
Theorem | cotr2g 13563* | Two ways of saying that the composition of two relations is included in a third relation. See its special instance cotr2 13564 for the main application. (Contributed by RP, 22-Mar-2020.) |
⊢ dom 𝐵 ⊆ 𝐷 & ⊢ (ran 𝐵 ∩ dom 𝐴) ⊆ 𝐸 & ⊢ ran 𝐴 ⊆ 𝐹 ⇒ ⊢ ((𝐴 ∘ 𝐵) ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐸 ∀𝑧 ∈ 𝐹 ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)) | ||
Theorem | cotr2 13564* | Two ways of saying a relation is transitive. Special instance of cotr2g 13563. (Contributed by RP, 22-Mar-2020.) |
⊢ dom 𝑅 ⊆ 𝐴 & ⊢ (dom 𝑅 ∩ ran 𝑅) ⊆ 𝐵 & ⊢ ran 𝑅 ⊆ 𝐶 ⇒ ⊢ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) | ||
Theorem | cotr3 13565* | Two ways of saying a relation is transitive. (Contributed by RP, 22-Mar-2020.) |
⊢ 𝐴 = dom 𝑅 & ⊢ 𝐵 = (𝐴 ∩ 𝐶) & ⊢ 𝐶 = ran 𝑅 ⇒ ⊢ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) | ||
Theorem | coemptyd 13566 | Deduction about composition of classes with no relational content in common. (Contributed by RP, 24-Dec-2019.) |
⊢ (𝜑 → (dom 𝐴 ∩ ran 𝐵) = ∅) ⇒ ⊢ (𝜑 → (𝐴 ∘ 𝐵) = ∅) | ||
Theorem | xptrrel 13567 | The cross product is always a transitive relation. (Contributed by RP, 24-Dec-2019.) |
⊢ ((𝐴 × 𝐵) ∘ (𝐴 × 𝐵)) ⊆ (𝐴 × 𝐵) | ||
Theorem | 0trrel 13568 | The empty class is a transitive relation. (Contributed by RP, 24-Dec-2019.) |
⊢ (∅ ∘ ∅) ⊆ ∅ | ||
Theorem | cleq1lem 13569 | Equality implies bijection. (Contributed by RP, 9-May-2020.) |
⊢ (𝐴 = 𝐵 → ((𝐴 ⊆ 𝐶 ∧ 𝜑) ↔ (𝐵 ⊆ 𝐶 ∧ 𝜑))) | ||
Theorem | cleq1 13570* | Equality of relations implies equality of closures. (Contributed by RP, 9-May-2020.) |
⊢ (𝑅 = 𝑆 → ∩ {𝑟 ∣ (𝑅 ⊆ 𝑟 ∧ 𝜑)} = ∩ {𝑟 ∣ (𝑆 ⊆ 𝑟 ∧ 𝜑)}) | ||
Theorem | clsslem 13571* | The closure of a subclass is a subclass of the closure. (Contributed by RP, 16-May-2020.) |
⊢ (𝑅 ⊆ 𝑆 → ∩ {𝑟 ∣ (𝑅 ⊆ 𝑟 ∧ 𝜑)} ⊆ ∩ {𝑟 ∣ (𝑆 ⊆ 𝑟 ∧ 𝜑)}) | ||
Syntax | ctcl 13572 | Extend class notation to include the transitive closure symbol. |
class t+ | ||
Syntax | crtcl 13573 | Extend class notation with reflexive-transitive closure. |
class t* | ||
Definition | df-trcl 13574* | Transitive closure of a relation. This is the smallest superset which has the transitive property. (Contributed by FL, 27-Jun-2011.) |
⊢ t+ = (𝑥 ∈ V ↦ ∩ {𝑧 ∣ (𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)}) | ||
Definition | df-rtrcl 13575* | Reflexive-transitive closure of a relation. This is the smallest superset which is reflexive property over all elements of its domain and range and has the transitive property. (Contributed by FL, 27-Jun-2011.) |
⊢ t* = (𝑥 ∈ V ↦ ∩ {𝑧 ∣ (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)}) | ||
Theorem | trcleq1 13576* | Equality of relations implies equality of transitive closures. (Contributed by RP, 9-May-2020.) |
⊢ (𝑅 = 𝑆 → ∩ {𝑟 ∣ (𝑅 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟)} = ∩ {𝑟 ∣ (𝑆 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟)}) | ||
Theorem | trclsslem 13577* | The transitive closure (as a relation) of a subclass is a subclass of the transitive closure. (Contributed by RP, 3-May-2020.) |
⊢ (𝑅 ⊆ 𝑆 → ∩ {𝑟 ∣ (𝑅 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟)} ⊆ ∩ {𝑟 ∣ (𝑆 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟)}) | ||
Theorem | trcleq2lem 13578 | Equality implies bijection. (Contributed by RP, 5-May-2020.) |
⊢ (𝐴 = 𝐵 → ((𝑅 ⊆ 𝐴 ∧ (𝐴 ∘ 𝐴) ⊆ 𝐴) ↔ (𝑅 ⊆ 𝐵 ∧ (𝐵 ∘ 𝐵) ⊆ 𝐵))) | ||
Theorem | cvbtrcl 13579* | Change of bound variable in class of all transitive relations which are supersets of a relation. (Contributed by RP, 5-May-2020.) |
⊢ {𝑥 ∣ (𝑅 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} = {𝑦 ∣ (𝑅 ⊆ 𝑦 ∧ (𝑦 ∘ 𝑦) ⊆ 𝑦)} | ||
Theorem | trcleq12lem 13580 | Equality implies bijection. (Contributed by RP, 9-May-2020.) |
⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵) → ((𝑅 ⊆ 𝐴 ∧ (𝐴 ∘ 𝐴) ⊆ 𝐴) ↔ (𝑆 ⊆ 𝐵 ∧ (𝐵 ∘ 𝐵) ⊆ 𝐵))) | ||
Theorem | trclexlem 13581 | Existence of relation implies existence of union with Cartesian product of domain and range. (Contributed by RP, 5-May-2020.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∈ V) | ||
Theorem | trclublem 13582* | If a relation exists then the class of transitive relations which are supersets of that relation is not empty. (Contributed by RP, 28-Apr-2020.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∪ (dom 𝑅 × ran 𝑅)) ∈ {𝑥 ∣ (𝑅 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)}) | ||
Theorem | trclubi 13583* | The Cartesian product of the domain and range of a relation is an upper bound for its transitive closure. (Contributed by RP, 2-Jan-2020.) (Revised by RP, 28-Apr-2020.) (Revised by AV, 26-Mar-2021.) |
⊢ Rel 𝑅 & ⊢ 𝑅 ∈ V ⇒ ⊢ ∩ {𝑠 ∣ (𝑅 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠)} ⊆ (dom 𝑅 × ran 𝑅) | ||
Theorem | trclubiOLD 13584* | Obsolete version of trclubi 13583 as of 26-Mar-2021. (Contributed by RP, 2-Jan-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Rel 𝑅 & ⊢ 𝑅 ∈ 𝑉 ⇒ ⊢ ∩ {𝑠 ∣ (𝑅 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠)} ⊆ (dom 𝑅 × ran 𝑅) | ||
Theorem | trclubgi 13585* | The union with the Cartesian product of its domain and range is an upper bound for a set's transitive closure. (Contributed by RP, 3-Jan-2020.) (Revised by RP, 28-Apr-2020.) (Revised by AV, 26-Mar-2021.) |
⊢ 𝑅 ∈ V ⇒ ⊢ ∩ {𝑠 ∣ (𝑅 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠)} ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)) | ||
Theorem | trclubgiOLD 13586* | Obsolete version of trclubgi 13585 as of 26-Mar-2021. (Contributed by RP, 3-Jan-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝑅 ∈ 𝑉 ⇒ ⊢ ∩ {𝑠 ∣ (𝑅 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠)} ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)) | ||
Theorem | trclub 13587* | The Cartesian product of the domain and range of a relation is an upper bound for its transitive closure. (Contributed by RP, 17-May-2020.) |
⊢ ((𝑅 ∈ 𝑉 ∧ Rel 𝑅) → ∩ {𝑟 ∣ (𝑅 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟)} ⊆ (dom 𝑅 × ran 𝑅)) | ||
Theorem | trclubg 13588* | The union with the Cartesian product of its domain and range is an upper bound for a set's transitive closure (as a relation). (Contributed by RP, 17-May-2020.) |
⊢ (𝑅 ∈ 𝑉 → ∩ {𝑟 ∣ (𝑅 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟)} ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) | ||
Theorem | trclfv 13589* | The transitive closure of a relation. (Contributed by RP, 28-Apr-2020.) |
⊢ (𝑅 ∈ 𝑉 → (t+‘𝑅) = ∩ {𝑥 ∣ (𝑅 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)}) | ||
Theorem | brintclab 13590* | Two ways to express a binary relation which is the intersection of a class. (Contributed by RP, 4-Apr-2020.) |
⊢ (𝐴∩ {𝑥 ∣ 𝜑}𝐵 ↔ ∀𝑥(𝜑 → 〈𝐴, 𝐵〉 ∈ 𝑥)) | ||
Theorem | brtrclfv 13591* | Two ways of expressing the transitive closure of a binary relation. (Contributed by RP, 9-May-2020.) |
⊢ (𝑅 ∈ 𝑉 → (𝐴(t+‘𝑅)𝐵 ↔ ∀𝑟((𝑅 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟) → 𝐴𝑟𝐵))) | ||
Theorem | brcnvtrclfv 13592* | Two ways of expressing the transitive closure of the converse of a binary relation. (Contributed by RP, 9-May-2020.) |
⊢ ((𝑅 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴◡(t+‘𝑅)𝐵 ↔ ∀𝑟((𝑅 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟) → 𝐵𝑟𝐴))) | ||
Theorem | brtrclfvcnv 13593* | Two ways of expressing the transitive closure of the converse of a binary relation. (Contributed by RP, 10-May-2020.) |
⊢ (𝑅 ∈ 𝑉 → (𝐴(t+‘◡𝑅)𝐵 ↔ ∀𝑟((◡𝑅 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟) → 𝐴𝑟𝐵))) | ||
Theorem | brcnvtrclfvcnv 13594* | Two ways of expressing the transitive closure of the converse of the converse of a binary relation. (Contributed by RP, 10-May-2020.) |
⊢ ((𝑅 ∈ 𝑈 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴◡(t+‘◡𝑅)𝐵 ↔ ∀𝑟((◡𝑅 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟) → 𝐵𝑟𝐴))) | ||
Theorem | trclfvss 13595 | The transitive closure (as a relation) of a subclass is a subclass of the transitive closure. (Contributed by RP, 3-May-2020.) |
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝑅 ⊆ 𝑆) → (t+‘𝑅) ⊆ (t+‘𝑆)) | ||
Theorem | trclfvub 13596 | The transitive closure of a relation has an upper bound. (Contributed by RP, 28-Apr-2020.) |
⊢ (𝑅 ∈ 𝑉 → (t+‘𝑅) ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) | ||
Theorem | trclfvlb 13597 | The transitive closure of a relation has a lower bound. (Contributed by RP, 28-Apr-2020.) |
⊢ (𝑅 ∈ 𝑉 → 𝑅 ⊆ (t+‘𝑅)) | ||
Theorem | trclfvcotr 13598 | The transitive closure of a relation is a transitive relation. (Contributed by RP, 29-Apr-2020.) |
⊢ (𝑅 ∈ 𝑉 → ((t+‘𝑅) ∘ (t+‘𝑅)) ⊆ (t+‘𝑅)) | ||
Theorem | trclfvlb2 13599 | The transitive closure of a relation has a lower bound. (Contributed by RP, 8-May-2020.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∘ 𝑅) ⊆ (t+‘𝑅)) | ||
Theorem | trclfvlb3 13600 | The transitive closure of a relation has a lower bound. (Contributed by RP, 8-May-2020.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ (t+‘𝑅)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |