Theorem mnuund

Description: Minimal universes are closed under binary unions. (Contributed by Rohan Ridenour, 13-Aug-2023)

	Ref	Expression
Hypotheses	mnuund.1	|- M = { k | A. l e. k ( ~P l C_ k /\ A. m E. n e. k ( ~P l C_ n /\ A. p e. l ( E. q e. k ( p e. q /\ q e. m ) -> E. r e. m ( p e. r /\ U. r C_ n ) ) ) ) }
	mnuund.2	|- ( ph -> U e. M )
	mnuund.3	|- ( ph -> A e. U )
	mnuund.4	|- ( ph -> B e. U )
Assertion	mnuund	|- ( ph -> ( A u. B ) e. U )

Proof

Step	Hyp	Ref	Expression
1		mnuund.1	|- M = { k | A. l e. k ( ~P l C_ k /\ A. m E. n e. k ( ~P l C_ n /\ A. p e. l ( E. q e. k ( p e. q /\ q e. m ) -> E. r e. m ( p e. r /\ U. r C_ n ) ) ) ) }
2		mnuund.2	|- ( ph -> U e. M )
3		mnuund.3	|- ( ph -> A e. U )
4		mnuund.4	|- ( ph -> B e. U )
5		uniprg	|- ( ( A e. U /\ B e. U ) -> U. { A , B } = ( A u. B ) )
6	3 4 5	syl2anc	|- ( ph -> U. { A , B } = ( A u. B ) )
7	1 2 3 4	mnuprd	|- ( ph -> { A , B } e. U )
8	1 2 7	mnuunid	|- ( ph -> U. { A , B } e. U )
9	6 8	eqeltrrd	|- ( ph -> ( A u. B ) e. U )