fliftcnv

Description: Converse of the relation F . (Contributed by Mario Carneiro, 23-Dec-2016)

	Ref	Expression
Hypotheses	flift.1	$⊢ F = ran (x \in X ⟼ ⟨A, B⟩)$
	flift.2	$⊢ (φ \land x \in X) \to A \in R$
	flift.3	$⊢ (φ \land x \in X) \to B \in S$
Assertion	fliftcnv	$⊢ φ \to F^{-1} = ran (x \in X ⟼ ⟨B, A⟩)$

Proof

Step	Hyp	Ref	Expression
1		flift.1	$⊢ F = ran (x \in X ⟼ ⟨A, B⟩)$
2		flift.2	$⊢ (φ \land x \in X) \to A \in R$
3		flift.3	$⊢ (φ \land x \in X) \to B \in S$
4		eqid	$⊢ ran (x \in X ⟼ ⟨B, A⟩) = ran (x \in X ⟼ ⟨B, A⟩)$
5	4 3 2	fliftrel	$⊢ φ \to ran (x \in X ⟼ ⟨B, A⟩) \subseteq S \times R$
6		relxp	$⊢ Rel (S \times R)$
7		relss	$⊢ ran (x \in X ⟼ ⟨B, A⟩) \subseteq S \times R \to (Rel (S \times R) \to Rel ran (x \in X ⟼ ⟨B, A⟩))$
8	5 6 7	mpisyl	$⊢ φ \to Rel ran (x \in X ⟼ ⟨B, A⟩)$
9		relcnv	$⊢ Rel F^{-1}$
10	8 9	jctil	$⊢ φ \to (Rel F^{-1} \land Rel ran (x \in X ⟼ ⟨B, A⟩))$
11	1 2 3	fliftel	$⊢ φ \to (z F y \leftrightarrow \exists x \in X (z = A \land y = B))$
12		vex	$⊢ y \in V$
13		vex	$⊢ z \in V$
14	12 13	brcnv	$⊢ y F^{-1} z \leftrightarrow z F y$
15		ancom	$⊢ (y = B \land z = A) \leftrightarrow (z = A \land y = B)$
16	15	rexbii	$⊢ \exists x \in X (y = B \land z = A) \leftrightarrow \exists x \in X (z = A \land y = B)$
17	11 14 16	3bitr4g	$⊢ φ \to (y F^{-1} z \leftrightarrow \exists x \in X (y = B \land z = A))$
18	4 3 2	fliftel	$⊢ φ \to (y ran (x \in X ⟼ ⟨B, A⟩) z \leftrightarrow \exists x \in X (y = B \land z = A))$
19	17 18	bitr4d	$⊢ φ \to (y F^{-1} z \leftrightarrow y ran (x \in X ⟼ ⟨B, A⟩) z)$
20		df-br	$⊢ y F^{-1} z \leftrightarrow ⟨y, z⟩ \in F^{-1}$
21		df-br	$⊢ y ran (x \in X ⟼ ⟨B, A⟩) z \leftrightarrow ⟨y, z⟩ \in ran (x \in X ⟼ ⟨B, A⟩)$
22	19 20 21	3bitr3g	$⊢ φ \to (⟨y, z⟩ \in F^{-1} \leftrightarrow ⟨y, z⟩ \in ran (x \in X ⟼ ⟨B, A⟩))$
23	22	eqrelrdv2	$⊢ ((Rel F^{-1} \land Rel ran (x \in X ⟼ ⟨B, A⟩)) \land φ) \to F^{-1} = ran (x \in X ⟼ ⟨B, A⟩)$
24	10 23	mpancom	$⊢ φ \to F^{-1} = ran (x \in X ⟼ ⟨B, A⟩)$

Metamath Proof Explorer

Theorem fliftcnv

Proof