Theorem mnutrd

Description: Minimal universes are transitive. (Contributed by Rohan Ridenour, 13-Aug-2023)

	Ref	Expression
Hypotheses	mnutrd.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 ) ) ) ) }
	mnutrd.2	|- ( ph -> U e. M )
Assertion	mnutrd	|- ( ph -> Tr U )

Proof

Step	Hyp	Ref	Expression
1		mnutrd.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		mnutrd.2	|- ( ph -> U e. M )
3	2	adantr	|- ( ( ph /\ ( x e. y /\ y e. U ) ) -> U e. M )
4		simprr	|- ( ( ph /\ ( x e. y /\ y e. U ) ) -> y e. U )
5		simprl	|- ( ( ph /\ ( x e. y /\ y e. U ) ) -> x e. y )
6	1 3 4 5	mnutrcld	|- ( ( ph /\ ( x e. y /\ y e. U ) ) -> x e. U )
7	6	ex	|- ( ph -> ( ( x e. y /\ y e. U ) -> x e. U ) )
8	7	alrimivv	|- ( ph -> A. x A. y ( ( x e. y /\ y e. U ) -> x e. U ) )
9		dftr2	|- ( Tr U <-> A. x A. y ( ( x e. y /\ y e. U ) -> x e. U ) )
10	8 9	sylibr	|- ( ph -> Tr U )