fcoinvbr

Description: Binary relation for the equivalence relation from fcoinver . (Contributed by Thierry Arnoux, 3-Jan-2020)

		Ref	Expression
	Hypothesis	fcoinvbr.e	$⊢ \underset{˙}{\sim} = F^{-1} \circ F$
	Assertion	fcoinvbr	$⊢ (F Fn A \land X \in A \land Y \in A) \to (X \underset{˙}{\sim} Y \leftrightarrow F (X) = F (Y))$

Proof

Step	Hyp	Ref	Expression
1		fcoinvbr.e	$⊢ \underset{˙}{\sim} = F^{-1} \circ F$
2	1	breqi	$⊢ X \underset{˙}{\sim} Y \leftrightarrow X (F^{-1} \circ F) Y$
3		brcog	$⊢ (X \in A \land Y \in A) \to (X (F^{-1} \circ F) Y \leftrightarrow \exists z (X F z \land z F^{-1} Y))$
4	2 3	bitrid	$⊢ (X \in A \land Y \in A) \to (X \underset{˙}{\sim} Y \leftrightarrow \exists z (X F z \land z F^{-1} Y))$
5	4	3adant1	$⊢ (F Fn A \land X \in A \land Y \in A) \to (X \underset{˙}{\sim} Y \leftrightarrow \exists z (X F z \land z F^{-1} Y))$
6		fvex	$⊢ F (X) \in V$
7	6	eqvinc	$⊢ F (X) = F (Y) \leftrightarrow \exists z (z = F (X) \land z = F (Y))$
8		eqcom	$⊢ z = F (X) \leftrightarrow F (X) = z$
9		eqcom	$⊢ z = F (Y) \leftrightarrow F (Y) = z$
10	8 9	anbi12i	$⊢ (z = F (X) \land z = F (Y)) \leftrightarrow (F (X) = z \land F (Y) = z)$
11	10	exbii	$⊢ \exists z (z = F (X) \land z = F (Y)) \leftrightarrow \exists z (F (X) = z \land F (Y) = z)$
12	7 11	bitri	$⊢ F (X) = F (Y) \leftrightarrow \exists z (F (X) = z \land F (Y) = z)$
13		fnbrfvb	$⊢ (F Fn A \land X \in A) \to (F (X) = z \leftrightarrow X F z)$
14	13	3adant3	$⊢ (F Fn A \land X \in A \land Y \in A) \to (F (X) = z \leftrightarrow X F z)$
15		fnbrfvb	$⊢ (F Fn A \land Y \in A) \to (F (Y) = z \leftrightarrow Y F z)$
16	15	3adant2	$⊢ (F Fn A \land X \in A \land Y \in A) \to (F (Y) = z \leftrightarrow Y F z)$
17	14 16	anbi12d	$⊢ (F Fn A \land X \in A \land Y \in A) \to ((F (X) = z \land F (Y) = z) \leftrightarrow (X F z \land Y F z))$
18		vex	$⊢ z \in V$
19		brcnvg	$⊢ (z \in V \land Y \in A) \to (z F^{-1} Y \leftrightarrow Y F z)$
20	18 19	mpan	$⊢ Y \in A \to (z F^{-1} Y \leftrightarrow Y F z)$
21	20	3ad2ant3	$⊢ (F Fn A \land X \in A \land Y \in A) \to (z F^{-1} Y \leftrightarrow Y F z)$
22	21	anbi2d	$⊢ (F Fn A \land X \in A \land Y \in A) \to ((X F z \land z F^{-1} Y) \leftrightarrow (X F z \land Y F z))$
23	17 22	bitr4d	$⊢ (F Fn A \land X \in A \land Y \in A) \to ((F (X) = z \land F (Y) = z) \leftrightarrow (X F z \land z F^{-1} Y))$
24	23	exbidv	$⊢ (F Fn A \land X \in A \land Y \in A) \to (\exists z (F (X) = z \land F (Y) = z) \leftrightarrow \exists z (X F z \land z F^{-1} Y))$
25	12 24	bitrid	$⊢ (F Fn A \land X \in A \land Y \in A) \to (F (X) = F (Y) \leftrightarrow \exists z (X F z \land z F^{-1} Y))$
26	5 25	bitr4d	$⊢ (F Fn A \land X \in A \land Y \in A) \to (X \underset{˙}{\sim} Y \leftrightarrow F (X) = F (Y))$

Metamath Proof Explorer

Theorem fcoinvbr

Proof