Metamath Proof Explorer

Theorem eulerpartlemt

Description: Lemma for eulerpart . (Contributed by Thierry Arnoux, 19-Sep-2017)

Ref Expression
Hypotheses eulerpart.p โŠข ๐‘ƒ = { ๐‘“ โˆˆ ( โ„•0 โ†‘m โ„• ) โˆฃ ( ( โ—ก ๐‘“ โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘“ โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) }
eulerpart.o โŠข ๐‘‚ = { ๐‘” โˆˆ ๐‘ƒ โˆฃ โˆ€ ๐‘› โˆˆ ( โ—ก ๐‘” โ€œ โ„• ) ยฌ 2 โˆฅ ๐‘› }
eulerpart.d โŠข ๐ท = { ๐‘” โˆˆ ๐‘ƒ โˆฃ โˆ€ ๐‘› โˆˆ โ„• ( ๐‘” โ€˜ ๐‘› ) โ‰ค 1 }
eulerpart.j โŠข ๐ฝ = { ๐‘ง โˆˆ โ„• โˆฃ ยฌ 2 โˆฅ ๐‘ง }
eulerpart.f โŠข ๐น = ( ๐‘ฅ โˆˆ ๐ฝ , ๐‘ฆ โˆˆ โ„•0 โ†ฆ ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) )
eulerpart.h โŠข ๐ป = { ๐‘Ÿ โˆˆ ( ( ๐’ซ โ„•0 โˆฉ Fin ) โ†‘m ๐ฝ ) โˆฃ ( ๐‘Ÿ supp โˆ… ) โˆˆ Fin }
eulerpart.m โŠข ๐‘€ = ( ๐‘Ÿ โˆˆ ๐ป โ†ฆ { โŸจ ๐‘ฅ , ๐‘ฆ โŸฉ โˆฃ ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) ) } )
eulerpart.r โŠข ๐‘… = { ๐‘“ โˆฃ ( โ—ก ๐‘“ โ€œ โ„• ) โˆˆ Fin }
eulerpart.t โŠข ๐‘‡ = { ๐‘“ โˆˆ ( โ„•0 โ†‘m โ„• ) โˆฃ ( โ—ก ๐‘“ โ€œ โ„• ) โŠ† ๐ฝ }
Assertion eulerpartlemt ( ( โ„•0 โ†‘m ๐ฝ ) โˆฉ ๐‘… ) = ran ( ๐‘š โˆˆ ( ๐‘‡ โˆฉ ๐‘… ) โ†ฆ ( ๐‘š โ†พ ๐ฝ ) )

Proof

