Metamath Proof Explorer

Theorem sprsymrelfvlem

Description: Lemma for sprsymrelf and sprsymrelfv . (Contributed by AV, 19-Nov-2021)

Ref Expression
Assertion sprsymrelfvlem 
|- ( P C_ ( Pairs ` V ) -> { <. x , y >. | E. c e. P c = { x , y } } e. ~P ( V X. V ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( V e. _V /\ P C_ ( Pairs ` V ) ) -> V e. _V )
2 eleq1 
 |-  ( c = { x , y } -> ( c e. P <-> { x , y } e. P ) )
3 prsssprel 
 |-  ( ( P C_ ( Pairs ` V ) /\ { x , y } e. P /\ ( x e. _V /\ y e. _V ) ) -> ( x e. V /\ y e. V ) )
4 3 3exp 
 |-  ( P C_ ( Pairs ` V ) -> ( { x , y } e. P -> ( ( x e. _V /\ y e. _V ) -> ( x e. V /\ y e. V ) ) ) )
5 4 com13 
 |-  ( ( x e. _V /\ y e. _V ) -> ( { x , y } e. P -> ( P C_ ( Pairs ` V ) -> ( x e. V /\ y e. V ) ) ) )
6 5 el2v 
 |-  ( { x , y } e. P -> ( P C_ ( Pairs ` V ) -> ( x e. V /\ y e. V ) ) )
7 2 6 syl6bi 
 |-  ( c = { x , y } -> ( c e. P -> ( P C_ ( Pairs ` V ) -> ( x e. V /\ y e. V ) ) ) )
8 7 com12 
 |-  ( c e. P -> ( c = { x , y } -> ( P C_ ( Pairs ` V ) -> ( x e. V /\ y e. V ) ) ) )
9 8 rexlimiv 
 |-  ( E. c e. P c = { x , y } -> ( P C_ ( Pairs ` V ) -> ( x e. V /\ y e. V ) ) )
10 9 com12 
 |-  ( P C_ ( Pairs ` V ) -> ( E. c e. P c = { x , y } -> ( x e. V /\ y e. V ) ) )
11 10 adantl 
 |-  ( ( V e. _V /\ P C_ ( Pairs ` V ) ) -> ( E. c e. P c = { x , y } -> ( x e. V /\ y e. V ) ) )
12 11 imp 
 |-  ( ( ( V e. _V /\ P C_ ( Pairs ` V ) ) /\ E. c e. P c = { x , y } ) -> ( x e. V /\ y e. V ) )
13 12 simpld 
 |-  ( ( ( V e. _V /\ P C_ ( Pairs ` V ) ) /\ E. c e. P c = { x , y } ) -> x e. V )
14 12 simprd 
 |-  ( ( ( V e. _V /\ P C_ ( Pairs ` V ) ) /\ E. c e. P c = { x , y } ) -> y e. V )
15 1 1 13 14 opabex2 
 |-  ( ( V e. _V /\ P C_ ( Pairs ` V ) ) -> { <. x , y >. | E. c e. P c = { x , y } } e. _V )
16 elopab 
 |-  ( p e. { <. x , y >. | E. c e. P c = { x , y } } <-> E. x E. y ( p = <. x , y >. /\ E. c e. P c = { x , y } ) )
17 9 adantl 
 |-  ( ( p = <. x , y >. /\ E. c e. P c = { x , y } ) -> ( P C_ ( Pairs ` V ) -> ( x e. V /\ y e. V ) ) )
18 17 adantld 
 |-  ( ( p = <. x , y >. /\ E. c e. P c = { x , y } ) -> ( ( V e. _V /\ P C_ ( Pairs ` V ) ) -> ( x e. V /\ y e. V ) ) )
19 18 imp 
 |-  ( ( ( p = <. x , y >. /\ E. c e. P c = { x , y } ) /\ ( V e. _V /\ P C_ ( Pairs ` V ) ) ) -> ( x e. V /\ y e. V ) )
20 eleq1 
 |-  ( p = <. x , y >. -> ( p e. ( V X. V ) <-> <. x , y >. e. ( V X. V ) ) )
21 20 ad2antrr 
 |-  ( ( ( p = <. x , y >. /\ E. c e. P c = { x , y } ) /\ ( V e. _V /\ P C_ ( Pairs ` V ) ) ) -> ( p e. ( V X. V ) <-> <. x , y >. e. ( V X. V ) ) )
22 opelxp 
 |-  ( <. x , y >. e. ( V X. V ) <-> ( x e. V /\ y e. V ) )
23 21 22 bitrdi 
 |-  ( ( ( p = <. x , y >. /\ E. c e. P c = { x , y } ) /\ ( V e. _V /\ P C_ ( Pairs ` V ) ) ) -> ( p e. ( V X. V ) <-> ( x e. V /\ y e. V ) ) )
24 19 23 mpbird 
 |-  ( ( ( p = <. x , y >. /\ E. c e. P c = { x , y } ) /\ ( V e. _V /\ P C_ ( Pairs ` V ) ) ) -> p e. ( V X. V ) )
25 24 ex 
 |-  ( ( p = <. x , y >. /\ E. c e. P c = { x , y } ) -> ( ( V e. _V /\ P C_ ( Pairs ` V ) ) -> p e. ( V X. V ) ) )
26 25 exlimivv 
 |-  ( E. x E. y ( p = <. x , y >. /\ E. c e. P c = { x , y } ) -> ( ( V e. _V /\ P C_ ( Pairs ` V ) ) -> p e. ( V X. V ) ) )
27 16 26 sylbi 
 |-  ( p e. { <. x , y >. | E. c e. P c = { x , y } } -> ( ( V e. _V /\ P C_ ( Pairs ` V ) ) -> p e. ( V X. V ) ) )
28 27 com12 
 |-  ( ( V e. _V /\ P C_ ( Pairs ` V ) ) -> ( p e. { <. x , y >. | E. c e. P c = { x , y } } -> p e. ( V X. V ) ) )
29 28 ssrdv 
 |-  ( ( V e. _V /\ P C_ ( Pairs ` V ) ) -> { <. x , y >. | E. c e. P c = { x , y } } C_ ( V X. V ) )
30 15 29 elpwd 
 |-  ( ( V e. _V /\ P C_ ( Pairs ` V ) ) -> { <. x , y >. | E. c e. P c = { x , y } } e. ~P ( V X. V ) )
31 30 ex 
 |-  ( V e. _V -> ( P C_ ( Pairs ` V ) -> { <. x , y >. | E. c e. P c = { x , y } } e. ~P ( V X. V ) ) )
32 fvprc 
 |-  ( -. V e. _V -> ( Pairs ` V ) = (/) )
33 32 sseq2d 
 |-  ( -. V e. _V -> ( P C_ ( Pairs ` V ) <-> P C_ (/) ) )
34 ss0b 
 |-  ( P C_ (/) <-> P = (/) )
35 33 34 bitrdi 
 |-  ( -. V e. _V -> ( P C_ ( Pairs ` V ) <-> P = (/) ) )
36 rex0 
 |-  -. E. c e. (/) c = { x , y }
37 rexeq 
 |-  ( P = (/) -> ( E. c e. P c = { x , y } <-> E. c e. (/) c = { x , y } ) )
38 36 37 mtbiri 
 |-  ( P = (/) -> -. E. c e. P c = { x , y } )
39 38 alrimivv 
 |-  ( P = (/) -> A. x A. y -. E. c e. P c = { x , y } )
40 opab0 
 |-  ( { <. x , y >. | E. c e. P c = { x , y } } = (/) <-> A. x A. y -. E. c e. P c = { x , y } )
41 39 40 sylibr 
 |-  ( P = (/) -> { <. x , y >. | E. c e. P c = { x , y } } = (/) )
42 0elpw 
 |-  (/) e. ~P ( V X. V )
43 41 42 eqeltrdi 
 |-  ( P = (/) -> { <. x , y >. | E. c e. P c = { x , y } } e. ~P ( V X. V ) )
44 35 43 syl6bi 
 |-  ( -. V e. _V -> ( P C_ ( Pairs ` V ) -> { <. x , y >. | E. c e. P c = { x , y } } e. ~P ( V X. V ) ) )
45 31 44 pm2.61i 
 |-  ( P C_ ( Pairs ` V ) -> { <. x , y >. | E. c e. P c = { x , y } } e. ~P ( V X. V ) )