Metamath Proof Explorer

Theorem sprsymrelfolem2

Description: Lemma 2 for sprsymrelfo . (Contributed by AV, 23-Nov-2021)

Ref Expression
Hypothesis sprsymrelfo.q 
|- Q = { q e. ( Pairs ` V ) | A. a e. V A. b e. V ( q = { a , b } -> a R b ) }
Assertion sprsymrelfolem2 
|- ( ( V e. W /\ R C_ ( V X. V ) /\ A. x e. V A. y e. V ( x R y <-> y R x ) ) -> ( x R y <-> E. c e. Q c = { x , y } ) )

Proof

Step Hyp Ref Expression
1 sprsymrelfo.q 
 |-  Q = { q e. ( Pairs ` V ) | A. a e. V A. b e. V ( q = { a , b } -> a R b ) }
2 df-br 
 |-  ( x R y <-> <. x , y >. e. R )
3 simpl 
 |-  ( ( V e. W /\ R C_ ( V X. V ) ) -> V e. W )
4 ssel 
 |-  ( R C_ ( V X. V ) -> ( <. x , y >. e. R -> <. x , y >. e. ( V X. V ) ) )
5 4 adantl 
 |-  ( ( V e. W /\ R C_ ( V X. V ) ) -> ( <. x , y >. e. R -> <. x , y >. e. ( V X. V ) ) )
6 5 imp 
 |-  ( ( ( V e. W /\ R C_ ( V X. V ) ) /\ <. x , y >. e. R ) -> <. x , y >. e. ( V X. V ) )
7 opelxp 
 |-  ( <. x , y >. e. ( V X. V ) <-> ( x e. V /\ y e. V ) )
8 6 7 sylib 
 |-  ( ( ( V e. W /\ R C_ ( V X. V ) ) /\ <. x , y >. e. R ) -> ( x e. V /\ y e. V ) )
9 prelspr 
 |-  ( ( V e. W /\ ( x e. V /\ y e. V ) ) -> { x , y } e. ( Pairs ` V ) )
10 3 8 9 syl2an2r 
 |-  ( ( ( V e. W /\ R C_ ( V X. V ) ) /\ <. x , y >. e. R ) -> { x , y } e. ( Pairs ` V ) )
11 10 ex 
 |-  ( ( V e. W /\ R C_ ( V X. V ) ) -> ( <. x , y >. e. R -> { x , y } e. ( Pairs ` V ) ) )
12 2 11 syl5bi 
 |-  ( ( V e. W /\ R C_ ( V X. V ) ) -> ( x R y -> { x , y } e. ( Pairs ` V ) ) )
