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 44441
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 488 . . . 4 ((𝐹:𝐴𝐵𝐴𝑉) → 𝐴𝑉)
21mptexd 7010 . . 3 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∈ V)
3 fundcmpsurinj.p . . . . . 6 𝑃 = {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝐹 “ {(𝐹𝑥)})}
43setpreimafvex 44417 . . . . 5 (𝐴𝑉𝑃 ∈ V)
54adantl 485 . . . 4 ((𝐹:𝐴𝐵𝐴𝑉) → 𝑃 ∈ V)
65mptexd 7010 . . 3 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑦𝑃 (𝐹𝑦)) ∈ V)
7 ffun 6518 . . . . 5 (𝐹:𝐴𝐵 → Fun 𝐹)
8 funimaexg 6436 . . . . 5 ((Fun 𝐹𝐴𝑉) → (𝐹𝐴) ∈ V)
97, 8sylan 583 . . . 4 ((𝐹:𝐴𝐵𝐴𝑉) → (𝐹𝐴) ∈ V)
109resiexd 7002 . . 3 ((𝐹:𝐴𝐵𝐴𝑉) → ( I ↾ (𝐹𝐴)) ∈ V)
112, 6, 103jca 1129 . 2 ((𝐹:𝐴𝐵𝐴𝑉) → ((𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∈ V ∧ (𝑦𝑃 (𝐹𝑦)) ∈ V ∧ ( I ↾ (𝐹𝐴)) ∈ V))
12 ffn 6515 . . . . 5 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
13 fveq2 6687 . . . . . . . . 9 (𝑎 = 𝑥 → (𝐹𝑎) = (𝐹𝑥))
1413sneqd 4538 . . . . . . . 8 (𝑎 = 𝑥 → {(𝐹𝑎)} = {(𝐹𝑥)})
1514imaeq2d 5913 . . . . . . 7 (𝑎 = 𝑥 → (𝐹 “ {(𝐹𝑎)}) = (𝐹 “ {(𝐹𝑥)}))
1615cbvmptv 5143 . . . . . 6 (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) = (𝑥𝐴 ↦ (𝐹 “ {(𝐹𝑥)}))
173, 16fundcmpsurinjlem2 44433 . . . . 5 ((𝐹 Fn 𝐴𝐴𝑉) → (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})):𝐴onto𝑃)
1812, 17sylan 583 . . . 4 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})):𝐴onto𝑃)
19 eqid 2739 . . . . . 6 (𝑦𝑃 (𝐹𝑦)) = (𝑦𝑃 (𝐹𝑦))
203, 19imasetpreimafvbij 44440 . . . . 5 ((𝐹 Fn 𝐴𝐴𝑉) → (𝑦𝑃 (𝐹𝑦)):𝑃1-1-onto→(𝐹𝐴))
2112, 20sylan 583 . . . 4 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑦𝑃 (𝐹𝑦)):𝑃1-1-onto→(𝐹𝐴))
22 f1oi 6668 . . . . . 6 ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1-onto→(𝐹𝐴)
23 f1of1 6630 . . . . . 6 (( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1-onto→(𝐹𝐴) → ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1→(𝐹𝐴))
24 fimass 6536 . . . . . . . 8 (𝐹:𝐴𝐵 → (𝐹𝐴) ⊆ 𝐵)
25 f1ss 6591 . . . . . . . 8 ((( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1→(𝐹𝐴) ∧ (𝐹𝐴) ⊆ 𝐵) → ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1𝐵)
2624, 25sylan2 596 . . . . . . 7 ((( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1→(𝐹𝐴) ∧ 𝐹:𝐴𝐵) → ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1𝐵)
2726ex 416 . . . . . 6 (( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1→(𝐹𝐴) → (𝐹:𝐴𝐵 → ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1𝐵))
2822, 23, 27mp2b 10 . . . . 5 (𝐹:𝐴𝐵 → ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1𝐵)
2928adantr 484 . . . 4 ((𝐹:𝐴𝐵𝐴𝑉) → ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1𝐵)
3018, 21, 293jca 1129 . . 3 ((𝐹:𝐴𝐵𝐴𝑉) → ((𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})):𝐴onto𝑃 ∧ (𝑦𝑃 (𝐹𝑦)):𝑃1-1-onto→(𝐹𝐴) ∧ ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1𝐵))
3112adantr 484 . . . . . . . . 9 ((𝐹:𝐴𝐵𝐴𝑉) → 𝐹 Fn 𝐴)
32 uniimaprimaeqfv 44416 . . . . . . . . 9 ((𝐹 Fn 𝐴𝑎𝐴) → (𝐹 “ (𝐹 “ {(𝐹𝑎)})) = (𝐹𝑎))
3331, 32sylan 583 . . . . . . . 8 (((𝐹:𝐴𝐵𝐴𝑉) ∧ 𝑎𝐴) → (𝐹 “ (𝐹 “ {(𝐹𝑎)})) = (𝐹𝑎))
3433fveq2d 6691 . . . . . . 7 (((𝐹:𝐴𝐵𝐴𝑉) ∧ 𝑎𝐴) → (( I ↾ (𝐹𝐴))‘ (𝐹 “ (𝐹 “ {(𝐹𝑎)}))) = (( I ↾ (𝐹𝐴))‘(𝐹𝑎)))
3534mpteq2dva 5135 . . . . . 6 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑎𝐴 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹 “ (𝐹 “ {(𝐹𝑎)})))) = (𝑎𝐴 ↦ (( I ↾ (𝐹𝐴))‘(𝐹𝑎))))
36 ffrn 6529 . . . . . . . . . 10 (𝐹:𝐴𝐵𝐹:𝐴⟶ran 𝐹)
3736adantr 484 . . . . . . . . 9 ((𝐹:𝐴𝐵𝐴𝑉) → 𝐹:𝐴⟶ran 𝐹)
3837funfvima2d 7018 . . . . . . . 8 (((𝐹:𝐴𝐵𝐴𝑉) ∧ 𝑎𝐴) → (𝐹𝑎) ∈ (𝐹𝐴))
39 fvresi 6958 . . . . . . . 8 ((𝐹𝑎) ∈ (𝐹𝐴) → (( I ↾ (𝐹𝐴))‘(𝐹𝑎)) = (𝐹𝑎))
4038, 39syl 17 . . . . . . 7 (((𝐹:𝐴𝐵𝐴𝑉) ∧ 𝑎𝐴) → (( I ↾ (𝐹𝐴))‘(𝐹𝑎)) = (𝐹𝑎))
4140mpteq2dva 5135 . . . . . 6 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑎𝐴 ↦ (( I ↾ (𝐹𝐴))‘(𝐹𝑎))) = (𝑎𝐴 ↦ (𝐹𝑎)))
4235, 41eqtrd 2774 . . . . 5 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑎𝐴 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹 “ (𝐹 “ {(𝐹𝑎)})))) = (𝑎𝐴 ↦ (𝐹𝑎)))
4312ad2antrr 726 . . . . . . 7 (((𝐹:𝐴𝐵𝐴𝑉) ∧ 𝑎𝐴) → 𝐹 Fn 𝐴)
441adantr 484 . . . . . . 7 (((𝐹:𝐴𝐵𝐴𝑉) ∧ 𝑎𝐴) → 𝐴𝑉)
45 simpr 488 . . . . . . 7 (((𝐹:𝐴𝐵𝐴𝑉) ∧ 𝑎𝐴) → 𝑎𝐴)
463preimafvelsetpreimafv 44422 . . . . . . 7 ((𝐹 Fn 𝐴𝐴𝑉𝑎𝐴) → (𝐹 “ {(𝐹𝑎)}) ∈ 𝑃)
4743, 44, 45, 46syl3anc 1372 . . . . . 6 (((𝐹:𝐴𝐵𝐴𝑉) ∧ 𝑎𝐴) → (𝐹 “ {(𝐹𝑎)}) ∈ 𝑃)
48 eqidd 2740 . . . . . 6 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})))
49 eqidd 2740 . . . . . 6 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑦𝑃 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹𝑦))) = (𝑦𝑃 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹𝑦))))
50 imaeq2 5909 . . . . . . . 8 (𝑦 = (𝐹 “ {(𝐹𝑎)}) → (𝐹𝑦) = (𝐹 “ (𝐹 “ {(𝐹𝑎)})))
5150unieqd 4820 . . . . . . 7 (𝑦 = (𝐹 “ {(𝐹𝑎)}) → (𝐹𝑦) = (𝐹 “ (𝐹 “ {(𝐹𝑎)})))
5251fveq2d 6691 . . . . . 6 (𝑦 = (𝐹 “ {(𝐹𝑎)}) → (( I ↾ (𝐹𝐴))‘ (𝐹𝑦)) = (( I ↾ (𝐹𝐴))‘ (𝐹 “ (𝐹 “ {(𝐹𝑎)}))))
5347, 48, 49, 52fmptco 6914 . . . . 5 ((𝐹:𝐴𝐵𝐴𝑉) → ((𝑦𝑃 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹𝑦))) ∘ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)}))) = (𝑎𝐴 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹 “ (𝐹 “ {(𝐹𝑎)})))))
54 dffn5 6741 . . . . . . 7 (𝐹 Fn 𝐴𝐹 = (𝑎𝐴 ↦ (𝐹𝑎)))
5512, 54sylib 221 . . . . . 6 (𝐹:𝐴𝐵𝐹 = (𝑎𝐴 ↦ (𝐹𝑎)))
5655adantr 484 . . . . 5 ((𝐹:𝐴𝐵𝐴𝑉) → 𝐹 = (𝑎𝐴 ↦ (𝐹𝑎)))
5742, 53, 563eqtr4rd 2785 . . . 4 ((𝐹:𝐴𝐵𝐴𝑉) → 𝐹 = ((𝑦𝑃 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹𝑦))) ∘ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)}))))
58 f1of 6631 . . . . . . . . . 10 (( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1-onto→(𝐹𝐴) → ( I ↾ (𝐹𝐴)):(𝐹𝐴)⟶(𝐹𝐴))
5922, 58mp1i 13 . . . . . . . . 9 (𝐹 Fn 𝐴 → ( I ↾ (𝐹𝐴)):(𝐹𝐴)⟶(𝐹𝐴))
60 fnima 6478 . . . . . . . . . . 11 (𝐹 Fn 𝐴 → (𝐹𝐴) = ran 𝐹)
6160eqcomd 2745 . . . . . . . . . 10 (𝐹 Fn 𝐴 → ran 𝐹 = (𝐹𝐴))
6261feq2d 6501 . . . . . . . . 9 (𝐹 Fn 𝐴 → (( I ↾ (𝐹𝐴)):ran 𝐹⟶(𝐹𝐴) ↔ ( I ↾ (𝐹𝐴)):(𝐹𝐴)⟶(𝐹𝐴)))
6359, 62mpbird 260 . . . . . . . 8 (𝐹 Fn 𝐴 → ( I ↾ (𝐹𝐴)):ran 𝐹⟶(𝐹𝐴))
643uniimaelsetpreimafv 44430 . . . . . . . 8 ((𝐹 Fn 𝐴𝑦𝑃) → (𝐹𝑦) ∈ ran 𝐹)
6563, 64cofmpt 6917 . . . . . . 7 (𝐹 Fn 𝐴 → (( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))) = (𝑦𝑃 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹𝑦))))
6665eqcomd 2745 . . . . . 6 (𝐹 Fn 𝐴 → (𝑦𝑃 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹𝑦))) = (( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))))
6731, 66syl 17 . . . . 5 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑦𝑃 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹𝑦))) = (( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))))
6867coeq1d 5714 . . . 4 ((𝐹:𝐴𝐵𝐴𝑉) → ((𝑦𝑃 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹𝑦))) ∘ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)}))) = ((( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))) ∘ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)}))))
6957, 68eqtrd 2774 . . 3 ((𝐹:𝐴𝐵𝐴𝑉) → 𝐹 = ((( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))) ∘ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)}))))
7030, 69jca 515 . 2 ((𝐹:𝐴𝐵𝐴𝑉) → (((𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})):𝐴onto𝑃 ∧ (𝑦𝑃 (𝐹𝑦)):𝑃1-1-onto→(𝐹𝐴) ∧ ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1𝐵) ∧ 𝐹 = ((( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))) ∘ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})))))
71 foeq1 6599 . . . . . 6 (𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) → (𝑔:𝐴onto𝑃 ↔ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})):𝐴onto𝑃))
72713ad2ant1 1134 . . . . 5 ((𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∧ = (𝑦𝑃 (𝐹𝑦)) ∧ 𝑖 = ( I ↾ (𝐹𝐴))) → (𝑔:𝐴onto𝑃 ↔ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})):𝐴onto𝑃))
73 f1oeq1 6619 . . . . . 6 ( = (𝑦𝑃 (𝐹𝑦)) → (:𝑃1-1-onto→(𝐹𝐴) ↔ (𝑦𝑃 (𝐹𝑦)):𝑃1-1-onto→(𝐹𝐴)))
74733ad2ant2 1135 . . . . 5 ((𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∧ = (𝑦𝑃 (𝐹𝑦)) ∧ 𝑖 = ( I ↾ (𝐹𝐴))) → (:𝑃1-1-onto→(𝐹𝐴) ↔ (𝑦𝑃 (𝐹𝑦)):𝑃1-1-onto→(𝐹𝐴)))
75 f1eq1 6580 . . . . . 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 5717 . . . . . 6 ((𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∧ = (𝑦𝑃 (𝐹𝑦)) ∧ 𝑖 = ( I ↾ (𝐹𝐴))) → (𝑖) = (( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))))
81 simp1 1137 . . . . . 6 ((𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∧ = (𝑦𝑃 (𝐹𝑦)) ∧ 𝑖 = ( I ↾ (𝐹𝐴))) → 𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})))
8280, 81coeq12d 5717 . . . . 5 ((𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∧ = (𝑦𝑃 (𝐹𝑦)) ∧ 𝑖 = ( I ↾ (𝐹𝐴))) → ((𝑖) ∘ 𝑔) = ((( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))) ∘ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)}))))
8382eqeq2d 2750 . . . 4 ((𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∧ = (𝑦𝑃 (𝐹𝑦)) ∧ 𝑖 = ( I ↾ (𝐹𝐴))) → (𝐹 = ((𝑖) ∘ 𝑔) ↔ 𝐹 = ((( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))) ∘ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})))))
8477, 83anbi12d 634 . . 3 ((𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∧ = (𝑦𝑃 (𝐹𝑦)) ∧ 𝑖 = ( I ↾ (𝐹𝐴))) → (((𝑔:𝐴onto𝑃:𝑃1-1-onto→(𝐹𝐴) ∧ 𝑖:(𝐹𝐴)–1-1𝐵) ∧ 𝐹 = ((𝑖) ∘ 𝑔)) ↔ (((𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})):𝐴onto𝑃 ∧ (𝑦𝑃 (𝐹𝑦)):𝑃1-1-onto→(𝐹𝐴) ∧ ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1𝐵) ∧ 𝐹 = ((( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))) ∘ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)}))))))
8584spc3egv 3510 . 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 209  wa 399  w3a 1088   = wceq 1542  wex 1786  wcel 2114  {cab 2717  wrex 3055  Vcvv 3400  wss 3853  {csn 4526   cuni 4806  cmpt 5120   I cid 5438  ccnv 5534  ran crn 5536  cres 5537  cima 5538  ccom 5539  Fun wfun 6344   Fn wfn 6345  wf 6346  1-1wf1 6347  ontowfo 6348  1-1-ontowf1o 6349  cfv 6350
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2711  ax-rep 5164  ax-sep 5177  ax-nul 5184  ax-pow 5242  ax-pr 5306  ax-un 7492
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2541  df-eu 2571  df-clab 2718  df-cleq 2731  df-clel 2812  df-nfc 2882  df-ne 2936  df-nel 3040  df-ral 3059  df-rex 3060  df-reu 3061  df-rab 3063  df-v 3402  df-sbc 3686  df-csb 3801  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4222  df-if 4425  df-pw 4500  df-sn 4527  df-pr 4529  df-op 4533  df-uni 4807  df-iun 4893  df-br 5041  df-opab 5103  df-mpt 5121  df-id 5439  df-xp 5541  df-rel 5542  df-cnv 5543  df-co 5544  df-dm 5545  df-rn 5546  df-res 5547  df-ima 5548  df-iota 6308  df-fun 6352  df-fn 6353  df-f 6354  df-f1 6355  df-fo 6356  df-f1o 6357  df-fv 6358
This theorem is referenced by:  fundcmpsurinjpreimafv  44442  fundcmpsurbijinj  44444
  Copyright terms: Public domain W3C validator