Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fundcmpsurbijinjpreimafv Structured version   Visualization version   GIF version

Theorem fundcmpsurbijinjpreimafv 47331
Description: Every function 𝐹:𝐴𝐵 can be decomposed into a surjective function onto 𝑃, a bijective function from 𝑃 and an injective function into the codomain of 𝐹. (Contributed by AV, 22-Mar-2024.)
Hypothesis
Ref Expression
fundcmpsurinj.p 𝑃 = {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝐹 “ {(𝐹𝑥)})}
Assertion
Ref Expression
fundcmpsurbijinjpreimafv ((𝐹:𝐴𝐵𝐴𝑉) → ∃𝑔𝑖((𝑔:𝐴onto𝑃:𝑃1-1-onto→(𝐹𝐴) ∧ 𝑖:(𝐹𝐴)–1-1𝐵) ∧ 𝐹 = ((𝑖) ∘ 𝑔)))
Distinct variable groups:   𝑥,𝐴,𝑧   𝑥,𝐹,𝑧   𝐴,𝑖,𝑔,   𝐵,𝑔,,𝑖   𝑥,𝐵,𝑧   𝑖,𝐹,𝑔,   𝑃,𝑖,𝑔,   𝑥,𝑃,𝑔,   𝑥,𝑉
Allowed substitution hints:   𝑃(𝑧)   𝑉(𝑧,𝑔,,𝑖)

