Metamath Proof Explorer

Theorem or2expropbilem1

Description: Lemma 1 for or2expropbi and ich2exprop . (Contributed by AV, 16-Jul-2023)

Ref Expression
Assertion or2expropbilem1 
|- ( ( A e. X /\ B e. X ) -> ( ( A = a /\ B = b ) -> ( ph -> E. x E. y ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ph ) ) ) )

Proof

Step Hyp Ref Expression
1 vex 
 |-  a e. _V
2 vex 
 |-  b e. _V
3 1 2 pm3.2i 
 |-  ( a e. _V /\ b e. _V )
4 3 a1i 
 |-  ( ( A e. X /\ B e. X ) -> ( a e. _V /\ b e. _V ) )
5 4 anim1ci 
 |-  ( ( ( A e. X /\ B e. X ) /\ ph ) -> ( ph /\ ( a e. _V /\ b e. _V ) ) )
6 5 adantr 
 |-  ( ( ( ( A e. X /\ B e. X ) /\ ph ) /\ ( A = a /\ B = b ) ) -> ( ph /\ ( a e. _V /\ b e. _V ) ) )
7 sbcid 
 |-  ( [. b / b ]. [. a / a ]. ph <-> [. a / a ]. ph )
8 sbcid 
 |-  ( [. a / a ]. ph <-> ph )
9 7 8 sylbbr 
 |-  ( ph -> [. b / b ]. [. a / a ]. ph )
10 9 adantl 
 |-  ( ( ( A e. X /\ B e. X ) /\ ph ) -> [. b / b ]. [. a / a ]. ph )
11 opeq12 
 |-  ( ( A = a /\ B = b ) -> <. A , B >. = <. a , b >. )
12 10 11 anim12ci 
 |-  ( ( ( ( A e. X /\ B e. X ) /\ ph ) /\ ( A = a /\ B = b ) ) -> ( <. A , B >. = <. a , b >. /\ [. b / b ]. [. a / a ]. ph ) )
13 nfv 
 |-  F/ x ( <. A , B >. = <. a , b >. /\ [. b / b ]. [. a / a ]. ph )
14 nfv 
 |-  F/ y ( <. A , B >. = <. a , b >. /\ [. b / b ]. [. a / a ]. ph )
15 opeq12 
 |-  ( ( x = a /\ y = b ) -> <. x , y >. = <. a , b >. )
16 15 eqeq2d 
 |-  ( ( x = a /\ y = b ) -> ( <. A , B >. = <. x , y >. <-> <. A , B >. = <. a , b >. ) )
17 dfsbcq 
 |-  ( y = b -> ( [. y / b ]. [. x / a ]. ph <-> [. b / b ]. [. x / a ]. ph ) )
18 dfsbcq 
 |-  ( x = a -> ( [. x / a ]. ph <-> [. a / a ]. ph ) )
19 18 sbcbidv 
 |-  ( x = a -> ( [. b / b ]. [. x / a ]. ph <-> [. b / b ]. [. a / a ]. ph ) )
20 17 19 sylan9bbr 
 |-  ( ( x = a /\ y = b ) -> ( [. y / b ]. [. x / a ]. ph <-> [. b / b ]. [. a / a ]. ph ) )
21 16 20 anbi12d 
 |-  ( ( x = a /\ y = b ) -> ( ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ph ) <-> ( <. A , B >. = <. a , b >. /\ [. b / b ]. [. a / a ]. ph ) ) )
22 21 adantl 
 |-  ( ( ph /\ ( x = a /\ y = b ) ) -> ( ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ph ) <-> ( <. A , B >. = <. a , b >. /\ [. b / b ]. [. a / a ]. ph ) ) )
23 13 14 22 spc2ed 
 |-  ( ( ph /\ ( a e. _V /\ b e. _V ) ) -> ( ( <. A , B >. = <. a , b >. /\ [. b / b ]. [. a / a ]. ph ) -> E. x E. y ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ph ) ) )
24 6 12 23 sylc 
 |-  ( ( ( ( A e. X /\ B e. X ) /\ ph ) /\ ( A = a /\ B = b ) ) -> E. x E. y ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ph ) )
25 24 exp31 
 |-  ( ( A e. X /\ B e. X ) -> ( ph -> ( ( A = a /\ B = b ) -> E. x E. y ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ph ) ) ) )
26 25 com23 
 |-  ( ( A e. X /\ B e. X ) -> ( ( A = a /\ B = b ) -> ( ph -> E. x E. y ( <. A , B >. = <. x , y >. /\ [. y / b ]. [. x / a ]. ph ) ) ) )