Theorem mreunirn

Description: Two ways to express the notion of being a Moore collection on an unspecified base. (Contributed by Stefan O'Rear, 30-Jan-2015)

	Ref	Expression
Assertion	mreunirn	⊢ ( 𝐶 ∈ ∪ ran Moore ↔ 𝐶 ∈ ( Moore ‘ ∪ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		fnmre	⊢ Moore Fn V
2		fnunirn	⊢ ( Moore Fn V → ( 𝐶 ∈ ∪ ran Moore ↔ ∃ 𝑥 ∈ V 𝐶 ∈ ( Moore ‘ 𝑥 ) ) )
3	1 2	ax-mp	⊢ ( 𝐶 ∈ ∪ ran Moore ↔ ∃ 𝑥 ∈ V 𝐶 ∈ ( Moore ‘ 𝑥 ) )
4		mreuni	⊢ ( 𝐶 ∈ ( Moore ‘ 𝑥 ) → ∪ 𝐶 = 𝑥 )
5	4	fveq2d	⊢ ( 𝐶 ∈ ( Moore ‘ 𝑥 ) → ( Moore ‘ ∪ 𝐶 ) = ( Moore ‘ 𝑥 ) )
6	5	eleq2d	⊢ ( 𝐶 ∈ ( Moore ‘ 𝑥 ) → ( 𝐶 ∈ ( Moore ‘ ∪ 𝐶 ) ↔ 𝐶 ∈ ( Moore ‘ 𝑥 ) ) )
7	6	ibir	⊢ ( 𝐶 ∈ ( Moore ‘ 𝑥 ) → 𝐶 ∈ ( Moore ‘ ∪ 𝐶 ) )
8	7	rexlimivw	⊢ ( ∃ 𝑥 ∈ V 𝐶 ∈ ( Moore ‘ 𝑥 ) → 𝐶 ∈ ( Moore ‘ ∪ 𝐶 ) )
9	3 8	sylbi	⊢ ( 𝐶 ∈ ∪ ran Moore → 𝐶 ∈ ( Moore ‘ ∪ 𝐶 ) )
10		fvssunirn	⊢ ( Moore ‘ ∪ 𝐶 ) ⊆ ∪ ran Moore
11	10	sseli	⊢ ( 𝐶 ∈ ( Moore ‘ ∪ 𝐶 ) → 𝐶 ∈ ∪ ran Moore )
12	9 11	impbii	⊢ ( 𝐶 ∈ ∪ ran Moore ↔ 𝐶 ∈ ( Moore ‘ ∪ 𝐶 ) )