brub

Description: Binary relation form of the upper bound functor. (Contributed by Scott Fenton, 3-May-2018)

	Ref	Expression
Hypotheses	brub.1	$⊢ S \in V$
	brub.2	$⊢ A \in V$
Assertion	brub	$⊢ S UB R A \leftrightarrow \forall x \in S x R A$

Step	Hyp	Ref	Expression
1		brub.1	$⊢ S \in V$
2		brub.2	$⊢ A \in V$
3		brxp	$⊢ S (V \times V) A \leftrightarrow (S \in V \land A \in V)$
4	1 2 3	mpbir2an	$⊢ S (V \times V) A$
5		brdif	$⊢ S ((V \times V) ∖ ((V ∖ R) \circ E^{-1})) A \leftrightarrow (S (V \times V) A \land \neg S ((V ∖ R) \circ E^{-1}) A)$
6	4 5	mpbiran	$⊢ S ((V \times V) ∖ ((V ∖ R) \circ E^{-1})) A \leftrightarrow \neg S ((V ∖ R) \circ E^{-1}) A$
7	1 2	coepr	$⊢ S ((V ∖ R) \circ E^{-1}) A \leftrightarrow \exists x \in S x (V ∖ R) A$
8	6 7	xchbinx	$⊢ S ((V \times V) ∖ ((V ∖ R) \circ E^{-1})) A \leftrightarrow \neg \exists x \in S x (V ∖ R) A$
9		df-ub	$⊢ UB R = (V \times V) ∖ ((V ∖ R) \circ E^{-1})$
10	9	breqi	$⊢ S UB R A \leftrightarrow S ((V \times V) ∖ ((V ∖ R) \circ E^{-1})) A$
11		brv	$⊢ x V A$
12		brdif	$⊢ x (V ∖ R) A \leftrightarrow (x V A \land \neg x R A)$
13	11 12	mpbiran	$⊢ x (V ∖ R) A \leftrightarrow \neg x R A$
14	13	rexbii	$⊢ \exists x \in S x (V ∖ R) A \leftrightarrow \exists x \in S \neg x R A$
15		rexnal	$⊢ \exists x \in S \neg x R A \leftrightarrow \neg \forall x \in S x R A$
16	14 15	bitri	$⊢ \exists x \in S x (V ∖ R) A \leftrightarrow \neg \forall x \in S x R A$
17	16	con2bii	$⊢ \forall x \in S x R A \leftrightarrow \neg \exists x \in S x (V ∖ R) A$
18	8 10 17	3bitr4i	$⊢ S UB R A \leftrightarrow \forall x \in S x R A$

Metamath Proof Explorer