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 45589
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 485 . . . 4 ((𝐹:𝐴𝐵𝐴𝑉) → 𝐴𝑉)
21mptexd 7174 . . 3 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∈ V)
3 fundcmpsurinj.p . . . . . 6 𝑃 = {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝐹 “ {(𝐹𝑥)})}
43setpreimafvex 45565 . . . . 5 (𝐴𝑉𝑃 ∈ V)
54adantl 482 . . . 4 ((𝐹:𝐴𝐵𝐴𝑉) → 𝑃 ∈ V)
65mptexd 7174 . . 3 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑦𝑃 (𝐹𝑦)) ∈ V)
7 ffun 6671 . . . . 5 (𝐹:𝐴𝐵 → Fun 𝐹)
8 funimaexg 6587 . . . . 5 ((Fun 𝐹𝐴𝑉) → (𝐹𝐴) ∈ V)
97, 8sylan 580 . . . 4 ((𝐹:𝐴𝐵𝐴𝑉) → (𝐹𝐴) ∈ V)
109resiexd 7166 . . 3 ((𝐹:𝐴𝐵𝐴𝑉) → ( I ↾ (𝐹𝐴)) ∈ V)
112, 6, 103jca 1128 . 2 ((𝐹:𝐴𝐵𝐴𝑉) → ((𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∈ V ∧ (𝑦𝑃 (𝐹𝑦)) ∈ V ∧ ( I ↾ (𝐹𝐴)) ∈ V))
12 ffn 6668 . . . . 5 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
13 fveq2 6842 . . . . . . . . 9 (𝑎 = 𝑥 → (𝐹𝑎) = (𝐹𝑥))
1413sneqd 4598 . . . . . . . 8 (𝑎 = 𝑥 → {(𝐹𝑎)} = {(𝐹𝑥)})
1514imaeq2d 6013 . . . . . . 7 (𝑎 = 𝑥 → (𝐹 “ {(𝐹𝑎)}) = (𝐹 “ {(𝐹𝑥)}))
1615cbvmptv 5218 . . . . . 6 (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) = (𝑥𝐴 ↦ (𝐹 “ {(𝐹𝑥)}))
173, 16fundcmpsurinjlem2 45581 . . . . 5 ((𝐹 Fn 𝐴𝐴𝑉) → (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})):𝐴onto𝑃)
1812, 17sylan 580 . . . 4 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})):𝐴onto𝑃)
19 eqid 2736 . . . . . 6 (𝑦𝑃 (𝐹𝑦)) = (𝑦𝑃 (𝐹𝑦))
203, 19imasetpreimafvbij 45588 . . . . 5 ((𝐹 Fn 𝐴𝐴𝑉) → (𝑦𝑃 (𝐹𝑦)):𝑃1-1-onto→(𝐹𝐴))
2112, 20sylan 580 . . . 4 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑦𝑃 (𝐹𝑦)):𝑃1-1-onto→(𝐹𝐴))
22 f1oi 6822 . . . . . 6 ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1-onto→(𝐹𝐴)
23 f1of1 6783 . . . . . 6 (( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1-onto→(𝐹𝐴) → ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1→(𝐹𝐴))
24 fimass 6689 . . . . . . . 8 (𝐹:𝐴𝐵 → (𝐹𝐴) ⊆ 𝐵)
25 f1ss 6744 . . . . . . . 8 ((( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1→(𝐹𝐴) ∧ (𝐹𝐴) ⊆ 𝐵) → ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1𝐵)
2624, 25sylan2 593 . . . . . . 7 ((( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1→(𝐹𝐴) ∧ 𝐹:𝐴𝐵) → ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1𝐵)
2726ex 413 . . . . . 6 (( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1→(𝐹𝐴) → (𝐹:𝐴𝐵 → ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1𝐵))
2822, 23, 27mp2b 10 . . . . 5 (𝐹:𝐴𝐵 → ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1𝐵)
2928adantr 481 . . . 4 ((𝐹:𝐴𝐵𝐴𝑉) → ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1𝐵)
3018, 21, 293jca 1128 . . 3 ((𝐹:𝐴𝐵𝐴𝑉) → ((𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})):𝐴onto𝑃 ∧ (𝑦𝑃 (𝐹𝑦)):𝑃1-1-onto→(𝐹𝐴) ∧ ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1𝐵))
3112adantr 481 . . . . . . . . 9 ((𝐹:𝐴𝐵𝐴𝑉) → 𝐹 Fn 𝐴)
32 uniimaprimaeqfv 45564 . . . . . . . . 9 ((𝐹 Fn 𝐴𝑎𝐴) → (𝐹 “ (𝐹 “ {(𝐹𝑎)})) = (𝐹𝑎))
3331, 32sylan 580 . . . . . . . 8 (((𝐹:𝐴𝐵𝐴𝑉) ∧ 𝑎𝐴) → (𝐹 “ (𝐹 “ {(𝐹𝑎)})) = (𝐹𝑎))
3433fveq2d 6846 . . . . . . 7 (((𝐹:𝐴𝐵𝐴𝑉) ∧ 𝑎𝐴) → (( I ↾ (𝐹𝐴))‘ (𝐹 “ (𝐹 “ {(𝐹𝑎)}))) = (( I ↾ (𝐹𝐴))‘(𝐹𝑎)))
3534mpteq2dva 5205 . . . . . 6 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑎𝐴 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹 “ (𝐹 “ {(𝐹𝑎)})))) = (𝑎𝐴 ↦ (( I ↾ (𝐹𝐴))‘(𝐹𝑎))))
36 ffrn 6682 . . . . . . . . . 10 (𝐹:𝐴𝐵𝐹:𝐴⟶ran 𝐹)
3736adantr 481 . . . . . . . . 9 ((𝐹:𝐴𝐵𝐴𝑉) → 𝐹:𝐴⟶ran 𝐹)
3837funfvima2d 7182 . . . . . . . 8 (((𝐹:𝐴𝐵𝐴𝑉) ∧ 𝑎𝐴) → (𝐹𝑎) ∈ (𝐹𝐴))
39 fvresi 7119 . . . . . . . 8 ((𝐹𝑎) ∈ (𝐹𝐴) → (( I ↾ (𝐹𝐴))‘(𝐹𝑎)) = (𝐹𝑎))
4038, 39syl 17 . . . . . . 7 (((𝐹:𝐴𝐵𝐴𝑉) ∧ 𝑎𝐴) → (( I ↾ (𝐹𝐴))‘(𝐹𝑎)) = (𝐹𝑎))
4140mpteq2dva 5205 . . . . . 6 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑎𝐴 ↦ (( I ↾ (𝐹𝐴))‘(𝐹𝑎))) = (𝑎𝐴 ↦ (𝐹𝑎)))
4235, 41eqtrd 2776 . . . . 5 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑎𝐴 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹 “ (𝐹 “ {(𝐹𝑎)})))) = (𝑎𝐴 ↦ (𝐹𝑎)))
4312ad2antrr 724 . . . . . . 7 (((𝐹:𝐴𝐵𝐴𝑉) ∧ 𝑎𝐴) → 𝐹 Fn 𝐴)
441adantr 481 . . . . . . 7 (((𝐹:𝐴𝐵𝐴𝑉) ∧ 𝑎𝐴) → 𝐴𝑉)
45 simpr 485 . . . . . . 7 (((𝐹:𝐴𝐵𝐴𝑉) ∧ 𝑎𝐴) → 𝑎𝐴)
463preimafvelsetpreimafv 45570 . . . . . . 7 ((𝐹 Fn 𝐴𝐴𝑉𝑎𝐴) → (𝐹 “ {(𝐹𝑎)}) ∈ 𝑃)
4743, 44, 45, 46syl3anc 1371 . . . . . 6 (((𝐹:𝐴𝐵𝐴𝑉) ∧ 𝑎𝐴) → (𝐹 “ {(𝐹𝑎)}) ∈ 𝑃)
48 eqidd 2737 . . . . . 6 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})))
49 eqidd 2737 . . . . . 6 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑦𝑃 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹𝑦))) = (𝑦𝑃 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹𝑦))))
50 imaeq2 6009 . . . . . . . 8 (𝑦 = (𝐹 “ {(𝐹𝑎)}) → (𝐹𝑦) = (𝐹 “ (𝐹 “ {(𝐹𝑎)})))
5150unieqd 4879 . . . . . . 7 (𝑦 = (𝐹 “ {(𝐹𝑎)}) → (𝐹𝑦) = (𝐹 “ (𝐹 “ {(𝐹𝑎)})))
5251fveq2d 6846 . . . . . 6 (𝑦 = (𝐹 “ {(𝐹𝑎)}) → (( I ↾ (𝐹𝐴))‘ (𝐹𝑦)) = (( I ↾ (𝐹𝐴))‘ (𝐹 “ (𝐹 “ {(𝐹𝑎)}))))
5347, 48, 49, 52fmptco 7075 . . . . 5 ((𝐹:𝐴𝐵𝐴𝑉) → ((𝑦𝑃 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹𝑦))) ∘ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)}))) = (𝑎𝐴 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹 “ (𝐹 “ {(𝐹𝑎)})))))
54 dffn5 6901 . . . . . . 7 (𝐹 Fn 𝐴𝐹 = (𝑎𝐴 ↦ (𝐹𝑎)))
5512, 54sylib 217 . . . . . 6 (𝐹:𝐴𝐵𝐹 = (𝑎𝐴 ↦ (𝐹𝑎)))
5655adantr 481 . . . . 5 ((𝐹:𝐴𝐵𝐴𝑉) → 𝐹 = (𝑎𝐴 ↦ (𝐹𝑎)))
5742, 53, 563eqtr4rd 2787 . . . 4 ((𝐹:𝐴𝐵𝐴𝑉) → 𝐹 = ((𝑦𝑃 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹𝑦))) ∘ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)}))))
58 f1of 6784 . . . . . . . . . 10 (( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1-onto→(𝐹𝐴) → ( I ↾ (𝐹𝐴)):(𝐹𝐴)⟶(𝐹𝐴))
5922, 58mp1i 13 . . . . . . . . 9 (𝐹 Fn 𝐴 → ( I ↾ (𝐹𝐴)):(𝐹𝐴)⟶(𝐹𝐴))
60 fnima 6631 . . . . . . . . . . 11 (𝐹 Fn 𝐴 → (𝐹𝐴) = ran 𝐹)
6160eqcomd 2742 . . . . . . . . . 10 (𝐹 Fn 𝐴 → ran 𝐹 = (𝐹𝐴))
6261feq2d 6654 . . . . . . . . 9 (𝐹 Fn 𝐴 → (( I ↾ (𝐹𝐴)):ran 𝐹⟶(𝐹𝐴) ↔ ( I ↾ (𝐹𝐴)):(𝐹𝐴)⟶(𝐹𝐴)))
6359, 62mpbird 256 . . . . . . . 8 (𝐹 Fn 𝐴 → ( I ↾ (𝐹𝐴)):ran 𝐹⟶(𝐹𝐴))
643uniimaelsetpreimafv 45578 . . . . . . . 8 ((𝐹 Fn 𝐴𝑦𝑃) → (𝐹𝑦) ∈ ran 𝐹)
6563, 64cofmpt 7078 . . . . . . 7 (𝐹 Fn 𝐴 → (( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))) = (𝑦𝑃 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹𝑦))))
6665eqcomd 2742 . . . . . 6 (𝐹 Fn 𝐴 → (𝑦𝑃 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹𝑦))) = (( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))))
6731, 66syl 17 . . . . 5 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑦𝑃 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹𝑦))) = (( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))))
6867coeq1d 5817 . . . 4 ((𝐹:𝐴𝐵𝐴𝑉) → ((𝑦𝑃 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹𝑦))) ∘ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)}))) = ((( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))) ∘ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)}))))
6957, 68eqtrd 2776 . . 3 ((𝐹:𝐴𝐵𝐴𝑉) → 𝐹 = ((( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))) ∘ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)}))))
7030, 69jca 512 . 2 ((𝐹:𝐴𝐵𝐴𝑉) → (((𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})):𝐴onto𝑃 ∧ (𝑦𝑃 (𝐹𝑦)):𝑃1-1-onto→(𝐹𝐴) ∧ ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1𝐵) ∧ 𝐹 = ((( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))) ∘ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})))))
71 foeq1 6752 . . . . . 6 (𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) → (𝑔:𝐴onto𝑃 ↔ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})):𝐴onto𝑃))
72713ad2ant1 1133 . . . . 5 ((𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∧ = (𝑦𝑃 (𝐹𝑦)) ∧ 𝑖 = ( I ↾ (𝐹𝐴))) → (𝑔:𝐴onto𝑃 ↔ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})):𝐴onto𝑃))
73 f1oeq1 6772 . . . . . 6 ( = (𝑦𝑃 (𝐹𝑦)) → (:𝑃1-1-onto→(𝐹𝐴) ↔ (𝑦𝑃 (𝐹𝑦)):𝑃1-1-onto→(𝐹𝐴)))
74733ad2ant2 1134 . . . . 5 ((𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∧ = (𝑦𝑃 (𝐹𝑦)) ∧ 𝑖 = ( I ↾ (𝐹𝐴))) → (:𝑃1-1-onto→(𝐹𝐴) ↔ (𝑦𝑃 (𝐹𝑦)):𝑃1-1-onto→(𝐹𝐴)))
75 f1eq1 6733 . . . . . 6 (𝑖 = ( I ↾ (𝐹𝐴)) → (𝑖:(𝐹𝐴)–1-1𝐵 ↔ ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1𝐵))
76753ad2ant3 1135 . . . . 5 ((𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∧ = (𝑦𝑃 (𝐹𝑦)) ∧ 𝑖 = ( I ↾ (𝐹𝐴))) → (𝑖:(𝐹𝐴)–1-1𝐵 ↔ ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1𝐵))
7772, 74, 763anbi123d 1436 . . . 4 ((𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∧ = (𝑦𝑃 (𝐹𝑦)) ∧ 𝑖 = ( I ↾ (𝐹𝐴))) → ((𝑔:𝐴onto𝑃:𝑃1-1-onto→(𝐹𝐴) ∧ 𝑖:(𝐹𝐴)–1-1𝐵) ↔ ((𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})):𝐴onto𝑃 ∧ (𝑦𝑃 (𝐹𝑦)):𝑃1-1-onto→(𝐹𝐴) ∧ ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1𝐵)))
78 simp3 1138 . . . . . . 7 ((𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∧ = (𝑦𝑃 (𝐹𝑦)) ∧ 𝑖 = ( I ↾ (𝐹𝐴))) → 𝑖 = ( I ↾ (𝐹𝐴)))
79 simp2 1137 . . . . . . 7 ((𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∧ = (𝑦𝑃 (𝐹𝑦)) ∧ 𝑖 = ( I ↾ (𝐹𝐴))) → = (𝑦𝑃 (𝐹𝑦)))
8078, 79coeq12d 5820 . . . . . 6 ((𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∧ = (𝑦𝑃 (𝐹𝑦)) ∧ 𝑖 = ( I ↾ (𝐹𝐴))) → (𝑖) = (( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))))
81 simp1 1136 . . . . . 6 ((𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∧ = (𝑦𝑃 (𝐹𝑦)) ∧ 𝑖 = ( I ↾ (𝐹𝐴))) → 𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})))
8280, 81coeq12d 5820 . . . . 5 ((𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∧ = (𝑦𝑃 (𝐹𝑦)) ∧ 𝑖 = ( I ↾ (𝐹𝐴))) → ((𝑖) ∘ 𝑔) = ((( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))) ∘ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)}))))
8382eqeq2d 2747 . . . 4 ((𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∧ = (𝑦𝑃 (𝐹𝑦)) ∧ 𝑖 = ( I ↾ (𝐹𝐴))) → (𝐹 = ((𝑖) ∘ 𝑔) ↔ 𝐹 = ((( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))) ∘ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})))))
8477, 83anbi12d 631 . . 3 ((𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∧ = (𝑦𝑃 (𝐹𝑦)) ∧ 𝑖 = ( I ↾ (𝐹𝐴))) → (((𝑔:𝐴onto𝑃:𝑃1-1-onto→(𝐹𝐴) ∧ 𝑖:(𝐹𝐴)–1-1𝐵) ∧ 𝐹 = ((𝑖) ∘ 𝑔)) ↔ (((𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})):𝐴onto𝑃 ∧ (𝑦𝑃 (𝐹𝑦)):𝑃1-1-onto→(𝐹𝐴) ∧ ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1𝐵) ∧ 𝐹 = ((( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))) ∘ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)}))))))
8584spc3egv 3562 . 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 396  w3a 1087   = wceq 1541  wex 1781  wcel 2106  {cab 2713  wrex 3073  Vcvv 3445  wss 3910  {csn 4586   cuni 4865  cmpt 5188   I cid 5530  ccnv 5632  ran crn 5634  cres 5635  cima 5636  ccom 5637  Fun wfun 6490   Fn wfn 6491  wf 6492  1-1wf1 6493  ontowfo 6494  1-1-ontowf1o 6495  cfv 6496
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504
This theorem is referenced by:  fundcmpsurinjpreimafv  45590  fundcmpsurbijinj  45592
  Copyright terms: Public domain W3C validator