Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  brapply Structured version   Visualization version   GIF version

Theorem brapply 32579
Description: Binary relation form of the Apply function. (Contributed by Scott Fenton, 12-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
Hypotheses
Ref Expression
brapply.1 𝐴 ∈ V
brapply.2 𝐵 ∈ V
brapply.3 𝐶 ∈ V
Assertion
Ref Expression
brapply (⟨𝐴, 𝐵⟩Apply𝐶𝐶 = (𝐴𝐵))

Proof of Theorem brapply
Dummy variables 𝑎 𝑏 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 snex 5131 . . . 4 {(𝐴 “ {𝐵})} ∈ V
21inex1 5026 . . 3 ({(𝐴 “ {𝐵})} ∩ Singletons ) ∈ V
3 unieq 4668 . . . . 5 (𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons ) → 𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons ))
43unieqd 4670 . . . 4 (𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons ) → 𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons ))
54eqeq2d 2835 . . 3 (𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons ) → (𝐶 = 𝑥𝐶 = ({(𝐴 “ {𝐵})} ∩ Singletons )))
62, 5ceqsexv 3459 . 2 (∃𝑥(𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons ) ∧ 𝐶 = 𝑥) ↔ 𝐶 = ({(𝐴 “ {𝐵})} ∩ Singletons ))
7 df-apply 32514 . . . 4 Apply = (( Bigcup Bigcup ) ∘ (((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V))) ∘ ((Singleton ∘ Img) ∘ pprod( I , Singleton))))
87breqi 4881 . . 3 (⟨𝐴, 𝐵⟩Apply𝐶 ↔ ⟨𝐴, 𝐵⟩(( Bigcup Bigcup ) ∘ (((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V))) ∘ ((Singleton ∘ Img) ∘ pprod( I , Singleton))))𝐶)
9 opex 5155 . . . 4 𝐴, 𝐵⟩ ∈ V
10 brapply.3 . . . 4 𝐶 ∈ V
119, 10brco 5529 . . 3 (⟨𝐴, 𝐵⟩(( Bigcup Bigcup ) ∘ (((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V))) ∘ ((Singleton ∘ Img) ∘ pprod( I , Singleton))))𝐶 ↔ ∃𝑥(⟨𝐴, 𝐵⟩(((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V))) ∘ ((Singleton ∘ Img) ∘ pprod( I , Singleton)))𝑥𝑥( Bigcup Bigcup )𝐶))
12 vex 3417 . . . . . . 7 𝑥 ∈ V
139, 12brco 5529 . . . . . 6 (⟨𝐴, 𝐵⟩(((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V))) ∘ ((Singleton ∘ Img) ∘ pprod( I , Singleton)))𝑥 ↔ ∃𝑦(⟨𝐴, 𝐵⟩((Singleton ∘ Img) ∘ pprod( I , Singleton))𝑦𝑦((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V)))𝑥))
14 vex 3417 . . . . . . . . . 10 𝑦 ∈ V
159, 14brco 5529 . . . . . . . . 9 (⟨𝐴, 𝐵⟩((Singleton ∘ Img) ∘ pprod( I , Singleton))𝑦 ↔ ∃𝑧(⟨𝐴, 𝐵⟩pprod( I , Singleton)𝑧𝑧(Singleton ∘ Img)𝑦))
16 brapply.1 . . . . . . . . . . . . 13 𝐴 ∈ V
17 brapply.2 . . . . . . . . . . . . 13 𝐵 ∈ V
18 vex 3417 . . . . . . . . . . . . 13 𝑧 ∈ V
1916, 17, 18brpprod3a 32527 . . . . . . . . . . . 12 (⟨𝐴, 𝐵⟩pprod( I , Singleton)𝑧 ↔ ∃𝑎𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝐴 I 𝑎𝐵Singleton𝑏))
20 3anrot 1126 . . . . . . . . . . . . . 14 ((𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝐴 I 𝑎𝐵Singleton𝑏) ↔ (𝐴 I 𝑎𝐵Singleton𝑏𝑧 = ⟨𝑎, 𝑏⟩))
21 vex 3417 . . . . . . . . . . . . . . . . 17 𝑎 ∈ V
2221ideq 5511 . . . . . . . . . . . . . . . 16 (𝐴 I 𝑎𝐴 = 𝑎)
23 eqcom 2832 . . . . . . . . . . . . . . . 16 (𝐴 = 𝑎𝑎 = 𝐴)
2422, 23bitri 267 . . . . . . . . . . . . . . 15 (𝐴 I 𝑎𝑎 = 𝐴)
25 vex 3417 . . . . . . . . . . . . . . . 16 𝑏 ∈ V
2617, 25brsingle 32558 . . . . . . . . . . . . . . 15 (𝐵Singleton𝑏𝑏 = {𝐵})
27 biid 253 . . . . . . . . . . . . . . 15 (𝑧 = ⟨𝑎, 𝑏⟩ ↔ 𝑧 = ⟨𝑎, 𝑏⟩)
2824, 26, 273anbi123i 1198 . . . . . . . . . . . . . 14 ((𝐴 I 𝑎𝐵Singleton𝑏𝑧 = ⟨𝑎, 𝑏⟩) ↔ (𝑎 = 𝐴𝑏 = {𝐵} ∧ 𝑧 = ⟨𝑎, 𝑏⟩))
2920, 28bitri 267 . . . . . . . . . . . . 13 ((𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝐴 I 𝑎𝐵Singleton𝑏) ↔ (𝑎 = 𝐴𝑏 = {𝐵} ∧ 𝑧 = ⟨𝑎, 𝑏⟩))
30292exbii 1948 . . . . . . . . . . . 12 (∃𝑎𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝐴 I 𝑎𝐵Singleton𝑏) ↔ ∃𝑎𝑏(𝑎 = 𝐴𝑏 = {𝐵} ∧ 𝑧 = ⟨𝑎, 𝑏⟩))
31 snex 5131 . . . . . . . . . . . . 13 {𝐵} ∈ V
32 opeq1 4625 . . . . . . . . . . . . . 14 (𝑎 = 𝐴 → ⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝑏⟩)
3332eqeq2d 2835 . . . . . . . . . . . . 13 (𝑎 = 𝐴 → (𝑧 = ⟨𝑎, 𝑏⟩ ↔ 𝑧 = ⟨𝐴, 𝑏⟩))
34 opeq2 4626 . . . . . . . . . . . . . 14 (𝑏 = {𝐵} → ⟨𝐴, 𝑏⟩ = ⟨𝐴, {𝐵}⟩)
3534eqeq2d 2835 . . . . . . . . . . . . 13 (𝑏 = {𝐵} → (𝑧 = ⟨𝐴, 𝑏⟩ ↔ 𝑧 = ⟨𝐴, {𝐵}⟩))
3616, 31, 33, 35ceqsex2v 3462 . . . . . . . . . . . 12 (∃𝑎𝑏(𝑎 = 𝐴𝑏 = {𝐵} ∧ 𝑧 = ⟨𝑎, 𝑏⟩) ↔ 𝑧 = ⟨𝐴, {𝐵}⟩)
3719, 30, 363bitri 289 . . . . . . . . . . 11 (⟨𝐴, 𝐵⟩pprod( I , Singleton)𝑧𝑧 = ⟨𝐴, {𝐵}⟩)
3837anbi1i 617 . . . . . . . . . 10 ((⟨𝐴, 𝐵⟩pprod( I , Singleton)𝑧𝑧(Singleton ∘ Img)𝑦) ↔ (𝑧 = ⟨𝐴, {𝐵}⟩ ∧ 𝑧(Singleton ∘ Img)𝑦))
3938exbii 1947 . . . . . . . . 9 (∃𝑧(⟨𝐴, 𝐵⟩pprod( I , Singleton)𝑧𝑧(Singleton ∘ Img)𝑦) ↔ ∃𝑧(𝑧 = ⟨𝐴, {𝐵}⟩ ∧ 𝑧(Singleton ∘ Img)𝑦))
40 opex 5155 . . . . . . . . . . 11 𝐴, {𝐵}⟩ ∈ V
41 breq1 4878 . . . . . . . . . . 11 (𝑧 = ⟨𝐴, {𝐵}⟩ → (𝑧(Singleton ∘ Img)𝑦 ↔ ⟨𝐴, {𝐵}⟩(Singleton ∘ Img)𝑦))
4240, 41ceqsexv 3459 . . . . . . . . . 10 (∃𝑧(𝑧 = ⟨𝐴, {𝐵}⟩ ∧ 𝑧(Singleton ∘ Img)𝑦) ↔ ⟨𝐴, {𝐵}⟩(Singleton ∘ Img)𝑦)
4340, 14brco 5529 . . . . . . . . . 10 (⟨𝐴, {𝐵}⟩(Singleton ∘ Img)𝑦 ↔ ∃𝑥(⟨𝐴, {𝐵}⟩Img𝑥𝑥Singleton𝑦))
4416, 31, 12brimg 32578 . . . . . . . . . . . . 13 (⟨𝐴, {𝐵}⟩Img𝑥𝑥 = (𝐴 “ {𝐵}))
4512, 14brsingle 32558 . . . . . . . . . . . . 13 (𝑥Singleton𝑦𝑦 = {𝑥})
4644, 45anbi12i 620 . . . . . . . . . . . 12 ((⟨𝐴, {𝐵}⟩Img𝑥𝑥Singleton𝑦) ↔ (𝑥 = (𝐴 “ {𝐵}) ∧ 𝑦 = {𝑥}))
4746exbii 1947 . . . . . . . . . . 11 (∃𝑥(⟨𝐴, {𝐵}⟩Img𝑥𝑥Singleton𝑦) ↔ ∃𝑥(𝑥 = (𝐴 “ {𝐵}) ∧ 𝑦 = {𝑥}))
4816imaex 7371 . . . . . . . . . . . 12 (𝐴 “ {𝐵}) ∈ V
49 sneq 4409 . . . . . . . . . . . . 13 (𝑥 = (𝐴 “ {𝐵}) → {𝑥} = {(𝐴 “ {𝐵})})
5049eqeq2d 2835 . . . . . . . . . . . 12 (𝑥 = (𝐴 “ {𝐵}) → (𝑦 = {𝑥} ↔ 𝑦 = {(𝐴 “ {𝐵})}))
5148, 50ceqsexv 3459 . . . . . . . . . . 11 (∃𝑥(𝑥 = (𝐴 “ {𝐵}) ∧ 𝑦 = {𝑥}) ↔ 𝑦 = {(𝐴 “ {𝐵})})
5247, 51bitri 267 . . . . . . . . . 10 (∃𝑥(⟨𝐴, {𝐵}⟩Img𝑥𝑥Singleton𝑦) ↔ 𝑦 = {(𝐴 “ {𝐵})})
5342, 43, 523bitri 289 . . . . . . . . 9 (∃𝑧(𝑧 = ⟨𝐴, {𝐵}⟩ ∧ 𝑧(Singleton ∘ Img)𝑦) ↔ 𝑦 = {(𝐴 “ {𝐵})})
5415, 39, 533bitri 289 . . . . . . . 8 (⟨𝐴, 𝐵⟩((Singleton ∘ Img) ∘ pprod( I , Singleton))𝑦𝑦 = {(𝐴 “ {𝐵})})
55 eqid 2825 . . . . . . . . 9 ((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V))) = ((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V)))
56 brxp 5392 . . . . . . . . . 10 (𝑦(V × V)𝑥 ↔ (𝑦 ∈ V ∧ 𝑥 ∈ V))
5714, 12, 56mpbir2an 702 . . . . . . . . 9 𝑦(V × V)𝑥
58 epel 5260 . . . . . . . . . . 11 (𝑧 E 𝑦𝑧𝑦)
5958anbi1ci 619 . . . . . . . . . 10 ((𝑧 Singletons 𝑧 E 𝑦) ↔ (𝑧𝑦𝑧 Singletons ))
6014brresi 5642 . . . . . . . . . 10 (𝑧( E ↾ Singletons )𝑦 ↔ (𝑧 Singletons 𝑧 E 𝑦))
61 elin 4025 . . . . . . . . . 10 (𝑧 ∈ (𝑦 Singletons ) ↔ (𝑧𝑦𝑧 Singletons ))
6259, 60, 613bitr4ri 296 . . . . . . . . 9 (𝑧 ∈ (𝑦 Singletons ) ↔ 𝑧( E ↾ Singletons )𝑦)
6314, 12, 55, 57, 62brtxpsd3 32537 . . . . . . . 8 (𝑦((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V)))𝑥𝑥 = (𝑦 Singletons ))
6454, 63anbi12i 620 . . . . . . 7 ((⟨𝐴, 𝐵⟩((Singleton ∘ Img) ∘ pprod( I , Singleton))𝑦𝑦((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V)))𝑥) ↔ (𝑦 = {(𝐴 “ {𝐵})} ∧ 𝑥 = (𝑦 Singletons )))
6564exbii 1947 . . . . . 6 (∃𝑦(⟨𝐴, 𝐵⟩((Singleton ∘ Img) ∘ pprod( I , Singleton))𝑦𝑦((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V)))𝑥) ↔ ∃𝑦(𝑦 = {(𝐴 “ {𝐵})} ∧ 𝑥 = (𝑦 Singletons )))
66 ineq1 4036 . . . . . . . 8 (𝑦 = {(𝐴 “ {𝐵})} → (𝑦 Singletons ) = ({(𝐴 “ {𝐵})} ∩ Singletons ))
6766eqeq2d 2835 . . . . . . 7 (𝑦 = {(𝐴 “ {𝐵})} → (𝑥 = (𝑦 Singletons ) ↔ 𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons )))
681, 67ceqsexv 3459 . . . . . 6 (∃𝑦(𝑦 = {(𝐴 “ {𝐵})} ∧ 𝑥 = (𝑦 Singletons )) ↔ 𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons ))
6913, 65, 683bitri 289 . . . . 5 (⟨𝐴, 𝐵⟩(((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V))) ∘ ((Singleton ∘ Img) ∘ pprod( I , Singleton)))𝑥𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons ))
7012, 10brco 5529 . . . . . 6 (𝑥( Bigcup Bigcup )𝐶 ↔ ∃𝑦(𝑥 Bigcup 𝑦𝑦 Bigcup 𝐶))
7114brbigcup 32539 . . . . . . . . 9 (𝑥 Bigcup 𝑦 𝑥 = 𝑦)
72 eqcom 2832 . . . . . . . . 9 ( 𝑥 = 𝑦𝑦 = 𝑥)
7371, 72bitri 267 . . . . . . . 8 (𝑥 Bigcup 𝑦𝑦 = 𝑥)
7410brbigcup 32539 . . . . . . . . 9 (𝑦 Bigcup 𝐶 𝑦 = 𝐶)
75 eqcom 2832 . . . . . . . . 9 ( 𝑦 = 𝐶𝐶 = 𝑦)
7674, 75bitri 267 . . . . . . . 8 (𝑦 Bigcup 𝐶𝐶 = 𝑦)
7773, 76anbi12i 620 . . . . . . 7 ((𝑥 Bigcup 𝑦𝑦 Bigcup 𝐶) ↔ (𝑦 = 𝑥𝐶 = 𝑦))
7877exbii 1947 . . . . . 6 (∃𝑦(𝑥 Bigcup 𝑦𝑦 Bigcup 𝐶) ↔ ∃𝑦(𝑦 = 𝑥𝐶 = 𝑦))
79 vuniex 7219 . . . . . . 7 𝑥 ∈ V
80 unieq 4668 . . . . . . . 8 (𝑦 = 𝑥 𝑦 = 𝑥)
8180eqeq2d 2835 . . . . . . 7 (𝑦 = 𝑥 → (𝐶 = 𝑦𝐶 = 𝑥))
8279, 81ceqsexv 3459 . . . . . 6 (∃𝑦(𝑦 = 𝑥𝐶 = 𝑦) ↔ 𝐶 = 𝑥)
8370, 78, 823bitri 289 . . . . 5 (𝑥( Bigcup Bigcup )𝐶𝐶 = 𝑥)
8469, 83anbi12i 620 . . . 4 ((⟨𝐴, 𝐵⟩(((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V))) ∘ ((Singleton ∘ Img) ∘ pprod( I , Singleton)))𝑥𝑥( Bigcup Bigcup )𝐶) ↔ (𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons ) ∧ 𝐶 = 𝑥))
8584exbii 1947 . . 3 (∃𝑥(⟨𝐴, 𝐵⟩(((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V))) ∘ ((Singleton ∘ Img) ∘ pprod( I , Singleton)))𝑥𝑥( Bigcup Bigcup )𝐶) ↔ ∃𝑥(𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons ) ∧ 𝐶 = 𝑥))
868, 11, 853bitri 289 . 2 (⟨𝐴, 𝐵⟩Apply𝐶 ↔ ∃𝑥(𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons ) ∧ 𝐶 = 𝑥))
87 dffv5 32565 . . 3 (𝐴𝐵) = ({(𝐴 “ {𝐵})} ∩ Singletons )
8887eqeq2i 2837 . 2 (𝐶 = (𝐴𝐵) ↔ 𝐶 = ({(𝐴 “ {𝐵})} ∩ Singletons ))
896, 86, 883bitr4i 295 1 (⟨𝐴, 𝐵⟩Apply𝐶𝐶 = (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 198  wa 386  w3a 1111   = wceq 1656  wex 1878  wcel 2164  Vcvv 3414  cdif 3795  cin 3797  csymdif 4071  {csn 4399  cop 4405   cuni 4660   class class class wbr 4875   I cid 5251   E cep 5256   × cxp 5344  ran crn 5347  cres 5348  cima 5349  ccom 5350  cfv 6127  ctxp 32471  pprodcpprod 32472   Bigcup cbigcup 32475  Singletoncsingle 32479   Singletons csingles 32480  Imgcimg 32483  Applycapply 32486
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-sep 5007  ax-nul 5015  ax-pow 5067  ax-pr 5129  ax-un 7214
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-ral 3122  df-rex 3123  df-rab 3126  df-v 3416  df-sbc 3663  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-symdif 4072  df-nul 4147  df-if 4309  df-pw 4382  df-sn 4400  df-pr 4402  df-op 4406  df-uni 4661  df-br 4876  df-opab 4938  df-mpt 4955  df-id 5252  df-eprel 5257  df-xp 5352  df-rel 5353  df-cnv 5354  df-co 5355  df-dm 5356  df-rn 5357  df-res 5358  df-ima 5359  df-iota 6090  df-fun 6129  df-fn 6130  df-f 6131  df-fo 6133  df-fv 6135  df-1st 7433  df-2nd 7434  df-txp 32495  df-pprod 32496  df-bigcup 32499  df-singleton 32503  df-singles 32504  df-image 32505  df-cart 32506  df-img 32507  df-apply 32514
This theorem is referenced by:  dfrecs2  32591  dfrdg4  32592
  Copyright terms: Public domain W3C validator