Metamath Proof Explorer


Theorem itgex

Description: An integral is a set. (Contributed by Mario Carneiro, 28-Jun-2014)

Ref Expression
Assertion itgex โˆซ ๐ด ๐ต d ๐‘ฅ โˆˆ V

Proof

Step Hyp Ref Expression
1 df-itg โŠข โˆซ ๐ด ๐ต d ๐‘ฅ = ฮฃ ๐‘˜ โˆˆ ( 0 ... 3 ) ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ โฆ‹ ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) / ๐‘ฆ โฆŒ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ๐‘ฆ ) , ๐‘ฆ , 0 ) ) ) )
2 sumex โŠข ฮฃ ๐‘˜ โˆˆ ( 0 ... 3 ) ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ โฆ‹ ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) / ๐‘ฆ โฆŒ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ๐‘ฆ ) , ๐‘ฆ , 0 ) ) ) ) โˆˆ V
3 1 2 eqeltri โŠข โˆซ ๐ด ๐ต d ๐‘ฅ โˆˆ V