Metamath Proof Explorer

Theorem wrddun2

Description: Superadditivity of word constructor. Class of words over union alphabet includes all words over either alphabet in the union; if B and C are non-empty and different, then this subclass relation is strict because of the words which have symbols both from B and from C . (Contributed by Ender Ting, 24-Jul-2026)

Ref Expression
Assertion wrddun2 ⊢ Word B ∪ Word C ⊆ Word B ∪ C

Proof

Step Hyp Ref Expression
1 elun ⊢ n ∈ Word B ∪ Word C ↔ n ∈ Word B ∨ n ∈ Word C
2 wrddun ⊢ n ∈ Word B ∨ n ∈ Word C → n ∈ Word B ∪ C
3 1 2 sylbi ⊢ n ∈ Word B ∪ Word C → n ∈ Word B ∪ C
4 3 ssriv ⊢ Word B ∪ Word C ⊆ Word B ∪ C