Metamath Proof Explorer

Theorem fundcmpsurinjpreimafv

Description: Every function F : A --> B can be decomposed into a surjective function onto P and an injective function from P . (Contributed by AV, 12-Mar-2024) (Proof shortened by AV, 22-Mar-2024)

Ref Expression
Hypothesis fundcmpsurinj.p ⊢ 𝑃 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) }
Assertion fundcmpsurinjpreimafv ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ∃ 𝑔 ∃ ℎ ( 𝑔 : 𝐴 –onto→ 𝑃 ∧ ℎ : 𝑃 –1-1→ 𝐵 ∧ 𝐹 = ( ℎ ∘ 𝑔 ) ) )

Proof

Step Hyp Ref Expression
1 fundcmpsurinj.p ⊢ 𝑃 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) }
2 1 fundcmpsurbijinjpreimafv ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ∃ 𝑔 ∃ 𝑓 ∃ 𝑗 ( ( 𝑔 : 𝐴 –onto→ 𝑃 ∧ 𝑓 : 𝑃 –1-1-onto→ ( 𝐹 “ 𝐴 ) ∧ 𝑗 : ( 𝐹 “ 𝐴 ) –1-1→ 𝐵 ) ∧ 𝐹 = ( ( 𝑗 ∘ 𝑓 ) ∘ 𝑔 ) ) )
3 vex ⊢ 𝑗 ∈ V
4 vex ⊢ 𝑓 ∈ V
5 3 4 coex ⊢ ( 𝑗 ∘ 𝑓 ) ∈ V
6 simprl1 ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) ∧ ( ( 𝑔 : 𝐴 –onto→ 𝑃 ∧ 𝑓 : 𝑃 –1-1-onto→ ( 𝐹 “ 𝐴 ) ∧ 𝑗 : ( 𝐹 “ 𝐴 ) –1-1→ 𝐵 ) ∧ 𝐹 = ( ( 𝑗 ∘ 𝑓 ) ∘ 𝑔 ) ) ) → 𝑔 : 𝐴 –onto→ 𝑃 )
7 simp3 ⊢ ( ( 𝑔 : 𝐴 –onto→ 𝑃 ∧ 𝑓 : 𝑃 –1-1-onto→ ( 𝐹 “ 𝐴 ) ∧ 𝑗 : ( 𝐹 “ 𝐴 ) –1-1→ 𝐵 ) → 𝑗 : ( 𝐹 “ 𝐴 ) –1-1→ 𝐵 )
8 f1of1 ⊢ ( 𝑓 : 𝑃 –1-1-onto→ ( 𝐹 “ 𝐴 ) → 𝑓 : 𝑃 –1-1→ ( 𝐹 “ 𝐴 ) )
9 8 3ad2ant2 ⊢ ( ( 𝑔 : 𝐴 –onto→ 𝑃 ∧ 𝑓 : 𝑃 –1-1-onto→ ( 𝐹 “ 𝐴 ) ∧ 𝑗 : ( 𝐹 “ 𝐴 ) –1-1→ 𝐵 ) → 𝑓 : 𝑃 –1-1→ ( 𝐹 “ 𝐴 ) )
10 f1co ⊢ ( ( 𝑗 : ( 𝐹 “ 𝐴 ) –1-1→ 𝐵 ∧ 𝑓 : 𝑃 –1-1→ ( 𝐹 “ 𝐴 ) ) → ( 𝑗 ∘ 𝑓 ) : 𝑃 –1-1→ 𝐵 )
11 7 9 10 syl2anc ⊢ ( ( 𝑔 : 𝐴 –onto→ 𝑃 ∧ 𝑓 : 𝑃 –1-1-onto→ ( 𝐹 “ 𝐴 ) ∧ 𝑗 : ( 𝐹 “ 𝐴 ) –1-1→ 𝐵 ) → ( 𝑗 ∘ 𝑓 ) : 𝑃 –1-1→ 𝐵 )
12 11 ad2antrl ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) ∧ ( ( 𝑔 : 𝐴 –onto→ 𝑃 ∧ 𝑓 : 𝑃 –1-1-onto→ ( 𝐹 “ 𝐴 ) ∧ 𝑗 : ( 𝐹 “ 𝐴 ) –1-1→ 𝐵 ) ∧ 𝐹 = ( ( 𝑗 ∘ 𝑓 ) ∘ 𝑔 ) ) ) → ( 𝑗 ∘ 𝑓 ) : 𝑃 –1-1→ 𝐵 )
13 simprr ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) ∧ ( ( 𝑔 : 𝐴 –onto→ 𝑃 ∧ 𝑓 : 𝑃 –1-1-onto→ ( 𝐹 “ 𝐴 ) ∧ 𝑗 : ( 𝐹 “ 𝐴 ) –1-1→ 𝐵 ) ∧ 𝐹 = ( ( 𝑗 ∘ 𝑓 ) ∘ 𝑔 ) ) ) → 𝐹 = ( ( 𝑗 ∘ 𝑓 ) ∘ 𝑔 ) )
14 6 12 13 3jca ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) ∧ ( ( 𝑔 : 𝐴 –onto→ 𝑃 ∧ 𝑓 : 𝑃 –1-1-onto→ ( 𝐹 “ 𝐴 ) ∧ 𝑗 : ( 𝐹 “ 𝐴 ) –1-1→ 𝐵 ) ∧ 𝐹 = ( ( 𝑗 ∘ 𝑓 ) ∘ 𝑔 ) ) ) → ( 𝑔 : 𝐴 –onto→ 𝑃 ∧ ( 𝑗 ∘ 𝑓 ) : 𝑃 –1-1→ 𝐵 ∧ 𝐹 = ( ( 𝑗 ∘ 𝑓 ) ∘ 𝑔 ) ) )
15 f1eq1 ⊢ ( ℎ = ( 𝑗 ∘ 𝑓 ) → ( ℎ : 𝑃 –1-1→ 𝐵 ↔ ( 𝑗 ∘ 𝑓 ) : 𝑃 –1-1→ 𝐵 ) )
16 coeq1 ⊢ ( ℎ = ( 𝑗 ∘ 𝑓 ) → ( ℎ ∘ 𝑔 ) = ( ( 𝑗 ∘ 𝑓 ) ∘ 𝑔 ) )
17 16 eqeq2d ⊢ ( ℎ = ( 𝑗 ∘ 𝑓 ) → ( 𝐹 = ( ℎ ∘ 𝑔 ) ↔ 𝐹 = ( ( 𝑗 ∘ 𝑓 ) ∘ 𝑔 ) ) )
18 15 17 3anbi23d ⊢ ( ℎ = ( 𝑗 ∘ 𝑓 ) → ( ( 𝑔 : 𝐴 –onto→ 𝑃 ∧ ℎ : 𝑃 –1-1→ 𝐵 ∧ 𝐹 = ( ℎ ∘ 𝑔 ) ) ↔ ( 𝑔 : 𝐴 –onto→ 𝑃 ∧ ( 𝑗 ∘ 𝑓 ) : 𝑃 –1-1→ 𝐵 ∧ 𝐹 = ( ( 𝑗 ∘ 𝑓 ) ∘ 𝑔 ) ) ) )
19 18 spcegv ⊢ ( ( 𝑗 ∘ 𝑓 ) ∈ V → ( ( 𝑔 : 𝐴 –onto→ 𝑃 ∧ ( 𝑗 ∘ 𝑓 ) : 𝑃 –1-1→ 𝐵 ∧ 𝐹 = ( ( 𝑗 ∘ 𝑓 ) ∘ 𝑔 ) ) → ∃ ℎ ( 𝑔 : 𝐴 –onto→ 𝑃 ∧ ℎ : 𝑃 –1-1→ 𝐵 ∧ 𝐹 = ( ℎ ∘ 𝑔 ) ) ) )
20 5 14 19 mpsyl ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) ∧ ( ( 𝑔 : 𝐴 –onto→ 𝑃 ∧ 𝑓 : 𝑃 –1-1-onto→ ( 𝐹 “ 𝐴 ) ∧ 𝑗 : ( 𝐹 “ 𝐴 ) –1-1→ 𝐵 ) ∧ 𝐹 = ( ( 𝑗 ∘ 𝑓 ) ∘ 𝑔 ) ) ) → ∃ ℎ ( 𝑔 : 𝐴 –onto→ 𝑃 ∧ ℎ : 𝑃 –1-1→ 𝐵 ∧ 𝐹 = ( ℎ ∘ 𝑔 ) ) )
21 20 ex ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ( ( ( 𝑔 : 𝐴 –onto→ 𝑃 ∧ 𝑓 : 𝑃 –1-1-onto→ ( 𝐹 “ 𝐴 ) ∧ 𝑗 : ( 𝐹 “ 𝐴 ) –1-1→ 𝐵 ) ∧ 𝐹 = ( ( 𝑗 ∘ 𝑓 ) ∘ 𝑔 ) ) → ∃ ℎ ( 𝑔 : 𝐴 –onto→ 𝑃 ∧ ℎ : 𝑃 –1-1→ 𝐵 ∧ 𝐹 = ( ℎ ∘ 𝑔 ) ) ) )
22 21 exlimdvv ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ( ∃ 𝑓 ∃ 𝑗 ( ( 𝑔 : 𝐴 –onto→ 𝑃 ∧ 𝑓 : 𝑃 –1-1-onto→ ( 𝐹 “ 𝐴 ) ∧ 𝑗 : ( 𝐹 “ 𝐴 ) –1-1→ 𝐵 ) ∧ 𝐹 = ( ( 𝑗 ∘ 𝑓 ) ∘ 𝑔 ) ) → ∃ ℎ ( 𝑔 : 𝐴 –onto→ 𝑃 ∧ ℎ : 𝑃 –1-1→ 𝐵 ∧ 𝐹 = ( ℎ ∘ 𝑔 ) ) ) )
23 22 eximdv ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ( ∃ 𝑔 ∃ 𝑓 ∃ 𝑗 ( ( 𝑔 : 𝐴 –onto→ 𝑃 ∧ 𝑓 : 𝑃 –1-1-onto→ ( 𝐹 “ 𝐴 ) ∧ 𝑗 : ( 𝐹 “ 𝐴 ) –1-1→ 𝐵 ) ∧ 𝐹 = ( ( 𝑗 ∘ 𝑓 ) ∘ 𝑔 ) ) → ∃ 𝑔 ∃ ℎ ( 𝑔 : 𝐴 –onto→ 𝑃 ∧ ℎ : 𝑃 –1-1→ 𝐵 ∧ 𝐹 = ( ℎ ∘ 𝑔 ) ) ) )
24 2 23 mpd ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ∃ 𝑔 ∃ ℎ ( 𝑔 : 𝐴 –onto→ 𝑃 ∧ ℎ : 𝑃 –1-1→ 𝐵 ∧ 𝐹 = ( ℎ ∘ 𝑔 ) ) )