Metamath Proof Explorer

Theorem fundcmpsurbijinjpreimafv

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

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

Proof

Step Hyp Ref Expression
1 fundcmpsurinj.p ⊢ 𝑃 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) }
2 simpr ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → 𝐴 ∈ 𝑉 )
3 2 mptexd ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ( 𝑎 ∈ 𝐴 ↦ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) ∈ V )
4 1 setpreimafvex ⊢ ( 𝐴 ∈ 𝑉 → 𝑃 ∈ V )
5 4 adantl ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → 𝑃 ∈ V )
6 5 mptexd ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ( 𝑦 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑦 ) ) ∈ V )
7 ffun ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → Fun 𝐹 )
8 funimaexg ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ 𝑉 ) → ( 𝐹 “ 𝐴 ) ∈ V )
9 7 8 sylan ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ( 𝐹 “ 𝐴 ) ∈ V )
10 9 resiexd ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ( I ↾ ( 𝐹 “ 𝐴 ) ) ∈ V )
11 3 6 10 3jca ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝑎 ∈ 𝐴 ↦ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) ∈ V ∧ ( 𝑦 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑦 ) ) ∈ V ∧ ( I ↾ ( 𝐹 “ 𝐴 ) ) ∈ V ) )
12 ffn ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 Fn 𝐴 )
13 fveq2 ⊢ ( 𝑎 = 𝑥 → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑥 ) )
14 13 sneqd ⊢ ( 𝑎 = 𝑥 → { ( 𝐹 ‘ 𝑎 ) } = { ( 𝐹 ‘ 𝑥 ) } )
15 14 imaeq2d ⊢ ( 𝑎 = 𝑥 → ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) )
16 15 cbvmptv ⊢ ( 𝑎 ∈ 𝐴 ↦ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) )
17 1 16 fundcmpsurinjlem2 ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ) → ( 𝑎 ∈ 𝐴 ↦ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) : 𝐴 –onto→ 𝑃 )
18 12 17 sylan ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ( 𝑎 ∈ 𝐴 ↦ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) : 𝐴 –onto→ 𝑃 )
19 eqid ⊢ ( 𝑦 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑦 ) ) = ( 𝑦 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑦 ) )
20 1 19 imasetpreimafvbij ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ) → ( 𝑦 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑦 ) ) : 𝑃 –1-1-onto→ ( 𝐹 “ 𝐴 ) )
21 12 20 sylan ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ( 𝑦 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑦 ) ) : 𝑃 –1-1-onto→ ( 𝐹 “ 𝐴 ) )
22 f1oi ⊢ ( I ↾ ( 𝐹 “ 𝐴 ) ) : ( 𝐹 “ 𝐴 ) –1-1-onto→ ( 𝐹 “ 𝐴 )
23 f1of1 ⊢ ( ( I ↾ ( 𝐹 “ 𝐴 ) ) : ( 𝐹 “ 𝐴 ) –1-1-onto→ ( 𝐹 “ 𝐴 ) → ( I ↾ ( 𝐹 “ 𝐴 ) ) : ( 𝐹 “ 𝐴 ) –1-1→ ( 𝐹 “ 𝐴 ) )
24 fimass ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐹 “ 𝐴 ) ⊆ 𝐵 )
25 f1ss ⊢ ( ( ( I ↾ ( 𝐹 “ 𝐴 ) ) : ( 𝐹 “ 𝐴 ) –1-1→ ( 𝐹 “ 𝐴 ) ∧ ( 𝐹 “ 𝐴 ) ⊆ 𝐵 ) → ( I ↾ ( 𝐹 “ 𝐴 ) ) : ( 𝐹 “ 𝐴 ) –1-1→ 𝐵 )
26 24 25 sylan2 ⊢ ( ( ( I ↾ ( 𝐹 “ 𝐴 ) ) : ( 𝐹 “ 𝐴 ) –1-1→ ( 𝐹 “ 𝐴 ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( I ↾ ( 𝐹 “ 𝐴 ) ) : ( 𝐹 “ 𝐴 ) –1-1→ 𝐵 )
27 26 ex ⊢ ( ( I ↾ ( 𝐹 “ 𝐴 ) ) : ( 𝐹 “ 𝐴 ) –1-1→ ( 𝐹 “ 𝐴 ) → ( 𝐹 : 𝐴 ⟶ 𝐵 → ( I ↾ ( 𝐹 “ 𝐴 ) ) : ( 𝐹 “ 𝐴 ) –1-1→ 𝐵 ) )
28 22 23 27 mp2b ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( I ↾ ( 𝐹 “ 𝐴 ) ) : ( 𝐹 “ 𝐴 ) –1-1→ 𝐵 )
29 28 adantr ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ( I ↾ ( 𝐹 “ 𝐴 ) ) : ( 𝐹 “ 𝐴 ) –1-1→ 𝐵 )
30 18 21 29 3jca ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝑎 ∈ 𝐴 ↦ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) : 𝐴 –onto→ 𝑃 ∧ ( 𝑦 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑦 ) ) : 𝑃 –1-1-onto→ ( 𝐹 “ 𝐴 ) ∧ ( I ↾ ( 𝐹 “ 𝐴 ) ) : ( 𝐹 “ 𝐴 ) –1-1→ 𝐵 ) )
31 12 adantr ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → 𝐹 Fn 𝐴 )
32 uniimaprimaeqfv ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑎 ∈ 𝐴 ) → ∪ ( 𝐹 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) = ( 𝐹 ‘ 𝑎 ) )
33 31 32 sylan ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑎 ∈ 𝐴 ) → ∪ ( 𝐹 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) = ( 𝐹 ‘ 𝑎 ) )
34 33 fveq2d ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑎 ∈ 𝐴 ) → ( ( I ↾ ( 𝐹 “ 𝐴 ) ) ‘ ∪ ( 𝐹 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) ) = ( ( I ↾ ( 𝐹 “ 𝐴 ) ) ‘ ( 𝐹 ‘ 𝑎 ) ) )
35 34 mpteq2dva ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ( 𝑎 ∈ 𝐴 ↦ ( ( I ↾ ( 𝐹 “ 𝐴 ) ) ‘ ∪ ( 𝐹 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) ) ) = ( 𝑎 ∈ 𝐴 ↦ ( ( I ↾ ( 𝐹 “ 𝐴 ) ) ‘ ( 𝐹 ‘ 𝑎 ) ) ) )
36 ffrn ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 : 𝐴 ⟶ ran 𝐹 )
37 36 adantr ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → 𝐹 : 𝐴 ⟶ ran 𝐹 )
38 37 funfvima2d ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑎 ) ∈ ( 𝐹 “ 𝐴 ) )
39 fvresi ⊢ ( ( 𝐹 ‘ 𝑎 ) ∈ ( 𝐹 “ 𝐴 ) → ( ( I ↾ ( 𝐹 “ 𝐴 ) ) ‘ ( 𝐹 ‘ 𝑎 ) ) = ( 𝐹 ‘ 𝑎 ) )
40 38 39 syl ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑎 ∈ 𝐴 ) → ( ( I ↾ ( 𝐹 “ 𝐴 ) ) ‘ ( 𝐹 ‘ 𝑎 ) ) = ( 𝐹 ‘ 𝑎 ) )
41 40 mpteq2dva ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ( 𝑎 ∈ 𝐴 ↦ ( ( I ↾ ( 𝐹 “ 𝐴 ) ) ‘ ( 𝐹 ‘ 𝑎 ) ) ) = ( 𝑎 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑎 ) ) )
42 35 41 eqtrd ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ( 𝑎 ∈ 𝐴 ↦ ( ( I ↾ ( 𝐹 “ 𝐴 ) ) ‘ ∪ ( 𝐹 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) ) ) = ( 𝑎 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑎 ) ) )
43 12 ad2antrr ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑎 ∈ 𝐴 ) → 𝐹 Fn 𝐴 )
44 2 adantr ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑎 ∈ 𝐴 ) → 𝐴 ∈ 𝑉 )
45 simpr ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑎 ∈ 𝐴 ) → 𝑎 ∈ 𝐴 )
46 1 preimafvelsetpreimafv ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ∧ 𝑎 ∈ 𝐴 ) → ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ∈ 𝑃 )
47 43 44 45 46 syl3anc ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑎 ∈ 𝐴 ) → ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ∈ 𝑃 )
48 eqidd ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ( 𝑎 ∈ 𝐴 ↦ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) = ( 𝑎 ∈ 𝐴 ↦ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) )
49 eqidd ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ( 𝑦 ∈ 𝑃 ↦ ( ( I ↾ ( 𝐹 “ 𝐴 ) ) ‘ ∪ ( 𝐹 “ 𝑦 ) ) ) = ( 𝑦 ∈ 𝑃 ↦ ( ( I ↾ ( 𝐹 “ 𝐴 ) ) ‘ ∪ ( 𝐹 “ 𝑦 ) ) ) )
50 imaeq2 ⊢ ( 𝑦 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) → ( 𝐹 “ 𝑦 ) = ( 𝐹 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) )
51 50 unieqd ⊢ ( 𝑦 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) → ∪ ( 𝐹 “ 𝑦 ) = ∪ ( 𝐹 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) )
52 51 fveq2d ⊢ ( 𝑦 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) → ( ( I ↾ ( 𝐹 “ 𝐴 ) ) ‘ ∪ ( 𝐹 “ 𝑦 ) ) = ( ( I ↾ ( 𝐹 “ 𝐴 ) ) ‘ ∪ ( 𝐹 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) ) )
53 47 48 49 52 fmptco ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝑦 ∈ 𝑃 ↦ ( ( I ↾ ( 𝐹 “ 𝐴 ) ) ‘ ∪ ( 𝐹 “ 𝑦 ) ) ) ∘ ( 𝑎 ∈ 𝐴 ↦ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) ) = ( 𝑎 ∈ 𝐴 ↦ ( ( I ↾ ( 𝐹 “ 𝐴 ) ) ‘ ∪ ( 𝐹 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) ) ) )
54 dffn5 ⊢ ( 𝐹 Fn 𝐴 ↔ 𝐹 = ( 𝑎 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑎 ) ) )
55 12 54 sylib ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 = ( 𝑎 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑎 ) ) )
56 55 adantr ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → 𝐹 = ( 𝑎 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑎 ) ) )
57 42 53 56 3eqtr4rd ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → 𝐹 = ( ( 𝑦 ∈ 𝑃 ↦ ( ( I ↾ ( 𝐹 “ 𝐴 ) ) ‘ ∪ ( 𝐹 “ 𝑦 ) ) ) ∘ ( 𝑎 ∈ 𝐴 ↦ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) ) )
58 f1of ⊢ ( ( I ↾ ( 𝐹 “ 𝐴 ) ) : ( 𝐹 “ 𝐴 ) –1-1-onto→ ( 𝐹 “ 𝐴 ) → ( I ↾ ( 𝐹 “ 𝐴 ) ) : ( 𝐹 “ 𝐴 ) ⟶ ( 𝐹 “ 𝐴 ) )
59 22 58 mp1i ⊢ ( 𝐹 Fn 𝐴 → ( I ↾ ( 𝐹 “ 𝐴 ) ) : ( 𝐹 “ 𝐴 ) ⟶ ( 𝐹 “ 𝐴 ) )
60 fnima ⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 “ 𝐴 ) = ran 𝐹 )
61 60 eqcomd ⊢ ( 𝐹 Fn 𝐴 → ran 𝐹 = ( 𝐹 “ 𝐴 ) )
62 61 feq2d ⊢ ( 𝐹 Fn 𝐴 → ( ( I ↾ ( 𝐹 “ 𝐴 ) ) : ran 𝐹 ⟶ ( 𝐹 “ 𝐴 ) ↔ ( I ↾ ( 𝐹 “ 𝐴 ) ) : ( 𝐹 “ 𝐴 ) ⟶ ( 𝐹 “ 𝐴 ) ) )
63 59 62 mpbird ⊢ ( 𝐹 Fn 𝐴 → ( I ↾ ( 𝐹 “ 𝐴 ) ) : ran 𝐹 ⟶ ( 𝐹 “ 𝐴 ) )
64 1 uniimaelsetpreimafv ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝑃 ) → ∪ ( 𝐹 “ 𝑦 ) ∈ ran 𝐹 )
65 63 64 cofmpt ⊢ ( 𝐹 Fn 𝐴 → ( ( I ↾ ( 𝐹 “ 𝐴 ) ) ∘ ( 𝑦 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑦 ) ) ) = ( 𝑦 ∈ 𝑃 ↦ ( ( I ↾ ( 𝐹 “ 𝐴 ) ) ‘ ∪ ( 𝐹 “ 𝑦 ) ) ) )
66 65 eqcomd ⊢ ( 𝐹 Fn 𝐴 → ( 𝑦 ∈ 𝑃 ↦ ( ( I ↾ ( 𝐹 “ 𝐴 ) ) ‘ ∪ ( 𝐹 “ 𝑦 ) ) ) = ( ( I ↾ ( 𝐹 “ 𝐴 ) ) ∘ ( 𝑦 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑦 ) ) ) )
67 31 66 syl ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ( 𝑦 ∈ 𝑃 ↦ ( ( I ↾ ( 𝐹 “ 𝐴 ) ) ‘ ∪ ( 𝐹 “ 𝑦 ) ) ) = ( ( I ↾ ( 𝐹 “ 𝐴 ) ) ∘ ( 𝑦 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑦 ) ) ) )
68 67 coeq1d ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝑦 ∈ 𝑃 ↦ ( ( I ↾ ( 𝐹 “ 𝐴 ) ) ‘ ∪ ( 𝐹 “ 𝑦 ) ) ) ∘ ( 𝑎 ∈ 𝐴 ↦ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) ) = ( ( ( I ↾ ( 𝐹 “ 𝐴 ) ) ∘ ( 𝑦 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑦 ) ) ) ∘ ( 𝑎 ∈ 𝐴 ↦ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) ) )
69 57 68 eqtrd ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → 𝐹 = ( ( ( I ↾ ( 𝐹 “ 𝐴 ) ) ∘ ( 𝑦 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑦 ) ) ) ∘ ( 𝑎 ∈ 𝐴 ↦ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) ) )
70 30 69 jca ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ( ( ( 𝑎 ∈ 𝐴 ↦ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) : 𝐴 –onto→ 𝑃 ∧ ( 𝑦 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑦 ) ) : 𝑃 –1-1-onto→ ( 𝐹 “ 𝐴 ) ∧ ( I ↾ ( 𝐹 “ 𝐴 ) ) : ( 𝐹 “ 𝐴 ) –1-1→ 𝐵 ) ∧ 𝐹 = ( ( ( I ↾ ( 𝐹 “ 𝐴 ) ) ∘ ( 𝑦 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑦 ) ) ) ∘ ( 𝑎 ∈ 𝐴 ↦ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) ) ) )
71 foeq1 ⊢ ( 𝑔 = ( 𝑎 ∈ 𝐴 ↦ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) → ( 𝑔 : 𝐴 –onto→ 𝑃 ↔ ( 𝑎 ∈ 𝐴 ↦ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) : 𝐴 –onto→ 𝑃 ) )
72 71 3ad2ant1 ⊢ ( ( 𝑔 = ( 𝑎 ∈ 𝐴 ↦ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) ∧ ℎ = ( 𝑦 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑦 ) ) ∧ 𝑖 = ( I ↾ ( 𝐹 “ 𝐴 ) ) ) → ( 𝑔 : 𝐴 –onto→ 𝑃 ↔ ( 𝑎 ∈ 𝐴 ↦ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) : 𝐴 –onto→ 𝑃 ) )
73 f1oeq1 ⊢ ( ℎ = ( 𝑦 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑦 ) ) → ( ℎ : 𝑃 –1-1-onto→ ( 𝐹 “ 𝐴 ) ↔ ( 𝑦 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑦 ) ) : 𝑃 –1-1-onto→ ( 𝐹 “ 𝐴 ) ) )
74 73 3ad2ant2 ⊢ ( ( 𝑔 = ( 𝑎 ∈ 𝐴 ↦ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) ∧ ℎ = ( 𝑦 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑦 ) ) ∧ 𝑖 = ( I ↾ ( 𝐹 “ 𝐴 ) ) ) → ( ℎ : 𝑃 –1-1-onto→ ( 𝐹 “ 𝐴 ) ↔ ( 𝑦 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑦 ) ) : 𝑃 –1-1-onto→ ( 𝐹 “ 𝐴 ) ) )
75 f1eq1 ⊢ ( 𝑖 = ( I ↾ ( 𝐹 “ 𝐴 ) ) → ( 𝑖 : ( 𝐹 “ 𝐴 ) –1-1→ 𝐵 ↔ ( I ↾ ( 𝐹 “ 𝐴 ) ) : ( 𝐹 “ 𝐴 ) –1-1→ 𝐵 ) )
76 75 3ad2ant3 ⊢ ( ( 𝑔 = ( 𝑎 ∈ 𝐴 ↦ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) ∧ ℎ = ( 𝑦 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑦 ) ) ∧ 𝑖 = ( I ↾ ( 𝐹 “ 𝐴 ) ) ) → ( 𝑖 : ( 𝐹 “ 𝐴 ) –1-1→ 𝐵 ↔ ( I ↾ ( 𝐹 “ 𝐴 ) ) : ( 𝐹 “ 𝐴 ) –1-1→ 𝐵 ) )
77 72 74 76 3anbi123d ⊢ ( ( 𝑔 = ( 𝑎 ∈ 𝐴 ↦ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) ∧ ℎ = ( 𝑦 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑦 ) ) ∧ 𝑖 = ( I ↾ ( 𝐹 “ 𝐴 ) ) ) → ( ( 𝑔 : 𝐴 –onto→ 𝑃 ∧ ℎ : 𝑃 –1-1-onto→ ( 𝐹 “ 𝐴 ) ∧ 𝑖 : ( 𝐹 “ 𝐴 ) –1-1→ 𝐵 ) ↔ ( ( 𝑎 ∈ 𝐴 ↦ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) : 𝐴 –onto→ 𝑃 ∧ ( 𝑦 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑦 ) ) : 𝑃 –1-1-onto→ ( 𝐹 “ 𝐴 ) ∧ ( I ↾ ( 𝐹 “ 𝐴 ) ) : ( 𝐹 “ 𝐴 ) –1-1→ 𝐵 ) ) )
78 simp3 ⊢ ( ( 𝑔 = ( 𝑎 ∈ 𝐴 ↦ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) ∧ ℎ = ( 𝑦 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑦 ) ) ∧ 𝑖 = ( I ↾ ( 𝐹 “ 𝐴 ) ) ) → 𝑖 = ( I ↾ ( 𝐹 “ 𝐴 ) ) )
79 simp2 ⊢ ( ( 𝑔 = ( 𝑎 ∈ 𝐴 ↦ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) ∧ ℎ = ( 𝑦 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑦 ) ) ∧ 𝑖 = ( I ↾ ( 𝐹 “ 𝐴 ) ) ) → ℎ = ( 𝑦 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑦 ) ) )
80 78 79 coeq12d ⊢ ( ( 𝑔 = ( 𝑎 ∈ 𝐴 ↦ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) ∧ ℎ = ( 𝑦 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑦 ) ) ∧ 𝑖 = ( I ↾ ( 𝐹 “ 𝐴 ) ) ) → ( 𝑖 ∘ ℎ ) = ( ( I ↾ ( 𝐹 “ 𝐴 ) ) ∘ ( 𝑦 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑦 ) ) ) )
81 simp1 ⊢ ( ( 𝑔 = ( 𝑎 ∈ 𝐴 ↦ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) ∧ ℎ = ( 𝑦 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑦 ) ) ∧ 𝑖 = ( I ↾ ( 𝐹 “ 𝐴 ) ) ) → 𝑔 = ( 𝑎 ∈ 𝐴 ↦ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) )
82 80 81 coeq12d ⊢ ( ( 𝑔 = ( 𝑎 ∈ 𝐴 ↦ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) ∧ ℎ = ( 𝑦 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑦 ) ) ∧ 𝑖 = ( I ↾ ( 𝐹 “ 𝐴 ) ) ) → ( ( 𝑖 ∘ ℎ ) ∘ 𝑔 ) = ( ( ( I ↾ ( 𝐹 “ 𝐴 ) ) ∘ ( 𝑦 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑦 ) ) ) ∘ ( 𝑎 ∈ 𝐴 ↦ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) ) )
83 82 eqeq2d ⊢ ( ( 𝑔 = ( 𝑎 ∈ 𝐴 ↦ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) ∧ ℎ = ( 𝑦 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑦 ) ) ∧ 𝑖 = ( I ↾ ( 𝐹 “ 𝐴 ) ) ) → ( 𝐹 = ( ( 𝑖 ∘ ℎ ) ∘ 𝑔 ) ↔ 𝐹 = ( ( ( I ↾ ( 𝐹 “ 𝐴 ) ) ∘ ( 𝑦 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑦 ) ) ) ∘ ( 𝑎 ∈ 𝐴 ↦ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) ) ) )
84 77 83 anbi12d ⊢ ( ( 𝑔 = ( 𝑎 ∈ 𝐴 ↦ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) ∧ ℎ = ( 𝑦 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑦 ) ) ∧ 𝑖 = ( I ↾ ( 𝐹 “ 𝐴 ) ) ) → ( ( ( 𝑔 : 𝐴 –onto→ 𝑃 ∧ ℎ : 𝑃 –1-1-onto→ ( 𝐹 “ 𝐴 ) ∧ 𝑖 : ( 𝐹 “ 𝐴 ) –1-1→ 𝐵 ) ∧ 𝐹 = ( ( 𝑖 ∘ ℎ ) ∘ 𝑔 ) ) ↔ ( ( ( 𝑎 ∈ 𝐴 ↦ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) : 𝐴 –onto→ 𝑃 ∧ ( 𝑦 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑦 ) ) : 𝑃 –1-1-onto→ ( 𝐹 “ 𝐴 ) ∧ ( I ↾ ( 𝐹 “ 𝐴 ) ) : ( 𝐹 “ 𝐴 ) –1-1→ 𝐵 ) ∧ 𝐹 = ( ( ( I ↾ ( 𝐹 “ 𝐴 ) ) ∘ ( 𝑦 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑦 ) ) ) ∘ ( 𝑎 ∈ 𝐴 ↦ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) ) ) ) )
85 84 spc3egv ⊢ ( ( ( 𝑎 ∈ 𝐴 ↦ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) ∈ V ∧ ( 𝑦 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑦 ) ) ∈ V ∧ ( I ↾ ( 𝐹 “ 𝐴 ) ) ∈ V ) → ( ( ( ( 𝑎 ∈ 𝐴 ↦ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) : 𝐴 –onto→ 𝑃 ∧ ( 𝑦 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑦 ) ) : 𝑃 –1-1-onto→ ( 𝐹 “ 𝐴 ) ∧ ( I ↾ ( 𝐹 “ 𝐴 ) ) : ( 𝐹 “ 𝐴 ) –1-1→ 𝐵 ) ∧ 𝐹 = ( ( ( I ↾ ( 𝐹 “ 𝐴 ) ) ∘ ( 𝑦 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑦 ) ) ) ∘ ( 𝑎 ∈ 𝐴 ↦ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) ) ) → ∃ 𝑔 ∃ ℎ ∃ 𝑖 ( ( 𝑔 : 𝐴 –onto→ 𝑃 ∧ ℎ : 𝑃 –1-1-onto→ ( 𝐹 “ 𝐴 ) ∧ 𝑖 : ( 𝐹 “ 𝐴 ) –1-1→ 𝐵 ) ∧ 𝐹 = ( ( 𝑖 ∘ ℎ ) ∘ 𝑔 ) ) ) )
86 11 70 85 sylc ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ∃ 𝑔 ∃ ℎ ∃ 𝑖 ( ( 𝑔 : 𝐴 –onto→ 𝑃 ∧ ℎ : 𝑃 –1-1-onto→ ( 𝐹 “ 𝐴 ) ∧ 𝑖 : ( 𝐹 “ 𝐴 ) –1-1→ 𝐵 ) ∧ 𝐹 = ( ( 𝑖 ∘ ℎ ) ∘ 𝑔 ) ) )