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

Theorem prodeq1f 11574
Description: Equality theorem for a product. (Contributed by Scott Fenton, 1-Dec-2017.)
Hypotheses
Ref Expression
prodeq1f.1 โ„ฒ๐‘˜๐ด
prodeq1f.2 โ„ฒ๐‘˜๐ต
Assertion
Ref Expression
prodeq1f (๐ด = ๐ต โ†’ โˆ๐‘˜ โˆˆ ๐ด ๐ถ = โˆ๐‘˜ โˆˆ ๐ต ๐ถ)

Proof of Theorem prodeq1f
Dummy variables ๐‘“ ๐‘— ๐‘š ๐‘› ๐‘ฅ ๐‘ฆ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sseq1 3190 . . . . . . 7 (๐ด = ๐ต โ†’ (๐ด โІ (โ„คโ‰ฅโ€˜๐‘š) โ†” ๐ต โІ (โ„คโ‰ฅโ€˜๐‘š)))
2 eleq2 2251 . . . . . . . . 9 (๐ด = ๐ต โ†’ (๐‘— โˆˆ ๐ด โ†” ๐‘— โˆˆ ๐ต))
32dcbid 839 . . . . . . . 8 (๐ด = ๐ต โ†’ (DECID ๐‘— โˆˆ ๐ด โ†” DECID ๐‘— โˆˆ ๐ต))
43ralbidv 2487 . . . . . . 7 (๐ด = ๐ต โ†’ (โˆ€๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘š)DECID ๐‘— โˆˆ ๐ด โ†” โˆ€๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘š)DECID ๐‘— โˆˆ ๐ต))
51, 4anbi12d 473 . . . . . 6 (๐ด = ๐ต โ†’ ((๐ด โІ (โ„คโ‰ฅโ€˜๐‘š) โˆง โˆ€๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘š)DECID ๐‘— โˆˆ ๐ด) โ†” (๐ต โІ (โ„คโ‰ฅโ€˜๐‘š) โˆง โˆ€๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘š)DECID ๐‘— โˆˆ ๐ต)))
6 prodeq1f.1 . . . . . . . . . . . . . 14 โ„ฒ๐‘˜๐ด
7 prodeq1f.2 . . . . . . . . . . . . . 14 โ„ฒ๐‘˜๐ต
86, 7nfeq 2337 . . . . . . . . . . . . 13 โ„ฒ๐‘˜ ๐ด = ๐ต
9 eleq2 2251 . . . . . . . . . . . . . . 15 (๐ด = ๐ต โ†’ (๐‘˜ โˆˆ ๐ด โ†” ๐‘˜ โˆˆ ๐ต))
109ifbid 3567 . . . . . . . . . . . . . 14 (๐ด = ๐ต โ†’ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1) = if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))
1110adantr 276 . . . . . . . . . . . . 13 ((๐ด = ๐ต โˆง ๐‘˜ โˆˆ โ„ค) โ†’ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1) = if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))
128, 11mpteq2da 4104 . . . . . . . . . . . 12 (๐ด = ๐ต โ†’ (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1)) = (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1)))
1312seqeq3d 10467 . . . . . . . . . . 11 (๐ด = ๐ต โ†’ seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1))) = seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))))
1413breq1d 4025 . . . . . . . . . 10 (๐ด = ๐ต โ†’ (seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1))) โ‡ ๐‘ฆ โ†” seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))) โ‡ ๐‘ฆ))
1514anbi2d 464 . . . . . . . . 9 (๐ด = ๐ต โ†’ ((๐‘ฆ # 0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1))) โ‡ ๐‘ฆ) โ†” (๐‘ฆ # 0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))) โ‡ ๐‘ฆ)))
1615exbidv 1835 . . . . . . . 8 (๐ด = ๐ต โ†’ (โˆƒ๐‘ฆ(๐‘ฆ # 0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1))) โ‡ ๐‘ฆ) โ†” โˆƒ๐‘ฆ(๐‘ฆ # 0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))) โ‡ ๐‘ฆ)))
1716rexbidv 2488 . . . . . . 7 (๐ด = ๐ต โ†’ (โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ # 0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1))) โ‡ ๐‘ฆ) โ†” โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ # 0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))) โ‡ ๐‘ฆ)))
1812seqeq3d 10467 . . . . . . . 8 (๐ด = ๐ต โ†’ seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1))) = seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))))
1918breq1d 4025 . . . . . . 7 (๐ด = ๐ต โ†’ (seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1))) โ‡ ๐‘ฅ โ†” seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))) โ‡ ๐‘ฅ))
2017, 19anbi12d 473 . . . . . 6 (๐ด = ๐ต โ†’ ((โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ # 0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1))) โ‡ ๐‘ฆ) โˆง seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1))) โ‡ ๐‘ฅ) โ†” (โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ # 0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))) โ‡ ๐‘ฆ) โˆง seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))) โ‡ ๐‘ฅ)))
215, 20anbi12d 473 . . . . 5 (๐ด = ๐ต โ†’ (((๐ด โІ (โ„คโ‰ฅโ€˜๐‘š) โˆง โˆ€๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘š)DECID ๐‘— โˆˆ ๐ด) โˆง (โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ # 0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1))) โ‡ ๐‘ฆ) โˆง seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1))) โ‡ ๐‘ฅ)) โ†” ((๐ต โІ (โ„คโ‰ฅโ€˜๐‘š) โˆง โˆ€๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘š)DECID ๐‘— โˆˆ ๐ต) โˆง (โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ # 0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))) โ‡ ๐‘ฆ) โˆง seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))) โ‡ ๐‘ฅ))))
2221rexbidv 2488 . . . 4 (๐ด = ๐ต โ†’ (โˆƒ๐‘š โˆˆ โ„ค ((๐ด โІ (โ„คโ‰ฅโ€˜๐‘š) โˆง โˆ€๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘š)DECID ๐‘— โˆˆ ๐ด) โˆง (โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ # 0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1))) โ‡ ๐‘ฆ) โˆง seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1))) โ‡ ๐‘ฅ)) โ†” โˆƒ๐‘š โˆˆ โ„ค ((๐ต โІ (โ„คโ‰ฅโ€˜๐‘š) โˆง โˆ€๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘š)DECID ๐‘— โˆˆ ๐ต) โˆง (โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ # 0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))) โ‡ ๐‘ฆ) โˆง seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))) โ‡ ๐‘ฅ))))
23 f1oeq3 5463 . . . . . . 7 (๐ด = ๐ต โ†’ (๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด โ†” ๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ต))
2423anbi1d 465 . . . . . 6 (๐ด = ๐ต โ†’ ((๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด โˆง ๐‘ฅ = (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ if(๐‘› โ‰ค ๐‘š, โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ถ, 1)))โ€˜๐‘š)) โ†” (๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ต โˆง ๐‘ฅ = (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ if(๐‘› โ‰ค ๐‘š, โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ถ, 1)))โ€˜๐‘š))))
2524exbidv 1835 . . . . 5 (๐ด = ๐ต โ†’ (โˆƒ๐‘“(๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด โˆง ๐‘ฅ = (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ if(๐‘› โ‰ค ๐‘š, โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ถ, 1)))โ€˜๐‘š)) โ†” โˆƒ๐‘“(๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ต โˆง ๐‘ฅ = (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ if(๐‘› โ‰ค ๐‘š, โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ถ, 1)))โ€˜๐‘š))))
2625rexbidv 2488 . . . 4 (๐ด = ๐ต โ†’ (โˆƒ๐‘š โˆˆ โ„• โˆƒ๐‘“(๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด โˆง ๐‘ฅ = (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ if(๐‘› โ‰ค ๐‘š, โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ถ, 1)))โ€˜๐‘š)) โ†” โˆƒ๐‘š โˆˆ โ„• โˆƒ๐‘“(๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ต โˆง ๐‘ฅ = (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ if(๐‘› โ‰ค ๐‘š, โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ถ, 1)))โ€˜๐‘š))))
2722, 26orbi12d 794 . . 3 (๐ด = ๐ต โ†’ ((โˆƒ๐‘š โˆˆ โ„ค ((๐ด โІ (โ„คโ‰ฅโ€˜๐‘š) โˆง โˆ€๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘š)DECID ๐‘— โˆˆ ๐ด) โˆง (โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ # 0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1))) โ‡ ๐‘ฆ) โˆง seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1))) โ‡ ๐‘ฅ)) โˆจ โˆƒ๐‘š โˆˆ โ„• โˆƒ๐‘“(๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด โˆง ๐‘ฅ = (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ if(๐‘› โ‰ค ๐‘š, โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ถ, 1)))โ€˜๐‘š))) โ†” (โˆƒ๐‘š โˆˆ โ„ค ((๐ต โІ (โ„คโ‰ฅโ€˜๐‘š) โˆง โˆ€๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘š)DECID ๐‘— โˆˆ ๐ต) โˆง (โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ # 0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))) โ‡ ๐‘ฆ) โˆง seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))) โ‡ ๐‘ฅ)) โˆจ โˆƒ๐‘š โˆˆ โ„• โˆƒ๐‘“(๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ต โˆง ๐‘ฅ = (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ if(๐‘› โ‰ค ๐‘š, โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ถ, 1)))โ€˜๐‘š)))))
2827iotabidv 5211 . 2 (๐ด = ๐ต โ†’ (โ„ฉ๐‘ฅ(โˆƒ๐‘š โˆˆ โ„ค ((๐ด โІ (โ„คโ‰ฅโ€˜๐‘š) โˆง โˆ€๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘š)DECID ๐‘— โˆˆ ๐ด) โˆง (โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ # 0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1))) โ‡ ๐‘ฆ) โˆง seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1))) โ‡ ๐‘ฅ)) โˆจ โˆƒ๐‘š โˆˆ โ„• โˆƒ๐‘“(๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด โˆง ๐‘ฅ = (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ if(๐‘› โ‰ค ๐‘š, โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ถ, 1)))โ€˜๐‘š)))) = (โ„ฉ๐‘ฅ(โˆƒ๐‘š โˆˆ โ„ค ((๐ต โІ (โ„คโ‰ฅโ€˜๐‘š) โˆง โˆ€๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘š)DECID ๐‘— โˆˆ ๐ต) โˆง (โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ # 0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))) โ‡ ๐‘ฆ) โˆง seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))) โ‡ ๐‘ฅ)) โˆจ โˆƒ๐‘š โˆˆ โ„• โˆƒ๐‘“(๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ต โˆง ๐‘ฅ = (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ if(๐‘› โ‰ค ๐‘š, โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ถ, 1)))โ€˜๐‘š)))))
29 df-proddc 11573 . 2 โˆ๐‘˜ โˆˆ ๐ด ๐ถ = (โ„ฉ๐‘ฅ(โˆƒ๐‘š โˆˆ โ„ค ((๐ด โІ (โ„คโ‰ฅโ€˜๐‘š) โˆง โˆ€๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘š)DECID ๐‘— โˆˆ ๐ด) โˆง (โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ # 0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1))) โ‡ ๐‘ฆ) โˆง seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ถ, 1))) โ‡ ๐‘ฅ)) โˆจ โˆƒ๐‘š โˆˆ โ„• โˆƒ๐‘“(๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด โˆง ๐‘ฅ = (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ if(๐‘› โ‰ค ๐‘š, โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ถ, 1)))โ€˜๐‘š))))
30 df-proddc 11573 . 2 โˆ๐‘˜ โˆˆ ๐ต ๐ถ = (โ„ฉ๐‘ฅ(โˆƒ๐‘š โˆˆ โ„ค ((๐ต โІ (โ„คโ‰ฅโ€˜๐‘š) โˆง โˆ€๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘š)DECID ๐‘— โˆˆ ๐ต) โˆง (โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ # 0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))) โ‡ ๐‘ฆ) โˆง seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ต, ๐ถ, 1))) โ‡ ๐‘ฅ)) โˆจ โˆƒ๐‘š โˆˆ โ„• โˆƒ๐‘“(๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ต โˆง ๐‘ฅ = (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ if(๐‘› โ‰ค ๐‘š, โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ถ, 1)))โ€˜๐‘š))))
3128, 29, 303eqtr4g 2245 1 (๐ด = ๐ต โ†’ โˆ๐‘˜ โˆˆ ๐ด ๐ถ = โˆ๐‘˜ โˆˆ ๐ต ๐ถ)
Colors of variables: wff set class
Syntax hints:   โ†’ wi 4   โˆง wa 104   โˆจ wo 709  DECID wdc 835   = wceq 1363  โˆƒwex 1502   โˆˆ wcel 2158  โ„ฒwnfc 2316  โˆ€wral 2465  โˆƒwrex 2466  โฆ‹csb 3069   โІ wss 3141  ifcif 3546   class class class wbr 4015   โ†ฆ cmpt 4076  โ„ฉcio 5188  โ€“1-1-ontoโ†’wf1o 5227  โ€˜cfv 5228  (class class class)co 5888  0cc0 7825  1c1 7826   ยท cmul 7830   โ‰ค cle 8007   # cap 8552  โ„•cn 8933  โ„คcz 9267  โ„คโ‰ฅcuz 9542  ...cfz 10022  seqcseq 10459   โ‡ cli 11300  โˆcprod 11572
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-ext 2169
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3an 981  df-tru 1366  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-ral 2470  df-rex 2471  df-v 2751  df-un 3145  df-in 3147  df-ss 3154  df-if 3547  df-sn 3610  df-pr 3611  df-op 3613  df-uni 3822  df-br 4016  df-opab 4077  df-mpt 4078  df-cnv 4646  df-dm 4648  df-rn 4649  df-res 4650  df-iota 5190  df-f 5232  df-f1 5233  df-fo 5234  df-f1o 5235  df-fv 5236  df-ov 5891  df-oprab 5892  df-mpo 5893  df-recs 6320  df-frec 6406  df-seqfrec 10460  df-proddc 11573
This theorem is referenced by:  prodeq1  11575
  Copyright terms: Public domain W3C validator