13 12 3adant3 
 |-  ( ( V e. W /\ R C_ ( V X. V ) /\ A. x e. V A. y e. V ( x R y <-> y R x ) ) -> ( x R y -> { x , y } e. ( Pairs ` V ) ) )
14 13 imp 
 |-  ( ( ( V e. W /\ R C_ ( V X. V ) /\ A. x e. V A. y e. V ( x R y <-> y R x ) ) /\ x R y ) -> { x , y } e. ( Pairs ` V ) )
15 vex 
 |-  x e. _V
16 vex 
 |-  y e. _V
17 vex 
 |-  a e. _V
18 vex 
 |-  b e. _V
19 15 16 17 18 preq12b 
 |-  ( { x , y } = { a , b } <-> ( ( x = a /\ y = b ) \/ ( x = b /\ y = a ) ) )
20 breq12 
 |-  ( ( x = a /\ y = b ) -> ( x R y <-> a R b ) )
21 20 biimpd 
 |-  ( ( x = a /\ y = b ) -> ( x R y -> a R b ) )
22 21 com12 
 |-  ( x R y -> ( ( x = a /\ y = b ) -> a R b ) )
23 22 adantl 
 |-  ( ( ( V e. W /\ R C_ ( V X. V ) /\ A. x e. V A. y e. V ( x R y <-> y R x ) ) /\ x R y ) -> ( ( x = a /\ y = b ) -> a R b ) )
24 23 adantr 
 |-  ( ( ( ( V e. W /\ R C_ ( V X. V ) /\ A. x e. V A. y e. V ( x R y <-> y R x ) ) /\ x R y ) /\ ( a e. V /\ b e. V ) ) -> ( ( x = a /\ y = b ) -> a R b ) )
25 24 com12 
 |-  ( ( x = a /\ y = b ) -> ( ( ( ( V e. W /\ R C_ ( V X. V ) /\ A. x e. V A. y e. V ( x R y <-> y R x ) ) /\ x R y ) /\ ( a e. V /\ b e. V ) ) -> a R b ) )
26 rsp2 
 |-  ( A. x e. V A. y e. V ( x R y <-> y R x ) -> ( ( x e. V /\ y e. V ) -> ( x R y <-> y R x ) ) )
27 26 ancomsd 
 |-  ( A. x e. V A. y e. V ( x R y <-> y R x ) -> ( ( y e. V /\ x e. V ) -> ( x R y <-> y R x ) ) )
28 27 imp 
 |-  ( ( A. x e. V A. y e. V ( x R y <-> y R x ) /\ ( y e. V /\ x e. V ) ) -> ( x R y <-> y R x ) )
29 28 biimpd 
 |-  ( ( A. x e. V A. y e. V ( x R y <-> y R x ) /\ ( y e. V /\ x e. V ) ) -> ( x R y -> y R x ) )
30 29 ex 
 |-  ( A. x e. V A. y e. V ( x R y <-> y R x ) -> ( ( y e. V /\ x e. V ) -> ( x R y -> y R x ) ) )
31 30 3ad2ant3 
 |-  ( ( V e. W /\ R C_ ( V X. V ) /\ A. x e. V A. y e. V ( x R y <-> y R x ) ) -> ( ( y e. V /\ x e. V ) -> ( x R y -> y R x ) ) )
32 31 com23 
 |-  ( ( V e. W /\ R C_ ( V X. V ) /\ A. x e. V A. y e. V ( x R y <-> y R x ) ) -> ( x R y -> ( ( y e. V /\ x e. V ) -> y R x ) ) )
33 32 imp 
 |-  ( ( ( V e. W /\ R C_ ( V X. V ) /\ A. x e. V A. y e. V ( x R y <-> y R x ) ) /\ x R y ) -> ( ( y e. V /\ x e. V ) -> y R x ) )
34 33 adantl 
 |-  ( ( ( x = b /\ y = a ) /\ ( ( V e. W /\ R C_ ( V X. V ) /\ A. x e. V A. y e. V ( x R y <-> y R x ) ) /\ x R y ) ) -> ( ( y e. V /\ x e. V ) -> y R x ) )
35 eleq1 
 |-  ( y = a -> ( y e. V <-> a e. V ) )
36 eleq1 
 |-  ( x = b -> ( x e. V <-> b e. V ) )
37 35 36 bi2anan9r 
 |-  ( ( x = b /\ y = a ) -> ( ( y e. V /\ x e. V ) <-> ( a e. V /\ b e. V ) ) )
38 breq12 
 |-  ( ( y = a /\ x = b ) -> ( y R x <-> a R b ) )
39 38 ancoms 
 |-  ( ( x = b /\ y = a ) -> ( y R x <-> a R b ) )
40 37 39 imbi12d 
 |-  ( ( x = b /\ y = a ) -> ( ( ( y e. V /\ x e. V ) -> y R x ) <-> ( ( a e. V /\ b e. V ) -> a R b ) ) )
41 40 adantr 
 |-  ( ( ( x = b /\ y = a ) /\ ( ( V e. W /\ R C_ ( V X. V ) /\ A. x e. V A. y e. V ( x R y <-> y R x ) ) /\ x R y ) ) -> ( ( ( y e. V /\ x e. V ) -> y R x ) <-> ( ( a e. V /\ b e. V ) -> a R b ) ) )
42 34 41 mpbid 
 |-  ( ( ( x = b /\ y = a ) /\ ( ( V e. W /\ R C_ ( V X. V ) /\ A. x e. V A. y e. V ( x R y <-> y R x ) ) /\ x R y ) ) -> ( ( a e. V /\ b e. V ) -> a R b ) )
43 42 expimpd 
 |-  ( ( x = b /\ y = a ) -> ( ( ( ( V e. W /\ R C_ ( V X. V ) /\ A. x e. V A. y e. V ( x R y <-> y R x ) ) /\ x R y ) /\ ( a e. V /\ b e. V ) ) -> a R b ) )
44 25 43 jaoi 
 |-  ( ( ( x = a /\ y = b ) \/ ( x = b /\ y = a ) ) -> ( ( ( ( V e. W /\ R C_ ( V X. V ) /\ A. x e. V A. y e. V ( x R y <-> y R x ) ) /\ x R y ) /\ ( a e. V /\ b e. V ) ) -> a R b ) )
45 44 com12 
 |-  ( ( ( ( V e. W /\ R C_ ( V X. V ) /\ A. x e. V A. y e. V ( x R y <-> y R x ) ) /\ x R y ) /\ ( a e. V /\ b e. V ) ) -> ( ( ( x = a /\ y = b ) \/ ( x = b /\ y = a ) ) -> a R b ) )
46 19 45 syl5bi 
 |-  ( ( ( ( V e. W /\ R C_ ( V X. V ) /\ A. x e. V A. y e. V ( x R y <-> y R x ) ) /\ x R y ) /\ ( a e. V /\ b e. V ) ) -> ( { x , y } = { a , b } -> a R b ) )
47 46 ralrimivva 
 |-  ( ( ( V e. W /\ R C_ ( V X. V ) /\ A. x e. V A. y e. V ( x R y <-> y R x ) ) /\ x R y ) -> A. a e. V A. b e. V ( { x , y } = { a , b } -> a R b ) )
48 1 eleq2i 
 |-  ( { x , y } e. Q <-> { x , y } e. { q e. ( Pairs ` V ) | A. a e. V A. b e. V ( q = { a , b } -> a R b ) } )
49 eqeq1 
 |-  ( q = { x , y } -> ( q = { a , b } <-> { x , y } = { a , b } ) )
50 49 imbi1d 
 |-  ( q = { x , y } -> ( ( q = { a , b } -> a R b ) <-> ( { x , y } = { a , b } -> a R b ) ) )
51 50 2ralbidv 
 |-  ( q = { x , y } -> ( A. a e. V A. b e. V ( q = { a , b } -> a R b ) <-> A. a e. V A. b e. V ( { x , y } = { a , b } -> a R b ) ) )
52 51 elrab 
 |-  ( { x , y } e. { q e. ( Pairs ` V ) | A. a e. V A. b e. V ( q = { a , b } -> a R b ) } <-> ( { x , y } e. ( Pairs ` V ) /\ A. a e. V A. b e. V ( { x , y } = { a , b } -> a R b ) ) )
53 48 52 bitri 
 |-  ( { x , y } e. Q <-> ( { x , y } e. ( Pairs ` V ) /\ A. a e. V A. b e. V ( { x , y } = { a , b } -> a R b ) ) )
54 14 47 53 sylanbrc 
 |-  ( ( ( V e. W /\ R C_ ( V X. V ) /\ A. x e. V A. y e. V ( x R y <-> y R x ) ) /\ x R y ) -> { x , y } e. Q )
55 eqidd 
 |-  ( ( ( V e. W /\ R C_ ( V X. V ) /\ A. x e. V A. y e. V ( x R y <-> y R x ) ) /\ x R y ) -> { x , y } = { x , y } )
56 eqeq1 
 |-  ( c = { x , y } -> ( c = { x , y } <-> { x , y } = { x , y } ) )
57 56 rspcev 
 |-  ( ( { x , y } e. Q /\ { x , y } = { x , y } ) -> E. c e. Q c = { x , y } )
58 54 55 57 syl2anc 
 |-  ( ( ( V e. W /\ R C_ ( V X. V ) /\ A. x e. V A. y e. V ( x R y <-> y R x ) ) /\ x R y ) -> E. c e. Q c = { x , y } )
59 58 ex 
 |-  ( ( V e. W /\ R C_ ( V X. V ) /\ A. x e. V A. y e. V ( x R y <-> y R x ) ) -> ( x R y -> E. c e. Q c = { x , y } ) )
60 1 eleq2i 
 |-  ( c e. Q <-> c e. { q e. ( Pairs ` V ) | A. a e. V A. b e. V ( q = { a , b } -> a R b ) } )
61 eqeq1 
 |-  ( q = c -> ( q = { a , b } <-> c = { a , b } ) )
62 61 imbi1d 
 |-  ( q = c -> ( ( q = { a , b } -> a R b ) <-> ( c = { a , b } -> a R b ) ) )
63 62 2ralbidv 
 |-  ( q = c -> ( A. a e. V A. b e. V ( q = { a , b } -> a R b ) <-> A. a e. V A. b e. V ( c = { a , b } -> a R b ) ) )
64 63 elrab 
 |-  ( c e. { q e. ( Pairs ` V ) | A. a e. V A. b e. V ( q = { a , b } -> a R b ) } <-> ( c e. ( Pairs ` V ) /\ A. a e. V A. b e. V ( c = { a , b } -> a R b ) ) )
65 60 64 bitri 
 |-  ( c e. Q <-> ( c e. ( Pairs ` V ) /\ A. a e. V A. b e. V ( c = { a , b } -> a R b ) ) )
66 eleq1 
 |-  ( c = { x , y } -> ( c e. ( Pairs ` V ) <-> { x , y } e. ( Pairs ` V ) ) )
67 prsprel 
 |-  ( ( { x , y } e. ( Pairs ` V ) /\ ( x e. _V /\ y e. _V ) ) -> ( x e. V /\ y e. V ) )
68 15 16 67 mpanr12 
 |-  ( { x , y } e. ( Pairs ` V ) -> ( x e. V /\ y e. V ) )
69 66 68 syl6bi 
 |-  ( c = { x , y } -> ( c e. ( Pairs ` V ) -> ( x e. V /\ y e. V ) ) )
70 69 com12 
 |-  ( c e. ( Pairs ` V ) -> ( c = { x , y } -> ( x e. V /\ y e. V ) ) )
71 70 adantr 
 |-  ( ( c e. ( Pairs ` V ) /\ A. a e. V A. b e. V ( c = { a , b } -> a R b ) ) -> ( c = { x , y } -> ( x e. V /\ y e. V ) ) )
72 71 imp 
 |-  ( ( ( c e. ( Pairs ` V ) /\ A. a e. V A. b e. V ( c = { a , b } -> a R b ) ) /\ c = { x , y } ) -> ( x e. V /\ y e. V ) )
73 preq1 
 |-  ( a = x -> { a , b } = { x , b } )
74 73 eqeq2d 
 |-  ( a = x -> ( c = { a , b } <-> c = { x , b } ) )
75 breq1 
 |-  ( a = x -> ( a R b <-> x R b ) )
76 74 75 imbi12d 
 |-  ( a = x -> ( ( c = { a , b } -> a R b ) <-> ( c = { x , b } -> x R b ) ) )
77 preq2 
 |-  ( b = y -> { x , b } = { x , y } )
78 77 eqeq2d 
 |-  ( b = y -> ( c = { x , b } <-> c = { x , y } ) )
79 breq2 
 |-  ( b = y -> ( x R b <-> x R y ) )
80 78 79 imbi12d 
 |-  ( b = y -> ( ( c = { x , b } -> x R b ) <-> ( c = { x , y } -> x R y ) ) )
81 76 80 rspc2v 
 |-  ( ( x e. V /\ y e. V ) -> ( A. a e. V A. b e. V ( c = { a , b } -> a R b ) -> ( c = { x , y } -> x R y ) ) )
82 81 a1d 
 |-  ( ( x e. V /\ y e. V ) -> ( c e. ( Pairs ` V ) -> ( A. a e. V A. b e. V ( c = { a , b } -> a R b ) -> ( c = { x , y } -> x R y ) ) ) )
83 82 imp4c 
 |-  ( ( x e. V /\ y e. V ) -> ( ( ( c e. ( Pairs ` V ) /\ A. a e. V A. b e. V ( c = { a , b } -> a R b ) ) /\ c = { x , y } ) -> x R y ) )
