Theorem rankse

Description: Construct a relation that is set-like on any class. (Contributed by BTernaryTau, 18-Sep-2026)

	Ref	Expression
Hypothesis	rankse.1	⊢ 𝑆 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( rank ‘ 𝑥 ) ∈ ( rank ‘ 𝑦 ) ∨ ( ( rank ‘ 𝑥 ) = ( rank ‘ 𝑦 ) ∧ 𝜑 ) ) }
Assertion	rankse	⊢ 𝑆 Se 𝐴

Proof

Step	Hyp	Ref	Expression
1		rankse.1	⊢ 𝑆 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( rank ‘ 𝑥 ) ∈ ( rank ‘ 𝑦 ) ∨ ( ( rank ‘ 𝑥 ) = ( rank ‘ 𝑦 ) ∧ 𝜑 ) ) }
2		rankon	⊢ ( rank ‘ 𝑦 ) ∈ On
3		id	⊢ ( ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) )
4	3	rgenw	⊢ ∀ 𝑥 ∈ 𝐴 ( ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) )
5		fveq2	⊢ ( 𝑣 = 𝑥 → ( rank ‘ 𝑣 ) = ( rank ‘ 𝑥 ) )
6	5	sseq1d	⊢ ( 𝑣 = 𝑥 → ( ( rank ‘ 𝑣 ) ⊆ ( rank ‘ 𝑦 ) ↔ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) )
7	6	ralrab2	⊢ ( ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ( rank ‘ 𝑣 ) ⊆ ( rank ‘ 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐴 ( ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) )
8	4 7	mpbir	⊢ ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ( rank ‘ 𝑣 ) ⊆ ( rank ‘ 𝑦 )
9		sseq2	⊢ ( 𝑢 = ( rank ‘ 𝑦 ) → ( ( rank ‘ 𝑣 ) ⊆ 𝑢 ↔ ( rank ‘ 𝑣 ) ⊆ ( rank ‘ 𝑦 ) ) )
10	9	ralbidv	⊢ ( 𝑢 = ( rank ‘ 𝑦 ) → ( ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ( rank ‘ 𝑣 ) ⊆ 𝑢 ↔ ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ( rank ‘ 𝑣 ) ⊆ ( rank ‘ 𝑦 ) ) )
11	10	rspcev	⊢ ( ( ( rank ‘ 𝑦 ) ∈ On ∧ ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ( rank ‘ 𝑣 ) ⊆ ( rank ‘ 𝑦 ) ) → ∃ 𝑢 ∈ On ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ( rank ‘ 𝑣 ) ⊆ 𝑢 )
12	2 8 11	mp2an	⊢ ∃ 𝑢 ∈ On ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ( rank ‘ 𝑣 ) ⊆ 𝑢
13		bndrank	⊢ ( ∃ 𝑢 ∈ On ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ( rank ‘ 𝑣 ) ⊆ 𝑢 → { 𝑥 ∈ 𝐴 ∣ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ∈ V )
14	12 13	ax-mp	⊢ { 𝑥 ∈ 𝐴 ∣ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ∈ V
15		simpl	⊢ ( ( ( rank ‘ 𝑥 ) = ( rank ‘ 𝑦 ) ∧ 𝜑 ) → ( rank ‘ 𝑥 ) = ( rank ‘ 𝑦 ) )
16	15	orim2i	⊢ ( ( ( rank ‘ 𝑥 ) ∈ ( rank ‘ 𝑦 ) ∨ ( ( rank ‘ 𝑥 ) = ( rank ‘ 𝑦 ) ∧ 𝜑 ) ) → ( ( rank ‘ 𝑥 ) ∈ ( rank ‘ 𝑦 ) ∨ ( rank ‘ 𝑥 ) = ( rank ‘ 𝑦 ) ) )
17	1	breqi	⊢ ( 𝑥 𝑆 𝑦 ↔ 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( rank ‘ 𝑥 ) ∈ ( rank ‘ 𝑦 ) ∨ ( ( rank ‘ 𝑥 ) = ( rank ‘ 𝑦 ) ∧ 𝜑 ) ) } 𝑦 )
18		df-br	⊢ ( 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( rank ‘ 𝑥 ) ∈ ( rank ‘ 𝑦 ) ∨ ( ( rank ‘ 𝑥 ) = ( rank ‘ 𝑦 ) ∧ 𝜑 ) ) } 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( rank ‘ 𝑥 ) ∈ ( rank ‘ 𝑦 ) ∨ ( ( rank ‘ 𝑥 ) = ( rank ‘ 𝑦 ) ∧ 𝜑 ) ) } )
19		opabidw	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( rank ‘ 𝑥 ) ∈ ( rank ‘ 𝑦 ) ∨ ( ( rank ‘ 𝑥 ) = ( rank ‘ 𝑦 ) ∧ 𝜑 ) ) } ↔ ( ( rank ‘ 𝑥 ) ∈ ( rank ‘ 𝑦 ) ∨ ( ( rank ‘ 𝑥 ) = ( rank ‘ 𝑦 ) ∧ 𝜑 ) ) )
20	17 18 19	3bitri	⊢ ( 𝑥 𝑆 𝑦 ↔ ( ( rank ‘ 𝑥 ) ∈ ( rank ‘ 𝑦 ) ∨ ( ( rank ‘ 𝑥 ) = ( rank ‘ 𝑦 ) ∧ 𝜑 ) ) )
21		rankon	⊢ ( rank ‘ 𝑥 ) ∈ On
22	21 2	onsseli	⊢ ( ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ↔ ( ( rank ‘ 𝑥 ) ∈ ( rank ‘ 𝑦 ) ∨ ( rank ‘ 𝑥 ) = ( rank ‘ 𝑦 ) ) )
23	16 20 22	3imtr4i	⊢ ( 𝑥 𝑆 𝑦 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) )
24	23	a1i	⊢ ( 𝑥 ∈ 𝐴 → ( 𝑥 𝑆 𝑦 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) )
25	24	ss2rabi	⊢ { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑆 𝑦 } ⊆ { 𝑥 ∈ 𝐴 ∣ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) }
26	14 25	ssexi	⊢ { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑆 𝑦 } ∈ V
27	26	rgenw	⊢ ∀ 𝑦 ∈ 𝐴 { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑆 𝑦 } ∈ V
28		nfcv	⊢ Ⅎ 𝑥 𝐴
29		nfcv	⊢ Ⅎ 𝑧 𝐴
30		nfv	⊢ Ⅎ 𝑧 𝑥 𝑆 𝑤
31		nfcv	⊢ Ⅎ 𝑥 𝑧
32		nfopab1	⊢ Ⅎ 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( rank ‘ 𝑥 ) ∈ ( rank ‘ 𝑦 ) ∨ ( ( rank ‘ 𝑥 ) = ( rank ‘ 𝑦 ) ∧ 𝜑 ) ) }
33	1 32	nfcxfr	⊢ Ⅎ 𝑥 𝑆
34		nfcv	⊢ Ⅎ 𝑥 𝑤
35	31 33 34	nfbr	⊢ Ⅎ 𝑥 𝑧 𝑆 𝑤
36		breq1	⊢ ( 𝑥 = 𝑧 → ( 𝑥 𝑆 𝑤 ↔ 𝑧 𝑆 𝑤 ) )
37	28 29 30 35 36	cbvrabw	⊢ { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑆 𝑤 } = { 𝑧 ∈ 𝐴 ∣ 𝑧 𝑆 𝑤 }
38	37	eleq1i	⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑆 𝑤 } ∈ V ↔ { 𝑧 ∈ 𝐴 ∣ 𝑧 𝑆 𝑤 } ∈ V )
39	38	ralbii	⊢ ( ∀ 𝑤 ∈ 𝐴 { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑆 𝑤 } ∈ V ↔ ∀ 𝑤 ∈ 𝐴 { 𝑧 ∈ 𝐴 ∣ 𝑧 𝑆 𝑤 } ∈ V )
40		nfv	⊢ Ⅎ 𝑤 { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑆 𝑦 } ∈ V
41		nfcv	⊢ Ⅎ 𝑦 𝑥
42		nfopab2	⊢ Ⅎ 𝑦 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( rank ‘ 𝑥 ) ∈ ( rank ‘ 𝑦 ) ∨ ( ( rank ‘ 𝑥 ) = ( rank ‘ 𝑦 ) ∧ 𝜑 ) ) }
43	1 42	nfcxfr	⊢ Ⅎ 𝑦 𝑆
44		nfcv	⊢ Ⅎ 𝑦 𝑤
45	41 43 44	nfbr	⊢ Ⅎ 𝑦 𝑥 𝑆 𝑤
46		nfcv	⊢ Ⅎ 𝑦 𝐴
47	45 46	nfrabw	⊢ Ⅎ 𝑦 { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑆 𝑤 }
48	47	nfel1	⊢ Ⅎ 𝑦 { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑆 𝑤 } ∈ V
49		breq2	⊢ ( 𝑦 = 𝑤 → ( 𝑥 𝑆 𝑦 ↔ 𝑥 𝑆 𝑤 ) )
50	49	rabbidv	⊢ ( 𝑦 = 𝑤 → { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑆 𝑦 } = { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑆 𝑤 } )
51	50	eleq1d	⊢ ( 𝑦 = 𝑤 → ( { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑆 𝑦 } ∈ V ↔ { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑆 𝑤 } ∈ V ) )
52	40 48 51	cbvralw	⊢ ( ∀ 𝑦 ∈ 𝐴 { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑆 𝑦 } ∈ V ↔ ∀ 𝑤 ∈ 𝐴 { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑆 𝑤 } ∈ V )
53		df-se	⊢ ( 𝑆 Se 𝐴 ↔ ∀ 𝑤 ∈ 𝐴 { 𝑧 ∈ 𝐴 ∣ 𝑧 𝑆 𝑤 } ∈ V )
54	39 52 53	3bitr4ri	⊢ ( 𝑆 Se 𝐴 ↔ ∀ 𝑦 ∈ 𝐴 { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑆 𝑦 } ∈ V )
55	27 54	mpbir	⊢ 𝑆 Se 𝐴