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 46009
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 486 . . . 4 ((𝐹:𝐴𝐵𝐴𝑉) → 𝐴𝑉)
21mptexd 7220 . . 3 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∈ V)
3 fundcmpsurinj.p . . . . . 6 𝑃 = {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝐹 “ {(𝐹𝑥)})}
43setpreimafvex 45985 . . . . 5 (𝐴𝑉𝑃 ∈ V)
54adantl 483 . . . 4 ((𝐹:𝐴𝐵𝐴𝑉) → 𝑃 ∈ V)
65mptexd 7220 . . 3 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑦𝑃 (𝐹𝑦)) ∈ V)
7 ffun 6716 . . . . 5 (𝐹:𝐴𝐵 → Fun 𝐹)
8 funimaexg 6630 . . . . 5 ((Fun 𝐹𝐴𝑉) → (𝐹𝐴) ∈ V)
97, 8sylan 581 . . . 4 ((𝐹:𝐴𝐵𝐴𝑉) → (𝐹𝐴) ∈ V)
109resiexd 7212 . . 3 ((𝐹:𝐴𝐵𝐴𝑉) → ( I ↾ (𝐹𝐴)) ∈ V)
112, 6, 103jca 1129 . 2 ((𝐹:𝐴𝐵𝐴𝑉) → ((𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∈ V ∧ (𝑦𝑃 (𝐹𝑦)) ∈ V ∧ ( I ↾ (𝐹𝐴)) ∈ V))
12 ffn 6713 . . . . 5 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
13 fveq2 6887 . . . . . . . . 9 (𝑎 = 𝑥 → (𝐹𝑎) = (𝐹𝑥))
1413sneqd 4638 . . . . . . . 8 (𝑎 = 𝑥 → {(𝐹𝑎)} = {(𝐹𝑥)})
1514imaeq2d 6056 . . . . . . 7 (𝑎 = 𝑥 → (𝐹 “ {(𝐹𝑎)}) = (𝐹 “ {(𝐹𝑥)}))
1615cbvmptv 5259 . . . . . 6 (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) = (𝑥𝐴 ↦ (𝐹 “ {(𝐹𝑥)}))
173, 16fundcmpsurinjlem2 46001 . . . . 5 ((𝐹 Fn 𝐴𝐴𝑉) → (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})):𝐴onto𝑃)
1812, 17sylan 581 . . . 4 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})):𝐴onto𝑃)
19 eqid 2733 . . . . . 6 (𝑦𝑃 (𝐹𝑦)) = (𝑦𝑃 (𝐹𝑦))
203, 19imasetpreimafvbij 46008 . . . . 5 ((𝐹 Fn 𝐴𝐴𝑉) → (𝑦𝑃 (𝐹𝑦)):𝑃1-1-onto→(𝐹𝐴))
2112, 20sylan 581 . . . 4 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑦𝑃 (𝐹𝑦)):𝑃1-1-onto→(𝐹𝐴))
22 f1oi 6867 . . . . . 6 ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1-onto→(𝐹𝐴)
23 f1of1 6828 . . . . . 6 (( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1-onto→(𝐹𝐴) → ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1→(𝐹𝐴))
24 fimass 6734 . . . . . . . 8 (𝐹:𝐴𝐵 → (𝐹𝐴) ⊆ 𝐵)
25 f1ss 6789 . . . . . . . 8 ((( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1→(𝐹𝐴) ∧ (𝐹𝐴) ⊆ 𝐵) → ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1𝐵)
2624, 25sylan2 594 . . . . . . 7 ((( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1→(𝐹𝐴) ∧ 𝐹:𝐴𝐵) → ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1𝐵)
2726ex 414 . . . . . 6 (( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1→(𝐹𝐴) → (𝐹:𝐴𝐵 → ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1𝐵))
2822, 23, 27mp2b 10 . . . . 5 (𝐹:𝐴𝐵 → ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1𝐵)
2928adantr 482 . . . 4 ((𝐹:𝐴𝐵𝐴𝑉) → ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1𝐵)
3018, 21, 293jca 1129 . . 3 ((𝐹:𝐴𝐵𝐴𝑉) → ((𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})):𝐴onto𝑃 ∧ (𝑦𝑃 (𝐹𝑦)):𝑃1-1-onto→(𝐹𝐴) ∧ ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1𝐵))
3112adantr 482 . . . . . . . . 9 ((𝐹:𝐴𝐵𝐴𝑉) → 𝐹 Fn 𝐴)
32 uniimaprimaeqfv 45984 . . . . . . . . 9 ((𝐹 Fn 𝐴𝑎𝐴) → (𝐹 “ (𝐹 “ {(𝐹𝑎)})) = (𝐹𝑎))
3331, 32sylan 581 . . . . . . . 8 (((𝐹:𝐴𝐵𝐴𝑉) ∧ 𝑎𝐴) → (𝐹 “ (𝐹 “ {(𝐹𝑎)})) = (𝐹𝑎))
3433fveq2d 6891 . . . . . . 7 (((𝐹:𝐴𝐵𝐴𝑉) ∧ 𝑎𝐴) → (( I ↾ (𝐹𝐴))‘ (𝐹 “ (𝐹 “ {(𝐹𝑎)}))) = (( I ↾ (𝐹𝐴))‘(𝐹𝑎)))
3534mpteq2dva 5246 . . . . . 6 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑎𝐴 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹 “ (𝐹 “ {(𝐹𝑎)})))) = (𝑎𝐴 ↦ (( I ↾ (𝐹𝐴))‘(𝐹𝑎))))
36 ffrn 6727 . . . . . . . . . 10 (𝐹:𝐴𝐵𝐹:𝐴⟶ran 𝐹)
3736adantr 482 . . . . . . . . 9 ((𝐹:𝐴𝐵𝐴𝑉) → 𝐹:𝐴⟶ran 𝐹)
3837funfvima2d 7228 . . . . . . . 8 (((𝐹:𝐴𝐵𝐴𝑉) ∧ 𝑎𝐴) → (𝐹𝑎) ∈ (𝐹𝐴))
39 fvresi 7165 . . . . . . . 8 ((𝐹𝑎) ∈ (𝐹𝐴) → (( I ↾ (𝐹𝐴))‘(𝐹𝑎)) = (𝐹𝑎))
4038, 39syl 17 . . . . . . 7 (((𝐹:𝐴𝐵𝐴𝑉) ∧ 𝑎𝐴) → (( I ↾ (𝐹𝐴))‘(𝐹𝑎)) = (𝐹𝑎))
4140mpteq2dva 5246 . . . . . 6 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑎𝐴 ↦ (( I ↾ (𝐹𝐴))‘(𝐹𝑎))) = (𝑎𝐴 ↦ (𝐹𝑎)))
4235, 41eqtrd 2773 . . . . 5 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑎𝐴 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹 “ (𝐹 “ {(𝐹𝑎)})))) = (𝑎𝐴 ↦ (𝐹𝑎)))
4312ad2antrr 725 . . . . . . 7 (((𝐹:𝐴𝐵𝐴𝑉) ∧ 𝑎𝐴) → 𝐹 Fn 𝐴)
441adantr 482 . . . . . . 7 (((𝐹:𝐴𝐵𝐴𝑉) ∧ 𝑎𝐴) → 𝐴𝑉)
45 simpr 486 . . . . . . 7 (((𝐹:𝐴𝐵𝐴𝑉) ∧ 𝑎𝐴) → 𝑎𝐴)
463preimafvelsetpreimafv 45990 . . . . . . 7 ((𝐹 Fn 𝐴𝐴𝑉𝑎𝐴) → (𝐹 “ {(𝐹𝑎)}) ∈ 𝑃)
4743, 44, 45, 46syl3anc 1372 . . . . . 6 (((𝐹:𝐴𝐵𝐴𝑉) ∧ 𝑎𝐴) → (𝐹 “ {(𝐹𝑎)}) ∈ 𝑃)
48 eqidd 2734 . . . . . 6 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})))
49 eqidd 2734 . . . . . 6 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑦𝑃 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹𝑦))) = (𝑦𝑃 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹𝑦))))
50 imaeq2 6052 . . . . . . . 8 (𝑦 = (𝐹 “ {(𝐹𝑎)}) → (𝐹𝑦) = (𝐹 “ (𝐹 “ {(𝐹𝑎)})))
5150unieqd 4920 . . . . . . 7 (𝑦 = (𝐹 “ {(𝐹𝑎)}) → (𝐹𝑦) = (𝐹 “ (𝐹 “ {(𝐹𝑎)})))
5251fveq2d 6891 . . . . . 6 (𝑦 = (𝐹 “ {(𝐹𝑎)}) → (( I ↾ (𝐹𝐴))‘ (𝐹𝑦)) = (( I ↾ (𝐹𝐴))‘ (𝐹 “ (𝐹 “ {(𝐹𝑎)}))))
5347, 48, 49, 52fmptco 7121 . . . . 5 ((𝐹:𝐴𝐵𝐴𝑉) → ((𝑦𝑃 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹𝑦))) ∘ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)}))) = (𝑎𝐴 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹 “ (𝐹 “ {(𝐹𝑎)})))))
54 dffn5 6946 . . . . . . 7 (𝐹 Fn 𝐴𝐹 = (𝑎𝐴 ↦ (𝐹𝑎)))
5512, 54sylib 217 . . . . . 6 (𝐹:𝐴𝐵𝐹 = (𝑎𝐴 ↦ (𝐹𝑎)))
5655adantr 482 . . . . 5 ((𝐹:𝐴𝐵𝐴𝑉) → 𝐹 = (𝑎𝐴 ↦ (𝐹𝑎)))
5742, 53, 563eqtr4rd 2784 . . . 4 ((𝐹:𝐴𝐵𝐴𝑉) → 𝐹 = ((𝑦𝑃 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹𝑦))) ∘ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)}))))
58 f1of 6829 . . . . . . . . . 10 (( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1-onto→(𝐹𝐴) → ( I ↾ (𝐹𝐴)):(𝐹𝐴)⟶(𝐹𝐴))
5922, 58mp1i 13 . . . . . . . . 9 (𝐹 Fn 𝐴 → ( I ↾ (𝐹𝐴)):(𝐹𝐴)⟶(𝐹𝐴))
60 fnima 6676 . . . . . . . . . . 11 (𝐹 Fn 𝐴 → (𝐹𝐴) = ran 𝐹)
6160eqcomd 2739 . . . . . . . . . 10 (𝐹 Fn 𝐴 → ran 𝐹 = (𝐹𝐴))
6261feq2d 6699 . . . . . . . . 9 (𝐹 Fn 𝐴 → (( I ↾ (𝐹𝐴)):ran 𝐹⟶(𝐹𝐴) ↔ ( I ↾ (𝐹𝐴)):(𝐹𝐴)⟶(𝐹𝐴)))
6359, 62mpbird 257 . . . . . . . 8 (𝐹 Fn 𝐴 → ( I ↾ (𝐹𝐴)):ran 𝐹⟶(𝐹𝐴))
643uniimaelsetpreimafv 45998 . . . . . . . 8 ((𝐹 Fn 𝐴𝑦𝑃) → (𝐹𝑦) ∈ ran 𝐹)
6563, 64cofmpt 7124 . . . . . . 7 (𝐹 Fn 𝐴 → (( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))) = (𝑦𝑃 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹𝑦))))
6665eqcomd 2739 . . . . . 6 (𝐹 Fn 𝐴 → (𝑦𝑃 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹𝑦))) = (( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))))
6731, 66syl 17 . . . . 5 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑦𝑃 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹𝑦))) = (( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))))
6867coeq1d 5858 . . . 4 ((𝐹:𝐴𝐵𝐴𝑉) → ((𝑦𝑃 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹𝑦))) ∘ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)}))) = ((( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))) ∘ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)}))))
6957, 68eqtrd 2773 . . 3 ((𝐹:𝐴𝐵𝐴𝑉) → 𝐹 = ((( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))) ∘ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)}))))
7030, 69jca 513 . 2 ((𝐹:𝐴𝐵𝐴𝑉) → (((𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})):𝐴onto𝑃 ∧ (𝑦𝑃 (𝐹𝑦)):𝑃1-1-onto→(𝐹𝐴) ∧ ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1𝐵) ∧ 𝐹 = ((( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))) ∘ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})))))
71 foeq1 6797 . . . . . 6 (𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) → (𝑔:𝐴onto𝑃 ↔ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})):𝐴onto𝑃))
72713ad2ant1 1134 . . . . 5 ((𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∧ = (𝑦𝑃 (𝐹𝑦)) ∧ 𝑖 = ( I ↾ (𝐹𝐴))) → (𝑔:𝐴onto𝑃 ↔ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})):𝐴onto𝑃))
73 f1oeq1 6817 . . . . . 6 ( = (𝑦𝑃 (𝐹𝑦)) → (:𝑃1-1-onto→(𝐹𝐴) ↔ (𝑦𝑃 (𝐹𝑦)):𝑃1-1-onto→(𝐹𝐴)))
74733ad2ant2 1135 . . . . 5 ((𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∧ = (𝑦𝑃 (𝐹𝑦)) ∧ 𝑖 = ( I ↾ (𝐹𝐴))) → (:𝑃1-1-onto→(𝐹𝐴) ↔ (𝑦𝑃 (𝐹𝑦)):𝑃1-1-onto→(𝐹𝐴)))
75 f1eq1 6778 . . . . . 6 (𝑖 = ( I ↾ (𝐹𝐴)) → (𝑖:(𝐹𝐴)–1-1𝐵 ↔ ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1𝐵))
76753ad2ant3 1136 . . . . 5 ((𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∧ = (𝑦𝑃 (𝐹𝑦)) ∧ 𝑖 = ( I ↾ (𝐹𝐴))) → (𝑖:(𝐹𝐴)–1-1𝐵 ↔ ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1𝐵))
7772, 74, 763anbi123d 1437 . . . 4 ((𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∧ = (𝑦𝑃 (𝐹𝑦)) ∧ 𝑖 = ( I ↾ (𝐹𝐴))) → ((𝑔:𝐴onto𝑃:𝑃1-1-onto→(𝐹𝐴) ∧ 𝑖:(𝐹𝐴)–1-1𝐵) ↔ ((𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})):𝐴onto𝑃 ∧ (𝑦𝑃 (𝐹𝑦)):𝑃1-1-onto→(𝐹𝐴) ∧ ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1𝐵)))
78 simp3 1139 . . . . . . 7 ((𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∧ = (𝑦𝑃 (𝐹𝑦)) ∧ 𝑖 = ( I ↾ (𝐹𝐴))) → 𝑖 = ( I ↾ (𝐹𝐴)))
79 simp2 1138 . . . . . . 7 ((𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∧ = (𝑦𝑃 (𝐹𝑦)) ∧ 𝑖 = ( I ↾ (𝐹𝐴))) → = (𝑦𝑃 (𝐹𝑦)))
8078, 79coeq12d 5861 . . . . . 6 ((𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∧ = (𝑦𝑃 (𝐹𝑦)) ∧ 𝑖 = ( I ↾ (𝐹𝐴))) → (𝑖) = (( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))))
81 simp1 1137 . . . . . 6 ((𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∧ = (𝑦𝑃 (𝐹𝑦)) ∧ 𝑖 = ( I ↾ (𝐹𝐴))) → 𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})))
8280, 81coeq12d 5861 . . . . 5 ((𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∧ = (𝑦𝑃 (𝐹𝑦)) ∧ 𝑖 = ( I ↾ (𝐹𝐴))) → ((𝑖) ∘ 𝑔) = ((( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))) ∘ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)}))))
8382eqeq2d 2744 . . . 4 ((𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∧ = (𝑦𝑃 (𝐹𝑦)) ∧ 𝑖 = ( I ↾ (𝐹𝐴))) → (𝐹 = ((𝑖) ∘ 𝑔) ↔ 𝐹 = ((( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))) ∘ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})))))
8477, 83anbi12d 632 . . 3 ((𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∧ = (𝑦𝑃 (𝐹𝑦)) ∧ 𝑖 = ( I ↾ (𝐹𝐴))) → (((𝑔:𝐴onto𝑃:𝑃1-1-onto→(𝐹𝐴) ∧ 𝑖:(𝐹𝐴)–1-1𝐵) ∧ 𝐹 = ((𝑖) ∘ 𝑔)) ↔ (((𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})):𝐴onto𝑃 ∧ (𝑦𝑃 (𝐹𝑦)):𝑃1-1-onto→(𝐹𝐴) ∧ ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1𝐵) ∧ 𝐹 = ((( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))) ∘ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)}))))))
8584spc3egv 3592 . 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 205  wa 397  w3a 1088   = wceq 1542  wex 1782  wcel 2107  {cab 2710  wrex 3071  Vcvv 3475  wss 3946  {csn 4626   cuni 4906  cmpt 5229   I cid 5571  ccnv 5673  ran crn 5675  cres 5676  cima 5677  ccom 5678  Fun wfun 6533   Fn wfn 6534  wf 6535  1-1wf1 6536  ontowfo 6537  1-1-ontowf1o 6538  cfv 6539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5283  ax-sep 5297  ax-nul 5304  ax-pow 5361  ax-pr 5425  ax-un 7719
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-nul 4321  df-if 4527  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4907  df-iun 4997  df-br 5147  df-opab 5209  df-mpt 5230  df-id 5572  df-xp 5680  df-rel 5681  df-cnv 5682  df-co 5683  df-dm 5684  df-rn 5685  df-res 5686  df-ima 5687  df-iota 6491  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547
This theorem is referenced by:  fundcmpsurinjpreimafv  46010  fundcmpsurbijinj  46012
  Copyright terms: Public domain W3C validator