Metamath Proof Explorer

Theorem sprsymrelf1lem

Description: Lemma for sprsymrelf1 . (Contributed by AV, 22-Nov-2021)

Ref Expression
Assertion sprsymrelf1lem 
|- ( ( a C_ ( Pairs ` V ) /\ b C_ ( Pairs ` V ) ) -> ( { <. x , y >. | E. c e. a c = { x , y } } = { <. x , y >. | E. c e. b c = { x , y } } -> a C_ b ) )

Proof

Step Hyp Ref Expression
1 prssspr 
 |-  ( ( a C_ ( Pairs ` V ) /\ p e. a ) -> E. i e. V E. j e. V p = { i , j } )
2 1 ad4ant14 
 |-  ( ( ( ( a C_ ( Pairs ` V ) /\ b C_ ( Pairs ` V ) ) /\ { <. x , y >. | E. c e. a c = { x , y } } = { <. x , y >. | E. c e. b c = { x , y } } ) /\ p e. a ) -> E. i e. V E. j e. V p = { i , j } )
3 simpr 
 |-  ( ( ( i e. V /\ j e. V ) /\ p = { i , j } ) -> p = { i , j } )
4 3 adantr 
 |-  ( ( ( ( i e. V /\ j e. V ) /\ p = { i , j } ) /\ ( ( a C_ ( Pairs ` V ) /\ b C_ ( Pairs ` V ) ) /\ { <. x , y >. | E. c e. a c = { x , y } } = { <. x , y >. | E. c e. b c = { x , y } } ) ) -> p = { i , j } )
5 4 eleq1d 
 |-  ( ( ( ( i e. V /\ j e. V ) /\ p = { i , j } ) /\ ( ( a C_ ( Pairs ` V ) /\ b C_ ( Pairs ` V ) ) /\ { <. x , y >. | E. c e. a c = { x , y } } = { <. x , y >. | E. c e. b c = { x , y } } ) ) -> ( p e. a <-> { i , j } e. a ) )
6 simpr 
 |-  ( ( ( ( i e. V /\ j e. V ) /\ p = { i , j } ) /\ { i , j } e. a ) -> { i , j } e. a )
7 eqeq1 
 |-  ( c = { i , j } -> ( c = { i , j } <-> { i , j } = { i , j } ) )
8 7 adantl 
 |-  ( ( ( ( ( i e. V /\ j e. V ) /\ p = { i , j } ) /\ { i , j } e. a ) /\ c = { i , j } ) -> ( c = { i , j } <-> { i , j } = { i , j } ) )
9 eqidd 
 |-  ( ( ( ( i e. V /\ j e. V ) /\ p = { i , j } ) /\ { i , j } e. a ) -> { i , j } = { i , j } )
10 6 8 9 rspcedvd 
 |-  ( ( ( ( i e. V /\ j e. V ) /\ p = { i , j } ) /\ { i , j } e. a ) -> E. c e. a c = { i , j } )
11 10 adantlr 
 |-  ( ( ( ( ( i e. V /\ j e. V ) /\ p = { i , j } ) /\ ( ( a C_ ( Pairs ` V ) /\ b C_ ( Pairs ` V ) ) /\ { <. x , y >. | E. c e. a c = { x , y } } = { <. x , y >. | E. c e. b c = { x , y } } ) ) /\ { i , j } e. a ) -> E. c e. a c = { i , j } )
12 preq12 
 |-  ( ( x = i /\ y = j ) -> { x , y } = { i , j } )
13 12 eqeq2d 
 |-  ( ( x = i /\ y = j ) -> ( c = { x , y } <-> c = { i , j } ) )
14 13 rexbidv 
 |-  ( ( x = i /\ y = j ) -> ( E. c e. a c = { x , y } <-> E. c e. a c = { i , j } ) )
15 14 opelopabga 
 |-  ( ( i e. V /\ j e. V ) -> ( <. i , j >. e. { <. x , y >. | E. c e. a c = { x , y } } <-> E. c e. a c = { i , j } ) )
16 15 bicomd 
 |-  ( ( i e. V /\ j e. V ) -> ( E. c e. a c = { i , j } <-> <. i , j >. e. { <. x , y >. | E. c e. a c = { x , y } } ) )
17 16 ad3antrrr 
 |-  ( ( ( ( ( i e. V /\ j e. V ) /\ p = { i , j } ) /\ ( ( a C_ ( Pairs ` V ) /\ b C_ ( Pairs ` V ) ) /\ { <. x , y >. | E. c e. a c = { x , y } } = { <. x , y >. | E. c e. b c = { x , y } } ) ) /\ { i , j } e. a ) -> ( E. c e. a c = { i , j } <-> <. i , j >. e. { <. x , y >. | E. c e. a c = { x , y } } ) )
18 11 17 mpbid 
 |-  ( ( ( ( ( i e. V /\ j e. V ) /\ p = { i , j } ) /\ ( ( a C_ ( Pairs ` V ) /\ b C_ ( Pairs ` V ) ) /\ { <. x , y >. | E. c e. a c = { x , y } } = { <. x , y >. | E. c e. b c = { x , y } } ) ) /\ { i , j } e. a ) -> <. i , j >. e. { <. x , y >. | E. c e. a c = { x , y } } )
19 18 ex 
 |-  ( ( ( ( i e. V /\ j e. V ) /\ p = { i , j } ) /\ ( ( a C_ ( Pairs ` V ) /\ b C_ ( Pairs ` V ) ) /\ { <. x , y >. | E. c e. a c = { x , y } } = { <. x , y >. | E. c e. b c = { x , y } } ) ) -> ( { i , j } e. a -> <. i , j >. e. { <. x , y >. | E. c e. a c = { x , y } } ) )
20 5 19 sylbid 
 |-  ( ( ( ( i e. V /\ j e. V ) /\ p = { i , j } ) /\ ( ( a C_ ( Pairs ` V ) /\ b C_ ( Pairs ` V ) ) /\ { <. x , y >. | E. c e. a c = { x , y } } = { <. x , y >. | E. c e. b c = { x , y } } ) ) -> ( p e. a -> <. i , j >. e. { <. x , y >. | E. c e. a c = { x , y } } ) )
21 eleq2 
 |-  ( { <. x , y >. | E. c e. a c = { x , y } } = { <. x , y >. | E. c e. b c = { x , y } } -> ( <. i , j >. e. { <. x , y >. | E. c e. a c = { x , y } } <-> <. i , j >. e. { <. x , y >. | E. c e. b c = { x , y } } ) )
22 21 ad2antll 
 |-  ( ( ( ( i e. V /\ j e. V ) /\ p = { i , j } ) /\ ( ( a C_ ( Pairs ` V ) /\ b C_ ( Pairs ` V ) ) /\ { <. x , y >. | E. c e. a c = { x , y } } = { <. x , y >. | E. c e. b c = { x , y } } ) ) -> ( <. i , j >. e. { <. x , y >. | E. c e. a c = { x , y } } <-> <. i , j >. e. { <. x , y >. | E. c e. b c = { x , y } } ) )
23 13 rexbidv 
 |-  ( ( x = i /\ y = j ) -> ( E. c e. b c = { x , y } <-> E. c e. b c = { i , j } ) )
24 23 opelopabga 
 |-  ( ( i e. _V /\ j e. _V ) -> ( <. i , j >. e. { <. x , y >. | E. c e. b c = { x , y } } <-> E. c e. b c = { i , j } ) )
25 24 el2v 
 |-  ( <. i , j >. e. { <. x , y >. | E. c e. b c = { x , y } } <-> E. c e. b c = { i , j } )
26 eqtr3 
 |-  ( ( p = { i , j } /\ c = { i , j } ) -> p = c )
27 26 equcomd 
 |-  ( ( p = { i , j } /\ c = { i , j } ) -> c = p )
28 27 eleq1d 
 |-  ( ( p = { i , j } /\ c = { i , j } ) -> ( c e. b <-> p e. b ) )
29 28 biimpd 
 |-  ( ( p = { i , j } /\ c = { i , j } ) -> ( c e. b -> p e. b ) )
30 29 ex 
 |-  ( p = { i , j } -> ( c = { i , j } -> ( c e. b -> p e. b ) ) )
31 30 com13 
 |-  ( c e. b -> ( c = { i , j } -> ( p = { i , j } -> p e. b ) ) )
32 31 imp 
 |-  ( ( c e. b /\ c = { i , j } ) -> ( p = { i , j } -> p e. b ) )
33 32 rexlimiva 
 |-  ( E. c e. b c = { i , j } -> ( p = { i , j } -> p e. b ) )
34 33 com12 
 |-  ( p = { i , j } -> ( E. c e. b c = { i , j } -> p e. b ) )
35 34 adantl 
 |-  ( ( ( i e. V /\ j e. V ) /\ p = { i , j } ) -> ( E. c e. b c = { i , j } -> p e. b ) )
36 35 adantr 
 |-  ( ( ( ( i e. V /\ j e. V ) /\ p = { i , j } ) /\ ( ( a C_ ( Pairs ` V ) /\ b C_ ( Pairs ` V ) ) /\ { <. x , y >. | E. c e. a c = { x , y } } = { <. x , y >. | E. c e. b c = { x , y } } ) ) -> ( E. c e. b c = { i , j } -> p e. b ) )
37 25 36 biimtrid 
 |-  ( ( ( ( i e. V /\ j e. V ) /\ p = { i , j } ) /\ ( ( a C_ ( Pairs ` V ) /\ b C_ ( Pairs ` V ) ) /\ { <. x , y >. | E. c e. a c = { x , y } } = { <. x , y >. | E. c e. b c = { x , y } } ) ) -> ( <. i , j >. e. { <. x , y >. | E. c e. b c = { x , y } } -> p e. b ) )
38 22 37 sylbid 
 |-  ( ( ( ( i e. V /\ j e. V ) /\ p = { i , j } ) /\ ( ( a C_ ( Pairs ` V ) /\ b C_ ( Pairs ` V ) ) /\ { <. x , y >. | E. c e. a c = { x , y } } = { <. x , y >. | E. c e. b c = { x , y } } ) ) -> ( <. i , j >. e. { <. x , y >. | E. c e. a c = { x , y } } -> p e. b ) )
39 20 38 syld 
 |-  ( ( ( ( i e. V /\ j e. V ) /\ p = { i , j } ) /\ ( ( a C_ ( Pairs ` V ) /\ b C_ ( Pairs ` V ) ) /\ { <. x , y >. | E. c e. a c = { x , y } } = { <. x , y >. | E. c e. b c = { x , y } } ) ) -> ( p e. a -> p e. b ) )
40 39 expimpd 
 |-  ( ( ( i e. V /\ j e. V ) /\ p = { i , j } ) -> ( ( ( ( a C_ ( Pairs ` V ) /\ b C_ ( Pairs ` V ) ) /\ { <. x , y >. | E. c e. a c = { x , y } } = { <. x , y >. | E. c e. b c = { x , y } } ) /\ p e. a ) -> p e. b ) )
41 40 rexlimdva2 
 |-  ( i e. V -> ( E. j e. V p = { i , j } -> ( ( ( ( a C_ ( Pairs ` V ) /\ b C_ ( Pairs ` V ) ) /\ { <. x , y >. | E. c e. a c = { x , y } } = { <. x , y >. | E. c e. b c = { x , y } } ) /\ p e. a ) -> p e. b ) ) )
42 41 rexlimiv 
 |-  ( E. i e. V E. j e. V p = { i , j } -> ( ( ( ( a C_ ( Pairs ` V ) /\ b C_ ( Pairs ` V ) ) /\ { <. x , y >. | E. c e. a c = { x , y } } = { <. x , y >. | E. c e. b c = { x , y } } ) /\ p e. a ) -> p e. b ) )
43 2 42 mpcom 
 |-  ( ( ( ( a C_ ( Pairs ` V ) /\ b C_ ( Pairs ` V ) ) /\ { <. x , y >. | E. c e. a c = { x , y } } = { <. x , y >. | E. c e. b c = { x , y } } ) /\ p e. a ) -> p e. b )
44 43 ex 
 |-  ( ( ( a C_ ( Pairs ` V ) /\ b C_ ( Pairs ` V ) ) /\ { <. x , y >. | E. c e. a c = { x , y } } = { <. x , y >. | E. c e. b c = { x , y } } ) -> ( p e. a -> p e. b ) )
45 44 ssrdv 
 |-  ( ( ( a C_ ( Pairs ` V ) /\ b C_ ( Pairs ` V ) ) /\ { <. x , y >. | E. c e. a c = { x , y } } = { <. x , y >. | E. c e. b c = { x , y } } ) -> a C_ b )
46 45 ex 
 |-  ( ( a C_ ( Pairs ` V ) /\ b C_ ( Pairs ` V ) ) -> ( { <. x , y >. | E. c e. a c = { x , y } } = { <. x , y >. | E. c e. b c = { x , y } } -> a C_ b ) )