Metamath Proof Explorer

Theorem wrddun

Description: Words in either of two alphabets are words in their union. (Contributed by Ender Ting, 24-Jul-2026)

Ref Expression
Assertion wrddun ⊢ A ∈ Word B ∨ A ∈ Word C → A ∈ Word B ∪ C

Proof

Step Hyp Ref Expression
1 ssun1 ⊢ B ⊆ B ∪ C
2 sswrd ⊢ B ⊆ B ∪ C → Word B ⊆ Word B ∪ C
3 1 2 ax-mp ⊢ Word B ⊆ Word B ∪ C
4 3 sseli ⊢ A ∈ Word B → A ∈ Word B ∪ C
5 ssun2 ⊢ C ⊆ B ∪ C
6 sswrd ⊢ C ⊆ B ∪ C → Word C ⊆ Word B ∪ C
7 5 6 ax-mp ⊢ Word C ⊆ Word B ∪ C
8 7 sseli ⊢ A ∈ Word C → A ∈ Word B ∪ C
9 4 8 jaoi ⊢ A ∈ Word B ∨ A ∈ Word C → A ∈ Word B ∪ C