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 35939
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 5436 . . . 4 {(𝐴 “ {𝐵})} ∈ V
21inex1 5317 . . 3 ({(𝐴 “ {𝐵})} ∩ Singletons ) ∈ V
3 unieq 4918 . . . . 5 (𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons ) → 𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons ))
43unieqd 4920 . . . 4 (𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons ) → 𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons ))
54eqeq2d 2748 . . 3 (𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons ) → (𝐶 = 𝑥𝐶 = ({(𝐴 “ {𝐵})} ∩ Singletons )))
62, 5ceqsexv 3532 . 2 (∃𝑥(𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons ) ∧ 𝐶 = 𝑥) ↔ 𝐶 = ({(𝐴 “ {𝐵})} ∩ Singletons ))
7 df-apply 35874 . . . 4 Apply = (( Bigcup Bigcup ) ∘ (((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V))) ∘ ((Singleton ∘ Img) ∘ pprod( I , Singleton))))
87breqi 5149 . . 3 (⟨𝐴, 𝐵⟩Apply𝐶 ↔ ⟨𝐴, 𝐵⟩(( Bigcup Bigcup ) ∘ (((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V))) ∘ ((Singleton ∘ Img) ∘ pprod( I , Singleton))))𝐶)
9 opex 5469 . . . 4 𝐴, 𝐵⟩ ∈ V
10 brapply.3 . . . 4 𝐶 ∈ V
119, 10brco 5881 . . 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 3484 . . . . . . 7 𝑥 ∈ V
139, 12brco 5881 . . . . . 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 3484 . . . . . . . . . 10 𝑦 ∈ V
159, 14brco 5881 . . . . . . . . 9 (⟨𝐴, 𝐵⟩((Singleton ∘ Img) ∘ pprod( I , Singleton))𝑦 ↔ ∃𝑧(⟨𝐴, 𝐵⟩pprod( I , Singleton)𝑧𝑧(Singleton ∘ Img)𝑦))
16 brapply.1 . . . . . . . . . . . . 13 𝐴 ∈ V
17 brapply.2 . . . . . . . . . . . . 13 𝐵 ∈ V
18 vex 3484 . . . . . . . . . . . . 13 𝑧 ∈ V
1916, 17, 18brpprod3a 35887 . . . . . . . . . . . 12 (⟨𝐴, 𝐵⟩pprod( I , Singleton)𝑧 ↔ ∃𝑎𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝐴 I 𝑎𝐵Singleton𝑏))
20 3anrot 1100 . . . . . . . . . . . . . 14 ((𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝐴 I 𝑎𝐵Singleton𝑏) ↔ (𝐴 I 𝑎𝐵Singleton𝑏𝑧 = ⟨𝑎, 𝑏⟩))
21 vex 3484 . . . . . . . . . . . . . . . . 17 𝑎 ∈ V
2221ideq 5863 . . . . . . . . . . . . . . . 16 (𝐴 I 𝑎𝐴 = 𝑎)
23 eqcom 2744 . . . . . . . . . . . . . . . 16 (𝐴 = 𝑎𝑎 = 𝐴)
2422, 23bitri 275 . . . . . . . . . . . . . . 15 (𝐴 I 𝑎𝑎 = 𝐴)
25 vex 3484 . . . . . . . . . . . . . . . 16 𝑏 ∈ V
2617, 25brsingle 35918 . . . . . . . . . . . . . . 15 (𝐵Singleton𝑏𝑏 = {𝐵})
27 biid 261 . . . . . . . . . . . . . . 15 (𝑧 = ⟨𝑎, 𝑏⟩ ↔ 𝑧 = ⟨𝑎, 𝑏⟩)
2824, 26, 273anbi123i 1156 . . . . . . . . . . . . . 14 ((𝐴 I 𝑎𝐵Singleton𝑏𝑧 = ⟨𝑎, 𝑏⟩) ↔ (𝑎 = 𝐴𝑏 = {𝐵} ∧ 𝑧 = ⟨𝑎, 𝑏⟩))
2920, 28bitri 275 . . . . . . . . . . . . 13 ((𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝐴 I 𝑎𝐵Singleton𝑏) ↔ (𝑎 = 𝐴𝑏 = {𝐵} ∧ 𝑧 = ⟨𝑎, 𝑏⟩))
30292exbii 1849 . . . . . . . . . . . 12 (∃𝑎𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝐴 I 𝑎𝐵Singleton𝑏) ↔ ∃𝑎𝑏(𝑎 = 𝐴𝑏 = {𝐵} ∧ 𝑧 = ⟨𝑎, 𝑏⟩))
31 snex 5436 . . . . . . . . . . . . 13 {𝐵} ∈ V
32 opeq1 4873 . . . . . . . . . . . . . 14 (𝑎 = 𝐴 → ⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝑏⟩)
3332eqeq2d 2748 . . . . . . . . . . . . 13 (𝑎 = 𝐴 → (𝑧 = ⟨𝑎, 𝑏⟩ ↔ 𝑧 = ⟨𝐴, 𝑏⟩))
34 opeq2 4874 . . . . . . . . . . . . . 14 (𝑏 = {𝐵} → ⟨𝐴, 𝑏⟩ = ⟨𝐴, {𝐵}⟩)
3534eqeq2d 2748 . . . . . . . . . . . . 13 (𝑏 = {𝐵} → (𝑧 = ⟨𝐴, 𝑏⟩ ↔ 𝑧 = ⟨𝐴, {𝐵}⟩))
3616, 31, 33, 35ceqsex2v 3536 . . . . . . . . . . . 12 (∃𝑎𝑏(𝑎 = 𝐴𝑏 = {𝐵} ∧ 𝑧 = ⟨𝑎, 𝑏⟩) ↔ 𝑧 = ⟨𝐴, {𝐵}⟩)
3719, 30, 363bitri 297 . . . . . . . . . . 11 (⟨𝐴, 𝐵⟩pprod( I , Singleton)𝑧𝑧 = ⟨𝐴, {𝐵}⟩)
3837anbi1i 624 . . . . . . . . . 10 ((⟨𝐴, 𝐵⟩pprod( I , Singleton)𝑧𝑧(Singleton ∘ Img)𝑦) ↔ (𝑧 = ⟨𝐴, {𝐵}⟩ ∧ 𝑧(Singleton ∘ Img)𝑦))
3938exbii 1848 . . . . . . . . 9 (∃𝑧(⟨𝐴, 𝐵⟩pprod( I , Singleton)𝑧𝑧(Singleton ∘ Img)𝑦) ↔ ∃𝑧(𝑧 = ⟨𝐴, {𝐵}⟩ ∧ 𝑧(Singleton ∘ Img)𝑦))
40 opex 5469 . . . . . . . . . . 11 𝐴, {𝐵}⟩ ∈ V
41 breq1 5146 . . . . . . . . . . 11 (𝑧 = ⟨𝐴, {𝐵}⟩ → (𝑧(Singleton ∘ Img)𝑦 ↔ ⟨𝐴, {𝐵}⟩(Singleton ∘ Img)𝑦))
4240, 41ceqsexv 3532 . . . . . . . . . 10 (∃𝑧(𝑧 = ⟨𝐴, {𝐵}⟩ ∧ 𝑧(Singleton ∘ Img)𝑦) ↔ ⟨𝐴, {𝐵}⟩(Singleton ∘ Img)𝑦)
4340, 14brco 5881 . . . . . . . . . 10 (⟨𝐴, {𝐵}⟩(Singleton ∘ Img)𝑦 ↔ ∃𝑥(⟨𝐴, {𝐵}⟩Img𝑥𝑥Singleton𝑦))
4416, 31, 12brimg 35938 . . . . . . . . . . . . 13 (⟨𝐴, {𝐵}⟩Img𝑥𝑥 = (𝐴 “ {𝐵}))
4512, 14brsingle 35918 . . . . . . . . . . . . 13 (𝑥Singleton𝑦𝑦 = {𝑥})
4644, 45anbi12i 628 . . . . . . . . . . . 12 ((⟨𝐴, {𝐵}⟩Img𝑥𝑥Singleton𝑦) ↔ (𝑥 = (𝐴 “ {𝐵}) ∧ 𝑦 = {𝑥}))
4746exbii 1848 . . . . . . . . . . 11 (∃𝑥(⟨𝐴, {𝐵}⟩Img𝑥𝑥Singleton𝑦) ↔ ∃𝑥(𝑥 = (𝐴 “ {𝐵}) ∧ 𝑦 = {𝑥}))
4816imaex 7936 . . . . . . . . . . . 12 (𝐴 “ {𝐵}) ∈ V
49 sneq 4636 . . . . . . . . . . . . 13 (𝑥 = (𝐴 “ {𝐵}) → {𝑥} = {(𝐴 “ {𝐵})})
5049eqeq2d 2748 . . . . . . . . . . . 12 (𝑥 = (𝐴 “ {𝐵}) → (𝑦 = {𝑥} ↔ 𝑦 = {(𝐴 “ {𝐵})}))
5148, 50ceqsexv 3532 . . . . . . . . . . 11 (∃𝑥(𝑥 = (𝐴 “ {𝐵}) ∧ 𝑦 = {𝑥}) ↔ 𝑦 = {(𝐴 “ {𝐵})})
5247, 51bitri 275 . . . . . . . . . 10 (∃𝑥(⟨𝐴, {𝐵}⟩Img𝑥𝑥Singleton𝑦) ↔ 𝑦 = {(𝐴 “ {𝐵})})
5342, 43, 523bitri 297 . . . . . . . . 9 (∃𝑧(𝑧 = ⟨𝐴, {𝐵}⟩ ∧ 𝑧(Singleton ∘ Img)𝑦) ↔ 𝑦 = {(𝐴 “ {𝐵})})
5415, 39, 533bitri 297 . . . . . . . 8 (⟨𝐴, 𝐵⟩((Singleton ∘ Img) ∘ pprod( I , Singleton))𝑦𝑦 = {(𝐴 “ {𝐵})})
55 eqid 2737 . . . . . . . . 9 ((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V))) = ((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V)))
56 brxp 5734 . . . . . . . . . 10 (𝑦(V × V)𝑥 ↔ (𝑦 ∈ V ∧ 𝑥 ∈ V))
5714, 12, 56mpbir2an 711 . . . . . . . . 9 𝑦(V × V)𝑥
58 epel 5587 . . . . . . . . . . 11 (𝑧 E 𝑦𝑧𝑦)
5958anbi1ci 626 . . . . . . . . . 10 ((𝑧 Singletons 𝑧 E 𝑦) ↔ (𝑧𝑦𝑧 Singletons ))
6014brresi 6006 . . . . . . . . . 10 (𝑧( E ↾ Singletons )𝑦 ↔ (𝑧 Singletons 𝑧 E 𝑦))
61 elin 3967 . . . . . . . . . 10 (𝑧 ∈ (𝑦 Singletons ) ↔ (𝑧𝑦𝑧 Singletons ))
6259, 60, 613bitr4ri 304 . . . . . . . . 9 (𝑧 ∈ (𝑦 Singletons ) ↔ 𝑧( E ↾ Singletons )𝑦)
6314, 12, 55, 57, 62brtxpsd3 35897 . . . . . . . 8 (𝑦((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V)))𝑥𝑥 = (𝑦 Singletons ))
6454, 63anbi12i 628 . . . . . . 7 ((⟨𝐴, 𝐵⟩((Singleton ∘ Img) ∘ pprod( I , Singleton))𝑦𝑦((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V)))𝑥) ↔ (𝑦 = {(𝐴 “ {𝐵})} ∧ 𝑥 = (𝑦 Singletons )))
6564exbii 1848 . . . . . 6 (∃𝑦(⟨𝐴, 𝐵⟩((Singleton ∘ Img) ∘ pprod( I , Singleton))𝑦𝑦((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V)))𝑥) ↔ ∃𝑦(𝑦 = {(𝐴 “ {𝐵})} ∧ 𝑥 = (𝑦 Singletons )))
66 ineq1 4213 . . . . . . . 8 (𝑦 = {(𝐴 “ {𝐵})} → (𝑦 Singletons ) = ({(𝐴 “ {𝐵})} ∩ Singletons ))
6766eqeq2d 2748 . . . . . . 7 (𝑦 = {(𝐴 “ {𝐵})} → (𝑥 = (𝑦 Singletons ) ↔ 𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons )))
681, 67ceqsexv 3532 . . . . . 6 (∃𝑦(𝑦 = {(𝐴 “ {𝐵})} ∧ 𝑥 = (𝑦 Singletons )) ↔ 𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons ))
6913, 65, 683bitri 297 . . . . 5 (⟨𝐴, 𝐵⟩(((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V))) ∘ ((Singleton ∘ Img) ∘ pprod( I , Singleton)))𝑥𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons ))
7012, 10brco 5881 . . . . . 6 (𝑥( Bigcup Bigcup )𝐶 ↔ ∃𝑦(𝑥 Bigcup 𝑦𝑦 Bigcup 𝐶))
7114brbigcup 35899 . . . . . . . . 9 (𝑥 Bigcup 𝑦 𝑥 = 𝑦)
72 eqcom 2744 . . . . . . . . 9 ( 𝑥 = 𝑦𝑦 = 𝑥)
7371, 72bitri 275 . . . . . . . 8 (𝑥 Bigcup 𝑦𝑦 = 𝑥)
7410brbigcup 35899 . . . . . . . . 9 (𝑦 Bigcup 𝐶 𝑦 = 𝐶)
75 eqcom 2744 . . . . . . . . 9 ( 𝑦 = 𝐶𝐶 = 𝑦)
7674, 75bitri 275 . . . . . . . 8 (𝑦 Bigcup 𝐶𝐶 = 𝑦)
7773, 76anbi12i 628 . . . . . . 7 ((𝑥 Bigcup 𝑦𝑦 Bigcup 𝐶) ↔ (𝑦 = 𝑥𝐶 = 𝑦))
7877exbii 1848 . . . . . 6 (∃𝑦(𝑥 Bigcup 𝑦𝑦 Bigcup 𝐶) ↔ ∃𝑦(𝑦 = 𝑥𝐶 = 𝑦))
79 vuniex 7759 . . . . . . 7 𝑥 ∈ V
80 unieq 4918 . . . . . . . 8 (𝑦 = 𝑥 𝑦 = 𝑥)
8180eqeq2d 2748 . . . . . . 7 (𝑦 = 𝑥 → (𝐶 = 𝑦𝐶 = 𝑥))
8279, 81ceqsexv 3532 . . . . . 6 (∃𝑦(𝑦 = 𝑥𝐶 = 𝑦) ↔ 𝐶 = 𝑥)
8370, 78, 823bitri 297 . . . . 5 (𝑥( Bigcup Bigcup )𝐶𝐶 = 𝑥)
8469, 83anbi12i 628 . . . 4 ((⟨𝐴, 𝐵⟩(((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V))) ∘ ((Singleton ∘ Img) ∘ pprod( I , Singleton)))𝑥𝑥( Bigcup Bigcup )𝐶) ↔ (𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons ) ∧ 𝐶 = 𝑥))
8584exbii 1848 . . 3 (∃𝑥(⟨𝐴, 𝐵⟩(((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V))) ∘ ((Singleton ∘ Img) ∘ pprod( I , Singleton)))𝑥𝑥( Bigcup Bigcup )𝐶) ↔ ∃𝑥(𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons ) ∧ 𝐶 = 𝑥))
868, 11, 853bitri 297 . 2 (⟨𝐴, 𝐵⟩Apply𝐶 ↔ ∃𝑥(𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons ) ∧ 𝐶 = 𝑥))
87 dffv5 35925 . . 3 (𝐴𝐵) = ({(𝐴 “ {𝐵})} ∩ Singletons )
8887eqeq2i 2750 . 2 (𝐶 = (𝐴𝐵) ↔ 𝐶 = ({(𝐴 “ {𝐵})} ∩ Singletons ))
896, 86, 883bitr4i 303 1 (⟨𝐴, 𝐵⟩Apply𝐶𝐶 = (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395  w3a 1087   = wceq 1540  wex 1779  wcel 2108  Vcvv 3480  cdif 3948  cin 3950  csymdif 4252  {csn 4626  cop 4632   cuni 4907   class class class wbr 5143   I cid 5577   E cep 5583   × cxp 5683  ran crn 5686  cres 5687  cima 5688  ccom 5689  cfv 6561  ctxp 35831  pprodcpprod 35832   Bigcup cbigcup 35835  Singletoncsingle 35839   Singletons csingles 35840  Imgcimg 35843  Applycapply 35846
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-symdif 4253  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-eprel 5584  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-fo 6567  df-fv 6569  df-1st 8014  df-2nd 8015  df-txp 35855  df-pprod 35856  df-bigcup 35859  df-singleton 35863  df-singles 35864  df-image 35865  df-cart 35866  df-img 35867  df-apply 35874
This theorem is referenced by:  dfrecs2  35951  dfrdg4  35952
  Copyright terms: Public domain W3C validator