brfvrcld2

Description: If two elements are connected by the reflexive closure of a relation, then they are equal or related by relation. (Contributed by RP, 21-Jul-2020)

		Ref	Expression
	Hypothesis	brfvrcld2.r	$⊢ φ \to R \in V$
	Assertion	brfvrcld2	$⊢ φ \to (A r* (R) B \leftrightarrow ((A \in (dom R \cup ran R) \land B \in (dom R \cup ran R) \land A = B) \lor A R B))$

Proof

Step	Hyp	Ref	Expression
1		brfvrcld2.r	$⊢ φ \to R \in V$
2	1	brfvrcld	$⊢ φ \to (A r* (R) B \leftrightarrow (A (R ↑_{r} 0) B \lor A (R ↑_{r} 1) B))$
3		relexp0g	$⊢ R \in V \to R ↑_{r} 0 = {I ↾}_{(dom R \cup ran R)}$
4	1 3	syl	$⊢ φ \to R ↑_{r} 0 = {I ↾}_{(dom R \cup ran R)}$
5	4	breqd	$⊢ φ \to (A (R ↑_{r} 0) B \leftrightarrow A ({I ↾}_{(dom R \cup ran R)}) B)$
6		relres	$⊢ Rel ({I ↾}_{(dom R \cup ran R)})$
7	6	releldmi	$⊢ A ({I ↾}_{(dom R \cup ran R)}) B \to A \in dom ({I ↾}_{(dom R \cup ran R)})$
8	6	relelrni	$⊢ A ({I ↾}_{(dom R \cup ran R)}) B \to B \in ran ({I ↾}_{(dom R \cup ran R)})$
9		dmresi	$⊢ dom ({I ↾}_{(dom R \cup ran R)}) = dom R \cup ran R$
10	9	eleq2i	$⊢ A \in dom ({I ↾}_{(dom R \cup ran R)}) \leftrightarrow A \in (dom R \cup ran R)$
11	10	biimpi	$⊢ A \in dom ({I ↾}_{(dom R \cup ran R)}) \to A \in (dom R \cup ran R)$
12		rnresi	$⊢ ran ({I ↾}_{(dom R \cup ran R)}) = dom R \cup ran R$
13	12	eleq2i	$⊢ B \in ran ({I ↾}_{(dom R \cup ran R)}) \leftrightarrow B \in (dom R \cup ran R)$
14	13	biimpi	$⊢ B \in ran ({I ↾}_{(dom R \cup ran R)}) \to B \in (dom R \cup ran R)$
15	11 14	anim12i	$⊢ (A \in dom ({I ↾}_{(dom R \cup ran R)}) \land B \in ran ({I ↾}_{(dom R \cup ran R)})) \to (A \in (dom R \cup ran R) \land B \in (dom R \cup ran R))$
16	7 8 15	syl2anc	$⊢ A ({I ↾}_{(dom R \cup ran R)}) B \to (A \in (dom R \cup ran R) \land B \in (dom R \cup ran R))$
17		resieq	$⊢ (A \in (dom R \cup ran R) \land B \in (dom R \cup ran R)) \to (A ({I ↾}_{(dom R \cup ran R)}) B \leftrightarrow A = B)$
18	16 17	biadanii	$⊢ A ({I ↾}_{(dom R \cup ran R)}) B \leftrightarrow ((A \in (dom R \cup ran R) \land B \in (dom R \cup ran R)) \land A = B)$
19		df-3an	$⊢ (A \in (dom R \cup ran R) \land B \in (dom R \cup ran R) \land A = B) \leftrightarrow ((A \in (dom R \cup ran R) \land B \in (dom R \cup ran R)) \land A = B)$
20	18 19	bitr4i	$⊢ A ({I ↾}_{(dom R \cup ran R)}) B \leftrightarrow (A \in (dom R \cup ran R) \land B \in (dom R \cup ran R) \land A = B)$
21	5 20	bitrdi	$⊢ φ \to (A (R ↑_{r} 0) B \leftrightarrow (A \in (dom R \cup ran R) \land B \in (dom R \cup ran R) \land A = B))$
22	1	relexp1d	$⊢ φ \to R ↑_{r} 1 = R$
23	22	breqd	$⊢ φ \to (A (R ↑_{r} 1) B \leftrightarrow A R B)$
24	21 23	orbi12d	$⊢ φ \to ((A (R ↑_{r} 0) B \lor A (R ↑_{r} 1) B) \leftrightarrow ((A \in (dom R \cup ran R) \land B \in (dom R \cup ran R) \land A = B) \lor A R B))$
25	2 24	bitrd	$⊢ φ \to (A r* (R) B \leftrightarrow ((A \in (dom R \cup ran R) \land B \in (dom R \cup ran R) \land A = B) \lor A R B))$

Metamath Proof Explorer

Theorem brfvrcld2

Proof