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 33407
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 5308 . . . 4 {(𝐴 “ {𝐵})} ∈ V
21inex1 5197 . . 3 ({(𝐴 “ {𝐵})} ∩ Singletons ) ∈ V
3 unieq 4825 . . . . 5 (𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons ) → 𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons ))
43unieqd 4828 . . . 4 (𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons ) → 𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons ))
54eqeq2d 2831 . . 3 (𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons ) → (𝐶 = 𝑥𝐶 = ({(𝐴 “ {𝐵})} ∩ Singletons )))
62, 5ceqsexv 3520 . 2 (∃𝑥(𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons ) ∧ 𝐶 = 𝑥) ↔ 𝐶 = ({(𝐴 “ {𝐵})} ∩ Singletons ))
7 df-apply 33342 . . . 4 Apply = (( Bigcup Bigcup ) ∘ (((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V))) ∘ ((Singleton ∘ Img) ∘ pprod( I , Singleton))))
87breqi 5048 . . 3 (⟨𝐴, 𝐵⟩Apply𝐶 ↔ ⟨𝐴, 𝐵⟩(( Bigcup Bigcup ) ∘ (((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V))) ∘ ((Singleton ∘ Img) ∘ pprod( I , Singleton))))𝐶)
9 opex 5332 . . . 4 𝐴, 𝐵⟩ ∈ V
10 brapply.3 . . . 4 𝐶 ∈ V
119, 10brco 5717 . . 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 3476 . . . . . . 7 𝑥 ∈ V
139, 12brco 5717 . . . . . 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 3476 . . . . . . . . . 10 𝑦 ∈ V
159, 14brco 5717 . . . . . . . . 9 (⟨𝐴, 𝐵⟩((Singleton ∘ Img) ∘ pprod( I , Singleton))𝑦 ↔ ∃𝑧(⟨𝐴, 𝐵⟩pprod( I , Singleton)𝑧𝑧(Singleton ∘ Img)𝑦))
16 brapply.1 . . . . . . . . . . . . 13 𝐴 ∈ V
17 brapply.2 . . . . . . . . . . . . 13 𝐵 ∈ V
18 vex 3476 . . . . . . . . . . . . 13 𝑧 ∈ V
1916, 17, 18brpprod3a 33355 . . . . . . . . . . . 12 (⟨𝐴, 𝐵⟩pprod( I , Singleton)𝑧 ↔ ∃𝑎𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝐴 I 𝑎𝐵Singleton𝑏))
20 3anrot 1096 . . . . . . . . . . . . . 14 ((𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝐴 I 𝑎𝐵Singleton𝑏) ↔ (𝐴 I 𝑎𝐵Singleton𝑏𝑧 = ⟨𝑎, 𝑏⟩))
21 vex 3476 . . . . . . . . . . . . . . . . 17 𝑎 ∈ V
2221ideq 5699 . . . . . . . . . . . . . . . 16 (𝐴 I 𝑎𝐴 = 𝑎)
23 eqcom 2827 . . . . . . . . . . . . . . . 16 (𝐴 = 𝑎𝑎 = 𝐴)
2422, 23bitri 277 . . . . . . . . . . . . . . 15 (𝐴 I 𝑎𝑎 = 𝐴)
25 vex 3476 . . . . . . . . . . . . . . . 16 𝑏 ∈ V
2617, 25brsingle 33386 . . . . . . . . . . . . . . 15 (𝐵Singleton𝑏𝑏 = {𝐵})
27 biid 263 . . . . . . . . . . . . . . 15 (𝑧 = ⟨𝑎, 𝑏⟩ ↔ 𝑧 = ⟨𝑎, 𝑏⟩)
2824, 26, 273anbi123i 1151 . . . . . . . . . . . . . 14 ((𝐴 I 𝑎𝐵Singleton𝑏𝑧 = ⟨𝑎, 𝑏⟩) ↔ (𝑎 = 𝐴𝑏 = {𝐵} ∧ 𝑧 = ⟨𝑎, 𝑏⟩))
2920, 28bitri 277 . . . . . . . . . . . . 13 ((𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝐴 I 𝑎𝐵Singleton𝑏) ↔ (𝑎 = 𝐴𝑏 = {𝐵} ∧ 𝑧 = ⟨𝑎, 𝑏⟩))
30292exbii 1849 . . . . . . . . . . . 12 (∃𝑎𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝐴 I 𝑎𝐵Singleton𝑏) ↔ ∃𝑎𝑏(𝑎 = 𝐴𝑏 = {𝐵} ∧ 𝑧 = ⟨𝑎, 𝑏⟩))
31 snex 5308 . . . . . . . . . . . . 13 {𝐵} ∈ V
32 opeq1 4779 . . . . . . . . . . . . . 14 (𝑎 = 𝐴 → ⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝑏⟩)
3332eqeq2d 2831 . . . . . . . . . . . . 13 (𝑎 = 𝐴 → (𝑧 = ⟨𝑎, 𝑏⟩ ↔ 𝑧 = ⟨𝐴, 𝑏⟩))
34 opeq2 4780 . . . . . . . . . . . . . 14 (𝑏 = {𝐵} → ⟨𝐴, 𝑏⟩ = ⟨𝐴, {𝐵}⟩)
3534eqeq2d 2831 . . . . . . . . . . . . 13 (𝑏 = {𝐵} → (𝑧 = ⟨𝐴, 𝑏⟩ ↔ 𝑧 = ⟨𝐴, {𝐵}⟩))
3616, 31, 33, 35ceqsex2v 3523 . . . . . . . . . . . 12 (∃𝑎𝑏(𝑎 = 𝐴𝑏 = {𝐵} ∧ 𝑧 = ⟨𝑎, 𝑏⟩) ↔ 𝑧 = ⟨𝐴, {𝐵}⟩)
3719, 30, 363bitri 299 . . . . . . . . . . 11 (⟨𝐴, 𝐵⟩pprod( I , Singleton)𝑧𝑧 = ⟨𝐴, {𝐵}⟩)
3837anbi1i 625 . . . . . . . . . 10 ((⟨𝐴, 𝐵⟩pprod( I , Singleton)𝑧𝑧(Singleton ∘ Img)𝑦) ↔ (𝑧 = ⟨𝐴, {𝐵}⟩ ∧ 𝑧(Singleton ∘ Img)𝑦))
3938exbii 1848 . . . . . . . . 9 (∃𝑧(⟨𝐴, 𝐵⟩pprod( I , Singleton)𝑧𝑧(Singleton ∘ Img)𝑦) ↔ ∃𝑧(𝑧 = ⟨𝐴, {𝐵}⟩ ∧ 𝑧(Singleton ∘ Img)𝑦))
40 opex 5332 . . . . . . . . . . 11 𝐴, {𝐵}⟩ ∈ V
41 breq1 5045 . . . . . . . . . . 11 (𝑧 = ⟨𝐴, {𝐵}⟩ → (𝑧(Singleton ∘ Img)𝑦 ↔ ⟨𝐴, {𝐵}⟩(Singleton ∘ Img)𝑦))
4240, 41ceqsexv 3520 . . . . . . . . . 10 (∃𝑧(𝑧 = ⟨𝐴, {𝐵}⟩ ∧ 𝑧(Singleton ∘ Img)𝑦) ↔ ⟨𝐴, {𝐵}⟩(Singleton ∘ Img)𝑦)
4340, 14brco 5717 . . . . . . . . . 10 (⟨𝐴, {𝐵}⟩(Singleton ∘ Img)𝑦 ↔ ∃𝑥(⟨𝐴, {𝐵}⟩Img𝑥𝑥Singleton𝑦))
4416, 31, 12brimg 33406 . . . . . . . . . . . . 13 (⟨𝐴, {𝐵}⟩Img𝑥𝑥 = (𝐴 “ {𝐵}))
4512, 14brsingle 33386 . . . . . . . . . . . . 13 (𝑥Singleton𝑦𝑦 = {𝑥})
4644, 45anbi12i 628 . . . . . . . . . . . 12 ((⟨𝐴, {𝐵}⟩Img𝑥𝑥Singleton𝑦) ↔ (𝑥 = (𝐴 “ {𝐵}) ∧ 𝑦 = {𝑥}))
4746exbii 1848 . . . . . . . . . . 11 (∃𝑥(⟨𝐴, {𝐵}⟩Img𝑥𝑥Singleton𝑦) ↔ ∃𝑥(𝑥 = (𝐴 “ {𝐵}) ∧ 𝑦 = {𝑥}))
4816imaex 7599 . . . . . . . . . . . 12 (𝐴 “ {𝐵}) ∈ V
49 sneq 4553 . . . . . . . . . . . . 13 (𝑥 = (𝐴 “ {𝐵}) → {𝑥} = {(𝐴 “ {𝐵})})
5049eqeq2d 2831 . . . . . . . . . . . 12 (𝑥 = (𝐴 “ {𝐵}) → (𝑦 = {𝑥} ↔ 𝑦 = {(𝐴 “ {𝐵})}))
5148, 50ceqsexv 3520 . . . . . . . . . . 11 (∃𝑥(𝑥 = (𝐴 “ {𝐵}) ∧ 𝑦 = {𝑥}) ↔ 𝑦 = {(𝐴 “ {𝐵})})
5247, 51bitri 277 . . . . . . . . . 10 (∃𝑥(⟨𝐴, {𝐵}⟩Img𝑥𝑥Singleton𝑦) ↔ 𝑦 = {(𝐴 “ {𝐵})})
5342, 43, 523bitri 299 . . . . . . . . 9 (∃𝑧(𝑧 = ⟨𝐴, {𝐵}⟩ ∧ 𝑧(Singleton ∘ Img)𝑦) ↔ 𝑦 = {(𝐴 “ {𝐵})})
5415, 39, 533bitri 299 . . . . . . . 8 (⟨𝐴, 𝐵⟩((Singleton ∘ Img) ∘ pprod( I , Singleton))𝑦𝑦 = {(𝐴 “ {𝐵})})
55 eqid 2820 . . . . . . . . 9 ((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V))) = ((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V)))
56 brxp 5577 . . . . . . . . . 10 (𝑦(V × V)𝑥 ↔ (𝑦 ∈ V ∧ 𝑥 ∈ V))
5714, 12, 56mpbir2an 709 . . . . . . . . 9 𝑦(V × V)𝑥
58 epel 5445 . . . . . . . . . . 11 (𝑧 E 𝑦𝑧𝑦)
5958anbi1ci 627 . . . . . . . . . 10 ((𝑧 Singletons 𝑧 E 𝑦) ↔ (𝑧𝑦𝑧 Singletons ))
6014brresi 5838 . . . . . . . . . 10 (𝑧( E ↾ Singletons )𝑦 ↔ (𝑧 Singletons 𝑧 E 𝑦))
61 elin 3929 . . . . . . . . . 10 (𝑧 ∈ (𝑦 Singletons ) ↔ (𝑧𝑦𝑧 Singletons ))
6259, 60, 613bitr4ri 306 . . . . . . . . 9 (𝑧 ∈ (𝑦 Singletons ) ↔ 𝑧( E ↾ Singletons )𝑦)
6314, 12, 55, 57, 62brtxpsd3 33365 . . . . . . . 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 4159 . . . . . . . 8 (𝑦 = {(𝐴 “ {𝐵})} → (𝑦 Singletons ) = ({(𝐴 “ {𝐵})} ∩ Singletons ))
6766eqeq2d 2831 . . . . . . 7 (𝑦 = {(𝐴 “ {𝐵})} → (𝑥 = (𝑦 Singletons ) ↔ 𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons )))
681, 67ceqsexv 3520 . . . . . 6 (∃𝑦(𝑦 = {(𝐴 “ {𝐵})} ∧ 𝑥 = (𝑦 Singletons )) ↔ 𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons ))
6913, 65, 683bitri 299 . . . . 5 (⟨𝐴, 𝐵⟩(((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V))) ∘ ((Singleton ∘ Img) ∘ pprod( I , Singleton)))𝑥𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons ))
7012, 10brco 5717 . . . . . 6 (𝑥( Bigcup Bigcup )𝐶 ↔ ∃𝑦(𝑥 Bigcup 𝑦𝑦 Bigcup 𝐶))
7114brbigcup 33367 . . . . . . . . 9 (𝑥 Bigcup 𝑦 𝑥 = 𝑦)
72 eqcom 2827 . . . . . . . . 9 ( 𝑥 = 𝑦𝑦 = 𝑥)
7371, 72bitri 277 . . . . . . . 8 (𝑥 Bigcup 𝑦𝑦 = 𝑥)
7410brbigcup 33367 . . . . . . . . 9 (𝑦 Bigcup 𝐶 𝑦 = 𝐶)
75 eqcom 2827 . . . . . . . . 9 ( 𝑦 = 𝐶𝐶 = 𝑦)
7674, 75bitri 277 . . . . . . . 8 (𝑦 Bigcup 𝐶𝐶 = 𝑦)
7773, 76anbi12i 628 . . . . . . 7 ((𝑥 Bigcup 𝑦𝑦 Bigcup 𝐶) ↔ (𝑦 = 𝑥𝐶 = 𝑦))
7877exbii 1848 . . . . . 6 (∃𝑦(𝑥 Bigcup 𝑦𝑦 Bigcup 𝐶) ↔ ∃𝑦(𝑦 = 𝑥𝐶 = 𝑦))
79 vuniex 7443 . . . . . . 7 𝑥 ∈ V
80 unieq 4825 . . . . . . . 8 (𝑦 = 𝑥 𝑦 = 𝑥)
8180eqeq2d 2831 . . . . . . 7 (𝑦 = 𝑥 → (𝐶 = 𝑦𝐶 = 𝑥))
8279, 81ceqsexv 3520 . . . . . 6 (∃𝑦(𝑦 = 𝑥𝐶 = 𝑦) ↔ 𝐶 = 𝑥)
8370, 78, 823bitri 299 . . . . 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 299 . 2 (⟨𝐴, 𝐵⟩Apply𝐶 ↔ ∃𝑥(𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons ) ∧ 𝐶 = 𝑥))
87 dffv5 33393 . . 3 (𝐴𝐵) = ({(𝐴 “ {𝐵})} ∩ Singletons )
8887eqeq2i 2833 . 2 (𝐶 = (𝐴𝐵) ↔ 𝐶 = ({(𝐴 “ {𝐵})} ∩ Singletons ))
896, 86, 883bitr4i 305 1 (⟨𝐴, 𝐵⟩Apply𝐶𝐶 = (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 208  wa 398  w3a 1083   = wceq 1537  wex 1780  wcel 2114  Vcvv 3473  cdif 3910  cin 3912  csymdif 4196  {csn 4543  cop 4549   cuni 4814   class class class wbr 5042   I cid 5435   E cep 5440   × cxp 5529  ran crn 5532  cres 5533  cima 5534  ccom 5535  cfv 6331  ctxp 33299  pprodcpprod 33300   Bigcup cbigcup 33303  Singletoncsingle 33307   Singletons csingles 33308  Imgcimg 33311  Applycapply 33314
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-sep 5179  ax-nul 5186  ax-pow 5242  ax-pr 5306  ax-un 7439
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ne 3007  df-ral 3130  df-rex 3131  df-rab 3134  df-v 3475  df-sbc 3753  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-symdif 4197  df-nul 4270  df-if 4444  df-pw 4517  df-sn 4544  df-pr 4546  df-op 4550  df-uni 4815  df-br 5043  df-opab 5105  df-mpt 5123  df-id 5436  df-eprel 5441  df-xp 5537  df-rel 5538  df-cnv 5539  df-co 5540  df-dm 5541  df-rn 5542  df-res 5543  df-ima 5544  df-iota 6290  df-fun 6333  df-fn 6334  df-f 6335  df-fo 6337  df-fv 6339  df-1st 7667  df-2nd 7668  df-txp 33323  df-pprod 33324  df-bigcup 33327  df-singleton 33331  df-singles 33332  df-image 33333  df-cart 33334  df-img 33335  df-apply 33342
This theorem is referenced by:  dfrecs2  33419  dfrdg4  33420
  Copyright terms: Public domain W3C validator