Metamath Proof Explorer

Theorem coi1in

Description: Precomposition with the identity expressed as intersection. (Contributed by BJ, 16-Aug-2026)

Ref Expression
Assertion coi1in 
|- ( A o. _I ) = ( A i^i ( _V X. _V ) )

Proof

Step Hyp Ref Expression
1 19.42vv 
 |-  ( E. y E. z ( x e. A /\ ( x = <. y , z >. /\ ( y e. _V /\ z e. _V ) ) ) <-> ( x e. A /\ E. y E. z ( x = <. y , z >. /\ ( y e. _V /\ z e. _V ) ) ) )
2 vex 
 |-  t e. _V
3 2 ideq 
 |-  ( y _I t <-> y = t )
4 3 anbi1i 
 |-  ( ( y _I t /\ t A z ) <-> ( y = t /\ t A z ) )
5 equcomi 
 |-  ( y = t -> t = y )
6 5 breq1d 
 |-  ( y = t -> ( t A z <-> y A z ) )
7 6 pm5.32i 
 |-  ( ( y = t /\ t A z ) <-> ( y = t /\ y A z ) )
8 4 7 bitri 
 |-  ( ( y _I t /\ t A z ) <-> ( y = t /\ y A z ) )
9 8 exbii 
 |-  ( E. t ( y _I t /\ t A z ) <-> E. t ( y = t /\ y A z ) )
10 ax6evr 
 |-  E. t y = t
11 19.41v 
 |-  ( E. t ( y = t /\ y A z ) <-> ( E. t y = t /\ y A z ) )
12 10 11 mpbiran 
 |-  ( E. t ( y = t /\ y A z ) <-> y A z )
13 df-br 
 |-  ( y A z <-> <. y , z >. e. A )
14 9 12 13 3bitri 
 |-  ( E. t ( y _I t /\ t A z ) <-> <. y , z >. e. A )
15 eleq1 
 |-  ( x = <. y , z >. -> ( x e. A <-> <. y , z >. e. A ) )
16 14 15 bitr4id 
 |-  ( x = <. y , z >. -> ( E. t ( y _I t /\ t A z ) <-> x e. A ) )
17 16 pm5.32i 
 |-  ( ( x = <. y , z >. /\ E. t ( y _I t /\ t A z ) ) <-> ( x = <. y , z >. /\ x e. A ) )
18 17 biancomi 
 |-  ( ( x = <. y , z >. /\ E. t ( y _I t /\ t A z ) ) <-> ( x e. A /\ x = <. y , z >. ) )
19 vex 
 |-  y e. _V
20 vex 
 |-  z e. _V
21 19 20 pm3.2i 
 |-  ( y e. _V /\ z e. _V )
22 21 biantru 
 |-  ( ( x e. A /\ x = <. y , z >. ) <-> ( ( x e. A /\ x = <. y , z >. ) /\ ( y e. _V /\ z e. _V ) ) )
23 anass 
 |-  ( ( ( x e. A /\ x = <. y , z >. ) /\ ( y e. _V /\ z e. _V ) ) <-> ( x e. A /\ ( x = <. y , z >. /\ ( y e. _V /\ z e. _V ) ) ) )
24 18 22 23 3bitri 
 |-  ( ( x = <. y , z >. /\ E. t ( y _I t /\ t A z ) ) <-> ( x e. A /\ ( x = <. y , z >. /\ ( y e. _V /\ z e. _V ) ) ) )
25 24 exbii 
 |-  ( E. z ( x = <. y , z >. /\ E. t ( y _I t /\ t A z ) ) <-> E. z ( x e. A /\ ( x = <. y , z >. /\ ( y e. _V /\ z e. _V ) ) ) )
26 25 exbii 
 |-  ( E. y E. z ( x = <. y , z >. /\ E. t ( y _I t /\ t A z ) ) <-> E. y E. z ( x e. A /\ ( x = <. y , z >. /\ ( y e. _V /\ z e. _V ) ) ) )
27 elxp 
 |-  ( x e. ( _V X. _V ) <-> E. y E. z ( x = <. y , z >. /\ ( y e. _V /\ z e. _V ) ) )
28 27 anbi2i 
 |-  ( ( x e. A /\ x e. ( _V X. _V ) ) <-> ( x e. A /\ E. y E. z ( x = <. y , z >. /\ ( y e. _V /\ z e. _V ) ) ) )
29 1 26 28 3bitr4i 
 |-  ( E. y E. z ( x = <. y , z >. /\ E. t ( y _I t /\ t A z ) ) <-> ( x e. A /\ x e. ( _V X. _V ) ) )
30 elco 
 |-  ( x e. ( A o. _I ) <-> E. y E. z ( x = <. y , z >. /\ E. t ( y _I t /\ t A z ) ) )
31 elin 
 |-  ( x e. ( A i^i ( _V X. _V ) ) <-> ( x e. A /\ x e. ( _V X. _V ) ) )
32 29 30 31 3bitr4i 
 |-  ( x e. ( A o. _I ) <-> x e. ( A i^i ( _V X. _V ) ) )
33 32 eqriv 
 |-  ( A o. _I ) = ( A i^i ( _V X. _V ) )