Theorem fundcmpsurinj

Description: Every function F : A --> B can be decomposed into a surjective and an injective function. (Contributed by AV, 13-Mar-2024)

	Ref	Expression
Assertion	fundcmpsurinj	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ∃ 𝑔 ∃ ℎ ∃ 𝑝 ( 𝑔 : 𝐴 –onto→ 𝑝 ∧ ℎ : 𝑝 –1-1→ 𝐵 ∧ 𝐹 = ( ℎ ∘ 𝑔 ) ) )

Proof

Step	Hyp	Ref	Expression
1		abrexexg	⊢ ( 𝐴 ∈ 𝑉 → { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) } ∈ V )
2	1	adantl	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) } ∈ V )
3		fveq2	⊢ ( 𝑥 = 𝑦 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
4	3	sneqd	⊢ ( 𝑥 = 𝑦 → { ( 𝐹 ‘ 𝑥 ) } = { ( 𝐹 ‘ 𝑦 ) } )
5	4	imaeq2d	⊢ ( 𝑥 = 𝑦 → ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) )
6	5	eqeq2d	⊢ ( 𝑥 = 𝑦 → ( 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ↔ 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) ) )
7	6	cbvrexvw	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ↔ ∃ 𝑦 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) )
8	7	abbii	⊢ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) } = { 𝑧 ∣ ∃ 𝑦 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) }
9	8	fundcmpsurinjpreimafv	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ∃ 𝑔 ∃ ℎ ( 𝑔 : 𝐴 –onto→ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) } ∧ ℎ : { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) } –1-1→ 𝐵 ∧ 𝐹 = ( ℎ ∘ 𝑔 ) ) )
10		foeq3	⊢ ( 𝑝 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) } → ( 𝑔 : 𝐴 –onto→ 𝑝 ↔ 𝑔 : 𝐴 –onto→ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) } ) )
11		f1eq2	⊢ ( 𝑝 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) } → ( ℎ : 𝑝 –1-1→ 𝐵 ↔ ℎ : { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) } –1-1→ 𝐵 ) )
12	10 11	3anbi12d	⊢ ( 𝑝 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) } → ( ( 𝑔 : 𝐴 –onto→ 𝑝 ∧ ℎ : 𝑝 –1-1→ 𝐵 ∧ 𝐹 = ( ℎ ∘ 𝑔 ) ) ↔ ( 𝑔 : 𝐴 –onto→ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) } ∧ ℎ : { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) } –1-1→ 𝐵 ∧ 𝐹 = ( ℎ ∘ 𝑔 ) ) ) )
13	12	2exbidv	⊢ ( 𝑝 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) } → ( ∃ 𝑔 ∃ ℎ ( 𝑔 : 𝐴 –onto→ 𝑝 ∧ ℎ : 𝑝 –1-1→ 𝐵 ∧ 𝐹 = ( ℎ ∘ 𝑔 ) ) ↔ ∃ 𝑔 ∃ ℎ ( 𝑔 : 𝐴 –onto→ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) } ∧ ℎ : { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) } –1-1→ 𝐵 ∧ 𝐹 = ( ℎ ∘ 𝑔 ) ) ) )
14	2 9 13	spcedv	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ∃ 𝑝 ∃ 𝑔 ∃ ℎ ( 𝑔 : 𝐴 –onto→ 𝑝 ∧ ℎ : 𝑝 –1-1→ 𝐵 ∧ 𝐹 = ( ℎ ∘ 𝑔 ) ) )
15		exrot3	⊢ ( ∃ 𝑝 ∃ 𝑔 ∃ ℎ ( 𝑔 : 𝐴 –onto→ 𝑝 ∧ ℎ : 𝑝 –1-1→ 𝐵 ∧ 𝐹 = ( ℎ ∘ 𝑔 ) ) ↔ ∃ 𝑔 ∃ ℎ ∃ 𝑝 ( 𝑔 : 𝐴 –onto→ 𝑝 ∧ ℎ : 𝑝 –1-1→ 𝐵 ∧ 𝐹 = ( ℎ ∘ 𝑔 ) ) )
16	14 15	sylib	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ∃ 𝑔 ∃ ℎ ∃ 𝑝 ( 𝑔 : 𝐴 –onto→ 𝑝 ∧ ℎ : 𝑝 –1-1→ 𝐵 ∧ 𝐹 = ( ℎ ∘ 𝑔 ) ) )