Theorem onprcr

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

	Ref	Expression
Hypotheses	onprcr.1	⊢ 𝐴 = { 𝑥 ∈ 𝑉 ∣ Ord 𝑥 }
	onprcr.2	⊢ Tr 𝐴
Assertion	onprcr	⊢ ¬ 𝐴 ∈ 𝑉

Proof

Step	Hyp	Ref	Expression
1		onprcr.1	⊢ 𝐴 = { 𝑥 ∈ 𝑉 ∣ Ord 𝑥 }
2		onprcr.2	⊢ Tr 𝐴
3		rabssab	⊢ { 𝑥 ∈ 𝑉 ∣ Ord 𝑥 } ⊆ { 𝑥 ∣ Ord 𝑥 }
4		df-on	⊢ On = { 𝑥 ∣ Ord 𝑥 }
5	3 1 4	3sstr4i	⊢ 𝐴 ⊆ On
6		epweon	⊢ E We On
7		wess	⊢ ( 𝐴 ⊆ On → ( E We On → E We 𝐴 ) )
8	5 6 7	mp2	⊢ E We 𝐴
9		df-ord	⊢ ( Ord 𝐴 ↔ ( Tr 𝐴 ∧ E We 𝐴 ) )
10	2 8 9	mpbir2an	⊢ Ord 𝐴
11		ordirr	⊢ ( Ord 𝐴 → ¬ 𝐴 ∈ 𝐴 )
12	10 11	ax-mp	⊢ ¬ 𝐴 ∈ 𝐴
13		ordeq	⊢ ( 𝑥 = 𝐴 → ( Ord 𝑥 ↔ Ord 𝐴 ) )
14	13	elrab3	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ { 𝑥 ∈ 𝑉 ∣ Ord 𝑥 } ↔ Ord 𝐴 ) )
15	10 14	mpbiri	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ { 𝑥 ∈ 𝑉 ∣ Ord 𝑥 } )
16	15 1	eleqtrrdi	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ 𝐴 )
17	12 16	mto	⊢ ¬ 𝐴 ∈ 𝑉