ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  fprod2dlemstep GIF version

Theorem fprod2dlemstep 11650
Description: Lemma for fprod2d 11651- induction step. (Contributed by Scott Fenton, 30-Jan-2018.)
Hypotheses
Ref Expression
fprod2d.1 (๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ โ†’ ๐ท = ๐ถ)
fprod2d.2 (๐œ‘ โ†’ ๐ด โˆˆ Fin)
fprod2d.3 ((๐œ‘ โˆง ๐‘— โˆˆ ๐ด) โ†’ ๐ต โˆˆ Fin)
fprod2d.4 ((๐œ‘ โˆง (๐‘— โˆˆ ๐ด โˆง ๐‘˜ โˆˆ ๐ต)) โ†’ ๐ถ โˆˆ โ„‚)
fprod2d.5 (๐œ‘ โ†’ ยฌ ๐‘ฆ โˆˆ ๐‘ฅ)
fprod2d.6 (๐œ‘ โ†’ (๐‘ฅ โˆช {๐‘ฆ}) โІ ๐ด)
fprod2dlemstep.x (๐œ‘ โ†’ ๐‘ฅ โˆˆ Fin)
fprod2d.7 (๐œ“ โ†” โˆ๐‘— โˆˆ ๐‘ฅ โˆ๐‘˜ โˆˆ ๐ต ๐ถ = โˆ๐‘ง โˆˆ โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต)๐ท)
Assertion
Ref Expression
fprod2dlemstep ((๐œ‘ โˆง ๐œ“) โ†’ โˆ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})โˆ๐‘˜ โˆˆ ๐ต ๐ถ = โˆ๐‘ง โˆˆ โˆช ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})({๐‘—} ร— ๐ต)๐ท)
Distinct variable groups:   ๐ด,๐‘—,๐‘˜   ๐ต,๐‘˜,๐‘ง   ๐‘ง,๐ถ   ๐ท,๐‘—,๐‘˜   ๐œ‘,๐‘—   ๐‘ฅ,๐‘—   ๐‘ฆ,๐‘—,๐‘ง   ๐œ‘,๐‘˜   ๐‘ฅ,๐‘˜   ๐‘ฆ,๐‘˜,๐‘ง   ๐œ‘,๐‘ง   ๐‘ฅ,๐‘ง   ๐‘ฆ,๐‘ง
Allowed substitution hints:   ๐œ‘(๐‘ฅ,๐‘ฆ)   ๐œ“(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘—,๐‘˜)   ๐ด(๐‘ฅ,๐‘ฆ,๐‘ง)   ๐ต(๐‘ฅ,๐‘ฆ,๐‘—)   ๐ถ(๐‘ฅ,๐‘ฆ,๐‘—,๐‘˜)   ๐ท(๐‘ฅ,๐‘ฆ,๐‘ง)

