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

Metamath Proof Explorer

Theorem exfo

Description: A relation equivalent to the existence of an onto mapping. The right-hand f is not necessarily a function. (Contributed by NM, 20-Mar-2007)

Ref Expression
Assertion exfo ( ∃ 𝑓 𝑓 : 𝐴 –onto→ 𝐵 ↔ ∃ 𝑓 ( ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝑥 𝑓 𝑦 ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐴 𝑦 𝑓 𝑥 ) )

Proof

Step Hyp Ref Expression
1 dffo4 ⊢ ( 𝑓 : 𝐴 –onto→ 𝐵 ↔ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐴 𝑦 𝑓 𝑥 ) )
2 dff4 ⊢ ( 𝑓 : 𝐴 ⟶ 𝐵 ↔ ( 𝑓 ⊆ ( 𝐴 × 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝑥 𝑓 𝑦 ) )
3 2 simprbi ⊢ ( 𝑓 : 𝐴 ⟶ 𝐵 → ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝑥 𝑓 𝑦 )
4 3 anim1i ⊢ ( ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐴 𝑦 𝑓 𝑥 ) → ( ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝑥 𝑓 𝑦 ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐴 𝑦 𝑓 𝑥 ) )
5 1 4 sylbi ⊢ ( 𝑓 : 𝐴 –onto→ 𝐵 → ( ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝑥 𝑓 𝑦 ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐴 𝑦 𝑓 𝑥 ) )
6 5 eximi ⊢ ( ∃ 𝑓 𝑓 : 𝐴 –onto→ 𝐵 → ∃ 𝑓 ( ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝑥 𝑓 𝑦 ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐴 𝑦 𝑓 𝑥 ) )
7 brinxp ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 𝑓 𝑦 ↔ 𝑥 ( 𝑓 ∩ ( 𝐴 × 𝐵 ) ) 𝑦 ) )
8 7 reubidva ⊢ ( 𝑥 ∈ 𝐴 → ( ∃! 𝑦 ∈ 𝐵 𝑥 𝑓 𝑦 ↔ ∃! 𝑦 ∈ 𝐵 𝑥 ( 𝑓 ∩ ( 𝐴 × 𝐵 ) ) 𝑦 ) )
9 8 biimpd ⊢ ( 𝑥 ∈ 𝐴 → ( ∃! 𝑦 ∈ 𝐵 𝑥 𝑓 𝑦 → ∃! 𝑦 ∈ 𝐵 𝑥 ( 𝑓 ∩ ( 𝐴 × 𝐵 ) ) 𝑦 ) )
10 9 ralimia ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝑥 𝑓 𝑦 → ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝑥 ( 𝑓 ∩ ( 𝐴 × 𝐵 ) ) 𝑦 )
11 inss2 ⊢ ( 𝑓 ∩ ( 𝐴 × 𝐵 ) ) ⊆ ( 𝐴 × 𝐵 )
12 10 11 jctil ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝑥 𝑓 𝑦 → ( ( 𝑓 ∩ ( 𝐴 × 𝐵 ) ) ⊆ ( 𝐴 × 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝑥 ( 𝑓 ∩ ( 𝐴 × 𝐵 ) ) 𝑦 ) )
13 dff4 ⊢ ( ( 𝑓 ∩ ( 𝐴 × 𝐵 ) ) : 𝐴 ⟶ 𝐵 ↔ ( ( 𝑓 ∩ ( 𝐴 × 𝐵 ) ) ⊆ ( 𝐴 × 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝑥 ( 𝑓 ∩ ( 𝐴 × 𝐵 ) ) 𝑦 ) )
14 12 13 sylibr ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝑥 𝑓 𝑦 → ( 𝑓 ∩ ( 𝐴 × 𝐵 ) ) : 𝐴 ⟶ 𝐵 )
15 rninxp ⊢ ( ran ( 𝑓 ∩ ( 𝐴 × 𝐵 ) ) = 𝐵 ↔ ∀ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐴 𝑦 𝑓 𝑥 )
16 15 biimpri ⊢ ( ∀ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐴 𝑦 𝑓 𝑥 → ran ( 𝑓 ∩ ( 𝐴 × 𝐵 ) ) = 𝐵 )
17 14 16 anim12i ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝑥 𝑓 𝑦 ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐴 𝑦 𝑓 𝑥 ) → ( ( 𝑓 ∩ ( 𝐴 × 𝐵 ) ) : 𝐴 ⟶ 𝐵 ∧ ran ( 𝑓 ∩ ( 𝐴 × 𝐵 ) ) = 𝐵 ) )
18 dffo2 ⊢ ( ( 𝑓 ∩ ( 𝐴 × 𝐵 ) ) : 𝐴 –onto→ 𝐵 ↔ ( ( 𝑓 ∩ ( 𝐴 × 𝐵 ) ) : 𝐴 ⟶ 𝐵 ∧ ran ( 𝑓 ∩ ( 𝐴 × 𝐵 ) ) = 𝐵 ) )
19 17 18 sylibr ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝑥 𝑓 𝑦 ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐴 𝑦 𝑓 𝑥 ) → ( 𝑓 ∩ ( 𝐴 × 𝐵 ) ) : 𝐴 –onto→ 𝐵 )
20 vex ⊢ 𝑓 ∈ V
21 20 inex1 ⊢ ( 𝑓 ∩ ( 𝐴 × 𝐵 ) ) ∈ V
22 foeq1 ⊢ ( 𝑔 = ( 𝑓 ∩ ( 𝐴 × 𝐵 ) ) → ( 𝑔 : 𝐴 –onto→ 𝐵 ↔ ( 𝑓 ∩ ( 𝐴 × 𝐵 ) ) : 𝐴 –onto→ 𝐵 ) )
23 21 22 spcev ⊢ ( ( 𝑓 ∩ ( 𝐴 × 𝐵 ) ) : 𝐴 –onto→ 𝐵 → ∃ 𝑔 𝑔 : 𝐴 –onto→ 𝐵 )
24 19 23 syl ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝑥 𝑓 𝑦 ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐴 𝑦 𝑓 𝑥 ) → ∃ 𝑔 𝑔 : 𝐴 –onto→ 𝐵 )
25 24 exlimiv ⊢ ( ∃ 𝑓 ( ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝑥 𝑓 𝑦 ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐴 𝑦 𝑓 𝑥 ) → ∃ 𝑔 𝑔 : 𝐴 –onto→ 𝐵 )
26 foeq1 ⊢ ( 𝑔 = 𝑓 → ( 𝑔 : 𝐴 –onto→ 𝐵 ↔ 𝑓 : 𝐴 –onto→ 𝐵 ) )
27 26 cbvexvw ⊢ ( ∃ 𝑔 𝑔 : 𝐴 –onto→ 𝐵 ↔ ∃ 𝑓 𝑓 : 𝐴 –onto→ 𝐵 )
28 25 27 sylib ⊢ ( ∃ 𝑓 ( ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝑥 𝑓 𝑦 ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐴 𝑦 𝑓 𝑥 ) → ∃ 𝑓 𝑓 : 𝐴 –onto→ 𝐵 )
29 6 28 impbii ⊢ ( ∃ 𝑓 𝑓 : 𝐴 –onto→ 𝐵 ↔ ∃ 𝑓 ( ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝑥 𝑓 𝑦 ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐴 𝑦 𝑓 𝑥 ) )