Metamath Proof Explorer

Theorem bj-imdirvallem

Description: Lemma for bj-imdirval and bj-iminvval . (Contributed by BJ, 23-May-2024)

Ref Expression
Hypotheses bj-imdirvallem.1 
|- ( ph -> A e. U )
bj-imdirvallem.2 
|- ( ph -> B e. V )
bj-imdirvallem.df 
|- C = ( a e. _V , b e. _V |-> ( r e. ~P ( a X. b ) |-> { <. x , y >. | ( ( x C_ a /\ y C_ b ) /\ ps ) } ) )
Assertion bj-imdirvallem 
|- ( ph -> ( A C B ) = ( r e. ~P ( A X. B ) |-> { <. x , y >. | ( ( x C_ A /\ y C_ B ) /\ ps ) } ) )

Proof

Step Hyp Ref Expression
1 bj-imdirvallem.1 
 |-  ( ph -> A e. U )
2 bj-imdirvallem.2 
 |-  ( ph -> B e. V )
3 bj-imdirvallem.df 
 |-  C = ( a e. _V , b e. _V |-> ( r e. ~P ( a X. b ) |-> { <. x , y >. | ( ( x C_ a /\ y C_ b ) /\ ps ) } ) )
4 3 a1i 
 |-  ( ph -> C = ( a e. _V , b e. _V |-> ( r e. ~P ( a X. b ) |-> { <. x , y >. | ( ( x C_ a /\ y C_ b ) /\ ps ) } ) ) )
5 xpeq12 
 |-  ( ( a = A /\ b = B ) -> ( a X. b ) = ( A X. B ) )
6 5 pweqd 
 |-  ( ( a = A /\ b = B ) -> ~P ( a X. b ) = ~P ( A X. B ) )
7 6 adantl 
 |-  ( ( ph /\ ( a = A /\ b = B ) ) -> ~P ( a X. b ) = ~P ( A X. B ) )
8 sseq2 
 |-  ( a = A -> ( x C_ a <-> x C_ A ) )
9 sseq2 
 |-  ( b = B -> ( y C_ b <-> y C_ B ) )
10 8 9 bi2anan9 
 |-  ( ( a = A /\ b = B ) -> ( ( x C_ a /\ y C_ b ) <-> ( x C_ A /\ y C_ B ) ) )
11 10 anbi1d 
 |-  ( ( a = A /\ b = B ) -> ( ( ( x C_ a /\ y C_ b ) /\ ps ) <-> ( ( x C_ A /\ y C_ B ) /\ ps ) ) )
12 11 opabbidv 
 |-  ( ( a = A /\ b = B ) -> { <. x , y >. | ( ( x C_ a /\ y C_ b ) /\ ps ) } = { <. x , y >. | ( ( x C_ A /\ y C_ B ) /\ ps ) } )
13 12 adantl 
 |-  ( ( ph /\ ( a = A /\ b = B ) ) -> { <. x , y >. | ( ( x C_ a /\ y C_ b ) /\ ps ) } = { <. x , y >. | ( ( x C_ A /\ y C_ B ) /\ ps ) } )
14 7 13 mpteq12dv 
 |-  ( ( ph /\ ( a = A /\ b = B ) ) -> ( r e. ~P ( a X. b ) |-> { <. x , y >. | ( ( x C_ a /\ y C_ b ) /\ ps ) } ) = ( r e. ~P ( A X. B ) |-> { <. x , y >. | ( ( x C_ A /\ y C_ B ) /\ ps ) } ) )
15 1 elexd 
 |-  ( ph -> A e. _V )
16 2 elexd 
 |-  ( ph -> B e. _V )
17 1 2 xpexd 
 |-  ( ph -> ( A X. B ) e. _V )
18 17 pwexd 
 |-  ( ph -> ~P ( A X. B ) e. _V )
19 18 mptexd 
 |-  ( ph -> ( r e. ~P ( A X. B ) |-> { <. x , y >. | ( ( x C_ A /\ y C_ B ) /\ ps ) } ) e. _V )
20 4 14 15 16 19 ovmpod 
 |-  ( ph -> ( A C B ) = ( r e. ~P ( A X. B ) |-> { <. x , y >. | ( ( x C_ A /\ y C_ B ) /\ ps ) } ) )