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→ 𝐵 ↔ ∃ 𝑓 ( ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝑥 𝑓 𝑦 ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐴 𝑦 𝑓 𝑥 ) )