Proof of Theorem fundcmpsurbijinjpreimafv
Dummy variables 𝑎 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 484 . . . 4 ((𝐹:𝐴𝐵𝐴𝑉) → 𝐴𝑉)
21mptexd 7243 . . 3 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∈ V)
3 fundcmpsurinj.p . . . . . 6 𝑃 = {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝐹 “ {(𝐹𝑥)})}
43setpreimafvex 47307 . . . . 5 (𝐴𝑉𝑃 ∈ V)
54adantl 481 . . . 4 ((𝐹:𝐴𝐵𝐴𝑉) → 𝑃 ∈ V)
65mptexd 7243 . . 3 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑦𝑃 (𝐹𝑦)) ∈ V)
7 ffun 6739 . . . . 5 (𝐹:𝐴𝐵 → Fun 𝐹)
8 funimaexg 6653 . . . . 5 ((Fun 𝐹𝐴𝑉) → (𝐹𝐴) ∈ V)
97, 8sylan 580 . . . 4 ((𝐹:𝐴𝐵𝐴𝑉) → (𝐹𝐴) ∈ V)
109resiexd 7235 . . 3 ((𝐹:𝐴𝐵𝐴𝑉) → ( I ↾ (𝐹𝐴)) ∈ V)
112, 6, 103jca 1127 . 2 ((𝐹:𝐴𝐵𝐴𝑉) → ((𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∈ V ∧ (𝑦𝑃 (𝐹𝑦)) ∈ V ∧ ( I ↾ (𝐹𝐴)) ∈ V))
12 ffn 6736 . . . . 5 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
13 fveq2 6906 . . . . . . . . 9 (𝑎 = 𝑥 → (𝐹𝑎) = (𝐹𝑥))
1413sneqd 4642 . . . . . . . 8 (𝑎 = 𝑥 → {(𝐹𝑎)} = {(𝐹𝑥)})
1514imaeq2d 6079 . . . . . . 7 (𝑎 = 𝑥 → (𝐹 “ {(𝐹𝑎)}) = (𝐹 “ {(𝐹𝑥)}))
1615cbvmptv 5260 . . . . . 6 (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) = (𝑥𝐴 ↦ (𝐹 “ {(𝐹𝑥)}))
173, 16fundcmpsurinjlem2 47323 . . . . 5 ((𝐹 Fn 𝐴𝐴𝑉) → (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})):𝐴onto𝑃)
1812, 17sylan 580 . . . 4 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})):𝐴onto𝑃)
19 eqid 2734 . . . . . 6 (𝑦𝑃 (𝐹𝑦)) = (𝑦𝑃 (𝐹𝑦))
203, 19imasetpreimafvbij 47330 . . . . 5 ((𝐹 Fn 𝐴𝐴𝑉) → (𝑦𝑃 (𝐹𝑦)):𝑃1-1-onto→(𝐹𝐴))
2112, 20sylan 580 . . . 4 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑦𝑃 (𝐹𝑦)):𝑃1-1-onto→(𝐹𝐴))
22 f1oi 6886 . . . . . 6 ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1-onto→(𝐹𝐴)
23 f1of1 6847 . . . . . 6 (( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1-onto→(𝐹𝐴) → ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1→(𝐹𝐴))
24 fimass 6756 . . . . . . . 8 (𝐹:𝐴𝐵 → (𝐹𝐴) ⊆ 𝐵)
25 f1ss 6809 . . . . . . . 8 ((( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1→(𝐹𝐴) ∧ (𝐹𝐴) ⊆ 𝐵) → ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1𝐵)
2624, 25sylan2 593 . . . . . . 7 ((( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1→(𝐹𝐴) ∧ 𝐹:𝐴𝐵) → ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1𝐵)
2726ex 412 . . . . . 6 (( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1→(𝐹𝐴) → (𝐹:𝐴𝐵 → ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1𝐵))
2822, 23, 27mp2b 10 . . . . 5 (𝐹:𝐴𝐵 → ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1𝐵)
2928adantr 480 . . . 4 ((𝐹:𝐴𝐵𝐴𝑉) → ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1𝐵)
3018, 21, 293jca 1127 . . 3 ((𝐹:𝐴𝐵𝐴𝑉) → ((𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})):𝐴onto𝑃 ∧ (𝑦𝑃 (𝐹𝑦)):𝑃1-1-onto→(𝐹𝐴) ∧ ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1𝐵))
3112adantr 480 . . . . . . . . 9 ((𝐹:𝐴𝐵𝐴𝑉) → 𝐹 Fn 𝐴)
32 uniimaprimaeqfv 47306 . . . . . . . . 9 ((𝐹 Fn 𝐴𝑎𝐴) → (𝐹 “ (𝐹 “ {(𝐹𝑎)})) = (𝐹𝑎))
3331, 32sylan 580 . . . . . . . 8 (((𝐹:𝐴𝐵𝐴𝑉) ∧ 𝑎𝐴) → (𝐹 “ (𝐹 “ {(𝐹𝑎)})) = (𝐹𝑎))
3433fveq2d 6910 . . . . . . 7 (((𝐹:𝐴𝐵𝐴𝑉) ∧ 𝑎𝐴) → (( I ↾ (𝐹𝐴))‘ (𝐹 “ (𝐹 “ {(𝐹𝑎)}))) = (( I ↾ (𝐹𝐴))‘(𝐹𝑎)))
3534mpteq2dva 5247 . . . . . 6 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑎𝐴 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹 “ (𝐹 “ {(𝐹𝑎)})))) = (𝑎𝐴 ↦ (( I ↾ (𝐹𝐴))‘(𝐹𝑎))))
36 ffrn 6749 . . . . . . . . . 10 (𝐹:𝐴𝐵𝐹:𝐴⟶ran 𝐹)
3736adantr 480 . . . . . . . . 9 ((𝐹:𝐴𝐵𝐴𝑉) → 𝐹:𝐴⟶ran 𝐹)
3837funfvima2d 7251 . . . . . . . 8 (((𝐹:𝐴𝐵𝐴𝑉) ∧ 𝑎𝐴) → (𝐹𝑎) ∈ (𝐹𝐴))
39 fvresi 7192 . . . . . . . 8 ((𝐹𝑎) ∈ (𝐹𝐴) → (( I ↾ (𝐹𝐴))‘(𝐹𝑎)) = (𝐹𝑎))
4038, 39syl 17 . . . . . . 7 (((𝐹:𝐴𝐵𝐴𝑉) ∧ 𝑎𝐴) → (( I ↾ (𝐹𝐴))‘(𝐹𝑎)) = (𝐹𝑎))
4140mpteq2dva 5247 . . . . . 6 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑎𝐴 ↦ (( I ↾ (𝐹𝐴))‘(𝐹𝑎))) = (𝑎𝐴 ↦ (𝐹𝑎)))
4235, 41eqtrd 2774 . . . . 5 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑎𝐴 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹 “ (𝐹 “ {(𝐹𝑎)})))) = (𝑎𝐴 ↦ (𝐹𝑎)))
4312ad2antrr 726 . . . . . . 7 (((𝐹:𝐴𝐵𝐴𝑉) ∧ 𝑎𝐴) → 𝐹 Fn 𝐴)
441adantr 480 . . . . . . 7 (((𝐹:𝐴𝐵𝐴𝑉) ∧ 𝑎𝐴) → 𝐴𝑉)
45 simpr 484 . . . . . . 7 (((𝐹:𝐴𝐵𝐴𝑉) ∧ 𝑎𝐴) → 𝑎𝐴)
463preimafvelsetpreimafv 47312 . . . . . . 7 ((𝐹 Fn 𝐴𝐴𝑉𝑎𝐴) → (𝐹 “ {(𝐹𝑎)}) ∈ 𝑃)
4743, 44, 45, 46syl3anc 1370 . . . . . 6 (((𝐹:𝐴𝐵𝐴𝑉) ∧ 𝑎𝐴) → (𝐹 “ {(𝐹𝑎)}) ∈ 𝑃)
48 eqidd 2735 . . . . . 6 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})))
49 eqidd 2735 . . . . . 6 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑦𝑃 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹𝑦))) = (𝑦𝑃 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹𝑦))))
50 imaeq2 6075 . . . . . . . 8 (𝑦 = (𝐹 “ {(𝐹𝑎)}) → (𝐹𝑦) = (𝐹 “ (𝐹 “ {(𝐹𝑎)})))
5150unieqd 4924 . . . . . . 7 (𝑦 = (𝐹 “ {(𝐹𝑎)}) → (𝐹𝑦) = (𝐹 “ (𝐹 “ {(𝐹𝑎)})))
5251fveq2d 6910 . . . . . 6 (𝑦 = (𝐹 “ {(𝐹𝑎)}) → (( I ↾ (𝐹𝐴))‘ (𝐹𝑦)) = (( I ↾ (𝐹𝐴))‘ (𝐹 “ (𝐹 “ {(𝐹𝑎)}))))
5347, 48, 49, 52fmptco 7148 . . . . 5 ((𝐹:𝐴𝐵𝐴𝑉) → ((𝑦𝑃 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹𝑦))) ∘ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)}))) = (𝑎𝐴 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹 “ (𝐹 “ {(𝐹𝑎)})))))
54 dffn5 6966 . . . . . . 7 (𝐹 Fn 𝐴𝐹 = (𝑎𝐴 ↦ (𝐹𝑎)))
5512, 54sylib 218 . . . . . 6 (𝐹:𝐴𝐵𝐹 = (𝑎𝐴 ↦ (𝐹𝑎)))
5655adantr 480 . . . . 5 ((𝐹:𝐴𝐵𝐴𝑉) → 𝐹 = (𝑎𝐴 ↦ (𝐹𝑎)))
5742, 53, 563eqtr4rd 2785 . . . 4 ((𝐹:𝐴𝐵𝐴𝑉) → 𝐹 = ((𝑦𝑃 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹𝑦))) ∘ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)}))))
58 f1of 6848 . . . . . . . . . 10 (( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1-onto→(𝐹𝐴) → ( I ↾ (𝐹𝐴)):(𝐹𝐴)⟶(𝐹𝐴))
5922, 58mp1i 13 . . . . . . . . 9 (𝐹 Fn 𝐴 → ( I ↾ (𝐹𝐴)):(𝐹𝐴)⟶(𝐹𝐴))
60 fnima 6698 . . . . . . . . . . 11 (𝐹 Fn 𝐴 → (𝐹𝐴) = ran 𝐹)
6160eqcomd 2740 . . . . . . . . . 10 (𝐹 Fn 𝐴 → ran 𝐹 = (𝐹𝐴))
6261feq2d 6722 . . . . . . . . 9 (𝐹 Fn 𝐴 → (( I ↾ (𝐹𝐴)):ran 𝐹⟶(𝐹𝐴) ↔ ( I ↾ (𝐹𝐴)):(𝐹𝐴)⟶(𝐹𝐴)))
6359, 62mpbird 257 . . . . . . . 8 (𝐹 Fn 𝐴 → ( I ↾ (𝐹𝐴)):ran 𝐹⟶(𝐹𝐴))
643uniimaelsetpreimafv 47320 . . . . . . . 8 ((𝐹 Fn 𝐴𝑦𝑃) → (𝐹𝑦) ∈ ran 𝐹)
6563, 64cofmpt 7151 . . . . . . 7 (𝐹 Fn 𝐴 → (( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))) = (𝑦𝑃 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹𝑦))))
6665eqcomd 2740 . . . . . 6 (𝐹 Fn 𝐴 → (𝑦𝑃 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹𝑦))) = (( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))))
6731, 66syl 17 . . . . 5 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑦𝑃 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹𝑦))) = (( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))))
6867coeq1d 5874 . . . 4 ((𝐹:𝐴𝐵𝐴𝑉) → ((𝑦𝑃 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹𝑦))) ∘ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)}))) = ((( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))) ∘ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)}))))
6957, 68eqtrd 2774 . . 3 ((𝐹:𝐴𝐵𝐴𝑉) → 𝐹 = ((( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))) ∘ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)}))))
7030, 69jca 511 . 2 ((𝐹:𝐴𝐵𝐴𝑉) → (((𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})):𝐴onto𝑃 ∧ (𝑦𝑃 (𝐹𝑦)):𝑃1-1-onto→(𝐹𝐴) ∧ ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1𝐵) ∧ 𝐹 = ((( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))) ∘ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})))))
71 foeq1 6816 . . . . . 6 (𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) → (𝑔:𝐴onto𝑃 ↔ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})):𝐴onto𝑃))
72713ad2ant1 1132 . . . . 5 ((𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∧ = (𝑦𝑃 (𝐹𝑦)) ∧ 𝑖 = ( I ↾ (𝐹𝐴))) → (𝑔:𝐴onto𝑃 ↔ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})):𝐴onto𝑃))
73 f1oeq1 6836 . . . . . 6 ( = (𝑦𝑃 (𝐹𝑦)) → (:𝑃1-1-onto→(𝐹𝐴) ↔ (𝑦𝑃 (𝐹𝑦)):𝑃1-1-onto→(𝐹𝐴)))
74733ad2ant2 1133 . . . . 5 ((𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∧ = (𝑦𝑃 (𝐹𝑦)) ∧ 𝑖 = ( I ↾ (𝐹𝐴))) → (:𝑃1-1-onto→(𝐹𝐴) ↔ (𝑦𝑃 (𝐹𝑦)):𝑃1-1-onto→(𝐹𝐴)))
75 f1eq1 6799 . . . . . 6 (𝑖 = ( I ↾ (𝐹𝐴)) → (𝑖:(𝐹𝐴)–1-1𝐵 ↔ ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1𝐵))
76753ad2ant3 1134 . . . . 5 ((𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∧ = (𝑦𝑃 (𝐹𝑦)) ∧ 𝑖 = ( I ↾ (𝐹𝐴))) → (𝑖:(𝐹𝐴)–1-1𝐵 ↔ ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1𝐵))
7772, 74, 763anbi123d 1435 . . . 4 ((𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∧ = (𝑦𝑃 (𝐹𝑦)) ∧ 𝑖 = ( I ↾ (𝐹𝐴))) → ((𝑔:𝐴onto𝑃:𝑃1-1-onto→(𝐹𝐴) ∧ 𝑖:(𝐹𝐴)–1-1𝐵) ↔ ((𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})):𝐴onto𝑃 ∧ (𝑦𝑃 (𝐹𝑦)):𝑃1-1-onto→(𝐹𝐴) ∧ ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1𝐵)))
78 simp3 1137 . . . . . . 7 ((𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∧ = (𝑦𝑃 (𝐹𝑦)) ∧ 𝑖 = ( I ↾ (𝐹𝐴))) → 𝑖 = ( I ↾ (𝐹𝐴)))
79 simp2 1136 . . . . . . 7 ((𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∧ = (𝑦𝑃 (𝐹𝑦)) ∧ 𝑖 = ( I ↾ (𝐹𝐴))) → = (𝑦𝑃 (𝐹𝑦)))
8078, 79coeq12d 5877 . . . . . 6 ((𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∧ = (𝑦𝑃 (𝐹𝑦)) ∧ 𝑖 = ( I ↾ (𝐹𝐴))) → (𝑖) = (( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))))
81 simp1 1135 . . . . . 6 ((𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∧ = (𝑦𝑃 (𝐹𝑦)) ∧ 𝑖 = ( I ↾ (𝐹𝐴))) → 𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})))
8280, 81coeq12d 5877 . . . . 5 ((𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∧ = (𝑦𝑃 (𝐹𝑦)) ∧ 𝑖 = ( I ↾ (𝐹𝐴))) → ((𝑖) ∘ 𝑔) = ((( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))) ∘ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)}))))
8382eqeq2d 2745 . . . 4 ((𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∧ = (𝑦𝑃 (𝐹𝑦)) ∧ 𝑖 = ( I ↾ (𝐹𝐴))) → (𝐹 = ((𝑖) ∘ 𝑔) ↔ 𝐹 = ((( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))) ∘ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})))))
8477, 83anbi12d 632 . . 3 ((𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∧ = (𝑦𝑃 (𝐹𝑦)) ∧ 𝑖 = ( I ↾ (𝐹𝐴))) → (((𝑔:𝐴onto𝑃:𝑃1-1-onto→(𝐹𝐴) ∧ 𝑖:(𝐹𝐴)–1-1𝐵) ∧ 𝐹 = ((𝑖) ∘ 𝑔)) ↔ (((𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})):𝐴onto𝑃 ∧ (𝑦𝑃 (𝐹𝑦)):𝑃1-1-onto→(𝐹𝐴) ∧ ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1𝐵) ∧ 𝐹 = ((( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))) ∘ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)}))))))
8584spc3egv 3602 . 2 (((𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∈ V ∧ (𝑦𝑃 (𝐹𝑦)) ∈ V ∧ ( I ↾ (𝐹𝐴)) ∈ V) → ((((𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})):𝐴onto𝑃 ∧ (𝑦𝑃 (𝐹𝑦)):𝑃1-1-onto→(𝐹𝐴) ∧ ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1𝐵) ∧ 𝐹 = ((( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))) ∘ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})))) → ∃𝑔𝑖((𝑔:𝐴onto𝑃:𝑃1-1-onto→(𝐹𝐴) ∧ 𝑖:(𝐹𝐴)–1-1𝐵) ∧ 𝐹 = ((𝑖) ∘ 𝑔))))
8611, 70, 85sylc 65 1 ((𝐹:𝐴𝐵𝐴𝑉) → ∃𝑔𝑖((𝑔:𝐴onto𝑃:𝑃1-1-onto→(𝐹𝐴) ∧ 𝑖:(𝐹𝐴)–1-1𝐵) ∧ 𝐹 = ((𝑖) ∘ 𝑔)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1086   = wceq 1536  wex 1775  wcel 2105  {cab 2711  wrex 3067  Vcvv 3477  wss 3962  {csn 4630   cuni 4911  cmpt 5230   I cid 5581  ccnv 5687  ran crn 5689  cres 5690  cima 5691  ccom 5692  Fun wfun 6556   Fn wfn 6557  wf 6558  1-1wf1 6559  ontowfo 6560  1-1-ontowf1o 6561  cfv 6562
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570
This theorem is referenced by:  fundcmpsurinjpreimafv  47332  fundcmpsurbijinj  47334
  Copyright terms: Public domain W3C validator