84 72 83 mpcom 
 |-  ( ( ( c e. ( Pairs ` V ) /\ A. a e. V A. b e. V ( c = { a , b } -> a R b ) ) /\ c = { x , y } ) -> x R y )
85 84 a1d 
 |-  ( ( ( c e. ( Pairs ` V ) /\ A. a e. V A. b e. V ( c = { a , b } -> a R b ) ) /\ c = { x , y } ) -> ( ( V e. W /\ R C_ ( V X. V ) /\ A. x e. V A. y e. V ( x R y <-> y R x ) ) -> x R y ) )
86 65 85 sylanb 
 |-  ( ( c e. Q /\ c = { x , y } ) -> ( ( V e. W /\ R C_ ( V X. V ) /\ A. x e. V A. y e. V ( x R y <-> y R x ) ) -> x R y ) )
87 86 rexlimiva 
 |-  ( E. c e. Q c = { x , y } -> ( ( V e. W /\ R C_ ( V X. V ) /\ A. x e. V A. y e. V ( x R y <-> y R x ) ) -> x R y ) )
88 87 com12 
 |-  ( ( V e. W /\ R C_ ( V X. V ) /\ A. x e. V A. y e. V ( x R y <-> y R x ) ) -> ( E. c e. Q c = { x , y } -> x R y ) )
89 59 88 impbid 
 |-  ( ( V e. W /\ R C_ ( V X. V ) /\ A. x e. V A. y e. V ( x R y <-> y R x ) ) -> ( x R y <-> E. c e. Q c = { x , y } ) )