Step Hyp Ref Expression
1 eulerpart.p โŠข ๐‘ƒ = { ๐‘“ โˆˆ ( โ„•0 โ†‘m โ„• ) โˆฃ ( ( โ—ก ๐‘“ โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘“ โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) }
2 eulerpart.o โŠข ๐‘‚ = { ๐‘” โˆˆ ๐‘ƒ โˆฃ โˆ€ ๐‘› โˆˆ ( โ—ก ๐‘” โ€œ โ„• ) ยฌ 2 โˆฅ ๐‘› }
3 eulerpart.d โŠข ๐ท = { ๐‘” โˆˆ ๐‘ƒ โˆฃ โˆ€ ๐‘› โˆˆ โ„• ( ๐‘” โ€˜ ๐‘› ) โ‰ค 1 }
4 eulerpart.j โŠข ๐ฝ = { ๐‘ง โˆˆ โ„• โˆฃ ยฌ 2 โˆฅ ๐‘ง }
5 eulerpart.f โŠข ๐น = ( ๐‘ฅ โˆˆ ๐ฝ , ๐‘ฆ โˆˆ โ„•0 โ†ฆ ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) )
6 eulerpart.h โŠข ๐ป = { ๐‘Ÿ โˆˆ ( ( ๐’ซ โ„•0 โˆฉ Fin ) โ†‘m ๐ฝ ) โˆฃ ( ๐‘Ÿ supp โˆ… ) โˆˆ Fin }
7 eulerpart.m โŠข ๐‘€ = ( ๐‘Ÿ โˆˆ ๐ป โ†ฆ { โŸจ ๐‘ฅ , ๐‘ฆ โŸฉ โˆฃ ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) ) } )
8 eulerpart.r โŠข ๐‘… = { ๐‘“ โˆฃ ( โ—ก ๐‘“ โ€œ โ„• ) โˆˆ Fin }
9 eulerpart.t โŠข ๐‘‡ = { ๐‘“ โˆˆ ( โ„•0 โ†‘m โ„• ) โˆฃ ( โ—ก ๐‘“ โ€œ โ„• ) โŠ† ๐ฝ }
10 elmapi โŠข ( ๐‘œ โˆˆ ( โ„•0 โ†‘m ๐ฝ ) โ†’ ๐‘œ : ๐ฝ โŸถ โ„•0 )
11 10 adantr โŠข ( ( ๐‘œ โˆˆ ( โ„•0 โ†‘m ๐ฝ ) โˆง ๐‘œ โˆˆ ๐‘… ) โ†’ ๐‘œ : ๐ฝ โŸถ โ„•0 )
12 c0ex โŠข 0 โˆˆ V
13 12 fconst โŠข ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) : ( โ„• โˆ– ๐ฝ ) โŸถ { 0 }
14 13 a1i โŠข ( ( ๐‘œ โˆˆ ( โ„•0 โ†‘m ๐ฝ ) โˆง ๐‘œ โˆˆ ๐‘… ) โ†’ ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) : ( โ„• โˆ– ๐ฝ ) โŸถ { 0 } )
15 disjdif โŠข ( ๐ฝ โˆฉ ( โ„• โˆ– ๐ฝ ) ) = โˆ…
16 15 a1i โŠข ( ( ๐‘œ โˆˆ ( โ„•0 โ†‘m ๐ฝ ) โˆง ๐‘œ โˆˆ ๐‘… ) โ†’ ( ๐ฝ โˆฉ ( โ„• โˆ– ๐ฝ ) ) = โˆ… )
17 fun โŠข ( ( ( ๐‘œ : ๐ฝ โŸถ โ„•0 โˆง ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) : ( โ„• โˆ– ๐ฝ ) โŸถ { 0 } ) โˆง ( ๐ฝ โˆฉ ( โ„• โˆ– ๐ฝ ) ) = โˆ… ) โ†’ ( ๐‘œ โˆช ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) ) : ( ๐ฝ โˆช ( โ„• โˆ– ๐ฝ ) ) โŸถ ( โ„•0 โˆช { 0 } ) )
18 11 14 16 17 syl21anc โŠข ( ( ๐‘œ โˆˆ ( โ„•0 โ†‘m ๐ฝ ) โˆง ๐‘œ โˆˆ ๐‘… ) โ†’ ( ๐‘œ โˆช ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) ) : ( ๐ฝ โˆช ( โ„• โˆ– ๐ฝ ) ) โŸถ ( โ„•0 โˆช { 0 } ) )
19 ssrab2 โŠข { ๐‘ง โˆˆ โ„• โˆฃ ยฌ 2 โˆฅ ๐‘ง } โŠ† โ„•
20 4 19 eqsstri โŠข ๐ฝ โŠ† โ„•
21 undif โŠข ( ๐ฝ โŠ† โ„• โ†” ( ๐ฝ โˆช ( โ„• โˆ– ๐ฝ ) ) = โ„• )
22 20 21 mpbi โŠข ( ๐ฝ โˆช ( โ„• โˆ– ๐ฝ ) ) = โ„•
23 0nn0 โŠข 0 โˆˆ โ„•0
24 snssi โŠข ( 0 โˆˆ โ„•0 โ†’ { 0 } โŠ† โ„•0 )
25 23 24 ax-mp โŠข { 0 } โŠ† โ„•0
26 ssequn2 โŠข ( { 0 } โŠ† โ„•0 โ†” ( โ„•0 โˆช { 0 } ) = โ„•0 )
27 25 26 mpbi โŠข ( โ„•0 โˆช { 0 } ) = โ„•0
28 22 27 feq23i โŠข ( ( ๐‘œ โˆช ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) ) : ( ๐ฝ โˆช ( โ„• โˆ– ๐ฝ ) ) โŸถ ( โ„•0 โˆช { 0 } ) โ†” ( ๐‘œ โˆช ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) ) : โ„• โŸถ โ„•0 )
29 18 28 sylib โŠข ( ( ๐‘œ โˆˆ ( โ„•0 โ†‘m ๐ฝ ) โˆง ๐‘œ โˆˆ ๐‘… ) โ†’ ( ๐‘œ โˆช ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) ) : โ„• โŸถ โ„•0 )
30 nn0ex โŠข โ„•0 โˆˆ V
31 nnex โŠข โ„• โˆˆ V
32 30 31 elmap โŠข ( ( ๐‘œ โˆช ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) ) โˆˆ ( โ„•0 โ†‘m โ„• ) โ†” ( ๐‘œ โˆช ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) ) : โ„• โŸถ โ„•0 )
33 29 32 sylibr โŠข ( ( ๐‘œ โˆˆ ( โ„•0 โ†‘m ๐ฝ ) โˆง ๐‘œ โˆˆ ๐‘… ) โ†’ ( ๐‘œ โˆช ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) ) โˆˆ ( โ„•0 โ†‘m โ„• ) )
34 cnvun โŠข โ—ก ( ๐‘œ โˆช ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) ) = ( โ—ก ๐‘œ โˆช โ—ก ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) )
35 34 imaeq1i โŠข ( โ—ก ( ๐‘œ โˆช ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) ) โ€œ โ„• ) = ( ( โ—ก ๐‘œ โˆช โ—ก ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) ) โ€œ โ„• )
36 imaundir โŠข ( ( โ—ก ๐‘œ โˆช โ—ก ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) ) โ€œ โ„• ) = ( ( โ—ก ๐‘œ โ€œ โ„• ) โˆช ( โ—ก ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) โ€œ โ„• ) )
37 35 36 eqtri โŠข ( โ—ก ( ๐‘œ โˆช ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) ) โ€œ โ„• ) = ( ( โ—ก ๐‘œ โ€œ โ„• ) โˆช ( โ—ก ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) โ€œ โ„• ) )
38 vex โŠข ๐‘œ โˆˆ V
39 cnveq โŠข ( ๐‘“ = ๐‘œ โ†’ โ—ก ๐‘“ = โ—ก ๐‘œ )
40 39 imaeq1d โŠข ( ๐‘“ = ๐‘œ โ†’ ( โ—ก ๐‘“ โ€œ โ„• ) = ( โ—ก ๐‘œ โ€œ โ„• ) )
41 40 eleq1d โŠข ( ๐‘“ = ๐‘œ โ†’ ( ( โ—ก ๐‘“ โ€œ โ„• ) โˆˆ Fin โ†” ( โ—ก ๐‘œ โ€œ โ„• ) โˆˆ Fin ) )
42 38 41 8 elab2 โŠข ( ๐‘œ โˆˆ ๐‘… โ†” ( โ—ก ๐‘œ โ€œ โ„• ) โˆˆ Fin )
43 42 biimpi โŠข ( ๐‘œ โˆˆ ๐‘… โ†’ ( โ—ก ๐‘œ โ€œ โ„• ) โˆˆ Fin )
44 43 adantl โŠข ( ( ๐‘œ โˆˆ ( โ„•0 โ†‘m ๐ฝ ) โˆง ๐‘œ โˆˆ ๐‘… ) โ†’ ( โ—ก ๐‘œ โ€œ โ„• ) โˆˆ Fin )
45 cnvxp โŠข โ—ก ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) = ( { 0 } ร— ( โ„• โˆ– ๐ฝ ) )
46 45 dmeqi โŠข dom โ—ก ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) = dom ( { 0 } ร— ( โ„• โˆ– ๐ฝ ) )
47 2nn โŠข 2 โˆˆ โ„•
48 2z โŠข 2 โˆˆ โ„ค
49 iddvds โŠข ( 2 โˆˆ โ„ค โ†’ 2 โˆฅ 2 )
50 48 49 ax-mp โŠข 2 โˆฅ 2
51 breq2 โŠข ( ๐‘ง = 2 โ†’ ( 2 โˆฅ ๐‘ง โ†” 2 โˆฅ 2 ) )
52 51 notbid โŠข ( ๐‘ง = 2 โ†’ ( ยฌ 2 โˆฅ ๐‘ง โ†” ยฌ 2 โˆฅ 2 ) )
53 52 4 elrab2 โŠข ( 2 โˆˆ ๐ฝ โ†” ( 2 โˆˆ โ„• โˆง ยฌ 2 โˆฅ 2 ) )
54 53 simprbi โŠข ( 2 โˆˆ ๐ฝ โ†’ ยฌ 2 โˆฅ 2 )
55 50 54 mt2 โŠข ยฌ 2 โˆˆ ๐ฝ
56 eldif โŠข ( 2 โˆˆ ( โ„• โˆ– ๐ฝ ) โ†” ( 2 โˆˆ โ„• โˆง ยฌ 2 โˆˆ ๐ฝ ) )
57 47 55 56 mpbir2an โŠข 2 โˆˆ ( โ„• โˆ– ๐ฝ )
58 ne0i โŠข ( 2 โˆˆ ( โ„• โˆ– ๐ฝ ) โ†’ ( โ„• โˆ– ๐ฝ ) โ‰  โˆ… )
59 dmxp โŠข ( ( โ„• โˆ– ๐ฝ ) โ‰  โˆ… โ†’ dom ( { 0 } ร— ( โ„• โˆ– ๐ฝ ) ) = { 0 } )
60 57 58 59 mp2b โŠข dom ( { 0 } ร— ( โ„• โˆ– ๐ฝ ) ) = { 0 }
61 46 60 eqtri โŠข dom โ—ก ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) = { 0 }
62 61 ineq1i โŠข ( dom โ—ก ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) โˆฉ โ„• ) = ( { 0 } โˆฉ โ„• )
63 incom โŠข ( โ„• โˆฉ { 0 } ) = ( { 0 } โˆฉ โ„• )
64 0nnn โŠข ยฌ 0 โˆˆ โ„•
65 disjsn โŠข ( ( โ„• โˆฉ { 0 } ) = โˆ… โ†” ยฌ 0 โˆˆ โ„• )
66 64 65 mpbir โŠข ( โ„• โˆฉ { 0 } ) = โˆ…
67 62 63 66 3eqtr2i โŠข ( dom โ—ก ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) โˆฉ โ„• ) = โˆ…
68 imadisj โŠข ( ( โ—ก ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) โ€œ โ„• ) = โˆ… โ†” ( dom โ—ก ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) โˆฉ โ„• ) = โˆ… )
69 67 68 mpbir โŠข ( โ—ก ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) โ€œ โ„• ) = โˆ…
70 0fin โŠข โˆ… โˆˆ Fin
71 69 70 eqeltri โŠข ( โ—ก ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) โ€œ โ„• ) โˆˆ Fin
72 unfi โŠข ( ( ( โ—ก ๐‘œ โ€œ โ„• ) โˆˆ Fin โˆง ( โ—ก ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) โ€œ โ„• ) โˆˆ Fin ) โ†’ ( ( โ—ก ๐‘œ โ€œ โ„• ) โˆช ( โ—ก ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) โ€œ โ„• ) ) โˆˆ Fin )
73 44 71 72 sylancl โŠข ( ( ๐‘œ โˆˆ ( โ„•0 โ†‘m ๐ฝ ) โˆง ๐‘œ โˆˆ ๐‘… ) โ†’ ( ( โ—ก ๐‘œ โ€œ โ„• ) โˆช ( โ—ก ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) โ€œ โ„• ) ) โˆˆ Fin )
74 37 73 eqeltrid โŠข ( ( ๐‘œ โˆˆ ( โ„•0 โ†‘m ๐ฝ ) โˆง ๐‘œ โˆˆ ๐‘… ) โ†’ ( โ—ก ( ๐‘œ โˆช ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) ) โ€œ โ„• ) โˆˆ Fin )
75 cnvimass โŠข ( โ—ก ๐‘œ โ€œ โ„• ) โŠ† dom ๐‘œ
76 75 11 fssdm โŠข ( ( ๐‘œ โˆˆ ( โ„•0 โ†‘m ๐ฝ ) โˆง ๐‘œ โˆˆ ๐‘… ) โ†’ ( โ—ก ๐‘œ โ€œ โ„• ) โŠ† ๐ฝ )
77 0ss โŠข โˆ… โŠ† ๐ฝ
78 69 77 eqsstri โŠข ( โ—ก ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) โ€œ โ„• ) โŠ† ๐ฝ
79 78 a1i โŠข ( ( ๐‘œ โˆˆ ( โ„•0 โ†‘m ๐ฝ ) โˆง ๐‘œ โˆˆ ๐‘… ) โ†’ ( โ—ก ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) โ€œ โ„• ) โŠ† ๐ฝ )
80 76 79 unssd โŠข ( ( ๐‘œ โˆˆ ( โ„•0 โ†‘m ๐ฝ ) โˆง ๐‘œ โˆˆ ๐‘… ) โ†’ ( ( โ—ก ๐‘œ โ€œ โ„• ) โˆช ( โ—ก ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) โ€œ โ„• ) ) โŠ† ๐ฝ )
81 37 80 eqsstrid โŠข ( ( ๐‘œ โˆˆ ( โ„•0 โ†‘m ๐ฝ ) โˆง ๐‘œ โˆˆ ๐‘… ) โ†’ ( โ—ก ( ๐‘œ โˆช ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) ) โ€œ โ„• ) โŠ† ๐ฝ )
82 1 2 3 4 5 6 7 8 9 eulerpartlemt0 โŠข ( ( ๐‘œ โˆช ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) ) โˆˆ ( ๐‘‡ โˆฉ ๐‘… ) โ†” ( ( ๐‘œ โˆช ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) ) โˆˆ ( โ„•0 โ†‘m โ„• ) โˆง ( โ—ก ( ๐‘œ โˆช ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) ) โ€œ โ„• ) โˆˆ Fin โˆง ( โ—ก ( ๐‘œ โˆช ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) ) โ€œ โ„• ) โŠ† ๐ฝ ) )
83 33 74 81 82 syl3anbrc โŠข ( ( ๐‘œ โˆˆ ( โ„•0 โ†‘m ๐ฝ ) โˆง ๐‘œ โˆˆ ๐‘… ) โ†’ ( ๐‘œ โˆช ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) ) โˆˆ ( ๐‘‡ โˆฉ ๐‘… ) )
84 resundir โŠข ( ( ๐‘œ โˆช ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) ) โ†พ ๐ฝ ) = ( ( ๐‘œ โ†พ ๐ฝ ) โˆช ( ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) โ†พ ๐ฝ ) )
85 ffn โŠข ( ๐‘œ : ๐ฝ โŸถ โ„•0 โ†’ ๐‘œ Fn ๐ฝ )
86 fnresdm โŠข ( ๐‘œ Fn ๐ฝ โ†’ ( ๐‘œ โ†พ ๐ฝ ) = ๐‘œ )
87 disjdifr โŠข ( ( โ„• โˆ– ๐ฝ ) โˆฉ ๐ฝ ) = โˆ…
88 fnconstg โŠข ( 0 โˆˆ โ„•0 โ†’ ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) Fn ( โ„• โˆ– ๐ฝ ) )
89 fnresdisj โŠข ( ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) Fn ( โ„• โˆ– ๐ฝ ) โ†’ ( ( ( โ„• โˆ– ๐ฝ ) โˆฉ ๐ฝ ) = โˆ… โ†” ( ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) โ†พ ๐ฝ ) = โˆ… ) )
90 23 88 89 mp2b โŠข ( ( ( โ„• โˆ– ๐ฝ ) โˆฉ ๐ฝ ) = โˆ… โ†” ( ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) โ†พ ๐ฝ ) = โˆ… )
91 87 90 mpbi โŠข ( ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) โ†พ ๐ฝ ) = โˆ…
92 91 a1i โŠข ( ๐‘œ Fn ๐ฝ โ†’ ( ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) โ†พ ๐ฝ ) = โˆ… )
93 86 92 uneq12d โŠข ( ๐‘œ Fn ๐ฝ โ†’ ( ( ๐‘œ โ†พ ๐ฝ ) โˆช ( ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) โ†พ ๐ฝ ) ) = ( ๐‘œ โˆช โˆ… ) )
94 11 85 93 3syl โŠข ( ( ๐‘œ โˆˆ ( โ„•0 โ†‘m ๐ฝ ) โˆง ๐‘œ โˆˆ ๐‘… ) โ†’ ( ( ๐‘œ โ†พ ๐ฝ ) โˆช ( ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) โ†พ ๐ฝ ) ) = ( ๐‘œ โˆช โˆ… ) )
95 un0 โŠข ( ๐‘œ โˆช โˆ… ) = ๐‘œ
96 94 95 eqtrdi โŠข ( ( ๐‘œ โˆˆ ( โ„•0 โ†‘m ๐ฝ ) โˆง ๐‘œ โˆˆ ๐‘… ) โ†’ ( ( ๐‘œ โ†พ ๐ฝ ) โˆช ( ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) โ†พ ๐ฝ ) ) = ๐‘œ )
97 84 96 eqtr2id โŠข ( ( ๐‘œ โˆˆ ( โ„•0 โ†‘m ๐ฝ ) โˆง ๐‘œ โˆˆ ๐‘… ) โ†’ ๐‘œ = ( ( ๐‘œ โˆช ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) ) โ†พ ๐ฝ ) )
98 reseq1 โŠข ( ๐‘š = ( ๐‘œ โˆช ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) ) โ†’ ( ๐‘š โ†พ ๐ฝ ) = ( ( ๐‘œ โˆช ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) ) โ†พ ๐ฝ ) )
99 98 rspceeqv โŠข ( ( ( ๐‘œ โˆช ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) ) โˆˆ ( ๐‘‡ โˆฉ ๐‘… ) โˆง ๐‘œ = ( ( ๐‘œ โˆช ( ( โ„• โˆ– ๐ฝ ) ร— { 0 } ) ) โ†พ ๐ฝ ) ) โ†’ โˆƒ ๐‘š โˆˆ ( ๐‘‡ โˆฉ ๐‘… ) ๐‘œ = ( ๐‘š โ†พ ๐ฝ ) )
100 83 97 99 syl2anc โŠข ( ( ๐‘œ โˆˆ ( โ„•0 โ†‘m ๐ฝ ) โˆง ๐‘œ โˆˆ ๐‘… ) โ†’ โˆƒ ๐‘š โˆˆ ( ๐‘‡ โˆฉ ๐‘… ) ๐‘œ = ( ๐‘š โ†พ ๐ฝ ) )
101 simpr โŠข ( ( ๐‘š โˆˆ ( ๐‘‡ โˆฉ ๐‘… ) โˆง ๐‘œ = ( ๐‘š โ†พ ๐ฝ ) ) โ†’ ๐‘œ = ( ๐‘š โ†พ ๐ฝ ) )
102 simpl โŠข ( ( ๐‘š โˆˆ ( ๐‘‡ โˆฉ ๐‘… ) โˆง ๐‘œ = ( ๐‘š โ†พ ๐ฝ ) ) โ†’ ๐‘š โˆˆ ( ๐‘‡ โˆฉ ๐‘… ) )
103 1 2 3 4 5 6 7 8 9 eulerpartlemt0 โŠข ( ๐‘š โˆˆ ( ๐‘‡ โˆฉ ๐‘… ) โ†” ( ๐‘š โˆˆ ( โ„•0 โ†‘m โ„• ) โˆง ( โ—ก ๐‘š โ€œ โ„• ) โˆˆ Fin โˆง ( โ—ก ๐‘š โ€œ โ„• ) โŠ† ๐ฝ ) )
104 102 103 sylib โŠข ( ( ๐‘š โˆˆ ( ๐‘‡ โˆฉ ๐‘… ) โˆง ๐‘œ = ( ๐‘š โ†พ ๐ฝ ) ) โ†’ ( ๐‘š โˆˆ ( โ„•0 โ†‘m โ„• ) โˆง ( โ—ก ๐‘š โ€œ โ„• ) โˆˆ Fin โˆง ( โ—ก ๐‘š โ€œ โ„• ) โŠ† ๐ฝ ) )
105 104 simp1d โŠข ( ( ๐‘š โˆˆ ( ๐‘‡ โˆฉ ๐‘… ) โˆง ๐‘œ = ( ๐‘š โ†พ ๐ฝ ) ) โ†’ ๐‘š โˆˆ ( โ„•0 โ†‘m โ„• ) )
106 30 31 elmap โŠข ( ๐‘š โˆˆ ( โ„•0 โ†‘m โ„• ) โ†” ๐‘š : โ„• โŸถ โ„•0 )
107 105 106 sylib โŠข ( ( ๐‘š โˆˆ ( ๐‘‡ โˆฉ ๐‘… ) โˆง ๐‘œ = ( ๐‘š โ†พ ๐ฝ ) ) โ†’ ๐‘š : โ„• โŸถ โ„•0 )
108 fssres โŠข ( ( ๐‘š : โ„• โŸถ โ„•0 โˆง ๐ฝ โŠ† โ„• ) โ†’ ( ๐‘š โ†พ ๐ฝ ) : ๐ฝ โŸถ โ„•0 )
109 107 20 108 sylancl โŠข ( ( ๐‘š โˆˆ ( ๐‘‡ โˆฉ ๐‘… ) โˆง ๐‘œ = ( ๐‘š โ†พ ๐ฝ ) ) โ†’ ( ๐‘š โ†พ ๐ฝ ) : ๐ฝ โŸถ โ„•0 )
110 4 31 rabex2 โŠข ๐ฝ โˆˆ V
111 30 110 elmap โŠข ( ( ๐‘š โ†พ ๐ฝ ) โˆˆ ( โ„•0 โ†‘m ๐ฝ ) โ†” ( ๐‘š โ†พ ๐ฝ ) : ๐ฝ โŸถ โ„•0 )
112 109 111 sylibr โŠข ( ( ๐‘š โˆˆ ( ๐‘‡ โˆฉ ๐‘… ) โˆง ๐‘œ = ( ๐‘š โ†พ ๐ฝ ) ) โ†’ ( ๐‘š โ†พ ๐ฝ ) โˆˆ ( โ„•0 โ†‘m ๐ฝ ) )
113 101 112 eqeltrd โŠข ( ( ๐‘š โˆˆ ( ๐‘‡ โˆฉ ๐‘… ) โˆง ๐‘œ = ( ๐‘š โ†พ ๐ฝ ) ) โ†’ ๐‘œ โˆˆ ( โ„•0 โ†‘m ๐ฝ ) )
114 ffun โŠข ( ๐‘š : โ„• โŸถ โ„•0 โ†’ Fun ๐‘š )
115 respreima โŠข ( Fun ๐‘š โ†’ ( โ—ก ( ๐‘š โ†พ ๐ฝ ) โ€œ โ„• ) = ( ( โ—ก ๐‘š โ€œ โ„• ) โˆฉ ๐ฝ ) )
116 107 114 115 3syl โŠข ( ( ๐‘š โˆˆ ( ๐‘‡ โˆฉ ๐‘… ) โˆง ๐‘œ = ( ๐‘š โ†พ ๐ฝ ) ) โ†’ ( โ—ก ( ๐‘š โ†พ ๐ฝ ) โ€œ โ„• ) = ( ( โ—ก ๐‘š โ€œ โ„• ) โˆฉ ๐ฝ ) )
117 104 simp2d โŠข ( ( ๐‘š โˆˆ ( ๐‘‡ โˆฉ ๐‘… ) โˆง ๐‘œ = ( ๐‘š โ†พ ๐ฝ ) ) โ†’ ( โ—ก ๐‘š โ€œ โ„• ) โˆˆ Fin )
118 infi โŠข ( ( โ—ก ๐‘š โ€œ โ„• ) โˆˆ Fin โ†’ ( ( โ—ก ๐‘š โ€œ โ„• ) โˆฉ ๐ฝ ) โˆˆ Fin )
119 117 118 syl โŠข ( ( ๐‘š โˆˆ ( ๐‘‡ โˆฉ ๐‘… ) โˆง ๐‘œ = ( ๐‘š โ†พ ๐ฝ ) ) โ†’ ( ( โ—ก ๐‘š โ€œ โ„• ) โˆฉ ๐ฝ ) โˆˆ Fin )
120 116 119 eqeltrd โŠข ( ( ๐‘š โˆˆ ( ๐‘‡ โˆฉ ๐‘… ) โˆง ๐‘œ = ( ๐‘š โ†พ ๐ฝ ) ) โ†’ ( โ—ก ( ๐‘š โ†พ ๐ฝ ) โ€œ โ„• ) โˆˆ Fin )
121 vex โŠข ๐‘š โˆˆ V
122 121 resex โŠข ( ๐‘š โ†พ ๐ฝ ) โˆˆ V
123 cnveq โŠข ( ๐‘“ = ( ๐‘š โ†พ ๐ฝ ) โ†’ โ—ก ๐‘“ = โ—ก ( ๐‘š โ†พ ๐ฝ ) )
124 123 imaeq1d โŠข ( ๐‘“ = ( ๐‘š โ†พ ๐ฝ ) โ†’ ( โ—ก ๐‘“ โ€œ โ„• ) = ( โ—ก ( ๐‘š โ†พ ๐ฝ ) โ€œ โ„• ) )
125 124 eleq1d โŠข ( ๐‘“ = ( ๐‘š โ†พ ๐ฝ ) โ†’ ( ( โ—ก ๐‘“ โ€œ โ„• ) โˆˆ Fin โ†” ( โ—ก ( ๐‘š โ†พ ๐ฝ ) โ€œ โ„• ) โˆˆ Fin ) )
126 122 125 8 elab2 โŠข ( ( ๐‘š โ†พ ๐ฝ ) โˆˆ ๐‘… โ†” ( โ—ก ( ๐‘š โ†พ ๐ฝ ) โ€œ โ„• ) โˆˆ Fin )
127 120 126 sylibr โŠข ( ( ๐‘š โˆˆ ( ๐‘‡ โˆฉ ๐‘… ) โˆง ๐‘œ = ( ๐‘š โ†พ ๐ฝ ) ) โ†’ ( ๐‘š โ†พ ๐ฝ ) โˆˆ ๐‘… )
128 101 127 eqeltrd โŠข ( ( ๐‘š โˆˆ ( ๐‘‡ โˆฉ ๐‘… ) โˆง ๐‘œ = ( ๐‘š โ†พ ๐ฝ ) ) โ†’ ๐‘œ โˆˆ ๐‘… )
129 113 128 jca โŠข ( ( ๐‘š โˆˆ ( ๐‘‡ โˆฉ ๐‘… ) โˆง ๐‘œ = ( ๐‘š โ†พ ๐ฝ ) ) โ†’ ( ๐‘œ โˆˆ ( โ„•0 โ†‘m ๐ฝ ) โˆง ๐‘œ โˆˆ ๐‘… ) )
130 129 rexlimiva โŠข ( โˆƒ ๐‘š โˆˆ ( ๐‘‡ โˆฉ ๐‘… ) ๐‘œ = ( ๐‘š โ†พ ๐ฝ ) โ†’ ( ๐‘œ โˆˆ ( โ„•0 โ†‘m ๐ฝ ) โˆง ๐‘œ โˆˆ ๐‘… ) )
131 100 130 impbii โŠข ( ( ๐‘œ โˆˆ ( โ„•0 โ†‘m ๐ฝ ) โˆง ๐‘œ โˆˆ ๐‘… ) โ†” โˆƒ ๐‘š โˆˆ ( ๐‘‡ โˆฉ ๐‘… ) ๐‘œ = ( ๐‘š โ†พ ๐ฝ ) )
132 131 abbii โŠข { ๐‘œ โˆฃ ( ๐‘œ โˆˆ ( โ„•0 โ†‘m ๐ฝ ) โˆง ๐‘œ โˆˆ ๐‘… ) } = { ๐‘œ โˆฃ โˆƒ ๐‘š โˆˆ ( ๐‘‡ โˆฉ ๐‘… ) ๐‘œ = ( ๐‘š โ†พ ๐ฝ ) }
133 df-in โŠข ( ( โ„•0 โ†‘m ๐ฝ ) โˆฉ ๐‘… ) = { ๐‘œ โˆฃ ( ๐‘œ โˆˆ ( โ„•0 โ†‘m ๐ฝ ) โˆง ๐‘œ โˆˆ ๐‘… ) }
134 eqid โŠข ( ๐‘š โˆˆ ( ๐‘‡ โˆฉ ๐‘… ) โ†ฆ ( ๐‘š โ†พ ๐ฝ ) ) = ( ๐‘š โˆˆ ( ๐‘‡ โˆฉ ๐‘… ) โ†ฆ ( ๐‘š โ†พ ๐ฝ ) )
135 134 rnmpt โŠข ran ( ๐‘š โˆˆ ( ๐‘‡ โˆฉ ๐‘… ) โ†ฆ ( ๐‘š โ†พ ๐ฝ ) ) = { ๐‘œ โˆฃ โˆƒ ๐‘š โˆˆ ( ๐‘‡ โˆฉ ๐‘… ) ๐‘œ = ( ๐‘š โ†พ ๐ฝ ) }
136 132 133 135 3eqtr4i โŠข ( ( โ„•0 โ†‘m ๐ฝ ) โˆฉ ๐‘… ) = ran ( ๐‘š โˆˆ ( ๐‘‡ โˆฉ ๐‘… ) โ†ฆ ( ๐‘š โ†พ ๐ฝ ) )