Metamath Proof Explorer

Theorem fundcmpsurinjALT

Description: Alternate proof of fundcmpsurinj , based on fundcmpsurinjimaid : Every function F : A --> B can be decomposed into a surjective and an injective function. (Proof modification is discouraged.) (New usage is discouraged.) (Contributed by AV, 13-Mar-2024)

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

Proof

Step Hyp Ref Expression
1 mptexg ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) ) ∈ V )
2 1 adantl ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) ) ∈ V )
3 ffun ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → Fun 𝐹 )
4 funimaexg ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ 𝑉 ) → ( 𝐹 “ 𝐴 ) ∈ V )
5 3 4 sylan ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ( 𝐹 “ 𝐴 ) ∈ V )
6 5 resiexd ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ( I ↾ ( 𝐹 “ 𝐴 ) ) ∈ V )
7 2 6 5 3jca ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) ) ∈ V ∧ ( I ↾ ( 𝐹 “ 𝐴 ) ) ∈ V ∧ ( 𝐹 “ 𝐴 ) ∈ V ) )
8 eqid ⊢ ( 𝐹 “ 𝐴 ) = ( 𝐹 “ 𝐴 )
9 eqid ⊢ ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) ) = ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) )
10 eqid ⊢ ( I ↾ ( 𝐹 “ 𝐴 ) ) = ( I ↾ ( 𝐹 “ 𝐴 ) )
11 8 9 10 fundcmpsurinjimaid ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) ) : 𝐴 –onto→ ( 𝐹 “ 𝐴 ) ∧ ( I ↾ ( 𝐹 “ 𝐴 ) ) : ( 𝐹 “ 𝐴 ) –1-1→ 𝐵 ∧ 𝐹 = ( ( I ↾ ( 𝐹 “ 𝐴 ) ) ∘ ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) ) ) ) )
12 11 adantr ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) ) : 𝐴 –onto→ ( 𝐹 “ 𝐴 ) ∧ ( I ↾ ( 𝐹 “ 𝐴 ) ) : ( 𝐹 “ 𝐴 ) –1-1→ 𝐵 ∧ 𝐹 = ( ( I ↾ ( 𝐹 “ 𝐴 ) ) ∘ ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) ) ) ) )
13 simp1 ⊢ ( ( 𝑔 = ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) ) ∧ ℎ = ( I ↾ ( 𝐹 “ 𝐴 ) ) ∧ 𝑝 = ( 𝐹 “ 𝐴 ) ) → 𝑔 = ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) ) )
14 eqidd ⊢ ( ( 𝑔 = ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) ) ∧ ℎ = ( I ↾ ( 𝐹 “ 𝐴 ) ) ∧ 𝑝 = ( 𝐹 “ 𝐴 ) ) → 𝐴 = 𝐴 )
15 simp3 ⊢ ( ( 𝑔 = ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) ) ∧ ℎ = ( I ↾ ( 𝐹 “ 𝐴 ) ) ∧ 𝑝 = ( 𝐹 “ 𝐴 ) ) → 𝑝 = ( 𝐹 “ 𝐴 ) )
16 13 14 15 foeq123d ⊢ ( ( 𝑔 = ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) ) ∧ ℎ = ( I ↾ ( 𝐹 “ 𝐴 ) ) ∧ 𝑝 = ( 𝐹 “ 𝐴 ) ) → ( 𝑔 : 𝐴 –onto→ 𝑝 ↔ ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) ) : 𝐴 –onto→ ( 𝐹 “ 𝐴 ) ) )
17 simpl ⊢ ( ( ℎ = ( I ↾ ( 𝐹 “ 𝐴 ) ) ∧ 𝑝 = ( 𝐹 “ 𝐴 ) ) → ℎ = ( I ↾ ( 𝐹 “ 𝐴 ) ) )
18 simpr ⊢ ( ( ℎ = ( I ↾ ( 𝐹 “ 𝐴 ) ) ∧ 𝑝 = ( 𝐹 “ 𝐴 ) ) → 𝑝 = ( 𝐹 “ 𝐴 ) )
19 eqidd ⊢ ( ( ℎ = ( I ↾ ( 𝐹 “ 𝐴 ) ) ∧ 𝑝 = ( 𝐹 “ 𝐴 ) ) → 𝐵 = 𝐵 )
20 17 18 19 f1eq123d ⊢ ( ( ℎ = ( I ↾ ( 𝐹 “ 𝐴 ) ) ∧ 𝑝 = ( 𝐹 “ 𝐴 ) ) → ( ℎ : 𝑝 –1-1→ 𝐵 ↔ ( I ↾ ( 𝐹 “ 𝐴 ) ) : ( 𝐹 “ 𝐴 ) –1-1→ 𝐵 ) )
21 20 3adant1 ⊢ ( ( 𝑔 = ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) ) ∧ ℎ = ( I ↾ ( 𝐹 “ 𝐴 ) ) ∧ 𝑝 = ( 𝐹 “ 𝐴 ) ) → ( ℎ : 𝑝 –1-1→ 𝐵 ↔ ( I ↾ ( 𝐹 “ 𝐴 ) ) : ( 𝐹 “ 𝐴 ) –1-1→ 𝐵 ) )
22 simpl ⊢ ( ( ℎ = ( I ↾ ( 𝐹 “ 𝐴 ) ) ∧ 𝑔 = ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) ) ) → ℎ = ( I ↾ ( 𝐹 “ 𝐴 ) ) )
23 simpr ⊢ ( ( ℎ = ( I ↾ ( 𝐹 “ 𝐴 ) ) ∧ 𝑔 = ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) ) ) → 𝑔 = ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) ) )
24 22 23 coeq12d ⊢ ( ( ℎ = ( I ↾ ( 𝐹 “ 𝐴 ) ) ∧ 𝑔 = ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) ) ) → ( ℎ ∘ 𝑔 ) = ( ( I ↾ ( 𝐹 “ 𝐴 ) ) ∘ ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) ) ) )
25 24 ancoms ⊢ ( ( 𝑔 = ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) ) ∧ ℎ = ( I ↾ ( 𝐹 “ 𝐴 ) ) ) → ( ℎ ∘ 𝑔 ) = ( ( I ↾ ( 𝐹 “ 𝐴 ) ) ∘ ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) ) ) )
26 25 3adant3 ⊢ ( ( 𝑔 = ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) ) ∧ ℎ = ( I ↾ ( 𝐹 “ 𝐴 ) ) ∧ 𝑝 = ( 𝐹 “ 𝐴 ) ) → ( ℎ ∘ 𝑔 ) = ( ( I ↾ ( 𝐹 “ 𝐴 ) ) ∘ ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) ) ) )
27 26 eqeq2d ⊢ ( ( 𝑔 = ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) ) ∧ ℎ = ( I ↾ ( 𝐹 “ 𝐴 ) ) ∧ 𝑝 = ( 𝐹 “ 𝐴 ) ) → ( 𝐹 = ( ℎ ∘ 𝑔 ) ↔ 𝐹 = ( ( I ↾ ( 𝐹 “ 𝐴 ) ) ∘ ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) ) ) ) )
28 16 21 27 3anbi123d ⊢ ( ( 𝑔 = ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) ) ∧ ℎ = ( I ↾ ( 𝐹 “ 𝐴 ) ) ∧ 𝑝 = ( 𝐹 “ 𝐴 ) ) → ( ( 𝑔 : 𝐴 –onto→ 𝑝 ∧ ℎ : 𝑝 –1-1→ 𝐵 ∧ 𝐹 = ( ℎ ∘ 𝑔 ) ) ↔ ( ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) ) : 𝐴 –onto→ ( 𝐹 “ 𝐴 ) ∧ ( I ↾ ( 𝐹 “ 𝐴 ) ) : ( 𝐹 “ 𝐴 ) –1-1→ 𝐵 ∧ 𝐹 = ( ( I ↾ ( 𝐹 “ 𝐴 ) ) ∘ ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) ) ) ) ) )
29 28 spc3egv ⊢ ( ( ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) ) ∈ V ∧ ( I ↾ ( 𝐹 “ 𝐴 ) ) ∈ V ∧ ( 𝐹 “ 𝐴 ) ∈ V ) → ( ( ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) ) : 𝐴 –onto→ ( 𝐹 “ 𝐴 ) ∧ ( I ↾ ( 𝐹 “ 𝐴 ) ) : ( 𝐹 “ 𝐴 ) –1-1→ 𝐵 ∧ 𝐹 = ( ( I ↾ ( 𝐹 “ 𝐴 ) ) ∘ ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) ) ) ) → ∃ 𝑔 ∃ ℎ ∃ 𝑝 ( 𝑔 : 𝐴 –onto→ 𝑝 ∧ ℎ : 𝑝 –1-1→ 𝐵 ∧ 𝐹 = ( ℎ ∘ 𝑔 ) ) ) )
30 7 12 29 sylc ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ∃ 𝑔 ∃ ℎ ∃ 𝑝 ( 𝑔 : 𝐴 –onto→ 𝑝 ∧ ℎ : 𝑝 –1-1→ 𝐵 ∧ 𝐹 = ( ℎ ∘ 𝑔 ) ) )