This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑆 ∈ V ↔ Word 𝑆 ∈ V )

Proof

Step Hyp Ref Expression
1 wrdexg ⊢ ( 𝑆 ∈ V → Word 𝑆 ∈ V )
2 opex ⊢ ⟨ 0 , 𝑠 ⟩ ∈ V
3 2 snid ⊢ ⟨ 0 , 𝑠 ⟩ ∈ { ⟨ 0 , 𝑠 ⟩ }
4 snopiswrd ⊢ ( 𝑠 ∈ 𝑆 → { ⟨ 0 , 𝑠 ⟩ } ∈ Word 𝑆 )
5 elunii ⊢ ( ( ⟨ 0 , 𝑠 ⟩ ∈ { ⟨ 0 , 𝑠 ⟩ } ∧ { ⟨ 0 , 𝑠 ⟩ } ∈ Word 𝑆 ) → ⟨ 0 , 𝑠 ⟩ ∈ ∪ Word 𝑆 )
6 3 4 5 sylancr ⊢ ( 𝑠 ∈ 𝑆 → ⟨ 0 , 𝑠 ⟩ ∈ ∪ Word 𝑆 )
7 c0ex ⊢ 0 ∈ V
8 vex ⊢ 𝑠 ∈ V
9 7 8 opeluu ⊢ ( ⟨ 0 , 𝑠 ⟩ ∈ ∪ Word 𝑆 → ( 0 ∈ ∪ ∪ ∪ Word 𝑆 ∧ 𝑠 ∈ ∪ ∪ ∪ Word 𝑆 ) )
10 6 9 syl ⊢ ( 𝑠 ∈ 𝑆 → ( 0 ∈ ∪ ∪ ∪ Word 𝑆 ∧ 𝑠 ∈ ∪ ∪ ∪ Word 𝑆 ) )
11 10 simprd ⊢ ( 𝑠 ∈ 𝑆 → 𝑠 ∈ ∪ ∪ ∪ Word 𝑆 )
12 11 ssriv ⊢ 𝑆 ⊆ ∪ ∪ ∪ Word 𝑆
13 uniexg ⊢ ( Word 𝑆 ∈ V → ∪ Word 𝑆 ∈ V )
14 uniexg ⊢ ( ∪ Word 𝑆 ∈ V → ∪ ∪ Word 𝑆 ∈ V )
15 uniexg ⊢ ( ∪ ∪ Word 𝑆 ∈ V → ∪ ∪ ∪ Word 𝑆 ∈ V )
16 13 14 15 3syl ⊢ ( Word 𝑆 ∈ V → ∪ ∪ ∪ Word 𝑆 ∈ V )
17 ssexg ⊢ ( ( 𝑆 ⊆ ∪ ∪ ∪ Word 𝑆 ∧ ∪ ∪ ∪ Word 𝑆 ∈ V ) → 𝑆 ∈ V )
18 12 16 17 sylancr ⊢ ( Word 𝑆 ∈ V → 𝑆 ∈ V )
19 1 18 impbii ⊢ ( 𝑆 ∈ V ↔ Word 𝑆 ∈ V )