funen1cnv

Description: If a function is equinumerous to ordinal 1, then its converse is also a function. (Contributed by BTernaryTau, 8-Oct-2023)

		Ref	Expression
	Assertion	funen1cnv	$⊢ (Fun F \land F \approx 1_{𝑜}) \to Fun F^{-1}$

Proof

Step	Hyp	Ref	Expression
1		en1	$⊢ F \approx 1_{𝑜} \leftrightarrow \exists p F = \{p\}$
2		funrel	$⊢ Fun \{p\} \to Rel \{p\}$
3		vsnid	$⊢ p \in \{p\}$
4		elrel	$⊢ (Rel \{p\} \land p \in \{p\}) \to \exists x \exists y p = ⟨x, y⟩$
5	2 3 4	sylancl	$⊢ Fun \{p\} \to \exists x \exists y p = ⟨x, y⟩$
6		sneq	$⊢ p = ⟨x, y⟩ \to \{p\} = \{⟨x, y⟩\}$
7	6	2eximi	$⊢ \exists x \exists y p = ⟨x, y⟩ \to \exists x \exists y \{p\} = \{⟨x, y⟩\}$
8	5 7	syl	$⊢ Fun \{p\} \to \exists x \exists y \{p\} = \{⟨x, y⟩\}$
9		funcnvsn	$⊢ Fun {\{⟨x, y⟩\}}^{-1}$
10	9	gen2	$⊢ \forall x \forall y Fun {\{⟨x, y⟩\}}^{-1}$
11		19.29r2	$⊢ (\exists x \exists y \{p\} = \{⟨x, y⟩\} \land \forall x \forall y Fun {\{⟨x, y⟩\}}^{-1}) \to \exists x \exists y (\{p\} = \{⟨x, y⟩\} \land Fun {\{⟨x, y⟩\}}^{-1})$
12		cnveq	$⊢ \{p\} = \{⟨x, y⟩\} \to {\{p\}}^{-1} = {\{⟨x, y⟩\}}^{-1}$
13	12	funeqd	$⊢ \{p\} = \{⟨x, y⟩\} \to (Fun {\{p\}}^{-1} \leftrightarrow Fun {\{⟨x, y⟩\}}^{-1})$
14	13	biimpar	$⊢ (\{p\} = \{⟨x, y⟩\} \land Fun {\{⟨x, y⟩\}}^{-1}) \to Fun {\{p\}}^{-1}$
15	14	exlimivv	$⊢ \exists x \exists y (\{p\} = \{⟨x, y⟩\} \land Fun {\{⟨x, y⟩\}}^{-1}) \to Fun {\{p\}}^{-1}$
16	11 15	syl	$⊢ (\exists x \exists y \{p\} = \{⟨x, y⟩\} \land \forall x \forall y Fun {\{⟨x, y⟩\}}^{-1}) \to Fun {\{p\}}^{-1}$
17	8 10 16	sylancl	$⊢ Fun \{p\} \to Fun {\{p\}}^{-1}$
18	17	ax-gen	$⊢ \forall p (Fun \{p\} \to Fun {\{p\}}^{-1})$
19		19.29r	$⊢ (\exists p F = \{p\} \land \forall p (Fun \{p\} \to Fun {\{p\}}^{-1})) \to \exists p (F = \{p\} \land (Fun \{p\} \to Fun {\{p\}}^{-1}))$
20		funeq	$⊢ F = \{p\} \to (Fun F \leftrightarrow Fun \{p\})$
21		cnveq	$⊢ F = \{p\} \to F^{-1} = {\{p\}}^{-1}$
22	21	funeqd	$⊢ F = \{p\} \to (Fun F^{-1} \leftrightarrow Fun {\{p\}}^{-1})$
23	20 22	imbi12d	$⊢ F = \{p\} \to ((Fun F \to Fun F^{-1}) \leftrightarrow (Fun \{p\} \to Fun {\{p\}}^{-1}))$
24	23	biimpar	$⊢ (F = \{p\} \land (Fun \{p\} \to Fun {\{p\}}^{-1})) \to (Fun F \to Fun F^{-1})$
25	24	exlimiv	$⊢ \exists p (F = \{p\} \land (Fun \{p\} \to Fun {\{p\}}^{-1})) \to (Fun F \to Fun F^{-1})$
26	19 25	syl	$⊢ (\exists p F = \{p\} \land \forall p (Fun \{p\} \to Fun {\{p\}}^{-1})) \to (Fun F \to Fun F^{-1})$
27	18 26	mpan2	$⊢ \exists p F = \{p\} \to (Fun F \to Fun F^{-1})$
28	1 27	sylbi	$⊢ F \approx 1_{𝑜} \to (Fun F \to Fun F^{-1})$
29	28	impcom	$⊢ (Fun F \land F \approx 1_{𝑜}) \to Fun F^{-1}$

Metamath Proof Explorer

Theorem funen1cnv

Proof