Theorem f1oexbi

Description: There is a one-to-one onto function from a set to a second set iff there is a one-to-one onto function from the second set to the first set. (Contributed by Alexander van der Vekens, 30-Sep-2018)

	Ref	Expression
Assertion	f1oexbi	⊢ ( ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 ↔ ∃ 𝑔 𝑔 : 𝐵 –1-1-onto→ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑓 ∈ V
2	1	cnvex	⊢ ◡ 𝑓 ∈ V
3		f1ocnv	⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ◡ 𝑓 : 𝐵 –1-1-onto→ 𝐴 )
4		f1oeq1	⊢ ( 𝑔 = ◡ 𝑓 → ( 𝑔 : 𝐵 –1-1-onto→ 𝐴 ↔ ◡ 𝑓 : 𝐵 –1-1-onto→ 𝐴 ) )
5	4	spcegv	⊢ ( ◡ 𝑓 ∈ V → ( ◡ 𝑓 : 𝐵 –1-1-onto→ 𝐴 → ∃ 𝑔 𝑔 : 𝐵 –1-1-onto→ 𝐴 ) )
6	2 3 5	mpsyl	⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ∃ 𝑔 𝑔 : 𝐵 –1-1-onto→ 𝐴 )
7	6	exlimiv	⊢ ( ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ∃ 𝑔 𝑔 : 𝐵 –1-1-onto→ 𝐴 )
8		vex	⊢ 𝑔 ∈ V
9	8	cnvex	⊢ ◡ 𝑔 ∈ V
10		f1ocnv	⊢ ( 𝑔 : 𝐵 –1-1-onto→ 𝐴 → ◡ 𝑔 : 𝐴 –1-1-onto→ 𝐵 )
11		f1oeq1	⊢ ( 𝑓 = ◡ 𝑔 → ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ↔ ◡ 𝑔 : 𝐴 –1-1-onto→ 𝐵 ) )
12	11	spcegv	⊢ ( ◡ 𝑔 ∈ V → ( ◡ 𝑔 : 𝐴 –1-1-onto→ 𝐵 → ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) )
13	9 10 12	mpsyl	⊢ ( 𝑔 : 𝐵 –1-1-onto→ 𝐴 → ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 )
14	13	exlimiv	⊢ ( ∃ 𝑔 𝑔 : 𝐵 –1-1-onto→ 𝐴 → ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 )
15	7 14	impbii	⊢ ( ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 ↔ ∃ 𝑔 𝑔 : 𝐵 –1-1-onto→ 𝐴 )