Theorem onprcr

Description: Relative version of onprc . (Contributed by Adrian Ducourtial, 15-Oct-2026)

	Ref	Expression
Hypotheses	onprcr.1	|- A = { x e. V | Ord x }
	onprcr.2	|- Tr A
Assertion	onprcr	|- -. A e. V

Proof

Step	Hyp	Ref	Expression
1		onprcr.1	|- A = { x e. V | Ord x }
2		onprcr.2	|- Tr A
3		rabssab	|- { x e. V | Ord x } C_ { x | Ord x }
4		df-on	|- On = { x | Ord x }
5	3 1 4	3sstr4i	|- A C_ On
6		epweon	|- _E We On
7		wess	|- ( A C_ On -> ( _E We On -> _E We A ) )
8	5 6 7	mp2	|- _E We A
9		df-ord	|- ( Ord A <-> ( Tr A /\ _E We A ) )
10	2 8 9	mpbir2an	|- Ord A
11		ordirr	|- ( Ord A -> -. A e. A )
12	10 11	ax-mp	|- -. A e. A
13		ordeq	|- ( x = A -> ( Ord x <-> Ord A ) )
14	13	elrab3	|- ( A e. V -> ( A e. { x e. V | Ord x } <-> Ord A ) )
15	10 14	mpbiri	|- ( A e. V -> A e. { x e. V | Ord x } )
16	15 1	eleqtrrdi	|- ( A e. V -> A e. A )
17	12 16	mto	|- -. A e. V