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 )