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

Theorem fprod2dlemstep 11643
Description: Lemma for fprod2d 11644- 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 2329 . . . . . 6 โ„ฒ๐‘šโˆ๐‘˜ โˆˆ ๐ต ๐ถ
5 nfcsb1v 3102 . . . . . . 7 โ„ฒ๐‘—โฆ‹๐‘š / ๐‘—โฆŒ๐ต
6 nfcsb1v 3102 . . . . . . 7 โ„ฒ๐‘—โฆ‹๐‘š / ๐‘—โฆŒ๐ถ
75, 6nfcprod 11576 . . . . . 6 โ„ฒ๐‘—โˆ๐‘˜ โˆˆ โฆ‹ ๐‘š / ๐‘—โฆŒ๐ตโฆ‹๐‘š / ๐‘—โฆŒ๐ถ
8 csbeq1a 3078 . . . . . . 7 (๐‘— = ๐‘š โ†’ ๐ต = โฆ‹๐‘š / ๐‘—โฆŒ๐ต)
9 csbeq1a 3078 . . . . . . . 8 (๐‘— = ๐‘š โ†’ ๐ถ = โฆ‹๐‘š / ๐‘—โฆŒ๐ถ)
109adantr 276 . . . . . . 7 ((๐‘— = ๐‘š โˆง ๐‘˜ โˆˆ ๐ต) โ†’ ๐ถ = โฆ‹๐‘š / ๐‘—โฆŒ๐ถ)
118, 10prodeq12dv 11590 . . . . . 6 (๐‘— = ๐‘š โ†’ โˆ๐‘˜ โˆˆ ๐ต ๐ถ = โˆ๐‘˜ โˆˆ โฆ‹ ๐‘š / ๐‘—โฆŒ๐ตโฆ‹๐‘š / ๐‘—โฆŒ๐ถ)
124, 7, 11cbvprodi 11581 . . . . 5 โˆ๐‘— โˆˆ {๐‘ฆ}โˆ๐‘˜ โˆˆ ๐ต ๐ถ = โˆ๐‘š โˆˆ {๐‘ฆ}โˆ๐‘˜ โˆˆ โฆ‹ ๐‘š / ๐‘—โฆŒ๐ตโฆ‹๐‘š / ๐‘—โฆŒ๐ถ
13 fprod2d.6 . . . . . . . . 9 (๐œ‘ โ†’ (๐‘ฅ โˆช {๐‘ฆ}) โІ ๐ด)
1413unssbd 3325 . . . . . . . 8 (๐œ‘ โ†’ {๐‘ฆ} โІ ๐ด)
15 vex 2752 . . . . . . . . 9 ๐‘ฆ โˆˆ V
1615snss 3739 . . . . . . . 8 (๐‘ฆ โˆˆ ๐ด โ†” {๐‘ฆ} โІ ๐ด)
1714, 16sylibr 134 . . . . . . 7 (๐œ‘ โ†’ ๐‘ฆ โˆˆ ๐ด)
18 fprod2d.3 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘— โˆˆ ๐ด) โ†’ ๐ต โˆˆ Fin)
1918ralrimiva 2560 . . . . . . . . 9 (๐œ‘ โ†’ โˆ€๐‘— โˆˆ ๐ด ๐ต โˆˆ Fin)
20 nfcsb1v 3102 . . . . . . . . . . 11 โ„ฒ๐‘—โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต
2120nfel1 2340 . . . . . . . . . 10 โ„ฒ๐‘—โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต โˆˆ Fin
22 csbeq1a 3078 . . . . . . . . . . 11 (๐‘— = ๐‘ฆ โ†’ ๐ต = โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)
2322eleq1d 2256 . . . . . . . . . 10 (๐‘— = ๐‘ฆ โ†’ (๐ต โˆˆ Fin โ†” โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต โˆˆ Fin))
2421, 23rspc 2847 . . . . . . . . 9 (๐‘ฆ โˆˆ ๐ด โ†’ (โˆ€๐‘— โˆˆ ๐ด ๐ต โˆˆ Fin โ†’ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต โˆˆ Fin))
2517, 19, 24sylc 62 . . . . . . . 8 (๐œ‘ โ†’ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต โˆˆ Fin)
26 fprod2d.4 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘— โˆˆ ๐ด โˆง ๐‘˜ โˆˆ ๐ต)) โ†’ ๐ถ โˆˆ โ„‚)
2726ralrimivva 2569 . . . . . . . . . 10 (๐œ‘ โ†’ โˆ€๐‘— โˆˆ ๐ด โˆ€๐‘˜ โˆˆ ๐ต ๐ถ โˆˆ โ„‚)
28 nfcsb1v 3102 . . . . . . . . . . . . 13 โ„ฒ๐‘—โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ
2928nfel1 2340 . . . . . . . . . . . 12 โ„ฒ๐‘—โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ โˆˆ โ„‚
3020, 29nfralw 2524 . . . . . . . . . . 11 โ„ฒ๐‘—โˆ€๐‘˜ โˆˆ โฆ‹ ๐‘ฆ / ๐‘—โฆŒ๐ตโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ โˆˆ โ„‚
31 csbeq1a 3078 . . . . . . . . . . . . 13 (๐‘— = ๐‘ฆ โ†’ ๐ถ = โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ)
3231eleq1d 2256 . . . . . . . . . . . 12 (๐‘— = ๐‘ฆ โ†’ (๐ถ โˆˆ โ„‚ โ†” โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ โˆˆ โ„‚))
3322, 32raleqbidv 2695 . . . . . . . . . . 11 (๐‘— = ๐‘ฆ โ†’ (โˆ€๐‘˜ โˆˆ ๐ต ๐ถ โˆˆ โ„‚ โ†” โˆ€๐‘˜ โˆˆ โฆ‹ ๐‘ฆ / ๐‘—โฆŒ๐ตโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ โˆˆ โ„‚))
3430, 33rspc 2847 . . . . . . . . . 10 (๐‘ฆ โˆˆ ๐ด โ†’ (โˆ€๐‘— โˆˆ ๐ด โˆ€๐‘˜ โˆˆ ๐ต ๐ถ โˆˆ โ„‚ โ†’ โˆ€๐‘˜ โˆˆ โฆ‹ ๐‘ฆ / ๐‘—โฆŒ๐ตโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ โˆˆ โ„‚))
3517, 27, 34sylc 62 . . . . . . . . 9 (๐œ‘ โ†’ โˆ€๐‘˜ โˆˆ โฆ‹ ๐‘ฆ / ๐‘—โฆŒ๐ตโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ โˆˆ โ„‚)
3635r19.21bi 2575 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต) โ†’ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ โˆˆ โ„‚)
3725, 36fprodcl 11628 . . . . . . 7 (๐œ‘ โ†’ โˆ๐‘˜ โˆˆ โฆ‹ ๐‘ฆ / ๐‘—โฆŒ๐ตโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ โˆˆ โ„‚)
38 csbeq1 3072 . . . . . . . . 9 (๐‘š = ๐‘ฆ โ†’ โฆ‹๐‘š / ๐‘—โฆŒ๐ต = โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)
39 csbeq1 3072 . . . . . . . . . 10 (๐‘š = ๐‘ฆ โ†’ โฆ‹๐‘š / ๐‘—โฆŒ๐ถ = โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ)
4039adantr 276 . . . . . . . . 9 ((๐‘š = ๐‘ฆ โˆง ๐‘˜ โˆˆ โฆ‹๐‘š / ๐‘—โฆŒ๐ต) โ†’ โฆ‹๐‘š / ๐‘—โฆŒ๐ถ = โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ)
4138, 40prodeq12dv 11590 . . . . . . . 8 (๐‘š = ๐‘ฆ โ†’ โˆ๐‘˜ โˆˆ โฆ‹ ๐‘š / ๐‘—โฆŒ๐ตโฆ‹๐‘š / ๐‘—โฆŒ๐ถ = โˆ๐‘˜ โˆˆ โฆ‹ ๐‘ฆ / ๐‘—โฆŒ๐ตโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ)
4241prodsn 11614 . . . . . . 7 ((๐‘ฆ โˆˆ ๐ด โˆง โˆ๐‘˜ โˆˆ โฆ‹ ๐‘ฆ / ๐‘—โฆŒ๐ตโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ โˆˆ โ„‚) โ†’ โˆ๐‘š โˆˆ {๐‘ฆ}โˆ๐‘˜ โˆˆ โฆ‹ ๐‘š / ๐‘—โฆŒ๐ตโฆ‹๐‘š / ๐‘—โฆŒ๐ถ = โˆ๐‘˜ โˆˆ โฆ‹ ๐‘ฆ / ๐‘—โฆŒ๐ตโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ)
4317, 37, 42syl2anc 411 . . . . . 6 (๐œ‘ โ†’ โˆ๐‘š โˆˆ {๐‘ฆ}โˆ๐‘˜ โˆˆ โฆ‹ ๐‘š / ๐‘—โฆŒ๐ตโฆ‹๐‘š / ๐‘—โฆŒ๐ถ = โˆ๐‘˜ โˆˆ โฆ‹ ๐‘ฆ / ๐‘—โฆŒ๐ตโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ)
44 nfcv 2329 . . . . . . . 8 โ„ฒ๐‘šโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ
45 nfcsb1v 3102 . . . . . . . 8 โ„ฒ๐‘˜โฆ‹๐‘š / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ
46 csbeq1a 3078 . . . . . . . 8 (๐‘˜ = ๐‘š โ†’ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ = โฆ‹๐‘š / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ)
4744, 45, 46cbvprodi 11581 . . . . . . 7 โˆ๐‘˜ โˆˆ โฆ‹ ๐‘ฆ / ๐‘—โฆŒ๐ตโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ = โˆ๐‘š โˆˆ โฆ‹ ๐‘ฆ / ๐‘—โฆŒ๐ตโฆ‹๐‘š / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ
48 csbeq1 3072 . . . . . . . . 9 (๐‘š = (2nd โ€˜๐‘ง) โ†’ โฆ‹๐‘š / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ = โฆ‹(2nd โ€˜๐‘ง) / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ)
49 snfig 6827 . . . . . . . . . . 11 (๐‘ฆ โˆˆ V โ†’ {๐‘ฆ} โˆˆ Fin)
5049elv 2753 . . . . . . . . . 10 {๐‘ฆ} โˆˆ Fin
51 xpfi 6942 . . . . . . . . . 10 (({๐‘ฆ} โˆˆ Fin โˆง โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต โˆˆ Fin) โ†’ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต) โˆˆ Fin)
5250, 25, 51sylancr 414 . . . . . . . . 9 (๐œ‘ โ†’ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต) โˆˆ Fin)
53 2ndconst 6236 . . . . . . . . . 10 (๐‘ฆ โˆˆ ๐ด โ†’ (2nd โ†พ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)):({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)โ€“1-1-ontoโ†’โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)
5417, 53syl 14 . . . . . . . . 9 (๐œ‘ โ†’ (2nd โ†พ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)):({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)โ€“1-1-ontoโ†’โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)
55 fvres 5551 . . . . . . . . . 10 (๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต) โ†’ ((2nd โ†พ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต))โ€˜๐‘ง) = (2nd โ€˜๐‘ง))
5655adantl 277 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)) โ†’ ((2nd โ†พ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต))โ€˜๐‘ง) = (2nd โ€˜๐‘ง))
5745nfel1 2340 . . . . . . . . . . 11 โ„ฒ๐‘˜โฆ‹๐‘š / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ โˆˆ โ„‚
5846eleq1d 2256 . . . . . . . . . . 11 (๐‘˜ = ๐‘š โ†’ (โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ โˆˆ โ„‚ โ†” โฆ‹๐‘š / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ โˆˆ โ„‚))
5957, 58rspc 2847 . . . . . . . . . 10 (๐‘š โˆˆ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต โ†’ (โˆ€๐‘˜ โˆˆ โฆ‹ ๐‘ฆ / ๐‘—โฆŒ๐ตโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ โˆˆ โ„‚ โ†’ โฆ‹๐‘š / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ โˆˆ โ„‚))
6035, 59mpan9 281 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘š โˆˆ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต) โ†’ โฆ‹๐‘š / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ โˆˆ โ„‚)
6148, 52, 54, 56, 60fprodf1o 11609 . . . . . . . 8 (๐œ‘ โ†’ โˆ๐‘š โˆˆ โฆ‹ ๐‘ฆ / ๐‘—โฆŒ๐ตโฆ‹๐‘š / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ = โˆ๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)โฆ‹(2nd โ€˜๐‘ง) / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ)
62 elxp 4655 . . . . . . . . . . . 12 (๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต) โ†” โˆƒ๐‘šโˆƒ๐‘˜(๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘ฆ} โˆง ๐‘˜ โˆˆ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)))
63 nfv 1538 . . . . . . . . . . . . . . 15 โ„ฒ๐‘— ๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ
64 nfv 1538 . . . . . . . . . . . . . . . 16 โ„ฒ๐‘— ๐‘š โˆˆ {๐‘ฆ}
6520nfcri 2323 . . . . . . . . . . . . . . . 16 โ„ฒ๐‘— ๐‘˜ โˆˆ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต
6664, 65nfan 1575 . . . . . . . . . . . . . . 15 โ„ฒ๐‘—(๐‘š โˆˆ {๐‘ฆ} โˆง ๐‘˜ โˆˆ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)
6763, 66nfan 1575 . . . . . . . . . . . . . 14 โ„ฒ๐‘—(๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘ฆ} โˆง ๐‘˜ โˆˆ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต))
6867nfex 1647 . . . . . . . . . . . . 13 โ„ฒ๐‘—โˆƒ๐‘˜(๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘ฆ} โˆง ๐‘˜ โˆˆ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต))
69 nfv 1538 . . . . . . . . . . . . 13 โ„ฒ๐‘šโˆƒ๐‘˜(๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ โˆง (๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ ๐ต))
70 opeq1 3790 . . . . . . . . . . . . . . . 16 (๐‘š = ๐‘— โ†’ โŸจ๐‘š, ๐‘˜โŸฉ = โŸจ๐‘—, ๐‘˜โŸฉ)
7170eqeq2d 2199 . . . . . . . . . . . . . . 15 (๐‘š = ๐‘— โ†’ (๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โ†” ๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ))
72 eleq1w 2248 . . . . . . . . . . . . . . . . . 18 (๐‘š = ๐‘— โ†’ (๐‘š โˆˆ {๐‘ฆ} โ†” ๐‘— โˆˆ {๐‘ฆ}))
73 velsn 3621 . . . . . . . . . . . . . . . . . 18 (๐‘— โˆˆ {๐‘ฆ} โ†” ๐‘— = ๐‘ฆ)
7472, 73bitrdi 196 . . . . . . . . . . . . . . . . 17 (๐‘š = ๐‘— โ†’ (๐‘š โˆˆ {๐‘ฆ} โ†” ๐‘— = ๐‘ฆ))
7574anbi1d 465 . . . . . . . . . . . . . . . 16 (๐‘š = ๐‘— โ†’ ((๐‘š โˆˆ {๐‘ฆ} โˆง ๐‘˜ โˆˆ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต) โ†” (๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)))
7622eleq2d 2257 . . . . . . . . . . . . . . . . 17 (๐‘— = ๐‘ฆ โ†’ (๐‘˜ โˆˆ ๐ต โ†” ๐‘˜ โˆˆ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต))
7776pm5.32i 454 . . . . . . . . . . . . . . . 16 ((๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ ๐ต) โ†” (๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต))
7875, 77bitr4di 198 . . . . . . . . . . . . . . 15 (๐‘š = ๐‘— โ†’ ((๐‘š โˆˆ {๐‘ฆ} โˆง ๐‘˜ โˆˆ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต) โ†” (๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ ๐ต)))
7971, 78anbi12d 473 . . . . . . . . . . . . . 14 (๐‘š = ๐‘— โ†’ ((๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘ฆ} โˆง ๐‘˜ โˆˆ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)) โ†” (๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ โˆง (๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ ๐ต))))
8079exbidv 1835 . . . . . . . . . . . . 13 (๐‘š = ๐‘— โ†’ (โˆƒ๐‘˜(๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘ฆ} โˆง ๐‘˜ โˆˆ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)) โ†” โˆƒ๐‘˜(๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ โˆง (๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ ๐ต))))
8168, 69, 80cbvexv1 1762 . . . . . . . . . . . 12 (โˆƒ๐‘šโˆƒ๐‘˜(๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘ฆ} โˆง ๐‘˜ โˆˆ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)) โ†” โˆƒ๐‘—โˆƒ๐‘˜(๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ โˆง (๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ ๐ต)))
8262, 81bitri 184 . . . . . . . . . . 11 (๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต) โ†” โˆƒ๐‘—โˆƒ๐‘˜(๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ โˆง (๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ ๐ต)))
83 nfv 1538 . . . . . . . . . . . 12 โ„ฒ๐‘—๐œ‘
84 nfcv 2329 . . . . . . . . . . . . . 14 โ„ฒ๐‘—(2nd โ€˜๐‘ง)
8584, 28nfcsbw 3105 . . . . . . . . . . . . 13 โ„ฒ๐‘—โฆ‹(2nd โ€˜๐‘ง) / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ
8685nfeq2 2341 . . . . . . . . . . . 12 โ„ฒ๐‘— ๐ท = โฆ‹(2nd โ€˜๐‘ง) / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ
87 nfv 1538 . . . . . . . . . . . . 13 โ„ฒ๐‘˜๐œ‘
88 nfcsb1v 3102 . . . . . . . . . . . . . 14 โ„ฒ๐‘˜โฆ‹(2nd โ€˜๐‘ง) / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ
8988nfeq2 2341 . . . . . . . . . . . . 13 โ„ฒ๐‘˜ ๐ท = โฆ‹(2nd โ€˜๐‘ง) / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ
90 fprod2d.1 . . . . . . . . . . . . . . . 16 (๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ โ†’ ๐ท = ๐ถ)
9190ad2antlr 489 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ) โˆง (๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ ๐ต)) โ†’ ๐ท = ๐ถ)
9231ad2antrl 490 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ) โˆง (๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ ๐ต)) โ†’ ๐ถ = โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ)
93 fveq2 5527 . . . . . . . . . . . . . . . . . 18 (๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ โ†’ (2nd โ€˜๐‘ง) = (2nd โ€˜โŸจ๐‘—, ๐‘˜โŸฉ))
94 vex 2752 . . . . . . . . . . . . . . . . . . 19 ๐‘— โˆˆ V
95 vex 2752 . . . . . . . . . . . . . . . . . . 19 ๐‘˜ โˆˆ V
9694, 95op2nd 6161 . . . . . . . . . . . . . . . . . 18 (2nd โ€˜โŸจ๐‘—, ๐‘˜โŸฉ) = ๐‘˜
9793, 96eqtr2di 2237 . . . . . . . . . . . . . . . . 17 (๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ โ†’ ๐‘˜ = (2nd โ€˜๐‘ง))
9897ad2antlr 489 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ) โˆง (๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ ๐ต)) โ†’ ๐‘˜ = (2nd โ€˜๐‘ง))
99 csbeq1a 3078 . . . . . . . . . . . . . . . 16 (๐‘˜ = (2nd โ€˜๐‘ง) โ†’ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ = โฆ‹(2nd โ€˜๐‘ง) / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ)
10098, 99syl 14 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ) โˆง (๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ ๐ต)) โ†’ โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ = โฆ‹(2nd โ€˜๐‘ง) / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ)
10191, 92, 1003eqtrd 2224 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ) โˆง (๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ ๐ต)) โ†’ ๐ท = โฆ‹(2nd โ€˜๐‘ง) / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ)
102101expl 378 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ โˆง (๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ ๐ต)) โ†’ ๐ท = โฆ‹(2nd โ€˜๐‘ง) / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ))
10387, 89, 102exlimd 1607 . . . . . . . . . . . 12 (๐œ‘ โ†’ (โˆƒ๐‘˜(๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ โˆง (๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ ๐ต)) โ†’ ๐ท = โฆ‹(2nd โ€˜๐‘ง) / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ))
10483, 86, 103exlimd 1607 . . . . . . . . . . 11 (๐œ‘ โ†’ (โˆƒ๐‘—โˆƒ๐‘˜(๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ โˆง (๐‘— = ๐‘ฆ โˆง ๐‘˜ โˆˆ ๐ต)) โ†’ ๐ท = โฆ‹(2nd โ€˜๐‘ง) / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ))
10582, 104biimtrid 152 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต) โ†’ ๐ท = โฆ‹(2nd โ€˜๐‘ง) / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ))
106105imp 124 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)) โ†’ ๐ท = โฆ‹(2nd โ€˜๐‘ง) / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ)
107106prodeq2dv 11587 . . . . . . . 8 (๐œ‘ โ†’ โˆ๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)๐ท = โˆ๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)โฆ‹(2nd โ€˜๐‘ง) / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ)
10861, 107eqtr4d 2223 . . . . . . 7 (๐œ‘ โ†’ โˆ๐‘š โˆˆ โฆ‹ ๐‘ฆ / ๐‘—โฆŒ๐ตโฆ‹๐‘š / ๐‘˜โฆŒโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ = โˆ๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)๐ท)
10947, 108eqtrid 2232 . . . . . 6 (๐œ‘ โ†’ โˆ๐‘˜ โˆˆ โฆ‹ ๐‘ฆ / ๐‘—โฆŒ๐ตโฆ‹๐‘ฆ / ๐‘—โฆŒ๐ถ = โˆ๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)๐ท)
11043, 109eqtrd 2220 . . . . 5 (๐œ‘ โ†’ โˆ๐‘š โˆˆ {๐‘ฆ}โˆ๐‘˜ โˆˆ โฆ‹ ๐‘š / ๐‘—โฆŒ๐ตโฆ‹๐‘š / ๐‘—โฆŒ๐ถ = โˆ๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)๐ท)
11112, 110eqtrid 2232 . . . 4 (๐œ‘ โ†’ โˆ๐‘— โˆˆ {๐‘ฆ}โˆ๐‘˜ โˆˆ ๐ต ๐ถ = โˆ๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)๐ท)
112111adantr 276 . . 3 ((๐œ‘ โˆง ๐œ“) โ†’ โˆ๐‘— โˆˆ {๐‘ฆ}โˆ๐‘˜ โˆˆ ๐ต ๐ถ = โˆ๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)๐ท)
1133, 112oveq12d 5906 . 2 ((๐œ‘ โˆง ๐œ“) โ†’ (โˆ๐‘— โˆˆ ๐‘ฅ โˆ๐‘˜ โˆˆ ๐ต ๐ถ ยท โˆ๐‘— โˆˆ {๐‘ฆ}โˆ๐‘˜ โˆˆ ๐ต ๐ถ) = (โˆ๐‘ง โˆˆ โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต)๐ท ยท โˆ๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)๐ท))
114 fprod2d.5 . . . . 5 (๐œ‘ โ†’ ยฌ ๐‘ฆ โˆˆ ๐‘ฅ)
115 disjsn 3666 . . . . 5 ((๐‘ฅ โˆฉ {๐‘ฆ}) = โˆ… โ†” ยฌ ๐‘ฆ โˆˆ ๐‘ฅ)
116114, 115sylibr 134 . . . 4 (๐œ‘ โ†’ (๐‘ฅ โˆฉ {๐‘ฆ}) = โˆ…)
117 eqidd 2188 . . . 4 (๐œ‘ โ†’ (๐‘ฅ โˆช {๐‘ฆ}) = (๐‘ฅ โˆช {๐‘ฆ}))
118 fprod2dlemstep.x . . . . 5 (๐œ‘ โ†’ ๐‘ฅ โˆˆ Fin)
11915a1i 9 . . . . 5 (๐œ‘ โ†’ ๐‘ฆ โˆˆ V)
120 unsnfi 6931 . . . . 5 ((๐‘ฅ โˆˆ Fin โˆง ๐‘ฆ โˆˆ V โˆง ยฌ ๐‘ฆ โˆˆ ๐‘ฅ) โ†’ (๐‘ฅ โˆช {๐‘ฆ}) โˆˆ Fin)
121118, 119, 114, 120syl3anc 1248 . . . 4 (๐œ‘ โ†’ (๐‘ฅ โˆช {๐‘ฆ}) โˆˆ Fin)
12213sselda 3167 . . . . 5 ((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โ†’ ๐‘— โˆˆ ๐ด)
12326anassrs 400 . . . . . 6 (((๐œ‘ โˆง ๐‘— โˆˆ ๐ด) โˆง ๐‘˜ โˆˆ ๐ต) โ†’ ๐ถ โˆˆ โ„‚)
12418, 123fprodcl 11628 . . . . 5 ((๐œ‘ โˆง ๐‘— โˆˆ ๐ด) โ†’ โˆ๐‘˜ โˆˆ ๐ต ๐ถ โˆˆ โ„‚)
125122, 124syldan 282 . . . 4 ((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โ†’ โˆ๐‘˜ โˆˆ ๐ต ๐ถ โˆˆ โ„‚)
126116, 117, 121, 125fprodsplit 11618 . . 3 (๐œ‘ โ†’ โˆ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})โˆ๐‘˜ โˆˆ ๐ต ๐ถ = (โˆ๐‘— โˆˆ ๐‘ฅ โˆ๐‘˜ โˆˆ ๐ต ๐ถ ยท โˆ๐‘— โˆˆ {๐‘ฆ}โˆ๐‘˜ โˆˆ ๐ต ๐ถ))
127126adantr 276 . 2 ((๐œ‘ โˆง ๐œ“) โ†’ โˆ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})โˆ๐‘˜ โˆˆ ๐ต ๐ถ = (โˆ๐‘— โˆˆ ๐‘ฅ โˆ๐‘˜ โˆˆ ๐ต ๐ถ ยท โˆ๐‘— โˆˆ {๐‘ฆ}โˆ๐‘˜ โˆˆ ๐ต ๐ถ))
128 eliun 3902 . . . . . . . . . 10 (๐‘ง โˆˆ โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต) โ†” โˆƒ๐‘— โˆˆ ๐‘ฅ ๐‘ง โˆˆ ({๐‘—} ร— ๐ต))
129 xp1st 6179 . . . . . . . . . . . . . 14 (๐‘ง โˆˆ ({๐‘—} ร— ๐ต) โ†’ (1st โ€˜๐‘ง) โˆˆ {๐‘—})
130 elsni 3622 . . . . . . . . . . . . . 14 ((1st โ€˜๐‘ง) โˆˆ {๐‘—} โ†’ (1st โ€˜๐‘ง) = ๐‘—)
131129, 130syl 14 . . . . . . . . . . . . 13 (๐‘ง โˆˆ ({๐‘—} ร— ๐ต) โ†’ (1st โ€˜๐‘ง) = ๐‘—)
132131eleq1d 2256 . . . . . . . . . . . 12 (๐‘ง โˆˆ ({๐‘—} ร— ๐ต) โ†’ ((1st โ€˜๐‘ง) โˆˆ ๐‘ฅ โ†” ๐‘— โˆˆ ๐‘ฅ))
133132biimparc 299 . . . . . . . . . . 11 ((๐‘— โˆˆ ๐‘ฅ โˆง ๐‘ง โˆˆ ({๐‘—} ร— ๐ต)) โ†’ (1st โ€˜๐‘ง) โˆˆ ๐‘ฅ)
134133rexlimiva 2599 . . . . . . . . . 10 (โˆƒ๐‘— โˆˆ ๐‘ฅ ๐‘ง โˆˆ ({๐‘—} ร— ๐ต) โ†’ (1st โ€˜๐‘ง) โˆˆ ๐‘ฅ)
135128, 134sylbi 121 . . . . . . . . 9 (๐‘ง โˆˆ โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต) โ†’ (1st โ€˜๐‘ง) โˆˆ ๐‘ฅ)
136 xp1st 6179 . . . . . . . . 9 (๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต) โ†’ (1st โ€˜๐‘ง) โˆˆ {๐‘ฆ})
137135, 136anim12i 338 . . . . . . . 8 ((๐‘ง โˆˆ โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต) โˆง ๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)) โ†’ ((1st โ€˜๐‘ง) โˆˆ ๐‘ฅ โˆง (1st โ€˜๐‘ง) โˆˆ {๐‘ฆ}))
138 elin 3330 . . . . . . . 8 (๐‘ง โˆˆ (โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต) โˆฉ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)) โ†” (๐‘ง โˆˆ โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต) โˆง ๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)))
139 elin 3330 . . . . . . . 8 ((1st โ€˜๐‘ง) โˆˆ (๐‘ฅ โˆฉ {๐‘ฆ}) โ†” ((1st โ€˜๐‘ง) โˆˆ ๐‘ฅ โˆง (1st โ€˜๐‘ง) โˆˆ {๐‘ฆ}))
140137, 138, 1393imtr4i 201 . . . . . . 7 (๐‘ง โˆˆ (โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต) โˆฉ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)) โ†’ (1st โ€˜๐‘ง) โˆˆ (๐‘ฅ โˆฉ {๐‘ฆ}))
141116eleq2d 2257 . . . . . . . 8 (๐œ‘ โ†’ ((1st โ€˜๐‘ง) โˆˆ (๐‘ฅ โˆฉ {๐‘ฆ}) โ†” (1st โ€˜๐‘ง) โˆˆ โˆ…))
142 noel 3438 . . . . . . . . 9 ยฌ (1st โ€˜๐‘ง) โˆˆ โˆ…
143142pm2.21i 647 . . . . . . . 8 ((1st โ€˜๐‘ง) โˆˆ โˆ… โ†’ ๐‘ง โˆˆ โˆ…)
144141, 143biimtrdi 163 . . . . . . 7 (๐œ‘ โ†’ ((1st โ€˜๐‘ง) โˆˆ (๐‘ฅ โˆฉ {๐‘ฆ}) โ†’ ๐‘ง โˆˆ โˆ…))
145140, 144syl5 32 . . . . . 6 (๐œ‘ โ†’ (๐‘ง โˆˆ (โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต) โˆฉ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)) โ†’ ๐‘ง โˆˆ โˆ…))
146145ssrdv 3173 . . . . 5 (๐œ‘ โ†’ (โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต) โˆฉ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)) โІ โˆ…)
147 ss0 3475 . . . . 5 ((โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต) โˆฉ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)) โІ โˆ… โ†’ (โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต) โˆฉ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)) = โˆ…)
148146, 147syl 14 . . . 4 (๐œ‘ โ†’ (โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต) โˆฉ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)) = โˆ…)
149 iunxun 3978 . . . . . 6 โˆช ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})({๐‘—} ร— ๐ต) = (โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต) โˆช โˆช ๐‘— โˆˆ {๐‘ฆ} ({๐‘—} ร— ๐ต))
150 nfcv 2329 . . . . . . . . 9 โ„ฒ๐‘š({๐‘—} ร— ๐ต)
151 nfcv 2329 . . . . . . . . . 10 โ„ฒ๐‘—{๐‘š}
152151, 5nfxp 4665 . . . . . . . . 9 โ„ฒ๐‘—({๐‘š} ร— โฆ‹๐‘š / ๐‘—โฆŒ๐ต)
153 sneq 3615 . . . . . . . . . 10 (๐‘— = ๐‘š โ†’ {๐‘—} = {๐‘š})
154153, 8xpeq12d 4663 . . . . . . . . 9 (๐‘— = ๐‘š โ†’ ({๐‘—} ร— ๐ต) = ({๐‘š} ร— โฆ‹๐‘š / ๐‘—โฆŒ๐ต))
155150, 152, 154cbviun 3935 . . . . . . . 8 โˆช ๐‘— โˆˆ {๐‘ฆ} ({๐‘—} ร— ๐ต) = โˆช ๐‘š โˆˆ {๐‘ฆ} ({๐‘š} ร— โฆ‹๐‘š / ๐‘—โฆŒ๐ต)
156 sneq 3615 . . . . . . . . . 10 (๐‘š = ๐‘ฆ โ†’ {๐‘š} = {๐‘ฆ})
157156, 38xpeq12d 4663 . . . . . . . . 9 (๐‘š = ๐‘ฆ โ†’ ({๐‘š} ร— โฆ‹๐‘š / ๐‘—โฆŒ๐ต) = ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต))
15815, 157iunxsn 3975 . . . . . . . 8 โˆช ๐‘š โˆˆ {๐‘ฆ} ({๐‘š} ร— โฆ‹๐‘š / ๐‘—โฆŒ๐ต) = ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)
159155, 158eqtri 2208 . . . . . . 7 โˆช ๐‘— โˆˆ {๐‘ฆ} ({๐‘—} ร— ๐ต) = ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)
160159uneq2i 3298 . . . . . 6 (โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต) โˆช โˆช ๐‘— โˆˆ {๐‘ฆ} ({๐‘—} ร— ๐ต)) = (โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต) โˆช ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต))
161149, 160eqtri 2208 . . . . 5 โˆช ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})({๐‘—} ร— ๐ต) = (โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต) โˆช ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต))
162161a1i 9 . . . 4 (๐œ‘ โ†’ โˆช ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})({๐‘—} ร— ๐ต) = (โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต) โˆช ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)))
163 snfig 6827 . . . . . . . 8 (๐‘— โˆˆ V โ†’ {๐‘—} โˆˆ Fin)
164163elv 2753 . . . . . . 7 {๐‘—} โˆˆ Fin
165122, 18syldan 282 . . . . . . 7 ((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โ†’ ๐ต โˆˆ Fin)
166 xpfi 6942 . . . . . . 7 (({๐‘—} โˆˆ Fin โˆง ๐ต โˆˆ Fin) โ†’ ({๐‘—} ร— ๐ต) โˆˆ Fin)
167164, 165, 166sylancr 414 . . . . . 6 ((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โ†’ ({๐‘—} ร— ๐ต) โˆˆ Fin)
168167ralrimiva 2560 . . . . 5 (๐œ‘ โ†’ โˆ€๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})({๐‘—} ร— ๐ต) โˆˆ Fin)
169 disjsnxp 6251 . . . . . 6 Disj ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})({๐‘—} ร— ๐ต)
170169a1i 9 . . . . 5 (๐œ‘ โ†’ Disj ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})({๐‘—} ร— ๐ต))
171 iunfidisj 6958 . . . . 5 (((๐‘ฅ โˆช {๐‘ฆ}) โˆˆ Fin โˆง โˆ€๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})({๐‘—} ร— ๐ต) โˆˆ Fin โˆง Disj ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})({๐‘—} ร— ๐ต)) โ†’ โˆช ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})({๐‘—} ร— ๐ต) โˆˆ Fin)
172121, 168, 170, 171syl3anc 1248 . . . 4 (๐œ‘ โ†’ โˆช ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})({๐‘—} ร— ๐ต) โˆˆ Fin)
173 eliun 3902 . . . . . 6 (๐‘ง โˆˆ โˆช ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})({๐‘—} ร— ๐ต) โ†” โˆƒ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})๐‘ง โˆˆ ({๐‘—} ร— ๐ต))
174 elxp 4655 . . . . . . . 8 (๐‘ง โˆˆ ({๐‘—} ร— ๐ต) โ†” โˆƒ๐‘šโˆƒ๐‘˜(๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘—} โˆง ๐‘˜ โˆˆ ๐ต)))
175 simprl 529 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โˆง (๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘—} โˆง ๐‘˜ โˆˆ ๐ต))) โ†’ ๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ)
176 simprrl 539 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โˆง (๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘—} โˆง ๐‘˜ โˆˆ ๐ต))) โ†’ ๐‘š โˆˆ {๐‘—})
177 elsni 3622 . . . . . . . . . . . . . . 15 (๐‘š โˆˆ {๐‘—} โ†’ ๐‘š = ๐‘—)
178176, 177syl 14 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โˆง (๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘—} โˆง ๐‘˜ โˆˆ ๐ต))) โ†’ ๐‘š = ๐‘—)
179178opeq1d 3796 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โˆง (๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘—} โˆง ๐‘˜ โˆˆ ๐ต))) โ†’ โŸจ๐‘š, ๐‘˜โŸฉ = โŸจ๐‘—, ๐‘˜โŸฉ)
180175, 179eqtrd 2220 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โˆง (๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘—} โˆง ๐‘˜ โˆˆ ๐ต))) โ†’ ๐‘ง = โŸจ๐‘—, ๐‘˜โŸฉ)
181180, 90syl 14 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โˆง (๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘—} โˆง ๐‘˜ โˆˆ ๐ต))) โ†’ ๐ท = ๐ถ)
182 simpll 527 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โˆง (๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘—} โˆง ๐‘˜ โˆˆ ๐ต))) โ†’ ๐œ‘)
183122adantr 276 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โˆง (๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘—} โˆง ๐‘˜ โˆˆ ๐ต))) โ†’ ๐‘— โˆˆ ๐ด)
184 simprrr 540 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โˆง (๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘—} โˆง ๐‘˜ โˆˆ ๐ต))) โ†’ ๐‘˜ โˆˆ ๐ต)
185182, 183, 184, 26syl12anc 1246 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โˆง (๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘—} โˆง ๐‘˜ โˆˆ ๐ต))) โ†’ ๐ถ โˆˆ โ„‚)
186181, 185eqeltrd 2264 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โˆง (๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘—} โˆง ๐‘˜ โˆˆ ๐ต))) โ†’ ๐ท โˆˆ โ„‚)
187186ex 115 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โ†’ ((๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘—} โˆง ๐‘˜ โˆˆ ๐ต)) โ†’ ๐ท โˆˆ โ„‚))
188187exlimdvv 1907 . . . . . . . 8 ((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โ†’ (โˆƒ๐‘šโˆƒ๐‘˜(๐‘ง = โŸจ๐‘š, ๐‘˜โŸฉ โˆง (๐‘š โˆˆ {๐‘—} โˆง ๐‘˜ โˆˆ ๐ต)) โ†’ ๐ท โˆˆ โ„‚))
189174, 188biimtrid 152 . . . . . . 7 ((๐œ‘ โˆง ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})) โ†’ (๐‘ง โˆˆ ({๐‘—} ร— ๐ต) โ†’ ๐ท โˆˆ โ„‚))
190189rexlimdva 2604 . . . . . 6 (๐œ‘ โ†’ (โˆƒ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})๐‘ง โˆˆ ({๐‘—} ร— ๐ต) โ†’ ๐ท โˆˆ โ„‚))
191173, 190biimtrid 152 . . . . 5 (๐œ‘ โ†’ (๐‘ง โˆˆ โˆช ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})({๐‘—} ร— ๐ต) โ†’ ๐ท โˆˆ โ„‚))
192191imp 124 . . . 4 ((๐œ‘ โˆง ๐‘ง โˆˆ โˆช ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})({๐‘—} ร— ๐ต)) โ†’ ๐ท โˆˆ โ„‚)
193148, 162, 172, 192fprodsplit 11618 . . 3 (๐œ‘ โ†’ โˆ๐‘ง โˆˆ โˆช ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})({๐‘—} ร— ๐ต)๐ท = (โˆ๐‘ง โˆˆ โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต)๐ท ยท โˆ๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)๐ท))
194193adantr 276 . 2 ((๐œ‘ โˆง ๐œ“) โ†’ โˆ๐‘ง โˆˆ โˆช ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})({๐‘—} ร— ๐ต)๐ท = (โˆ๐‘ง โˆˆ โˆช ๐‘— โˆˆ ๐‘ฅ ({๐‘—} ร— ๐ต)๐ท ยท โˆ๐‘ง โˆˆ ({๐‘ฆ} ร— โฆ‹๐‘ฆ / ๐‘—โฆŒ๐ต)๐ท))
195113, 127, 1943eqtr4d 2230 1 ((๐œ‘ โˆง ๐œ“) โ†’ โˆ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})โˆ๐‘˜ โˆˆ ๐ต ๐ถ = โˆ๐‘ง โˆˆ โˆช ๐‘— โˆˆ (๐‘ฅ โˆช {๐‘ฆ})({๐‘—} ร— ๐ต)๐ท)
Colors of variables: wff set class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โˆง wa 104   โ†” wb 105   = wceq 1363  โˆƒwex 1502   โˆˆ wcel 2158  โˆ€wral 2465  โˆƒwrex 2466  Vcvv 2749  โฆ‹csb 3069   โˆช cun 3139   โˆฉ cin 3140   โІ wss 3141  โˆ…c0 3434  {csn 3604  โŸจcop 3607  โˆช ciun 3898  Disj wdisj 3992   ร— cxp 4636   โ†พ cres 4640  โ€“1-1-ontoโ†’wf1o 5227  โ€˜cfv 5228  (class class class)co 5888  1st c1st 6152  2nd c2nd 6153  Fincfn 6753  โ„‚cc 7822   ยท cmul 7829  โˆcprod 11571
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 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-13 2160  ax-14 2161  ax-ext 2169  ax-coll 4130  ax-sep 4133  ax-nul 4141  ax-pow 4186  ax-pr 4221  ax-un 4445  ax-setind 4548  ax-iinf 4599  ax-cnex 7915  ax-resscn 7916  ax-1cn 7917  ax-1re 7918  ax-icn 7919  ax-addcl 7920  ax-addrcl 7921  ax-mulcl 7922  ax-mulrcl 7923  ax-addcom 7924  ax-mulcom 7925  ax-addass 7926  ax-mulass 7927  ax-distr 7928  ax-i2m1 7929  ax-0lt1 7930  ax-1rid 7931  ax-0id 7932  ax-rnegex 7933  ax-precex 7934  ax-cnre 7935  ax-pre-ltirr 7936  ax-pre-ltwlin 7937  ax-pre-lttrn 7938  ax-pre-apti 7939  ax-pre-ltadd 7940  ax-pre-mulgt0 7941  ax-pre-mulext 7942  ax-arch 7943  ax-caucvg 7944
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 980  df-3an 981  df-tru 1366  df-fal 1369  df-nf 1471  df-sb 1773  df-eu 2039  df-mo 2040  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-ne 2358  df-nel 2453  df-ral 2470  df-rex 2471  df-reu 2472  df-rmo 2473  df-rab 2474  df-v 2751  df-sbc 2975  df-csb 3070  df-dif 3143  df-un 3145  df-in 3147  df-ss 3154  df-nul 3435  df-if 3547  df-pw 3589  df-sn 3610  df-pr 3611  df-op 3613  df-uni 3822  df-int 3857  df-iun 3900  df-disj 3993  df-br 4016  df-opab 4077  df-mpt 4078  df-tr 4114  df-id 4305  df-po 4308  df-iso 4309  df-iord 4378  df-on 4380  df-ilim 4381  df-suc 4383  df-iom 4602  df-xp 4644  df-rel 4645  df-cnv 4646  df-co 4647  df-dm 4648  df-rn 4649  df-res 4650  df-ima 4651  df-iota 5190  df-fun 5230  df-fn 5231  df-f 5232  df-f1 5233  df-fo 5234  df-f1o 5235  df-fv 5236  df-isom 5237  df-riota 5844  df-ov 5891  df-oprab 5892  df-mpo 5893  df-1st 6154  df-2nd 6155  df-recs 6319  df-irdg 6384  df-frec 6405  df-1o 6430  df-oadd 6434  df-er 6548  df-en 6754  df-dom 6755  df-fin 6756  df-pnf 8007  df-mnf 8008  df-xr 8009  df-ltxr 8010  df-le 8011  df-sub 8143  df-neg 8144  df-reap 8545  df-ap 8552  df-div 8643  df-inn 8933  df-2 8991  df-3 8992  df-4 8993  df-n0 9190  df-z 9267  df-uz 9542  df-q 9633  df-rp 9667  df-fz 10022  df-fzo 10156  df-seqfrec 10459  df-exp 10533  df-ihash 10769  df-cj 10864  df-re 10865  df-im 10866  df-rsqrt 11020  df-abs 11021  df-clim 11300  df-proddc 11572
This theorem is referenced by:  fprod2d  11644
  Copyright terms: Public domain W3C validator