Metamath Proof Explorer

Theorem wrdexb

Description: The set of words over a set is a set, bidirectional version. (Contributed by Mario Carneiro, 26-Feb-2016) (Proof shortened by AV, 23-Nov-2018)

Ref Expression
Assertion wrdexb ⊢ S ∈ V ↔ Word S ∈ V

Proof

Step Hyp Ref Expression
1 wrdexg ⊢ S ∈ V → Word S ∈ V
2 opex ⊢ 0 s ∈ V
3 2 snid ⊢ 0 s ∈ 0 s
4 snopiswrd ⊢ s ∈ S → 0 s ∈ Word S
5 elunii ⊢ 0 s ∈ 0 s ∧ 0 s ∈ Word S → 0 s ∈ ⋃ Word S
6 3 4 5 sylancr ⊢ s ∈ S → 0 s ∈ ⋃ Word S
7 c0ex ⊢ 0 ∈ V
8 vex ⊢ s ∈ V
9 7 8 opeluu ⊢ 0 s ∈ ⋃ Word S → 0 ∈ ⋃ ⋃ ⋃ Word S ∧ s ∈ ⋃ ⋃ ⋃ Word S
10 6 9 syl ⊢ s ∈ S → 0 ∈ ⋃ ⋃ ⋃ Word S ∧ s ∈ ⋃ ⋃ ⋃ Word S
11 10 simprd ⊢ s ∈ S → s ∈ ⋃ ⋃ ⋃ Word S
12 11 ssriv ⊢ S ⊆ ⋃ ⋃ ⋃ Word S
13 uniexg ⊢ Word S ∈ V → ⋃ Word S ∈ V
14 uniexg ⊢ ⋃ Word S ∈ V → ⋃ ⋃ Word S ∈ V
15 uniexg ⊢ ⋃ ⋃ Word S ∈ V → ⋃ ⋃ ⋃ Word S ∈ V
16 13 14 15 3syl ⊢ Word S ∈ V → ⋃ ⋃ ⋃ Word S ∈ V
17 ssexg ⊢ S ⊆ ⋃ ⋃ ⋃ Word S ∧ ⋃ ⋃ ⋃ Word S ∈ V → S ∈ V
18 12 16 17 sylancr ⊢ Word S ∈ V → S ∈ V
19 1 18 impbii ⊢ S ∈ V ↔ Word S ∈ V