Metamath Proof Explorer

Theorem fundcmpsurbijinj

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

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

Proof

Step Hyp Ref Expression
1 ffun ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → Fun 𝐹 )
2 funimaexg ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ 𝑉 ) → ( 𝐹 “ 𝐴 ) ∈ V )
3 1 2 sylan ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ( 𝐹 “ 𝐴 ) ∈ V )
4 abrexexg ⊢ ( 𝐴 ∈ 𝑉 → { 𝑧 ∣ ∃ 𝑦 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) } ∈ V )
5 4 adantl ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → { 𝑧 ∣ ∃ 𝑦 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) } ∈ V )
6 fveq2 ⊢ ( 𝑦 = 𝑥 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) )
7 6 sneqd ⊢ ( 𝑦 = 𝑥 → { ( 𝐹 ‘ 𝑦 ) } = { ( 𝐹 ‘ 𝑥 ) } )
8 7 imaeq2d ⊢ ( 𝑦 = 𝑥 → ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) )
9 8 eqeq2d ⊢ ( 𝑦 = 𝑥 → ( 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) ↔ 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) )
10 9 cbvrexvw ⊢ ( ∃ 𝑦 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) ↔ ∃ 𝑥 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) )
11 10 abbii ⊢ { 𝑧 ∣ ∃ 𝑦 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) } = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) }
12 11 fundcmpsurbijinjpreimafv ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ∃ 𝑔 ∃ ℎ ∃ 𝑖 ( ( 𝑔 : 𝐴 –onto→ { 𝑧 ∣ ∃ 𝑦 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) } ∧ ℎ : { 𝑧 ∣ ∃ 𝑦 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) } –1-1-onto→ ( 𝐹 “ 𝐴 ) ∧ 𝑖 : ( 𝐹 “ 𝐴 ) –1-1→ 𝐵 ) ∧ 𝐹 = ( ( 𝑖 ∘ ℎ ) ∘ 𝑔 ) ) )
13 foeq3 ⊢ ( 𝑝 = { 𝑧 ∣ ∃ 𝑦 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) } → ( 𝑔 : 𝐴 –onto→ 𝑝 ↔ 𝑔 : 𝐴 –onto→ { 𝑧 ∣ ∃ 𝑦 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) } ) )
14 13 adantl ⊢ ( ( 𝑞 = ( 𝐹 “ 𝐴 ) ∧ 𝑝 = { 𝑧 ∣ ∃ 𝑦 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) } ) → ( 𝑔 : 𝐴 –onto→ 𝑝 ↔ 𝑔 : 𝐴 –onto→ { 𝑧 ∣ ∃ 𝑦 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) } ) )
15 f1oeq23 ⊢ ( ( 𝑝 = { 𝑧 ∣ ∃ 𝑦 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) } ∧ 𝑞 = ( 𝐹 “ 𝐴 ) ) → ( ℎ : 𝑝 –1-1-onto→ 𝑞 ↔ ℎ : { 𝑧 ∣ ∃ 𝑦 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) } –1-1-onto→ ( 𝐹 “ 𝐴 ) ) )
16 15 ancoms ⊢ ( ( 𝑞 = ( 𝐹 “ 𝐴 ) ∧ 𝑝 = { 𝑧 ∣ ∃ 𝑦 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) } ) → ( ℎ : 𝑝 –1-1-onto→ 𝑞 ↔ ℎ : { 𝑧 ∣ ∃ 𝑦 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) } –1-1-onto→ ( 𝐹 “ 𝐴 ) ) )
17 f1eq2 ⊢ ( 𝑞 = ( 𝐹 “ 𝐴 ) → ( 𝑖 : 𝑞 –1-1→ 𝐵 ↔ 𝑖 : ( 𝐹 “ 𝐴 ) –1-1→ 𝐵 ) )
18 17 adantr ⊢ ( ( 𝑞 = ( 𝐹 “ 𝐴 ) ∧ 𝑝 = { 𝑧 ∣ ∃ 𝑦 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) } ) → ( 𝑖 : 𝑞 –1-1→ 𝐵 ↔ 𝑖 : ( 𝐹 “ 𝐴 ) –1-1→ 𝐵 ) )
19 14 16 18 3anbi123d ⊢ ( ( 𝑞 = ( 𝐹 “ 𝐴 ) ∧ 𝑝 = { 𝑧 ∣ ∃ 𝑦 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) } ) → ( ( 𝑔 : 𝐴 –onto→ 𝑝 ∧ ℎ : 𝑝 –1-1-onto→ 𝑞 ∧ 𝑖 : 𝑞 –1-1→ 𝐵 ) ↔ ( 𝑔 : 𝐴 –onto→ { 𝑧 ∣ ∃ 𝑦 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) } ∧ ℎ : { 𝑧 ∣ ∃ 𝑦 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) } –1-1-onto→ ( 𝐹 “ 𝐴 ) ∧ 𝑖 : ( 𝐹 “ 𝐴 ) –1-1→ 𝐵 ) ) )
20 19 anbi1d ⊢ ( ( 𝑞 = ( 𝐹 “ 𝐴 ) ∧ 𝑝 = { 𝑧 ∣ ∃ 𝑦 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) } ) → ( ( ( 𝑔 : 𝐴 –onto→ 𝑝 ∧ ℎ : 𝑝 –1-1-onto→ 𝑞 ∧ 𝑖 : 𝑞 –1-1→ 𝐵 ) ∧ 𝐹 = ( ( 𝑖 ∘ ℎ ) ∘ 𝑔 ) ) ↔ ( ( 𝑔 : 𝐴 –onto→ { 𝑧 ∣ ∃ 𝑦 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) } ∧ ℎ : { 𝑧 ∣ ∃ 𝑦 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) } –1-1-onto→ ( 𝐹 “ 𝐴 ) ∧ 𝑖 : ( 𝐹 “ 𝐴 ) –1-1→ 𝐵 ) ∧ 𝐹 = ( ( 𝑖 ∘ ℎ ) ∘ 𝑔 ) ) ) )
21 20 3exbidv ⊢ ( ( 𝑞 = ( 𝐹 “ 𝐴 ) ∧ 𝑝 = { 𝑧 ∣ ∃ 𝑦 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) } ) → ( ∃ 𝑔 ∃ ℎ ∃ 𝑖 ( ( 𝑔 : 𝐴 –onto→ 𝑝 ∧ ℎ : 𝑝 –1-1-onto→ 𝑞 ∧ 𝑖 : 𝑞 –1-1→ 𝐵 ) ∧ 𝐹 = ( ( 𝑖 ∘ ℎ ) ∘ 𝑔 ) ) ↔ ∃ 𝑔 ∃ ℎ ∃ 𝑖 ( ( 𝑔 : 𝐴 –onto→ { 𝑧 ∣ ∃ 𝑦 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) } ∧ ℎ : { 𝑧 ∣ ∃ 𝑦 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) } –1-1-onto→ ( 𝐹 “ 𝐴 ) ∧ 𝑖 : ( 𝐹 “ 𝐴 ) –1-1→ 𝐵 ) ∧ 𝐹 = ( ( 𝑖 ∘ ℎ ) ∘ 𝑔 ) ) ) )
22 21 spc2egv ⊢ ( ( ( 𝐹 “ 𝐴 ) ∈ V ∧ { 𝑧 ∣ ∃ 𝑦 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) } ∈ V ) → ( ∃ 𝑔 ∃ ℎ ∃ 𝑖 ( ( 𝑔 : 𝐴 –onto→ { 𝑧 ∣ ∃ 𝑦 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) } ∧ ℎ : { 𝑧 ∣ ∃ 𝑦 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) } –1-1-onto→ ( 𝐹 “ 𝐴 ) ∧ 𝑖 : ( 𝐹 “ 𝐴 ) –1-1→ 𝐵 ) ∧ 𝐹 = ( ( 𝑖 ∘ ℎ ) ∘ 𝑔 ) ) → ∃ 𝑞 ∃ 𝑝 ∃ 𝑔 ∃ ℎ ∃ 𝑖 ( ( 𝑔 : 𝐴 –onto→ 𝑝 ∧ ℎ : 𝑝 –1-1-onto→ 𝑞 ∧ 𝑖 : 𝑞 –1-1→ 𝐵 ) ∧ 𝐹 = ( ( 𝑖 ∘ ℎ ) ∘ 𝑔 ) ) ) )
23 22 imp ⊢ ( ( ( ( 𝐹 “ 𝐴 ) ∈ V ∧ { 𝑧 ∣ ∃ 𝑦 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) } ∈ V ) ∧ ∃ 𝑔 ∃ ℎ ∃ 𝑖 ( ( 𝑔 : 𝐴 –onto→ { 𝑧 ∣ ∃ 𝑦 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) } ∧ ℎ : { 𝑧 ∣ ∃ 𝑦 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) } –1-1-onto→ ( 𝐹 “ 𝐴 ) ∧ 𝑖 : ( 𝐹 “ 𝐴 ) –1-1→ 𝐵 ) ∧ 𝐹 = ( ( 𝑖 ∘ ℎ ) ∘ 𝑔 ) ) ) → ∃ 𝑞 ∃ 𝑝 ∃ 𝑔 ∃ ℎ ∃ 𝑖 ( ( 𝑔 : 𝐴 –onto→ 𝑝 ∧ ℎ : 𝑝 –1-1-onto→ 𝑞 ∧ 𝑖 : 𝑞 –1-1→ 𝐵 ) ∧ 𝐹 = ( ( 𝑖 ∘ ℎ ) ∘ 𝑔 ) ) )
24 3 5 12 23 syl21anc ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ∃ 𝑞 ∃ 𝑝 ∃ 𝑔 ∃ ℎ ∃ 𝑖 ( ( 𝑔 : 𝐴 –onto→ 𝑝 ∧ ℎ : 𝑝 –1-1-onto→ 𝑞 ∧ 𝑖 : 𝑞 –1-1→ 𝐵 ) ∧ 𝐹 = ( ( 𝑖 ∘ ℎ ) ∘ 𝑔 ) ) )
25 exrot4 ⊢ ( ∃ 𝑞 ∃ 𝑝 ∃ 𝑔 ∃ ℎ ∃ 𝑖 ( ( 𝑔 : 𝐴 –onto→ 𝑝 ∧ ℎ : 𝑝 –1-1-onto→ 𝑞 ∧ 𝑖 : 𝑞 –1-1→ 𝐵 ) ∧ 𝐹 = ( ( 𝑖 ∘ ℎ ) ∘ 𝑔 ) ) ↔ ∃ 𝑔 ∃ ℎ ∃ 𝑞 ∃ 𝑝 ∃ 𝑖 ( ( 𝑔 : 𝐴 –onto→ 𝑝 ∧ ℎ : 𝑝 –1-1-onto→ 𝑞 ∧ 𝑖 : 𝑞 –1-1→ 𝐵 ) ∧ 𝐹 = ( ( 𝑖 ∘ ℎ ) ∘ 𝑔 ) ) )
26 excom13 ⊢ ( ∃ 𝑞 ∃ 𝑝 ∃ 𝑖 ( ( 𝑔 : 𝐴 –onto→ 𝑝 ∧ ℎ : 𝑝 –1-1-onto→ 𝑞 ∧ 𝑖 : 𝑞 –1-1→ 𝐵 ) ∧ 𝐹 = ( ( 𝑖 ∘ ℎ ) ∘ 𝑔 ) ) ↔ ∃ 𝑖 ∃ 𝑝 ∃ 𝑞 ( ( 𝑔 : 𝐴 –onto→ 𝑝 ∧ ℎ : 𝑝 –1-1-onto→ 𝑞 ∧ 𝑖 : 𝑞 –1-1→ 𝐵 ) ∧ 𝐹 = ( ( 𝑖 ∘ ℎ ) ∘ 𝑔 ) ) )
27 26 2exbii ⊢ ( ∃ 𝑔 ∃ ℎ ∃ 𝑞 ∃ 𝑝 ∃ 𝑖 ( ( 𝑔 : 𝐴 –onto→ 𝑝 ∧ ℎ : 𝑝 –1-1-onto→ 𝑞 ∧ 𝑖 : 𝑞 –1-1→ 𝐵 ) ∧ 𝐹 = ( ( 𝑖 ∘ ℎ ) ∘ 𝑔 ) ) ↔ ∃ 𝑔 ∃ ℎ ∃ 𝑖 ∃ 𝑝 ∃ 𝑞 ( ( 𝑔 : 𝐴 –onto→ 𝑝 ∧ ℎ : 𝑝 –1-1-onto→ 𝑞 ∧ 𝑖 : 𝑞 –1-1→ 𝐵 ) ∧ 𝐹 = ( ( 𝑖 ∘ ℎ ) ∘ 𝑔 ) ) )
28 25 27 bitri ⊢ ( ∃ 𝑞 ∃ 𝑝 ∃ 𝑔 ∃ ℎ ∃ 𝑖 ( ( 𝑔 : 𝐴 –onto→ 𝑝 ∧ ℎ : 𝑝 –1-1-onto→ 𝑞 ∧ 𝑖 : 𝑞 –1-1→ 𝐵 ) ∧ 𝐹 = ( ( 𝑖 ∘ ℎ ) ∘ 𝑔 ) ) ↔ ∃ 𝑔 ∃ ℎ ∃ 𝑖 ∃ 𝑝 ∃ 𝑞 ( ( 𝑔 : 𝐴 –onto→ 𝑝 ∧ ℎ : 𝑝 –1-1-onto→ 𝑞 ∧ 𝑖 : 𝑞 –1-1→ 𝐵 ) ∧ 𝐹 = ( ( 𝑖 ∘ ℎ ) ∘ 𝑔 ) ) )
29 24 28 sylib ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ∃ 𝑔 ∃ ℎ ∃ 𝑖 ∃ 𝑝 ∃ 𝑞 ( ( 𝑔 : 𝐴 –onto→ 𝑝 ∧ ℎ : 𝑝 –1-1-onto→ 𝑞 ∧ 𝑖 : 𝑞 –1-1→ 𝐵 ) ∧ 𝐹 = ( ( 𝑖 ∘ ℎ ) ∘ 𝑔 ) ) )