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 44859
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 7100 . . 3 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∈ V)
3 fundcmpsurinj.p . . . . . 6 𝑃 = {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝐹 “ {(𝐹𝑥)})}
43setpreimafvex 44835 . . . . 5 (𝐴𝑉𝑃 ∈ V)
54adantl 482 . . . 4 ((𝐹:𝐴𝐵𝐴𝑉) → 𝑃 ∈ V)
65mptexd 7100 . . 3 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑦𝑃 (𝐹𝑦)) ∈ V)
7 ffun 6603 . . . . 5 (𝐹:𝐴𝐵 → Fun 𝐹)
8 funimaexg 6520 . . . . 5 ((Fun 𝐹𝐴𝑉) → (𝐹𝐴) ∈ V)
97, 8sylan 580 . . . 4 ((𝐹:𝐴𝐵𝐴𝑉) → (𝐹𝐴) ∈ V)
109resiexd 7092 . . 3 ((𝐹:𝐴𝐵𝐴𝑉) → ( I ↾ (𝐹𝐴)) ∈ V)
112, 6, 103jca 1127 . 2 ((𝐹:𝐴𝐵𝐴𝑉) → ((𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∈ V ∧ (𝑦𝑃 (𝐹𝑦)) ∈ V ∧ ( I ↾ (𝐹𝐴)) ∈ V))
12 ffn 6600 . . . . 5 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
13 fveq2 6774 . . . . . . . . 9 (𝑎 = 𝑥 → (𝐹𝑎) = (𝐹𝑥))
1413sneqd 4573 . . . . . . . 8 (𝑎 = 𝑥 → {(𝐹𝑎)} = {(𝐹𝑥)})
1514imaeq2d 5969 . . . . . . 7 (𝑎 = 𝑥 → (𝐹 “ {(𝐹𝑎)}) = (𝐹 “ {(𝐹𝑥)}))
1615cbvmptv 5187 . . . . . 6 (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) = (𝑥𝐴 ↦ (𝐹 “ {(𝐹𝑥)}))
173, 16fundcmpsurinjlem2 44851 . . . . 5 ((𝐹 Fn 𝐴𝐴𝑉) → (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})):𝐴onto𝑃)
1812, 17sylan 580 . . . 4 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})):𝐴onto𝑃)
19 eqid 2738 . . . . . 6 (𝑦𝑃 (𝐹𝑦)) = (𝑦𝑃 (𝐹𝑦))
203, 19imasetpreimafvbij 44858 . . . . 5 ((𝐹 Fn 𝐴𝐴𝑉) → (𝑦𝑃 (𝐹𝑦)):𝑃1-1-onto→(𝐹𝐴))
2112, 20sylan 580 . . . 4 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑦𝑃 (𝐹𝑦)):𝑃1-1-onto→(𝐹𝐴))
22 f1oi 6754 . . . . . 6 ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1-onto→(𝐹𝐴)
23 f1of1 6715 . . . . . 6 (( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1-onto→(𝐹𝐴) → ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1→(𝐹𝐴))
24 fimass 6621 . . . . . . . 8 (𝐹:𝐴𝐵 → (𝐹𝐴) ⊆ 𝐵)
25 f1ss 6676 . . . . . . . 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 1127 . . 3 ((𝐹:𝐴𝐵𝐴𝑉) → ((𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})):𝐴onto𝑃 ∧ (𝑦𝑃 (𝐹𝑦)):𝑃1-1-onto→(𝐹𝐴) ∧ ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1𝐵))
3112adantr 481 . . . . . . . . 9 ((𝐹:𝐴𝐵𝐴𝑉) → 𝐹 Fn 𝐴)
32 uniimaprimaeqfv 44834 . . . . . . . . 9 ((𝐹 Fn 𝐴𝑎𝐴) → (𝐹 “ (𝐹 “ {(𝐹𝑎)})) = (𝐹𝑎))
3331, 32sylan 580 . . . . . . . 8 (((𝐹:𝐴𝐵𝐴𝑉) ∧ 𝑎𝐴) → (𝐹 “ (𝐹 “ {(𝐹𝑎)})) = (𝐹𝑎))
3433fveq2d 6778 . . . . . . 7 (((𝐹:𝐴𝐵𝐴𝑉) ∧ 𝑎𝐴) → (( I ↾ (𝐹𝐴))‘ (𝐹 “ (𝐹 “ {(𝐹𝑎)}))) = (( I ↾ (𝐹𝐴))‘(𝐹𝑎)))
3534mpteq2dva 5174 . . . . . 6 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑎𝐴 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹 “ (𝐹 “ {(𝐹𝑎)})))) = (𝑎𝐴 ↦ (( I ↾ (𝐹𝐴))‘(𝐹𝑎))))
36 ffrn 6614 . . . . . . . . . 10 (𝐹:𝐴𝐵𝐹:𝐴⟶ran 𝐹)
3736adantr 481 . . . . . . . . 9 ((𝐹:𝐴𝐵𝐴𝑉) → 𝐹:𝐴⟶ran 𝐹)
3837funfvima2d 7108 . . . . . . . 8 (((𝐹:𝐴𝐵𝐴𝑉) ∧ 𝑎𝐴) → (𝐹𝑎) ∈ (𝐹𝐴))
39 fvresi 7045 . . . . . . . 8 ((𝐹𝑎) ∈ (𝐹𝐴) → (( I ↾ (𝐹𝐴))‘(𝐹𝑎)) = (𝐹𝑎))
4038, 39syl 17 . . . . . . 7 (((𝐹:𝐴𝐵𝐴𝑉) ∧ 𝑎𝐴) → (( I ↾ (𝐹𝐴))‘(𝐹𝑎)) = (𝐹𝑎))
4140mpteq2dva 5174 . . . . . 6 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑎𝐴 ↦ (( I ↾ (𝐹𝐴))‘(𝐹𝑎))) = (𝑎𝐴 ↦ (𝐹𝑎)))
4235, 41eqtrd 2778 . . . . 5 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑎𝐴 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹 “ (𝐹 “ {(𝐹𝑎)})))) = (𝑎𝐴 ↦ (𝐹𝑎)))
4312ad2antrr 723 . . . . . . 7 (((𝐹:𝐴𝐵𝐴𝑉) ∧ 𝑎𝐴) → 𝐹 Fn 𝐴)
441adantr 481 . . . . . . 7 (((𝐹:𝐴𝐵𝐴𝑉) ∧ 𝑎𝐴) → 𝐴𝑉)
45 simpr 485 . . . . . . 7 (((𝐹:𝐴𝐵𝐴𝑉) ∧ 𝑎𝐴) → 𝑎𝐴)
463preimafvelsetpreimafv 44840 . . . . . . 7 ((𝐹 Fn 𝐴𝐴𝑉𝑎𝐴) → (𝐹 “ {(𝐹𝑎)}) ∈ 𝑃)
4743, 44, 45, 46syl3anc 1370 . . . . . 6 (((𝐹:𝐴𝐵𝐴𝑉) ∧ 𝑎𝐴) → (𝐹 “ {(𝐹𝑎)}) ∈ 𝑃)
48 eqidd 2739 . . . . . 6 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})))
49 eqidd 2739 . . . . . 6 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑦𝑃 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹𝑦))) = (𝑦𝑃 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹𝑦))))
50 imaeq2 5965 . . . . . . . 8 (𝑦 = (𝐹 “ {(𝐹𝑎)}) → (𝐹𝑦) = (𝐹 “ (𝐹 “ {(𝐹𝑎)})))
5150unieqd 4853 . . . . . . 7 (𝑦 = (𝐹 “ {(𝐹𝑎)}) → (𝐹𝑦) = (𝐹 “ (𝐹 “ {(𝐹𝑎)})))
5251fveq2d 6778 . . . . . 6 (𝑦 = (𝐹 “ {(𝐹𝑎)}) → (( I ↾ (𝐹𝐴))‘ (𝐹𝑦)) = (( I ↾ (𝐹𝐴))‘ (𝐹 “ (𝐹 “ {(𝐹𝑎)}))))
5347, 48, 49, 52fmptco 7001 . . . . 5 ((𝐹:𝐴𝐵𝐴𝑉) → ((𝑦𝑃 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹𝑦))) ∘ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)}))) = (𝑎𝐴 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹 “ (𝐹 “ {(𝐹𝑎)})))))
54 dffn5 6828 . . . . . . 7 (𝐹 Fn 𝐴𝐹 = (𝑎𝐴 ↦ (𝐹𝑎)))
5512, 54sylib 217 . . . . . 6 (𝐹:𝐴𝐵𝐹 = (𝑎𝐴 ↦ (𝐹𝑎)))
5655adantr 481 . . . . 5 ((𝐹:𝐴𝐵𝐴𝑉) → 𝐹 = (𝑎𝐴 ↦ (𝐹𝑎)))
5742, 53, 563eqtr4rd 2789 . . . 4 ((𝐹:𝐴𝐵𝐴𝑉) → 𝐹 = ((𝑦𝑃 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹𝑦))) ∘ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)}))))
58 f1of 6716 . . . . . . . . . 10 (( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1-onto→(𝐹𝐴) → ( I ↾ (𝐹𝐴)):(𝐹𝐴)⟶(𝐹𝐴))
5922, 58mp1i 13 . . . . . . . . 9 (𝐹 Fn 𝐴 → ( I ↾ (𝐹𝐴)):(𝐹𝐴)⟶(𝐹𝐴))
60 fnima 6563 . . . . . . . . . . 11 (𝐹 Fn 𝐴 → (𝐹𝐴) = ran 𝐹)
6160eqcomd 2744 . . . . . . . . . 10 (𝐹 Fn 𝐴 → ran 𝐹 = (𝐹𝐴))
6261feq2d 6586 . . . . . . . . 9 (𝐹 Fn 𝐴 → (( I ↾ (𝐹𝐴)):ran 𝐹⟶(𝐹𝐴) ↔ ( I ↾ (𝐹𝐴)):(𝐹𝐴)⟶(𝐹𝐴)))
6359, 62mpbird 256 . . . . . . . 8 (𝐹 Fn 𝐴 → ( I ↾ (𝐹𝐴)):ran 𝐹⟶(𝐹𝐴))
643uniimaelsetpreimafv 44848 . . . . . . . 8 ((𝐹 Fn 𝐴𝑦𝑃) → (𝐹𝑦) ∈ ran 𝐹)
6563, 64cofmpt 7004 . . . . . . 7 (𝐹 Fn 𝐴 → (( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))) = (𝑦𝑃 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹𝑦))))
6665eqcomd 2744 . . . . . 6 (𝐹 Fn 𝐴 → (𝑦𝑃 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹𝑦))) = (( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))))
6731, 66syl 17 . . . . 5 ((𝐹:𝐴𝐵𝐴𝑉) → (𝑦𝑃 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹𝑦))) = (( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))))
6867coeq1d 5770 . . . 4 ((𝐹:𝐴𝐵𝐴𝑉) → ((𝑦𝑃 ↦ (( I ↾ (𝐹𝐴))‘ (𝐹𝑦))) ∘ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)}))) = ((( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))) ∘ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)}))))
6957, 68eqtrd 2778 . . 3 ((𝐹:𝐴𝐵𝐴𝑉) → 𝐹 = ((( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))) ∘ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)}))))
7030, 69jca 512 . 2 ((𝐹:𝐴𝐵𝐴𝑉) → (((𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})):𝐴onto𝑃 ∧ (𝑦𝑃 (𝐹𝑦)):𝑃1-1-onto→(𝐹𝐴) ∧ ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1𝐵) ∧ 𝐹 = ((( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))) ∘ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})))))
71 foeq1 6684 . . . . . 6 (𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) → (𝑔:𝐴onto𝑃 ↔ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})):𝐴onto𝑃))
72713ad2ant1 1132 . . . . 5 ((𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∧ = (𝑦𝑃 (𝐹𝑦)) ∧ 𝑖 = ( I ↾ (𝐹𝐴))) → (𝑔:𝐴onto𝑃 ↔ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})):𝐴onto𝑃))
73 f1oeq1 6704 . . . . . 6 ( = (𝑦𝑃 (𝐹𝑦)) → (:𝑃1-1-onto→(𝐹𝐴) ↔ (𝑦𝑃 (𝐹𝑦)):𝑃1-1-onto→(𝐹𝐴)))
74733ad2ant2 1133 . . . . 5 ((𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∧ = (𝑦𝑃 (𝐹𝑦)) ∧ 𝑖 = ( I ↾ (𝐹𝐴))) → (:𝑃1-1-onto→(𝐹𝐴) ↔ (𝑦𝑃 (𝐹𝑦)):𝑃1-1-onto→(𝐹𝐴)))
75 f1eq1 6665 . . . . . 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 5773 . . . . . 6 ((𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∧ = (𝑦𝑃 (𝐹𝑦)) ∧ 𝑖 = ( I ↾ (𝐹𝐴))) → (𝑖) = (( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))))
81 simp1 1135 . . . . . 6 ((𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∧ = (𝑦𝑃 (𝐹𝑦)) ∧ 𝑖 = ( I ↾ (𝐹𝐴))) → 𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})))
8280, 81coeq12d 5773 . . . . 5 ((𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∧ = (𝑦𝑃 (𝐹𝑦)) ∧ 𝑖 = ( I ↾ (𝐹𝐴))) → ((𝑖) ∘ 𝑔) = ((( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))) ∘ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)}))))
8382eqeq2d 2749 . . . 4 ((𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∧ = (𝑦𝑃 (𝐹𝑦)) ∧ 𝑖 = ( I ↾ (𝐹𝐴))) → (𝐹 = ((𝑖) ∘ 𝑔) ↔ 𝐹 = ((( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))) ∘ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})))))
8477, 83anbi12d 631 . . 3 ((𝑔 = (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})) ∧ = (𝑦𝑃 (𝐹𝑦)) ∧ 𝑖 = ( I ↾ (𝐹𝐴))) → (((𝑔:𝐴onto𝑃:𝑃1-1-onto→(𝐹𝐴) ∧ 𝑖:(𝐹𝐴)–1-1𝐵) ∧ 𝐹 = ((𝑖) ∘ 𝑔)) ↔ (((𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)})):𝐴onto𝑃 ∧ (𝑦𝑃 (𝐹𝑦)):𝑃1-1-onto→(𝐹𝐴) ∧ ( I ↾ (𝐹𝐴)):(𝐹𝐴)–1-1𝐵) ∧ 𝐹 = ((( I ↾ (𝐹𝐴)) ∘ (𝑦𝑃 (𝐹𝑦))) ∘ (𝑎𝐴 ↦ (𝐹 “ {(𝐹𝑎)}))))))
8584spc3egv 3542 . 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 1086   = wceq 1539  wex 1782  wcel 2106  {cab 2715  wrex 3065  Vcvv 3432  wss 3887  {csn 4561   cuni 4839  cmpt 5157   I cid 5488  ccnv 5588  ran crn 5590  cres 5591  cima 5592  ccom 5593  Fun wfun 6427   Fn wfn 6428  wf 6429  1-1wf1 6430  ontowfo 6431  1-1-ontowf1o 6432  cfv 6433
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441
This theorem is referenced by:  fundcmpsurinjpreimafv  44860  fundcmpsurbijinj  44862
  Copyright terms: Public domain W3C validator