Proof of Theorem fprod2dlemstep
Dummy variable ๐‘š is distinct from all other variables.
StepHypRef Expression
1 simpr 110 . . . 4 ((๐œ‘ โˆง ๐œ“) โ†’ ๐œ“)
2 fprod2d.7 . . . 4 (๐œ“ โ†” โˆ๐‘— โˆˆ ๐‘ฅ โˆ๐‘˜ โˆˆ ๐ต ๐ถ = โˆ๐‘ง โˆˆ โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต)๐ท)
31, 2sylib 122 . . 3 ((๐œ‘ โˆง ๐œ“) โ†’ โˆ๐‘— โˆˆ ๐‘ฅ โˆ๐‘˜ โˆˆ ๐ต ๐ถ = โˆ๐‘ง โˆˆ โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต)๐ท)
4 nfcv 2332 . . . . . 6 โ„ฒ๐‘šโˆ๐‘˜ โˆˆ ๐ต ๐ถ
5 nfcsb1v 3105 . . . . . . 7 โ„ฒ๐‘—โฆ‹๐‘š / ๐‘—โฆŒ๐ต
6 nfcsb1v 3105 . . . . . . 7 โ„ฒ๐‘—โฆ‹๐‘š / ๐‘—โฆŒ๐ถ
75, 6nfcprod 11583 . . . . . 6 โ„ฒ๐‘—โˆ๐‘˜ โˆˆ โฆ‹ ๐‘š / ๐‘—โฆŒ๐ตโฆ‹๐‘š / ๐‘—โฆŒ๐ถ
8 csbeq1a 3081 . . . . . . 7 (๐‘— = ๐‘š โ†’ ๐ต = โฆ‹๐‘š / ๐‘—โฆŒ๐ต)
9 csbeq1a 3081 . . . . . . . 8 (๐‘— = ๐‘š โ†’ ๐ถ = โฆ‹๐‘š / ๐‘—โฆŒ๐ถ)
109adantr 276 . . . . . . 7 ((๐‘— = ๐‘š โˆง ๐‘˜ โˆˆ ๐ต) โ†’ ๐ถ = โฆ‹๐‘š / ๐‘—โฆŒ๐ถ)
118, 10prodeq12dv 11597 . . . . . 6 (๐‘— = ๐‘š โ†’ โˆ๐‘˜ โˆˆ ๐ต ๐ถ = โˆ๐‘˜ โˆˆ โฆ‹ ๐‘š / ๐‘—โฆŒ๐ตโฆ‹๐‘š / ๐‘—โฆŒ๐ถ)
124, 7, 11cbvprodi 11588 . . . . 5 โˆ๐‘— โˆˆ {๐‘ฆ}โˆ๐‘˜ โˆˆ ๐ต ๐ถ = โˆ๐‘š โˆˆ {๐‘ฆ}โˆ๐‘˜ โˆˆ โฆ‹ ๐‘š / ๐‘—โฆŒ๐ตโฆ‹๐‘š / ๐‘—โฆŒ๐ถ
13 fprod2d.6 . . . . . . . . 9 (๐œ‘ โ†’ (๐‘ฅ โˆช {๐‘ฆ}) โІ ๐ด)
1413unssbd 3328 . . . . . . . 8 (๐œ‘ โ†’ {๐‘ฆ} โІ ๐ด)
15 vex 2755 . . . . . . . . 9 ๐‘ฆ โˆˆ V
1615snss 3742 . . . . . . . 8 (๐‘ฆ โˆˆ ๐ด โ†” {๐‘ฆ} โІ ๐ด)
1714, 16sylibr 134 . . . . . . 7 (๐œ‘ โ†’ ๐‘ฆ โˆˆ ๐ด)
18 fprod2d.3 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘— โˆˆ ๐ด) โ†’ ๐ต โˆˆ Fin)
1918ralrimiva 2563 . . . . . . . . 9 (๐œ‘ โ†’ โˆ€๐‘— โˆˆ ๐ด ๐ต โˆˆ Fin)
20 nfcsb1v 3105 . . . . . . . . . . 11 โ„ฒ๐‘—โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต
2120nfel1 2343 . . . . . . . . . 10 โ„ฒ๐‘—โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต โˆˆ Fin
22 csbeq1a 3081 . . . . . . . . . . 11 (๐‘— = ๐‘ฆ โ†’ ๐ต = โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)
2322eleq1d 2258 . . . . . . . . . 10 (๐‘— = ๐‘ฆ โ†’ (๐ต โˆˆ Fin โ†” โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต โˆˆ Fin))
2421, 23rspc 2850 . . . . . . . . 9 (๐‘ฆ โˆˆ ๐ด โ†’ (โˆ€๐‘— โˆˆ ๐ด ๐ต โˆˆ Fin โ†’ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต โˆˆ Fin))
2517, 19, 24sylc 62 . . . . . . . 8 (๐œ‘ โ†’ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต โˆˆ Fin)
26 fprod2d.4 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘— โˆˆ ๐ด โˆง ๐‘˜ โˆˆ ๐ต)) โ†’ ๐ถ โˆˆ โ„‚)
2726ralrimivva 2572 . . . . . . . . . 10 (๐œ‘ โ†’ โˆ€๐‘— โˆˆ ๐ด โˆ€๐‘˜ โˆˆ ๐ต ๐ถ โˆˆ โ„‚)
28 nfcsb1v 3105 . . . . . . . . . . . . 13 โ„ฒ๐‘—โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ
2928nfel1 2343 . . . . . . . . . . . 12 โ„ฒ๐‘—โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ โˆˆ โ„‚
3020, 29nfralw 2527 . . . . . . . . . . 11 โ„ฒ๐‘—โˆ€๐‘˜ โˆˆ โฆ‹ ๐‘ฆ / ๐‘—โฆŒ๐ตโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ โˆˆ โ„‚
31 csbeq1a 3081 . . . . . . . . . . . . 13 (๐‘— = ๐‘ฆ โ†’ ๐ถ = โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ)
3231eleq1d 2258 . . . . . . . . . . . 12 (๐‘— = ๐‘ฆ โ†’ (๐ถ โˆˆ โ„‚ โ†” โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ โˆˆ โ„‚))
3322, 32raleqbidv 2698 . . . . . . . . . . 11 (๐‘— = ๐‘ฆ โ†’ (โˆ€๐‘˜ โˆˆ ๐ต ๐ถ โˆˆ โ„‚ โ†” โˆ€๐‘˜ โˆˆ โฆ‹ ๐‘ฆ / ๐‘—โฆŒ๐ตโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ โˆˆ โ„‚))
3430, 33rspc 2850 . . . . . . . . . 10 (๐‘ฆ โˆˆ ๐ด โ†’ (โˆ€๐‘— โˆˆ ๐ด โˆ€๐‘˜ โˆˆ ๐ต ๐ถ โˆˆ โ„‚ โ†’ โˆ€๐‘˜ โˆˆ โฆ‹ ๐‘ฆ / ๐‘—โฆŒ๐ตโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ โˆˆ โ„‚))
3517, 27, 34sylc 62 . . . . . . . . 9 (๐œ‘ โ†’ โˆ€๐‘˜ โˆˆ โฆ‹ ๐‘ฆ / ๐‘—โฆŒ๐ตโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ โˆˆ โ„‚)
3635r19.21bi 2578 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต) โ†’ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ โˆˆ โ„‚)
3725, 36fprodcl 11635 . . . . . . 7 (๐œ‘ โ†’ โˆ๐‘˜ โˆˆ โฆ‹ ๐‘ฆ / ๐‘—โฆŒ๐ตโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ โˆˆ โ„‚)
38 csbeq1 3075 . . . . . . . . 9 (๐‘š = ๐‘ฆ โ†’ โฆ‹๐‘š / ๐‘—โฆŒ๐ต = โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)
39 csbeq1 3075 . . . . . . . . . 10 (๐‘š = ๐‘ฆ โ†’ โฆ‹๐‘š / ๐‘—โฆŒ๐ถ = โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ)
4039adantr 276 . . . . . . . . 9 ((๐‘š = ๐‘ฆ โˆง ๐‘˜ โˆˆ โฆ‹๐‘š / ๐‘—โฆŒ๐ต) โ†’ โฆ‹๐‘š / ๐‘—โฆŒ๐ถ = โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ)
4138, 40prodeq12dv 11597 . . . . . . . 8 (๐‘š = ๐‘ฆ โ†’ โˆ๐‘˜ โˆˆ โฆ‹ ๐‘š / ๐‘—โฆŒ๐ตโฆ‹๐‘š / ๐‘—โฆŒ๐ถ = โˆ๐‘˜ โˆˆ โฆ‹ ๐‘ฆ / ๐‘—โฆŒ๐ตโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ)
4241prodsn 11621 . . . . . . 7 ((๐‘ฆ โˆˆ ๐ด โˆง โˆ๐‘˜ โˆˆ โฆ‹ ๐‘ฆ / ๐‘—โฆŒ๐ตโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ โˆˆ โ„‚) โ†’ โˆ๐‘š โˆˆ {๐‘ฆ}โˆ๐‘˜ โˆˆ โฆ‹ ๐‘š / ๐‘—โฆŒ๐ตโฆ‹๐‘š / ๐‘—โฆŒ๐ถ = โˆ๐‘˜ โˆˆ โฆ‹ ๐‘ฆ / ๐‘—โฆŒ๐ตโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ)
4317, 37, 42syl2anc 411 . . . . . 6 (๐œ‘ โ†’ โˆ๐‘š โˆˆ {๐‘ฆ}โˆ๐‘˜ โˆˆ โฆ‹ ๐‘š / ๐‘—โฆŒ๐ตโฆ‹๐‘š / ๐‘—โฆŒ๐ถ = โˆ๐‘˜ โˆˆ โฆ‹ ๐‘ฆ / ๐‘—โฆŒ๐ตโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ)
44 nfcv 2332 . . . . . . . 8 โ„ฒ๐‘šโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ
45 nfcsb1v 3105 . . . . . . . 8 โ„ฒ๐‘˜โฆ‹๐‘š / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ
46 csbeq1a 3081 . . . . . . . 8 (๐‘˜ = ๐‘š โ†’ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ = โฆ‹๐‘š / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ)
4744, 45, 46cbvprodi 11588 . . . . . . 7 โˆ๐‘˜ โˆˆ โฆ‹ ๐‘ฆ / ๐‘—โฆŒ๐ตโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ = โˆ๐‘š โˆˆ โฆ‹ ๐‘ฆ / ๐‘—โฆŒ๐ตโฆ‹๐‘š / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ
48 csbeq1 3075 . . . . . . . . 9 (๐‘š = (2nd โ€˜๐‘ง) โ†’ โฆ‹๐‘š / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ = โฆ‹(2nd โ€˜๐‘ง) / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ)
49 snfig 6833 . . . . . . . . . . 11 (๐‘ฆ โˆˆ V โ†’ {๐‘ฆ} โˆˆ Fin)
5049elv 2756 . . . . . . . . . 10 {๐‘ฆ} โˆˆ Fin
51 xpfi 6948 . . . . . . . . . 10 (({๐‘ฆ} โˆˆ Fin โˆง โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต โˆˆ Fin) โ†’ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต) โˆˆ Fin)
5250, 25, 51sylancr 414 . . . . . . . . 9 (๐œ‘ โ†’ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต) โˆˆ Fin)
53 2ndconst 6242 . . . . . . . . . 10 (๐‘ฆ โˆˆ ๐ด โ†’ (2nd โ†พ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)):({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)โ€“1-1-ontoโ†’โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)
5417, 53syl 14 . . . . . . . . 9 (๐œ‘ โ†’ (2nd โ†พ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)):({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)โ€“1-1-ontoโ†’โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)
55 fvres 5555 . . . . . . . . . 10 (๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต) โ†’ ((2nd โ†พ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต))โ€˜๐‘ง) = (2nd โ€˜๐‘ง))
5655adantl 277 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)) โ†’ ((2nd โ†พ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต))โ€˜๐‘ง) = (2nd โ€˜๐‘ง))
5745nfel1 2343 . . . . . . . . . . 11 โ„ฒ๐‘˜โฆ‹๐‘š / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ โˆˆ โ„‚
5846eleq1d 2258 . . . . . . . . . . 11 (๐‘˜ = ๐‘š โ†’ (โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ โˆˆ โ„‚ โ†” โฆ‹๐‘š / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ โˆˆ โ„‚))
5957, 58rspc 2850 . . . . . . . . . 10 (๐‘š โˆˆ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต โ†’ (โˆ€๐‘˜ โˆˆ โฆ‹ ๐‘ฆ / ๐‘—โฆŒ๐ตโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ โˆˆ โ„‚ โ†’ โฆ‹๐‘š / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ โˆˆ โ„‚))
6035, 59mpan9 281 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘š โˆˆ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต) โ†’ โฆ‹๐‘š / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ โˆˆ โ„‚)
6148, 52, 54, 56, 60fprodf1o 11616 . . . . . . . 8 (๐œ‘ โ†’ โˆ๐‘š โˆˆ โฆ‹ ๐‘ฆ / ๐‘—โฆŒ๐ตโฆ‹๐‘š / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ = โˆ๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)โฆ‹(2nd โ€˜๐‘ง) / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ)
62 elxp 4658 . . . . . . . . . . . 12 (๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต) โ†” โˆƒ๐‘šโˆƒ๐‘˜(๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘ฆ} โˆง ๐‘˜ โˆˆ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)))
63 nfv 1539 . . . . . . . . . . . . . . 15 โ„ฒ๐‘— ๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ
64 nfv 1539 . . . . . . . . . . . . . . . 16 โ„ฒ๐‘— ๐‘š โˆˆ {๐‘ฆ}
6520nfcri 2326 . . . . . . . . . . . . . . . 16 โ„ฒ๐‘— ๐‘˜ โˆˆ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต
6664, 65nfan 1576 . . . . . . . . . . . . . . 15 โ„ฒ๐‘—(๐‘š โˆˆ {๐‘ฆ} โˆง ๐‘˜ โˆˆ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)
6763, 66nfan 1576 . . . . . . . . . . . . . 14 โ„ฒ๐‘—(๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘ฆ} โˆง ๐‘˜ โˆˆ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต))
6867nfex 1648 . . . . . . . . . . . . 13 โ„ฒ๐‘—โˆƒ๐‘˜(๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘ฆ} โˆง ๐‘˜ โˆˆ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต))
69 nfv 1539 . . . . . . . . . . . . 13 โ„ฒ๐‘šโˆƒ๐‘˜(๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ โˆง (๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ ๐ต))
70 opeq1 3793 . . . . . . . . . . . . . . . 16 (๐‘š = ๐‘— โ†’ โŸจ๐‘š, ๐‘˜โŸฉ = โŸจ๐‘—, ๐‘˜โŸฉ)
7170eqeq2d 2201 . . . . . . . . . . . . . . 15 (๐‘š = ๐‘— โ†’ (๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โ†” ๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ))
72 eleq1w 2250 . . . . . . . . . . . . . . . . . 18 (๐‘š = ๐‘— โ†’ (๐‘š โˆˆ {๐‘ฆ} โ†” ๐‘— โˆˆ {๐‘ฆ}))
73 velsn 3624 . . . . . . . . . . . . . . . . . 18 (๐‘— โˆˆ {๐‘ฆ} โ†” ๐‘— = ๐‘ฆ)
7472, 73bitrdi 196 . . . . . . . . . . . . . . . . 17 (๐‘š = ๐‘— โ†’ (๐‘š โˆˆ {๐‘ฆ} โ†” ๐‘— = ๐‘ฆ))
7574anbi1d 465 . . . . . . . . . . . . . . . 16 (๐‘š = ๐‘— โ†’ ((๐‘š โˆˆ {๐‘ฆ} โˆง ๐‘˜ โˆˆ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต) โ†” (๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)))
7622eleq2d 2259 . . . . . . . . . . . . . . . . 17 (๐‘— = ๐‘ฆ โ†’ (๐‘˜ โˆˆ ๐ต โ†” ๐‘˜ โˆˆ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต))
7776pm5.32i 454 . . . . . . . . . . . . . . . 16 ((๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ ๐ต) โ†” (๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต))
7875, 77bitr4di 198 . . . . . . . . . . . . . . 15 (๐‘š = ๐‘— โ†’ ((๐‘š โˆˆ {๐‘ฆ} โˆง ๐‘˜ โˆˆ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต) โ†” (๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ ๐ต)))
7971, 78anbi12d 473 . . . . . . . . . . . . . 14 (๐‘š = ๐‘— โ†’ ((๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘ฆ} โˆง ๐‘˜ โˆˆ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)) โ†” (๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ โˆง (๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ ๐ต))))
8079exbidv 1836 . . . . . . . . . . . . 13 (๐‘š = ๐‘— โ†’ (โˆƒ๐‘˜(๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘ฆ} โˆง ๐‘˜ โˆˆ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)) โ†” โˆƒ๐‘˜(๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ โˆง (๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ ๐ต))))
8168, 69, 80cbvexv1 1763 . . . . . . . . . . . 12 (โˆƒ๐‘šโˆƒ๐‘˜(๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘ฆ} โˆง ๐‘˜ โˆˆ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)) โ†” โˆƒ๐‘—โˆƒ๐‘˜(๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ โˆง (๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ ๐ต)))
8262, 81bitri 184 . . . . . . . . . . 11 (๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต) โ†” โˆƒ๐‘—โˆƒ๐‘˜(๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ โˆง (๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ ๐ต)))
83 nfv 1539 . . . . . . . . . . . 12 โ„ฒ๐‘—๐œ‘
84 nfcv 2332 . . . . . . . . . . . . . 14 โ„ฒ๐‘—(2nd โ€˜๐‘ง)
8584, 28nfcsbw 3108 . . . . . . . . . . . . 13 โ„ฒ๐‘—โฆ‹(2nd โ€˜๐‘ง) / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ
8685nfeq2 2344 . . . . . . . . . . . 12 โ„ฒ๐‘— ๐ท = โฆ‹(2nd โ€˜๐‘ง) / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ
87 nfv 1539 . . . . . . . . . . . . 13 โ„ฒ๐‘˜๐œ‘
88 nfcsb1v 3105 . . . . . . . . . . . . . 14 โ„ฒ๐‘˜โฆ‹(2nd โ€˜๐‘ง) / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ
8988nfeq2 2344 . . . . . . . . . . . . 13 โ„ฒ๐‘˜ ๐ท = โฆ‹(2nd โ€˜๐‘ง) / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ
90 fprod2d.1 . . . . . . . . . . . . . . . 16 (๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ โ†’ ๐ท = ๐ถ)
9190ad2antlr 489 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ) โˆง (๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ ๐ต)) โ†’ ๐ท = ๐ถ)
9231ad2antrl 490 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ) โˆง (๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ ๐ต)) โ†’ ๐ถ = โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ)
93 fveq2 5531 . . . . . . . . . . . . . . . . . 18 (๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ โ†’ (2nd โ€˜๐‘ง) = (2nd โ€˜โŸจ๐‘—, ๐‘˜โŸฉ))
94 vex 2755 . . . . . . . . . . . . . . . . . . 19 ๐‘— โˆˆ V
95 vex 2755 . . . . . . . . . . . . . . . . . . 19 ๐‘˜ โˆˆ V
9694, 95op2nd 6167 . . . . . . . . . . . . . . . . . 18 (2nd โ€˜โŸจ๐‘—, ๐‘˜โŸฉ) = ๐‘˜
9793, 96eqtr2di 2239 . . . . . . . . . . . . . . . . 17 (๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ โ†’ ๐‘˜ = (2nd โ€˜๐‘ง))
9897ad2antlr 489 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ) โˆง (๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ ๐ต)) โ†’ ๐‘˜ = (2nd โ€˜๐‘ง))
99 csbeq1a 3081 . . . . . . . . . . . . . . . 16 (๐‘˜ = (2nd โ€˜๐‘ง) โ†’ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ = โฆ‹(2nd โ€˜๐‘ง) / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ)
10098, 99syl 14 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ) โˆง (๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ ๐ต)) โ†’ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ = โฆ‹(2nd โ€˜๐‘ง) / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ)
10191, 92, 1003eqtrd 2226 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ) โˆง (๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ ๐ต)) โ†’ ๐ท = โฆ‹(2nd โ€˜๐‘ง) / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ)
102101expl 378 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ โˆง (๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ ๐ต)) โ†’ ๐ท = โฆ‹(2nd โ€˜๐‘ง) / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ))
10387, 89, 102exlimd 1608 . . . . . . . . . . . 12 (๐œ‘ โ†’ (โˆƒ๐‘˜(๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ โˆง (๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ ๐ต)) โ†’ ๐ท = โฆ‹(2nd โ€˜๐‘ง) / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ))
10483, 86, 103exlimd 1608 . . . . . . . . . . 11 (๐œ‘ โ†’ (โˆƒ๐‘—โˆƒ๐‘˜(๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ โˆง (๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ ๐ต)) โ†’ ๐ท = โฆ‹(2nd โ€˜๐‘ง) / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ))
10582, 104biimtrid 152 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต) โ†’ ๐ท = โฆ‹(2nd โ€˜๐‘ง) / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ))
106105imp 124 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)) โ†’ ๐ท = โฆ‹(2nd โ€˜๐‘ง) / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ)
107106prodeq2dv 11594 . . . . . . . 8 (๐œ‘ โ†’ โˆ๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)๐ท = โˆ๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)โฆ‹(2nd โ€˜๐‘ง) / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ)
10861, 107eqtr4d 2225 . . . . . . 7 (๐œ‘ โ†’ โˆ๐‘š โˆˆ โฆ‹ ๐‘ฆ / ๐‘—โฆŒ๐ตโฆ‹๐‘š / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ = โˆ๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)๐ท)
10947, 108eqtrid 2234 . . . . . 6 (๐œ‘ โ†’ โˆ๐‘˜ โˆˆ โฆ‹ ๐‘ฆ / ๐‘—โฆŒ๐ตโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ = โˆ๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)๐ท)
11043, 109eqtrd 2222 . . . . 5 (๐œ‘ โ†’ โˆ๐‘š โˆˆ {๐‘ฆ}โˆ๐‘˜ โˆˆ โฆ‹ ๐‘š / ๐‘—โฆŒ๐ตโฆ‹๐‘š / ๐‘—โฆŒ๐ถ = โˆ๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)๐ท)
11112, 110eqtrid 2234 . . . 4 (๐œ‘ โ†’ โˆ๐‘— โˆˆ {๐‘ฆ}โˆ๐‘˜ โˆˆ ๐ต ๐ถ = โˆ๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)๐ท)
112111adantr 276 . . 3 ((๐œ‘ โˆง ๐œ“) โ†’ โˆ๐‘— โˆˆ {๐‘ฆ}โˆ๐‘˜ โˆˆ ๐ต ๐ถ = โˆ๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)๐ท)
1133, 112oveq12d 5910 . 2 ((๐œ‘ โˆง ๐œ“) โ†’ (โˆ๐‘— โˆˆ ๐‘ฅ โˆ๐‘˜ โˆˆ ๐ต ๐ถ ยท โˆ๐‘— โˆˆ {๐‘ฆ}โˆ๐‘˜ โˆˆ ๐ต ๐ถ) = (โˆ๐‘ง โˆˆ โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต)๐ท ยท โˆ๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)๐ท))
114 fprod2d.5 . . . . 5 (๐œ‘ โ†’ ยฌ ๐‘ฆ โˆˆ ๐‘ฅ)
115 disjsn 3669 . . . . 5 ((๐‘ฅ โˆฉ {๐‘ฆ}) = โˆ… โ†” ยฌ ๐‘ฆ โˆˆ ๐‘ฅ)
116114, 115sylibr 134 . . . 4 (๐œ‘ โ†’ (๐‘ฅ โˆฉ {๐‘ฆ}) = โˆ…)
117 eqidd 2190 . . . 4 (๐œ‘ โ†’ (๐‘ฅ โˆช {๐‘ฆ}) = (๐‘ฅ โˆช {๐‘ฆ}))
118 fprod2dlemstep.x . . . . 5 (๐œ‘ โ†’ ๐‘ฅ โˆˆ Fin)
11915a1i 9 . . . . 5 (๐œ‘ โ†’ ๐‘ฆ โˆˆ V)
120 unsnfi 6937 . . . . 5 ((๐‘ฅ โˆˆ Fin โˆง ๐‘ฆ โˆˆ V โˆง ยฌ ๐‘ฆ โˆˆ ๐‘ฅ) โ†’ (๐‘ฅ โˆช {๐‘ฆ}) โˆˆ Fin)
121118, 119, 114, 120syl3anc 1249 . . . 4 (๐œ‘ โ†’ (๐‘ฅ โˆช {๐‘ฆ}) โˆˆ Fin)
12213sselda 3170 . . . . 5 ((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โ†’ ๐‘— โˆˆ ๐ด)
12326anassrs 400 . . . . . 6 (((๐œ‘ โˆง ๐‘— โˆˆ ๐ด) โˆง ๐‘˜ โˆˆ ๐ต) โ†’ ๐ถ โˆˆ โ„‚)
12418, 123fprodcl 11635 . . . . 5 ((๐œ‘ โˆง ๐‘— โˆˆ ๐ด) โ†’ โˆ๐‘˜ โˆˆ ๐ต ๐ถ โˆˆ โ„‚)
125122, 124syldan 282 . . . 4 ((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โ†’ โˆ๐‘˜ โˆˆ ๐ต ๐ถ โˆˆ โ„‚)
126116, 117, 121, 125fprodsplit 11625 . . 3 (๐œ‘ โ†’ โˆ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})โˆ๐‘˜ โˆˆ ๐ต ๐ถ = (โˆ๐‘— โˆˆ ๐‘ฅ โˆ๐‘˜ โˆˆ ๐ต ๐ถ ยท โˆ๐‘— โˆˆ {๐‘ฆ}โˆ๐‘˜ โˆˆ ๐ต ๐ถ))
127126adantr 276 . 2 ((๐œ‘ โˆง ๐œ“) โ†’ โˆ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})โˆ๐‘˜ โˆˆ ๐ต ๐ถ = (โˆ๐‘— โˆˆ ๐‘ฅ โˆ๐‘˜ โˆˆ ๐ต ๐ถ ยท โˆ๐‘— โˆˆ {๐‘ฆ}โˆ๐‘˜ โˆˆ ๐ต ๐ถ))
128 eliun 3905 . . . . . . . . . 10 (๐‘ง โˆˆ โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต) โ†” โˆƒ๐‘— โˆˆ ๐‘ฅ ๐‘ง โˆˆ ({๐‘—} ร— ๐ต))
129 xp1st 6185 . . . . . . . . . . . . . 14 (๐‘ง โˆˆ ({๐‘—} ร— ๐ต) โ†’ (1st โ€˜๐‘ง) โˆˆ {๐‘—})
130 elsni 3625 . . . . . . . . . . . . . 14 ((1st โ€˜๐‘ง) โˆˆ {๐‘—} โ†’ (1st โ€˜๐‘ง) = ๐‘—)
131129, 130syl 14 . . . . . . . . . . . . 13 (๐‘ง โˆˆ ({๐‘—} ร— ๐ต) โ†’ (1st โ€˜๐‘ง) = ๐‘—)
132131eleq1d 2258 . . . . . . . . . . . 12 (๐‘ง โˆˆ ({๐‘—} ร— ๐ต) โ†’ ((1st โ€˜๐‘ง) โˆˆ ๐‘ฅ โ†” ๐‘— โˆˆ ๐‘ฅ))
133132biimparc 299 . . . . . . . . . . 11 ((๐‘— โˆˆ ๐‘ฅ โˆง ๐‘ง โˆˆ ({๐‘—} ร— ๐ต)) โ†’ (1st โ€˜๐‘ง) โˆˆ ๐‘ฅ)
134133rexlimiva 2602 . . . . . . . . . 10 (โˆƒ๐‘— โˆˆ ๐‘ฅ ๐‘ง โˆˆ ({๐‘—} ร— ๐ต) โ†’ (1st โ€˜๐‘ง) โˆˆ ๐‘ฅ)
135128, 134sylbi 121 . . . . . . . . 9 (๐‘ง โˆˆ โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต) โ†’ (1st โ€˜๐‘ง) โˆˆ ๐‘ฅ)
136 xp1st 6185 . . . . . . . . 9 (๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต) โ†’ (1st โ€˜๐‘ง) โˆˆ {๐‘ฆ})
137135, 136anim12i 338 . . . . . . . 8 ((๐‘ง โˆˆ โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต) โˆง ๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)) โ†’ ((1st โ€˜๐‘ง) โˆˆ ๐‘ฅ โˆง (1st โ€˜๐‘ง) โˆˆ {๐‘ฆ}))
138 elin 3333 . . . . . . . 8 (๐‘ง โˆˆ (โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต) โˆฉ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)) โ†” (๐‘ง โˆˆ โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต) โˆง ๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)))
139 elin 3333 . . . . . . . 8 ((1st โ€˜๐‘ง) โˆˆ (๐‘ฅ โˆฉ {๐‘ฆ}) โ†” ((1st โ€˜๐‘ง) โˆˆ ๐‘ฅ โˆง (1st โ€˜๐‘ง) โˆˆ {๐‘ฆ}))
140137, 138, 1393imtr4i 201 . . . . . . 7 (๐‘ง โˆˆ (โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต) โˆฉ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)) โ†’ (1st โ€˜๐‘ง) โˆˆ (๐‘ฅ โˆฉ {๐‘ฆ}))
141116eleq2d 2259 . . . . . . . 8 (๐œ‘ โ†’ ((1st โ€˜๐‘ง) โˆˆ (๐‘ฅ โˆฉ {๐‘ฆ}) โ†” (1st โ€˜๐‘ง) โˆˆ โˆ…))
142 noel 3441 . . . . . . . . 9 ยฌ (1st โ€˜๐‘ง) โˆˆ โˆ…
143142pm2.21i 647 . . . . . . . 8 ((1st โ€˜๐‘ง) โˆˆ โˆ… โ†’ ๐‘ง โˆˆ โˆ…)
144141, 143biimtrdi 163 . . . . . . 7 (๐œ‘ โ†’ ((1st โ€˜๐‘ง) โˆˆ (๐‘ฅ โˆฉ {๐‘ฆ}) โ†’ ๐‘ง โˆˆ โˆ…))
145140, 144syl5 32 . . . . . 6 (๐œ‘ โ†’ (๐‘ง โˆˆ (โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต) โˆฉ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)) โ†’ ๐‘ง โˆˆ โˆ…))
146145ssrdv 3176 . . . . 5 (๐œ‘ โ†’ (โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต) โˆฉ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)) โІ โˆ…)
147 ss0 3478 . . . . 5 ((โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต) โˆฉ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)) โІ โˆ… โ†’ (โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต) โˆฉ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)) = โˆ…)
148146, 147syl 14 . . . 4 (๐œ‘ โ†’ (โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต) โˆฉ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)) = โˆ…)
149 iunxun 3981 . . . . . 6 โˆช ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})({๐‘—} ร— ๐ต) = (โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต) โˆช โˆช ๐‘— โˆˆ {๐‘ฆ} ({๐‘—} ร— ๐ต))
150 nfcv 2332 . . . . . . . . 9 โ„ฒ๐‘š({๐‘—} ร— ๐ต)
151 nfcv 2332 . . . . . . . . . 10 โ„ฒ๐‘—{๐‘š}
152151, 5nfxp 4668 . . . . . . . . 9 โ„ฒ๐‘—({๐‘š} ร— โฆ‹๐‘š / ๐‘—โฆŒ๐ต)
153 sneq 3618 . . . . . . . . . 10 (๐‘— = ๐‘š โ†’ {๐‘—} = {๐‘š})
154153, 8xpeq12d 4666 . . . . . . . . 9 (๐‘— = ๐‘š โ†’ ({๐‘—} ร— ๐ต) = ({๐‘š} ร— โฆ‹๐‘š / ๐‘—โฆŒ๐ต))
155150, 152, 154cbviun 3938 . . . . . . . 8 โˆช ๐‘— โˆˆ {๐‘ฆ} ({๐‘—} ร— ๐ต) = โˆช ๐‘š โˆˆ {๐‘ฆ} ({๐‘š} ร— โฆ‹๐‘š / ๐‘—โฆŒ๐ต)
156 sneq 3618 . . . . . . . . . 10 (๐‘š = ๐‘ฆ โ†’ {๐‘š} = {๐‘ฆ})
157156, 38xpeq12d 4666 . . . . . . . . 9 (๐‘š = ๐‘ฆ โ†’ ({๐‘š} ร— โฆ‹๐‘š / ๐‘—โฆŒ๐ต) = ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต))
15815, 157iunxsn 3978 . . . . . . . 8 โˆช ๐‘š โˆˆ {๐‘ฆ} ({๐‘š} ร— โฆ‹๐‘š / ๐‘—โฆŒ๐ต) = ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)
159155, 158eqtri 2210 . . . . . . 7 โˆช ๐‘— โˆˆ {๐‘ฆ} ({๐‘—} ร— ๐ต) = ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)
160159uneq2i 3301 . . . . . 6 (โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต) โˆช โˆช ๐‘— โˆˆ {๐‘ฆ} ({๐‘—} ร— ๐ต)) = (โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต) โˆช ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต))
161149, 160eqtri 2210 . . . . 5 โˆช ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})({๐‘—} ร— ๐ต) = (โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต) โˆช ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต))
162161a1i 9 . . . 4 (๐œ‘ โ†’ โˆช ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})({๐‘—} ร— ๐ต) = (โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต) โˆช ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)))
163 snfig 6833 . . . . . . . 8 (๐‘— โˆˆ V โ†’ {๐‘—} โˆˆ Fin)
164163elv 2756 . . . . . . 7 {๐‘—} โˆˆ Fin
165122, 18syldan 282 . . . . . . 7 ((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โ†’ ๐ต โˆˆ Fin)
166 xpfi 6948 . . . . . . 7 (({๐‘—} โˆˆ Fin โˆง ๐ต โˆˆ Fin) โ†’ ({๐‘—} ร— ๐ต) โˆˆ Fin)
167164, 165, 166sylancr 414 . . . . . 6 ((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โ†’ ({๐‘—} ร— ๐ต) โˆˆ Fin)
168167ralrimiva 2563 . . . . 5 (๐œ‘ โ†’ โˆ€๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})({๐‘—} ร— ๐ต) โˆˆ Fin)
169 disjsnxp 6257 . . . . . 6 Disj ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})({๐‘—} ร— ๐ต)
170169a1i 9 . . . . 5 (๐œ‘ โ†’ Disj ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})({๐‘—} ร— ๐ต))
171 iunfidisj 6965 . . . . 5 (((๐‘ฅ โˆช {๐‘ฆ}) โˆˆ Fin โˆง โˆ€๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})({๐‘—} ร— ๐ต) โˆˆ Fin โˆง Disj ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})({๐‘—} ร— ๐ต)) โ†’ โˆช ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})({๐‘—} ร— ๐ต) โˆˆ Fin)
172121, 168, 170, 171syl3anc 1249 . . . 4 (๐œ‘ โ†’ โˆช ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})({๐‘—} ร— ๐ต) โˆˆ Fin)
173 eliun 3905 . . . . . 6 (๐‘ง โˆˆ โˆช ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})({๐‘—} ร— ๐ต) โ†” โˆƒ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})๐‘ง โˆˆ ({๐‘—} ร— ๐ต))
174 elxp 4658 . . . . . . . 8 (๐‘ง โˆˆ ({๐‘—} ร— ๐ต) โ†” โˆƒ๐‘šโˆƒ๐‘˜(๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘—} โˆง ๐‘˜ โˆˆ ๐ต)))
175 simprl 529 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โˆง (๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘—} โˆง ๐‘˜ โˆˆ ๐ต))) โ†’ ๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ)
176 simprrl 539 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โˆง (๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘—} โˆง ๐‘˜ โˆˆ ๐ต))) โ†’ ๐‘š โˆˆ {๐‘—})
177 elsni 3625 . . . . . . . . . . . . . . 15 (๐‘š โˆˆ {๐‘—} โ†’ ๐‘š = ๐‘—)
178176, 177syl 14 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โˆง (๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘—} โˆง ๐‘˜ โˆˆ ๐ต))) โ†’ ๐‘š = ๐‘—)
179178opeq1d 3799 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โˆง (๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘—} โˆง ๐‘˜ โˆˆ ๐ต))) โ†’ โŸจ๐‘š, ๐‘˜โŸฉ = โŸจ๐‘—, ๐‘˜โŸฉ)
180175, 179eqtrd 2222 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โˆง (๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘—} โˆง ๐‘˜ โˆˆ ๐ต))) โ†’ ๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ)
181180, 90syl 14 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โˆง (๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘—} โˆง ๐‘˜ โˆˆ ๐ต))) โ†’ ๐ท = ๐ถ)
182 simpll 527 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โˆง (๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘—} โˆง ๐‘˜ โˆˆ ๐ต))) โ†’ ๐œ‘)
183122adantr 276 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โˆง (๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘—} โˆง ๐‘˜ โˆˆ ๐ต))) โ†’ ๐‘— โˆˆ ๐ด)
184 simprrr 540 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โˆง (๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘—} โˆง ๐‘˜ โˆˆ ๐ต))) โ†’ ๐‘˜ โˆˆ ๐ต)
185182, 183, 184, 26syl12anc 1247 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โˆง (๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘—} โˆง ๐‘˜ โˆˆ ๐ต))) โ†’ ๐ถ โˆˆ โ„‚)
186181, 185eqeltrd 2266 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โˆง (๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘—} โˆง ๐‘˜ โˆˆ ๐ต))) โ†’ ๐ท โˆˆ โ„‚)
187186ex 115 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โ†’ ((๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘—} โˆง ๐‘˜ โˆˆ ๐ต)) โ†’ ๐ท โˆˆ โ„‚))
188187exlimdvv 1909 . . . . . . . 8 ((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โ†’ (โˆƒ๐‘šโˆƒ๐‘˜(๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘—} โˆง ๐‘˜ โˆˆ ๐ต)) โ†’ ๐ท โˆˆ โ„‚))
189174, 188biimtrid 152 . . . . . . 7 ((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โ†’ (๐‘ง โˆˆ ({๐‘—} ร— ๐ต) โ†’ ๐ท โˆˆ โ„‚))
190189rexlimdva 2607 . . . . . 6 (๐œ‘ โ†’ (โˆƒ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})๐‘ง โˆˆ ({๐‘—} ร— ๐ต) โ†’ ๐ท โˆˆ โ„‚))
191173, 190biimtrid 152 . . . . 5 (๐œ‘ โ†’ (๐‘ง โˆˆ โˆช ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})({๐‘—} ร— ๐ต) โ†’ ๐ท โˆˆ โ„‚))
192191imp 124 . . . 4 ((๐œ‘ โˆง ๐‘ง โˆˆ โˆช ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})({๐‘—} ร— ๐ต)) โ†’ ๐ท โˆˆ โ„‚)
193148, 162, 172, 192fprodsplit 11625 . . 3 (๐œ‘ โ†’ โˆ๐‘ง โˆˆ โˆช ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})({๐‘—} ร— ๐ต)๐ท = (โˆ๐‘ง โˆˆ โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต)๐ท ยท โˆ๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)๐ท))
194193adantr 276 . 2 ((๐œ‘ โˆง ๐œ“) โ†’ โˆ๐‘ง โˆˆ โˆช ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})({๐‘—} ร— ๐ต)๐ท = (โˆ๐‘ง โˆˆ โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต)๐ท ยท โˆ๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)๐ท))
195113, 127, 1943eqtr4d 2232 1 ((๐œ‘ โˆง ๐œ“) โ†’ โˆ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})โˆ๐‘˜ โˆˆ ๐ต ๐ถ = โˆ๐‘ง โˆˆ โˆช ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})({๐‘—} ร— ๐ต)๐ท)
Colors of variables: wff set class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โˆง wa 104   โ†” wb 105   = wceq 1364  โˆƒwex 1503   โˆˆ wcel 2160  โˆ€wral 2468  โˆƒwrex 2469  Vcvv 2752  โฆ‹csb 3072   โˆช cun 3142   โˆฉ cin 3143   โІ wss 3144  โˆ…c0 3437  {csn 3607  โŸจcop 3610  โˆช ciun 3901  Disj wdisj 3995   ร— cxp 4639   โ†พ cres 4643  โ€“1-1-ontoโ†’wf1o 5231  โ€˜cfv 5232  (class class class)co 5892  1st c1st 6158  2nd c2nd 6159  Fincfn 6759  โ„‚cc 7829   ยท cmul 7836  โˆcprod 11578
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-coll 4133  ax-sep 4136  ax-nul 4144  ax-pow 4189  ax-pr 4224  ax-un 4448  ax-setind 4551  ax-iinf 4602  ax-cnex 7922  ax-resscn 7923  ax-1cn 7924  ax-1re 7925  ax-icn 7926  ax-addcl 7927  ax-addrcl 7928  ax-mulcl 7929  ax-mulrcl 7930  ax-addcom 7931  ax-mulcom 7932  ax-addass 7933  ax-mulass 7934  ax-distr 7935  ax-i2m1 7936  ax-0lt1 7937  ax-1rid 7938  ax-0id 7939  ax-rnegex 7940  ax-precex 7941  ax-cnre 7942  ax-pre-ltirr 7943  ax-pre-ltwlin 7944  ax-pre-lttrn 7945  ax-pre-apti 7946  ax-pre-ltadd 7947  ax-pre-mulgt0 7948  ax-pre-mulext 7949  ax-arch 7950  ax-caucvg 7951
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ne 2361  df-nel 2456  df-ral 2473  df-rex 2474  df-reu 2475  df-rmo 2476  df-rab 2477  df-v 2754  df-sbc 2978  df-csb 3073  df-dif 3146  df-un 3148  df-in 3150  df-ss 3157  df-nul 3438  df-if 3550  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-int 3860  df-iun 3903  df-disj 3996  df-br 4019  df-opab 4080  df-mpt 4081  df-tr 4117  df-id 4308  df-po 4311  df-iso 4312  df-iord 4381  df-on 4383  df-ilim 4384  df-suc 4386  df-iom 4605  df-xp 4647  df-rel 4648  df-cnv 4649  df-co 4650  df-dm 4651  df-rn 4652  df-res 4653  df-ima 4654  df-iota 5193  df-fun 5234  df-fn 5235  df-f 5236  df-f1 5237  df-fo 5238  df-f1o 5239  df-fv 5240  df-isom 5241  df-riota 5848  df-ov 5895  df-oprab 5896  df-mpo 5897  df-1st 6160  df-2nd 6161  df-recs 6325  df-irdg 6390  df-frec 6411  df-1o 6436  df-oadd 6440  df-er 6554  df-en 6760  df-dom 6761  df-fin 6762  df-pnf 8014  df-mnf 8015  df-xr 8016  df-ltxr 8017  df-le 8018  df-sub 8150  df-neg 8151  df-reap 8552  df-ap 8559  df-div 8650  df-inn 8940  df-2 8998  df-3 8999  df-4 9000  df-n0 9197  df-z 9274  df-uz 9549  df-q 9640  df-rp 9674  df-fz 10029  df-fzo 10163  df-seqfrec 10466  df-exp 10540  df-ihash 10776  df-cj 10871  df-re 10872  df-im 10873  df-rsqrt 11027  df-abs 11028  df-clim 11307  df-proddc 11579
This theorem is referenced by:  fprod2d  11651
  Copyright terms: Public domain W3C validator