catprsc2

Description: An alternate construction of the preorder induced by a category. See catprs2 for details. See also catprsc for a different construction. The two constructions are different because df-cat does not require the domain of H to be B X. B . (Contributed by Zhi Wang, 23-Sep-2024)

		Ref	Expression
	Hypothesis	catprsc2.1	$⊢ φ \to \underset{˙}{\leq} = \{⟨x, y⟩ \| x H y \neq \emptyset\}$
	Assertion	catprsc2	$⊢ φ \to \forall z \in B \forall w \in B (z \underset{˙}{\leq} w \leftrightarrow z H w \neq \emptyset)$

Proof

Step	Hyp	Ref	Expression
1		catprsc2.1	$⊢ φ \to \underset{˙}{\leq} = \{⟨x, y⟩ \| x H y \neq \emptyset\}$
2	1	breqd	$⊢ φ \to (z \underset{˙}{\leq} w \leftrightarrow z \{⟨x, y⟩ \| x H y \neq \emptyset\} w)$
3		vex	$⊢ z \in V$
4		vex	$⊢ w \in V$
5		oveq12	$⊢ (x = z \land y = w) \to x H y = z H w$
6	5	neeq1d	$⊢ (x = z \land y = w) \to (x H y \neq \emptyset \leftrightarrow z H w \neq \emptyset)$
7		eqid	$⊢ \{⟨x, y⟩ \| x H y \neq \emptyset\} = \{⟨x, y⟩ \| x H y \neq \emptyset\}$
8	3 4 6 7	braba	$⊢ z \{⟨x, y⟩ \| x H y \neq \emptyset\} w \leftrightarrow z H w \neq \emptyset$
9	2 8	bitrdi	$⊢ φ \to (z \underset{˙}{\leq} w \leftrightarrow z H w \neq \emptyset)$
10	9	adantr	$⊢ (φ \land (z \in B \land w \in B)) \to (z \underset{˙}{\leq} w \leftrightarrow z H w \neq \emptyset)$
11	10	ralrimivva	$⊢ φ \to \forall z \in B \forall w \in B (z \underset{˙}{\leq} w \leftrightarrow z H w \neq \emptyset)$

Metamath Proof Explorer

Theorem catprsc2

Proof