This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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→ 𝐴 )