rankse

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

		Ref	Expression
	Hypothesis	rankse.1	$⊢ S = \{⟨x, y⟩ \| (rank (x) \in rank (y) \lor (rank (x) = rank (y) \land φ))\}$
	Assertion	rankse	$⊢ S Se A$

Proof

Step	Hyp	Ref	Expression
1		rankse.1	$⊢ S = \{⟨x, y⟩ \| (rank (x) \in rank (y) \lor (rank (x) = rank (y) \land φ))\}$
2		rankon	$⊢ rank (y) \in On$
3		id	$⊢ rank (x) \subseteq rank (y) \to rank (x) \subseteq rank (y)$
4	3	rgenw	$⊢ \forall x \in A (rank (x) \subseteq rank (y) \to rank (x) \subseteq rank (y))$
5		fveq2	$⊢ v = x \to rank (v) = rank (x)$
6	5	sseq1d	$⊢ v = x \to (rank (v) \subseteq rank (y) \leftrightarrow rank (x) \subseteq rank (y))$
7	6	ralrab2	$⊢ \forall v \in \{x \in A \| rank (x) \subseteq rank (y)\} rank (v) \subseteq rank (y) \leftrightarrow \forall x \in A (rank (x) \subseteq rank (y) \to rank (x) \subseteq rank (y))$
8	4 7	mpbir	$⊢ \forall v \in \{x \in A \| rank (x) \subseteq rank (y)\} rank (v) \subseteq rank (y)$
9		sseq2	$⊢ u = rank (y) \to (rank (v) \subseteq u \leftrightarrow rank (v) \subseteq rank (y))$
10	9	ralbidv	$⊢ u = rank (y) \to (\forall v \in \{x \in A \| rank (x) \subseteq rank (y)\} rank (v) \subseteq u \leftrightarrow \forall v \in \{x \in A \| rank (x) \subseteq rank (y)\} rank (v) \subseteq rank (y))$
11	10	rspcev	$⊢ (rank (y) \in On \land \forall v \in \{x \in A \| rank (x) \subseteq rank (y)\} rank (v) \subseteq rank (y)) \to \exists u \in On \forall v \in \{x \in A \| rank (x) \subseteq rank (y)\} rank (v) \subseteq u$
12	2 8 11	mp2an	$⊢ \exists u \in On \forall v \in \{x \in A \| rank (x) \subseteq rank (y)\} rank (v) \subseteq u$
13		bndrank	$⊢ \exists u \in On \forall v \in \{x \in A \| rank (x) \subseteq rank (y)\} rank (v) \subseteq u \to \{x \in A \| rank (x) \subseteq rank (y)\} \in V$
14	12 13	ax-mp	$⊢ \{x \in A \| rank (x) \subseteq rank (y)\} \in V$
15		simpl	$⊢ (rank (x) = rank (y) \land φ) \to rank (x) = rank (y)$
16	15	orim2i	$⊢ (rank (x) \in rank (y) \lor (rank (x) = rank (y) \land φ)) \to (rank (x) \in rank (y) \lor rank (x) = rank (y))$
17	1	breqi	$⊢ x S y \leftrightarrow x \{⟨x, y⟩ \| (rank (x) \in rank (y) \lor (rank (x) = rank (y) \land φ))\} y$
18		df-br	$⊢ x \{⟨x, y⟩ \| (rank (x) \in rank (y) \lor (rank (x) = rank (y) \land φ))\} y \leftrightarrow ⟨x, y⟩ \in \{⟨x, y⟩ \| (rank (x) \in rank (y) \lor (rank (x) = rank (y) \land φ))\}$
19		opabidw	$⊢ ⟨x, y⟩ \in \{⟨x, y⟩ \| (rank (x) \in rank (y) \lor (rank (x) = rank (y) \land φ))\} \leftrightarrow (rank (x) \in rank (y) \lor (rank (x) = rank (y) \land φ))$
20	17 18 19	3bitri	$⊢ x S y \leftrightarrow (rank (x) \in rank (y) \lor (rank (x) = rank (y) \land φ))$
21		rankon	$⊢ rank (x) \in On$
22	21 2	onsseli	$⊢ rank (x) \subseteq rank (y) \leftrightarrow (rank (x) \in rank (y) \lor rank (x) = rank (y))$
23	16 20 22	3imtr4i	$⊢ x S y \to rank (x) \subseteq rank (y)$
24	23	a1i	$⊢ x \in A \to (x S y \to rank (x) \subseteq rank (y))$
25	24	ss2rabi	$⊢ \{x \in A \| x S y\} \subseteq \{x \in A \| rank (x) \subseteq rank (y)\}$
26	14 25	ssexi	$⊢ \{x \in A \| x S y\} \in V$
27	26	rgenw	$⊢ \forall y \in A \{x \in A \| x S y\} \in V$
28		nfcv	$⊢ \underline{Ⅎ} x A$
29		nfcv	$⊢ \underline{Ⅎ} z A$
30		nfv	$⊢ Ⅎ z x S w$
31		nfcv	$⊢ \underline{Ⅎ} x z$
32		nfopab1	$⊢ \underline{Ⅎ} x \{⟨x, y⟩ \| (rank (x) \in rank (y) \lor (rank (x) = rank (y) \land φ))\}$
33	1 32	nfcxfr	$⊢ \underline{Ⅎ} x S$
34		nfcv	$⊢ \underline{Ⅎ} x w$
35	31 33 34	nfbr	$⊢ Ⅎ x z S w$
36		breq1	$⊢ x = z \to (x S w \leftrightarrow z S w)$
37	28 29 30 35 36	cbvrabw	$⊢ \{x \in A \| x S w\} = \{z \in A \| z S w\}$
38	37	eleq1i	$⊢ \{x \in A \| x S w\} \in V \leftrightarrow \{z \in A \| z S w\} \in V$
39	38	ralbii	$⊢ \forall w \in A \{x \in A \| x S w\} \in V \leftrightarrow \forall w \in A \{z \in A \| z S w\} \in V$
40		nfv	$⊢ Ⅎ w \{x \in A \| x S y\} \in V$
41		nfcv	$⊢ \underline{Ⅎ} y x$
42		nfopab2	$⊢ \underline{Ⅎ} y \{⟨x, y⟩ \| (rank (x) \in rank (y) \lor (rank (x) = rank (y) \land φ))\}$
43	1 42	nfcxfr	$⊢ \underline{Ⅎ} y S$
44		nfcv	$⊢ \underline{Ⅎ} y w$
45	41 43 44	nfbr	$⊢ Ⅎ y x S w$
46		nfcv	$⊢ \underline{Ⅎ} y A$
47	45 46	nfrabw	$⊢ \underline{Ⅎ} y \{x \in A \| x S w\}$
48	47	nfel1	$⊢ Ⅎ y \{x \in A \| x S w\} \in V$
49		breq2	$⊢ y = w \to (x S y \leftrightarrow x S w)$
50	49	rabbidv	$⊢ y = w \to \{x \in A \| x S y\} = \{x \in A \| x S w\}$
51	50	eleq1d	$⊢ y = w \to (\{x \in A \| x S y\} \in V \leftrightarrow \{x \in A \| x S w\} \in V)$
52	40 48 51	cbvralw	$⊢ \forall y \in A \{x \in A \| x S y\} \in V \leftrightarrow \forall w \in A \{x \in A \| x S w\} \in V$
53		df-se	$⊢ S Se A \leftrightarrow \forall w \in A \{z \in A \| z S w\} \in V$
54	39 52 53	3bitr4ri	$⊢ S Se A \leftrightarrow \forall y \in A \{x \in A \| x S y\} \in V$
55	27 54	mpbir	$⊢ S Se A$

Metamath Proof Explorer

Theorem rankse

Proof