Theorem fnmrc

Description: Moore-closure is a well-behaved function. (Contributed by Stefan O'Rear, 1-Feb-2015)

	Ref	Expression
Assertion	fnmrc	⊢ mrCls Fn ∪ ran Moore

Proof

Step	Hyp	Ref	Expression
1		df-mrc	⊢ mrCls = ( 𝑐 ∈ ∪ ran Moore ↦ ( 𝑥 ∈ 𝒫 ∪ 𝑐 ↦ ∩ { 𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠 } ) )
2	1	fnmpt	⊢ ( ∀ 𝑐 ∈ ∪ ran Moore ( 𝑥 ∈ 𝒫 ∪ 𝑐 ↦ ∩ { 𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠 } ) ∈ V → mrCls Fn ∪ ran Moore )
3		mreunirn	⊢ ( 𝑐 ∈ ∪ ran Moore ↔ 𝑐 ∈ ( Moore ‘ ∪ 𝑐 ) )
4		mrcflem	⊢ ( 𝑐 ∈ ( Moore ‘ ∪ 𝑐 ) → ( 𝑥 ∈ 𝒫 ∪ 𝑐 ↦ ∩ { 𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠 } ) : 𝒫 ∪ 𝑐 ⟶ 𝑐 )
5		fssxp	⊢ ( ( 𝑥 ∈ 𝒫 ∪ 𝑐 ↦ ∩ { 𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠 } ) : 𝒫 ∪ 𝑐 ⟶ 𝑐 → ( 𝑥 ∈ 𝒫 ∪ 𝑐 ↦ ∩ { 𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠 } ) ⊆ ( 𝒫 ∪ 𝑐 × 𝑐 ) )
6	4 5	syl	⊢ ( 𝑐 ∈ ( Moore ‘ ∪ 𝑐 ) → ( 𝑥 ∈ 𝒫 ∪ 𝑐 ↦ ∩ { 𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠 } ) ⊆ ( 𝒫 ∪ 𝑐 × 𝑐 ) )
7		vuniex	⊢ ∪ 𝑐 ∈ V
8	7	pwex	⊢ 𝒫 ∪ 𝑐 ∈ V
9		vex	⊢ 𝑐 ∈ V
10	8 9	xpex	⊢ ( 𝒫 ∪ 𝑐 × 𝑐 ) ∈ V
11		ssexg	⊢ ( ( ( 𝑥 ∈ 𝒫 ∪ 𝑐 ↦ ∩ { 𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠 } ) ⊆ ( 𝒫 ∪ 𝑐 × 𝑐 ) ∧ ( 𝒫 ∪ 𝑐 × 𝑐 ) ∈ V ) → ( 𝑥 ∈ 𝒫 ∪ 𝑐 ↦ ∩ { 𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠 } ) ∈ V )
12	6 10 11	sylancl	⊢ ( 𝑐 ∈ ( Moore ‘ ∪ 𝑐 ) → ( 𝑥 ∈ 𝒫 ∪ 𝑐 ↦ ∩ { 𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠 } ) ∈ V )
13	3 12	sylbi	⊢ ( 𝑐 ∈ ∪ ran Moore → ( 𝑥 ∈ 𝒫 ∪ 𝑐 ↦ ∩ { 𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠 } ) ∈ V )
14	2 13	mprg	⊢ mrCls Fn ∪ ran Moore