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 33297
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 5323 . . . 4 {(𝐴 “ {𝐵})} ∈ V
21inex1 5213 . . 3 ({(𝐴 “ {𝐵})} ∩ Singletons ) ∈ V
3 unieq 4840 . . . . 5 (𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons ) → 𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons ))
43unieqd 4842 . . . 4 (𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons ) → 𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons ))
54eqeq2d 2832 . . 3 (𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons ) → (𝐶 = 𝑥𝐶 = ({(𝐴 “ {𝐵})} ∩ Singletons )))
62, 5ceqsexv 3542 . 2 (∃𝑥(𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons ) ∧ 𝐶 = 𝑥) ↔ 𝐶 = ({(𝐴 “ {𝐵})} ∩ Singletons ))
7 df-apply 33232 . . . 4 Apply = (( Bigcup Bigcup ) ∘ (((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V))) ∘ ((Singleton ∘ Img) ∘ pprod( I , Singleton))))
87breqi 5064 . . 3 (⟨𝐴, 𝐵⟩Apply𝐶 ↔ ⟨𝐴, 𝐵⟩(( Bigcup Bigcup ) ∘ (((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V))) ∘ ((Singleton ∘ Img) ∘ pprod( I , Singleton))))𝐶)
9 opex 5348 . . . 4 𝐴, 𝐵⟩ ∈ V
10 brapply.3 . . . 4 𝐶 ∈ V
119, 10brco 5735 . . 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 3498 . . . . . . 7 𝑥 ∈ V
139, 12brco 5735 . . . . . 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 3498 . . . . . . . . . 10 𝑦 ∈ V
159, 14brco 5735 . . . . . . . . 9 (⟨𝐴, 𝐵⟩((Singleton ∘ Img) ∘ pprod( I , Singleton))𝑦 ↔ ∃𝑧(⟨𝐴, 𝐵⟩pprod( I , Singleton)𝑧𝑧(Singleton ∘ Img)𝑦))
16 brapply.1 . . . . . . . . . . . . 13 𝐴 ∈ V
17 brapply.2 . . . . . . . . . . . . 13 𝐵 ∈ V
18 vex 3498 . . . . . . . . . . . . 13 𝑧 ∈ V
1916, 17, 18brpprod3a 33245 . . . . . . . . . . . 12 (⟨𝐴, 𝐵⟩pprod( I , Singleton)𝑧 ↔ ∃𝑎𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝐴 I 𝑎𝐵Singleton𝑏))
20 3anrot 1092 . . . . . . . . . . . . . 14 ((𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝐴 I 𝑎𝐵Singleton𝑏) ↔ (𝐴 I 𝑎𝐵Singleton𝑏𝑧 = ⟨𝑎, 𝑏⟩))
21 vex 3498 . . . . . . . . . . . . . . . . 17 𝑎 ∈ V
2221ideq 5717 . . . . . . . . . . . . . . . 16 (𝐴 I 𝑎𝐴 = 𝑎)
23 eqcom 2828 . . . . . . . . . . . . . . . 16 (𝐴 = 𝑎𝑎 = 𝐴)
2422, 23bitri 276 . . . . . . . . . . . . . . 15 (𝐴 I 𝑎𝑎 = 𝐴)
25 vex 3498 . . . . . . . . . . . . . . . 16 𝑏 ∈ V
2617, 25brsingle 33276 . . . . . . . . . . . . . . 15 (𝐵Singleton𝑏𝑏 = {𝐵})
27 biid 262 . . . . . . . . . . . . . . 15 (𝑧 = ⟨𝑎, 𝑏⟩ ↔ 𝑧 = ⟨𝑎, 𝑏⟩)
2824, 26, 273anbi123i 1147 . . . . . . . . . . . . . 14 ((𝐴 I 𝑎𝐵Singleton𝑏𝑧 = ⟨𝑎, 𝑏⟩) ↔ (𝑎 = 𝐴𝑏 = {𝐵} ∧ 𝑧 = ⟨𝑎, 𝑏⟩))
2920, 28bitri 276 . . . . . . . . . . . . 13 ((𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝐴 I 𝑎𝐵Singleton𝑏) ↔ (𝑎 = 𝐴𝑏 = {𝐵} ∧ 𝑧 = ⟨𝑎, 𝑏⟩))
30292exbii 1840 . . . . . . . . . . . 12 (∃𝑎𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝐴 I 𝑎𝐵Singleton𝑏) ↔ ∃𝑎𝑏(𝑎 = 𝐴𝑏 = {𝐵} ∧ 𝑧 = ⟨𝑎, 𝑏⟩))
31 snex 5323 . . . . . . . . . . . . 13 {𝐵} ∈ V
32 opeq1 4797 . . . . . . . . . . . . . 14 (𝑎 = 𝐴 → ⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝑏⟩)
3332eqeq2d 2832 . . . . . . . . . . . . 13 (𝑎 = 𝐴 → (𝑧 = ⟨𝑎, 𝑏⟩ ↔ 𝑧 = ⟨𝐴, 𝑏⟩))
34 opeq2 4798 . . . . . . . . . . . . . 14 (𝑏 = {𝐵} → ⟨𝐴, 𝑏⟩ = ⟨𝐴, {𝐵}⟩)
3534eqeq2d 2832 . . . . . . . . . . . . 13 (𝑏 = {𝐵} → (𝑧 = ⟨𝐴, 𝑏⟩ ↔ 𝑧 = ⟨𝐴, {𝐵}⟩))
3616, 31, 33, 35ceqsex2v 3545 . . . . . . . . . . . 12 (∃𝑎𝑏(𝑎 = 𝐴𝑏 = {𝐵} ∧ 𝑧 = ⟨𝑎, 𝑏⟩) ↔ 𝑧 = ⟨𝐴, {𝐵}⟩)
3719, 30, 363bitri 298 . . . . . . . . . . 11 (⟨𝐴, 𝐵⟩pprod( I , Singleton)𝑧𝑧 = ⟨𝐴, {𝐵}⟩)
3837anbi1i 623 . . . . . . . . . 10 ((⟨𝐴, 𝐵⟩pprod( I , Singleton)𝑧𝑧(Singleton ∘ Img)𝑦) ↔ (𝑧 = ⟨𝐴, {𝐵}⟩ ∧ 𝑧(Singleton ∘ Img)𝑦))
3938exbii 1839 . . . . . . . . 9 (∃𝑧(⟨𝐴, 𝐵⟩pprod( I , Singleton)𝑧𝑧(Singleton ∘ Img)𝑦) ↔ ∃𝑧(𝑧 = ⟨𝐴, {𝐵}⟩ ∧ 𝑧(Singleton ∘ Img)𝑦))
40 opex 5348 . . . . . . . . . . 11 𝐴, {𝐵}⟩ ∈ V
41 breq1 5061 . . . . . . . . . . 11 (𝑧 = ⟨𝐴, {𝐵}⟩ → (𝑧(Singleton ∘ Img)𝑦 ↔ ⟨𝐴, {𝐵}⟩(Singleton ∘ Img)𝑦))
4240, 41ceqsexv 3542 . . . . . . . . . 10 (∃𝑧(𝑧 = ⟨𝐴, {𝐵}⟩ ∧ 𝑧(Singleton ∘ Img)𝑦) ↔ ⟨𝐴, {𝐵}⟩(Singleton ∘ Img)𝑦)
4340, 14brco 5735 . . . . . . . . . 10 (⟨𝐴, {𝐵}⟩(Singleton ∘ Img)𝑦 ↔ ∃𝑥(⟨𝐴, {𝐵}⟩Img𝑥𝑥Singleton𝑦))
4416, 31, 12brimg 33296 . . . . . . . . . . . . 13 (⟨𝐴, {𝐵}⟩Img𝑥𝑥 = (𝐴 “ {𝐵}))
4512, 14brsingle 33276 . . . . . . . . . . . . 13 (𝑥Singleton𝑦𝑦 = {𝑥})
4644, 45anbi12i 626 . . . . . . . . . . . 12 ((⟨𝐴, {𝐵}⟩Img𝑥𝑥Singleton𝑦) ↔ (𝑥 = (𝐴 “ {𝐵}) ∧ 𝑦 = {𝑥}))
4746exbii 1839 . . . . . . . . . . 11 (∃𝑥(⟨𝐴, {𝐵}⟩Img𝑥𝑥Singleton𝑦) ↔ ∃𝑥(𝑥 = (𝐴 “ {𝐵}) ∧ 𝑦 = {𝑥}))
4816imaex 7609 . . . . . . . . . . . 12 (𝐴 “ {𝐵}) ∈ V
49 sneq 4569 . . . . . . . . . . . . 13 (𝑥 = (𝐴 “ {𝐵}) → {𝑥} = {(𝐴 “ {𝐵})})
5049eqeq2d 2832 . . . . . . . . . . . 12 (𝑥 = (𝐴 “ {𝐵}) → (𝑦 = {𝑥} ↔ 𝑦 = {(𝐴 “ {𝐵})}))
5148, 50ceqsexv 3542 . . . . . . . . . . 11 (∃𝑥(𝑥 = (𝐴 “ {𝐵}) ∧ 𝑦 = {𝑥}) ↔ 𝑦 = {(𝐴 “ {𝐵})})
5247, 51bitri 276 . . . . . . . . . 10 (∃𝑥(⟨𝐴, {𝐵}⟩Img𝑥𝑥Singleton𝑦) ↔ 𝑦 = {(𝐴 “ {𝐵})})
5342, 43, 523bitri 298 . . . . . . . . 9 (∃𝑧(𝑧 = ⟨𝐴, {𝐵}⟩ ∧ 𝑧(Singleton ∘ Img)𝑦) ↔ 𝑦 = {(𝐴 “ {𝐵})})
5415, 39, 533bitri 298 . . . . . . . 8 (⟨𝐴, 𝐵⟩((Singleton ∘ Img) ∘ pprod( I , Singleton))𝑦𝑦 = {(𝐴 “ {𝐵})})
55 eqid 2821 . . . . . . . . 9 ((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V))) = ((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V)))
56 brxp 5595 . . . . . . . . . 10 (𝑦(V × V)𝑥 ↔ (𝑦 ∈ V ∧ 𝑥 ∈ V))
5714, 12, 56mpbir2an 707 . . . . . . . . 9 𝑦(V × V)𝑥
58 epel 5463 . . . . . . . . . . 11 (𝑧 E 𝑦𝑧𝑦)
5958anbi1ci 625 . . . . . . . . . 10 ((𝑧 Singletons 𝑧 E 𝑦) ↔ (𝑧𝑦𝑧 Singletons ))
6014brresi 5856 . . . . . . . . . 10 (𝑧( E ↾ Singletons )𝑦 ↔ (𝑧 Singletons 𝑧 E 𝑦))
61 elin 4168 . . . . . . . . . 10 (𝑧 ∈ (𝑦 Singletons ) ↔ (𝑧𝑦𝑧 Singletons ))
6259, 60, 613bitr4ri 305 . . . . . . . . 9 (𝑧 ∈ (𝑦 Singletons ) ↔ 𝑧( E ↾ Singletons )𝑦)
6314, 12, 55, 57, 62brtxpsd3 33255 . . . . . . . 8 (𝑦((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V)))𝑥𝑥 = (𝑦 Singletons ))
6454, 63anbi12i 626 . . . . . . 7 ((⟨𝐴, 𝐵⟩((Singleton ∘ Img) ∘ pprod( I , Singleton))𝑦𝑦((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V)))𝑥) ↔ (𝑦 = {(𝐴 “ {𝐵})} ∧ 𝑥 = (𝑦 Singletons )))
6564exbii 1839 . . . . . 6 (∃𝑦(⟨𝐴, 𝐵⟩((Singleton ∘ Img) ∘ pprod( I , Singleton))𝑦𝑦((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V)))𝑥) ↔ ∃𝑦(𝑦 = {(𝐴 “ {𝐵})} ∧ 𝑥 = (𝑦 Singletons )))
66 ineq1 4180 . . . . . . . 8 (𝑦 = {(𝐴 “ {𝐵})} → (𝑦 Singletons ) = ({(𝐴 “ {𝐵})} ∩ Singletons ))
6766eqeq2d 2832 . . . . . . 7 (𝑦 = {(𝐴 “ {𝐵})} → (𝑥 = (𝑦 Singletons ) ↔ 𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons )))
681, 67ceqsexv 3542 . . . . . 6 (∃𝑦(𝑦 = {(𝐴 “ {𝐵})} ∧ 𝑥 = (𝑦 Singletons )) ↔ 𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons ))
6913, 65, 683bitri 298 . . . . 5 (⟨𝐴, 𝐵⟩(((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V))) ∘ ((Singleton ∘ Img) ∘ pprod( I , Singleton)))𝑥𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons ))
7012, 10brco 5735 . . . . . 6 (𝑥( Bigcup Bigcup )𝐶 ↔ ∃𝑦(𝑥 Bigcup 𝑦𝑦 Bigcup 𝐶))
7114brbigcup 33257 . . . . . . . . 9 (𝑥 Bigcup 𝑦 𝑥 = 𝑦)
72 eqcom 2828 . . . . . . . . 9 ( 𝑥 = 𝑦𝑦 = 𝑥)
7371, 72bitri 276 . . . . . . . 8 (𝑥 Bigcup 𝑦𝑦 = 𝑥)
7410brbigcup 33257 . . . . . . . . 9 (𝑦 Bigcup 𝐶 𝑦 = 𝐶)
75 eqcom 2828 . . . . . . . . 9 ( 𝑦 = 𝐶𝐶 = 𝑦)
7674, 75bitri 276 . . . . . . . 8 (𝑦 Bigcup 𝐶𝐶 = 𝑦)
7773, 76anbi12i 626 . . . . . . 7 ((𝑥 Bigcup 𝑦𝑦 Bigcup 𝐶) ↔ (𝑦 = 𝑥𝐶 = 𝑦))
7877exbii 1839 . . . . . 6 (∃𝑦(𝑥 Bigcup 𝑦𝑦 Bigcup 𝐶) ↔ ∃𝑦(𝑦 = 𝑥𝐶 = 𝑦))
79 vuniex 7455 . . . . . . 7 𝑥 ∈ V
80 unieq 4840 . . . . . . . 8 (𝑦 = 𝑥 𝑦 = 𝑥)
8180eqeq2d 2832 . . . . . . 7 (𝑦 = 𝑥 → (𝐶 = 𝑦𝐶 = 𝑥))
8279, 81ceqsexv 3542 . . . . . 6 (∃𝑦(𝑦 = 𝑥𝐶 = 𝑦) ↔ 𝐶 = 𝑥)
8370, 78, 823bitri 298 . . . . 5 (𝑥( Bigcup Bigcup )𝐶𝐶 = 𝑥)
8469, 83anbi12i 626 . . . 4 ((⟨𝐴, 𝐵⟩(((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V))) ∘ ((Singleton ∘ Img) ∘ pprod( I , Singleton)))𝑥𝑥( Bigcup Bigcup )𝐶) ↔ (𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons ) ∧ 𝐶 = 𝑥))
8584exbii 1839 . . 3 (∃𝑥(⟨𝐴, 𝐵⟩(((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V))) ∘ ((Singleton ∘ Img) ∘ pprod( I , Singleton)))𝑥𝑥( Bigcup Bigcup )𝐶) ↔ ∃𝑥(𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons ) ∧ 𝐶 = 𝑥))
868, 11, 853bitri 298 . 2 (⟨𝐴, 𝐵⟩Apply𝐶 ↔ ∃𝑥(𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons ) ∧ 𝐶 = 𝑥))
87 dffv5 33283 . . 3 (𝐴𝐵) = ({(𝐴 “ {𝐵})} ∩ Singletons )
8887eqeq2i 2834 . 2 (𝐶 = (𝐴𝐵) ↔ 𝐶 = ({(𝐴 “ {𝐵})} ∩ Singletons ))
896, 86, 883bitr4i 304 1 (⟨𝐴, 𝐵⟩Apply𝐶𝐶 = (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 207  wa 396  w3a 1079   = wceq 1528  wex 1771  wcel 2105  Vcvv 3495  cdif 3932  cin 3934  csymdif 4217  {csn 4559  cop 4565   cuni 4832   class class class wbr 5058   I cid 5453   E cep 5458   × cxp 5547  ran crn 5550  cres 5551  cima 5552  ccom 5553  cfv 6349  ctxp 33189  pprodcpprod 33190   Bigcup cbigcup 33193  Singletoncsingle 33197   Singletons csingles 33198  Imgcimg 33201  Applycapply 33204
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-symdif 4218  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-eprel 5459  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-fo 6355  df-fv 6357  df-1st 7680  df-2nd 7681  df-txp 33213  df-pprod 33214  df-bigcup 33217  df-singleton 33221  df-singles 33222  df-image 33223  df-cart 33224  df-img 33225  df-apply 33232
This theorem is referenced by:  dfrecs2  33309  dfrdg4  33310
  Copyright terms: Public domain W3C validator