tposf12

Description: Condition for an injective transposition. (Contributed by NM, 10-Sep-2015)

		Ref	Expression
	Assertion	tposf12	$⊢ Rel A \to (F : A \underset{1-1}{⟶} B \to tpos F : A^{-1} \underset{1-1}{⟶} B)$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (Rel A \land F : A \underset{1-1}{⟶} B) \to F : A \underset{1-1}{⟶} B$
2		relcnv	$⊢ Rel A^{-1}$
3		cnvf1o	$⊢ Rel A^{-1} \to (x \in A^{-1} ⟼ ⋃ {\{x\}}^{-1}) : A^{-1} \underset{1-1 onto}{⟶} {A^{-1}}^{-1}$
4		f1of1	$⊢ (x \in A^{-1} ⟼ ⋃ {\{x\}}^{-1}) : A^{-1} \underset{1-1 onto}{⟶} {A^{-1}}^{-1} \to (x \in A^{-1} ⟼ ⋃ {\{x\}}^{-1}) : A^{-1} \underset{1-1}{⟶} {A^{-1}}^{-1}$
5	2 3 4	mp2b	$⊢ (x \in A^{-1} ⟼ ⋃ {\{x\}}^{-1}) : A^{-1} \underset{1-1}{⟶} {A^{-1}}^{-1}$
6		simpl	$⊢ (Rel A \land F : A \underset{1-1}{⟶} B) \to Rel A$
7		dfrel2	$⊢ Rel A \leftrightarrow {A^{-1}}^{-1} = A$
8	6 7	sylib	$⊢ (Rel A \land F : A \underset{1-1}{⟶} B) \to {A^{-1}}^{-1} = A$
9		f1eq3	$⊢ {A^{-1}}^{-1} = A \to ((x \in A^{-1} ⟼ ⋃ {\{x\}}^{-1}) : A^{-1} \underset{1-1}{⟶} {A^{-1}}^{-1} \leftrightarrow (x \in A^{-1} ⟼ ⋃ {\{x\}}^{-1}) : A^{-1} \underset{1-1}{⟶} A)$
10	8 9	syl	$⊢ (Rel A \land F : A \underset{1-1}{⟶} B) \to ((x \in A^{-1} ⟼ ⋃ {\{x\}}^{-1}) : A^{-1} \underset{1-1}{⟶} {A^{-1}}^{-1} \leftrightarrow (x \in A^{-1} ⟼ ⋃ {\{x\}}^{-1}) : A^{-1} \underset{1-1}{⟶} A)$
11	5 10	mpbii	$⊢ (Rel A \land F : A \underset{1-1}{⟶} B) \to (x \in A^{-1} ⟼ ⋃ {\{x\}}^{-1}) : A^{-1} \underset{1-1}{⟶} A$
12		f1dm	$⊢ F : A \underset{1-1}{⟶} B \to dom F = A$
13	1 12	syl	$⊢ (Rel A \land F : A \underset{1-1}{⟶} B) \to dom F = A$
14	13	cnveqd	$⊢ (Rel A \land F : A \underset{1-1}{⟶} B) \to {dom F}^{-1} = A^{-1}$
15		mpteq1	$⊢ {dom F}^{-1} = A^{-1} \to (x \in {dom F}^{-1} ⟼ ⋃ {\{x\}}^{-1}) = (x \in A^{-1} ⟼ ⋃ {\{x\}}^{-1})$
16		f1eq1	$⊢ (x \in {dom F}^{-1} ⟼ ⋃ {\{x\}}^{-1}) = (x \in A^{-1} ⟼ ⋃ {\{x\}}^{-1}) \to ((x \in {dom F}^{-1} ⟼ ⋃ {\{x\}}^{-1}) : A^{-1} \underset{1-1}{⟶} A \leftrightarrow (x \in A^{-1} ⟼ ⋃ {\{x\}}^{-1}) : A^{-1} \underset{1-1}{⟶} A)$
17	14 15 16	3syl	$⊢ (Rel A \land F : A \underset{1-1}{⟶} B) \to ((x \in {dom F}^{-1} ⟼ ⋃ {\{x\}}^{-1}) : A^{-1} \underset{1-1}{⟶} A \leftrightarrow (x \in A^{-1} ⟼ ⋃ {\{x\}}^{-1}) : A^{-1} \underset{1-1}{⟶} A)$
18	11 17	mpbird	$⊢ (Rel A \land F : A \underset{1-1}{⟶} B) \to (x \in {dom F}^{-1} ⟼ ⋃ {\{x\}}^{-1}) : A^{-1} \underset{1-1}{⟶} A$
19		f1co	$⊢ (F : A \underset{1-1}{⟶} B \land (x \in {dom F}^{-1} ⟼ ⋃ {\{x\}}^{-1}) : A^{-1} \underset{1-1}{⟶} A) \to (F \circ (x \in {dom F}^{-1} ⟼ ⋃ {\{x\}}^{-1})) : A^{-1} \underset{1-1}{⟶} B$
20	1 18 19	syl2anc	$⊢ (Rel A \land F : A \underset{1-1}{⟶} B) \to (F \circ (x \in {dom F}^{-1} ⟼ ⋃ {\{x\}}^{-1})) : A^{-1} \underset{1-1}{⟶} B$
21	12	releqd	$⊢ F : A \underset{1-1}{⟶} B \to (Rel dom F \leftrightarrow Rel A)$
22	21	biimparc	$⊢ (Rel A \land F : A \underset{1-1}{⟶} B) \to Rel dom F$
23		dftpos2	$⊢ Rel dom F \to tpos F = F \circ (x \in {dom F}^{-1} ⟼ ⋃ {\{x\}}^{-1})$
24		f1eq1	$⊢ tpos F = F \circ (x \in {dom F}^{-1} ⟼ ⋃ {\{x\}}^{-1}) \to (tpos F : A^{-1} \underset{1-1}{⟶} B \leftrightarrow (F \circ (x \in {dom F}^{-1} ⟼ ⋃ {\{x\}}^{-1})) : A^{-1} \underset{1-1}{⟶} B)$
25	22 23 24	3syl	$⊢ (Rel A \land F : A \underset{1-1}{⟶} B) \to (tpos F : A^{-1} \underset{1-1}{⟶} B \leftrightarrow (F \circ (x \in {dom F}^{-1} ⟼ ⋃ {\{x\}}^{-1})) : A^{-1} \underset{1-1}{⟶} B)$
26	20 25	mpbird	$⊢ (Rel A \land F : A \underset{1-1}{⟶} B) \to tpos F : A^{-1} \underset{1-1}{⟶} B$
27	26	ex	$⊢ Rel A \to (F : A \underset{1-1}{⟶} B \to tpos F : A^{-1} \underset{1-1}{⟶} B)$

Metamath Proof Explorer

Theorem tposf12

Proof