Metamath Proof Explorer

Theorem relop

Description: A necessary and sufficient condition for a Kuratowski ordered pair to be a relation. (Contributed by NM, 3-Jun-2008) A relation is a class of ordered pairs, so the fact that an ordered pair may sometimes be itself a relation is an "accident" depending on the specific encoding of ordered pairs as classes (in set.mm, the Kuratowski encoding). A more meaningful statement is relsnopg , as funsng is to funop . (New usage is discouraged.)

Ref Expression
Hypotheses relop.1 
|- A e. _V
relop.2 
|- B e. _V
Assertion relop 
|- ( Rel <. A , B >. <-> E. x E. y ( A = { x } /\ B = { x , y } ) )

Proof

Step Hyp Ref Expression
1 relop.1 
 |-  A e. _V
2 relop.2 
 |-  B e. _V
3 df-rel 
 |-  ( Rel <. A , B >. <-> <. A , B >. C_ ( _V X. _V ) )
4 dfss2 
 |-  ( <. A , B >. C_ ( _V X. _V ) <-> A. z ( z e. <. A , B >. -> z e. ( _V X. _V ) ) )
5 1 2 elop 
 |-  ( z e. <. A , B >. <-> ( z = { A } \/ z = { A , B } ) )
6 elvv 
 |-  ( z e. ( _V X. _V ) <-> E. x E. y z = <. x , y >. )
7 5 6 imbi12i 
 |-  ( ( z e. <. A , B >. -> z e. ( _V X. _V ) ) <-> ( ( z = { A } \/ z = { A , B } ) -> E. x E. y z = <. x , y >. ) )
8 jaob 
 |-  ( ( ( z = { A } \/ z = { A , B } ) -> E. x E. y z = <. x , y >. ) <-> ( ( z = { A } -> E. x E. y z = <. x , y >. ) /\ ( z = { A , B } -> E. x E. y z = <. x , y >. ) ) )
9 7 8 bitri 
 |-  ( ( z e. <. A , B >. -> z e. ( _V X. _V ) ) <-> ( ( z = { A } -> E. x E. y z = <. x , y >. ) /\ ( z = { A , B } -> E. x E. y z = <. x , y >. ) ) )
10 9 albii 
 |-  ( A. z ( z e. <. A , B >. -> z e. ( _V X. _V ) ) <-> A. z ( ( z = { A } -> E. x E. y z = <. x , y >. ) /\ ( z = { A , B } -> E. x E. y z = <. x , y >. ) ) )
11 19.26 
 |-  ( A. z ( ( z = { A } -> E. x E. y z = <. x , y >. ) /\ ( z = { A , B } -> E. x E. y z = <. x , y >. ) ) <-> ( A. z ( z = { A } -> E. x E. y z = <. x , y >. ) /\ A. z ( z = { A , B } -> E. x E. y z = <. x , y >. ) ) )
12 10 11 bitri 
 |-  ( A. z ( z e. <. A , B >. -> z e. ( _V X. _V ) ) <-> ( A. z ( z = { A } -> E. x E. y z = <. x , y >. ) /\ A. z ( z = { A , B } -> E. x E. y z = <. x , y >. ) ) )
13 4 12 bitri 
 |-  ( <. A , B >. C_ ( _V X. _V ) <-> ( A. z ( z = { A } -> E. x E. y z = <. x , y >. ) /\ A. z ( z = { A , B } -> E. x E. y z = <. x , y >. ) ) )
14 snex 
 |-  { A } e. _V
15 eqeq1 
 |-  ( z = { A } -> ( z = { A } <-> { A } = { A } ) )
16 eqeq1 
 |-  ( z = { A } -> ( z = <. x , y >. <-> { A } = <. x , y >. ) )
17 eqcom 
 |-  ( { A } = <. x , y >. <-> <. x , y >. = { A } )
18 vex 
 |-  x e. _V
19 vex 
 |-  y e. _V
20 18 19 opeqsn 
 |-  ( <. x , y >. = { A } <-> ( x = y /\ A = { x } ) )
21 17 20 bitri 
 |-  ( { A } = <. x , y >. <-> ( x = y /\ A = { x } ) )
22 16 21 bitrdi 
 |-  ( z = { A } -> ( z = <. x , y >. <-> ( x = y /\ A = { x } ) ) )
23 22 2exbidv 
 |-  ( z = { A } -> ( E. x E. y z = <. x , y >. <-> E. x E. y ( x = y /\ A = { x } ) ) )
24 15 23 imbi12d 
 |-  ( z = { A } -> ( ( z = { A } -> E. x E. y z = <. x , y >. ) <-> ( { A } = { A } -> E. x E. y ( x = y /\ A = { x } ) ) ) )
25 14 24 spcv 
 |-  ( A. z ( z = { A } -> E. x E. y z = <. x , y >. ) -> ( { A } = { A } -> E. x E. y ( x = y /\ A = { x } ) ) )
26 sneq 
 |-  ( w = x -> { w } = { x } )
27 26 eqeq2d 
 |-  ( w = x -> ( A = { w } <-> A = { x } ) )
28 27 cbvexvw 
 |-  ( E. w A = { w } <-> E. x A = { x } )
29 ax6evr 
 |-  E. y x = y
30 19.41v 
 |-  ( E. y ( x = y /\ A = { x } ) <-> ( E. y x = y /\ A = { x } ) )
31 29 30 mpbiran 
 |-  ( E. y ( x = y /\ A = { x } ) <-> A = { x } )
32 31 exbii 
 |-  ( E. x E. y ( x = y /\ A = { x } ) <-> E. x A = { x } )
33 eqid 
 |-  { A } = { A }
34 33 a1bi 
 |-  ( E. x E. y ( x = y /\ A = { x } ) <-> ( { A } = { A } -> E. x E. y ( x = y /\ A = { x } ) ) )
35 28 32 34 3bitr2ri 
 |-  ( ( { A } = { A } -> E. x E. y ( x = y /\ A = { x } ) ) <-> E. w A = { w } )
36 25 35 sylib 
 |-  ( A. z ( z = { A } -> E. x E. y z = <. x , y >. ) -> E. w A = { w } )
37 eqid 
 |-  { A , B } = { A , B }
38 prex 
 |-  { A , B } e. _V
39 eqeq1 
 |-  ( z = { A , B } -> ( z = { A , B } <-> { A , B } = { A , B } ) )
40 eqeq1 
 |-  ( z = { A , B } -> ( z = <. x , y >. <-> { A , B } = <. x , y >. ) )
41 40 2exbidv 
 |-  ( z = { A , B } -> ( E. x E. y z = <. x , y >. <-> E. x E. y { A , B } = <. x , y >. ) )
42 39 41 imbi12d 
 |-  ( z = { A , B } -> ( ( z = { A , B } -> E. x E. y z = <. x , y >. ) <-> ( { A , B } = { A , B } -> E. x E. y { A , B } = <. x , y >. ) ) )
43 38 42 spcv 
 |-  ( A. z ( z = { A , B } -> E. x E. y z = <. x , y >. ) -> ( { A , B } = { A , B } -> E. x E. y { A , B } = <. x , y >. ) )
44 37 43 mpi 
 |-  ( A. z ( z = { A , B } -> E. x E. y z = <. x , y >. ) -> E. x E. y { A , B } = <. x , y >. )
45 eqcom 
 |-  ( { A , B } = <. x , y >. <-> <. x , y >. = { A , B } )
46 18 19 1 2 opeqpr 
 |-  ( <. x , y >. = { A , B } <-> ( ( A = { x } /\ B = { x , y } ) \/ ( A = { x , y } /\ B = { x } ) ) )
47 45 46 bitri 
 |-  ( { A , B } = <. x , y >. <-> ( ( A = { x } /\ B = { x , y } ) \/ ( A = { x , y } /\ B = { x } ) ) )
48 idd 
 |-  ( A = { w } -> ( ( A = { x } /\ B = { x , y } ) -> ( A = { x } /\ B = { x , y } ) ) )
49 eqtr2 
 |-  ( ( A = { x , y } /\ A = { w } ) -> { x , y } = { w } )
50 18 19 preqsn 
 |-  ( { x , y } = { w } <-> ( x = y /\ y = w ) )
51 50 simplbi 
 |-  ( { x , y } = { w } -> x = y )
52 49 51 syl 
 |-  ( ( A = { x , y } /\ A = { w } ) -> x = y )
53 dfsn2 
 |-  { x } = { x , x }
54 preq2 
 |-  ( x = y -> { x , x } = { x , y } )
55 53 54 syl5req 
 |-  ( x = y -> { x , y } = { x } )
56 55 eqeq2d 
 |-  ( x = y -> ( A = { x , y } <-> A = { x } ) )
57 53 54 syl5eq 
 |-  ( x = y -> { x } = { x , y } )
58 57 eqeq2d 
 |-  ( x = y -> ( B = { x } <-> B = { x , y } ) )
59 56 58 anbi12d 
 |-  ( x = y -> ( ( A = { x , y } /\ B = { x } ) <-> ( A = { x } /\ B = { x , y } ) ) )
60 59 biimpd 
 |-  ( x = y -> ( ( A = { x , y } /\ B = { x } ) -> ( A = { x } /\ B = { x , y } ) ) )
61 60 expd 
 |-  ( x = y -> ( A = { x , y } -> ( B = { x } -> ( A = { x } /\ B = { x , y } ) ) ) )
62 61 com12 
 |-  ( A = { x , y } -> ( x = y -> ( B = { x } -> ( A = { x } /\ B = { x , y } ) ) ) )
63 62 adantr 
 |-  ( ( A = { x , y } /\ A = { w } ) -> ( x = y -> ( B = { x } -> ( A = { x } /\ B = { x , y } ) ) ) )
64 52 63 mpd 
 |-  ( ( A = { x , y } /\ A = { w } ) -> ( B = { x } -> ( A = { x } /\ B = { x , y } ) ) )
65 64 expcom 
 |-  ( A = { w } -> ( A = { x , y } -> ( B = { x } -> ( A = { x } /\ B = { x , y } ) ) ) )
66 65 impd 
 |-  ( A = { w } -> ( ( A = { x , y } /\ B = { x } ) -> ( A = { x } /\ B = { x , y } ) ) )
67 48 66 jaod 
 |-  ( A = { w } -> ( ( ( A = { x } /\ B = { x , y } ) \/ ( A = { x , y } /\ B = { x } ) ) -> ( A = { x } /\ B = { x , y } ) ) )
68 47 67 syl5bi 
 |-  ( A = { w } -> ( { A , B } = <. x , y >. -> ( A = { x } /\ B = { x , y } ) ) )
69 68 2eximdv 
 |-  ( A = { w } -> ( E. x E. y { A , B } = <. x , y >. -> E. x E. y ( A = { x } /\ B = { x , y } ) ) )
70 69 exlimiv 
 |-  ( E. w A = { w } -> ( E. x E. y { A , B } = <. x , y >. -> E. x E. y ( A = { x } /\ B = { x , y } ) ) )
71 70 imp 
 |-  ( ( E. w A = { w } /\ E. x E. y { A , B } = <. x , y >. ) -> E. x E. y ( A = { x } /\ B = { x , y } ) )
72 36 44 71 syl2an 
 |-  ( ( A. z ( z = { A } -> E. x E. y z = <. x , y >. ) /\ A. z ( z = { A , B } -> E. x E. y z = <. x , y >. ) ) -> E. x E. y ( A = { x } /\ B = { x , y } ) )
73 13 72 sylbi 
 |-  ( <. A , B >. C_ ( _V X. _V ) -> E. x E. y ( A = { x } /\ B = { x , y } ) )
74 simpr 
 |-  ( ( A = { x } /\ z = { A } ) -> z = { A } )
75 equid 
 |-  x = x
76 75 jctl 
 |-  ( A = { x } -> ( x = x /\ A = { x } ) )
77 18 18 opeqsn 
 |-  ( <. x , x >. = { A } <-> ( x = x /\ A = { x } ) )
78 76 77 sylibr 
 |-  ( A = { x } -> <. x , x >. = { A } )
79 78 adantr 
 |-  ( ( A = { x } /\ z = { A } ) -> <. x , x >. = { A } )
80 74 79 eqtr4d 
 |-  ( ( A = { x } /\ z = { A } ) -> z = <. x , x >. )
81 opeq12 
 |-  ( ( w = x /\ v = x ) -> <. w , v >. = <. x , x >. )
82 81 eqeq2d 
 |-  ( ( w = x /\ v = x ) -> ( z = <. w , v >. <-> z = <. x , x >. ) )
83 18 18 82 spc2ev 
 |-  ( z = <. x , x >. -> E. w E. v z = <. w , v >. )
84 80 83 syl 
 |-  ( ( A = { x } /\ z = { A } ) -> E. w E. v z = <. w , v >. )
85 84 adantlr 
 |-  ( ( ( A = { x } /\ B = { x , y } ) /\ z = { A } ) -> E. w E. v z = <. w , v >. )
86 preq12 
 |-  ( ( A = { x } /\ B = { x , y } ) -> { A , B } = { { x } , { x , y } } )
87 86 eqeq2d 
 |-  ( ( A = { x } /\ B = { x , y } ) -> ( z = { A , B } <-> z = { { x } , { x , y } } ) )
88 87 biimpa 
 |-  ( ( ( A = { x } /\ B = { x , y } ) /\ z = { A , B } ) -> z = { { x } , { x , y } } )
89 18 19 dfop 
 |-  <. x , y >. = { { x } , { x , y } }
90 88 89 eqtr4di 
 |-  ( ( ( A = { x } /\ B = { x , y } ) /\ z = { A , B } ) -> z = <. x , y >. )
91 opeq12 
 |-  ( ( w = x /\ v = y ) -> <. w , v >. = <. x , y >. )
92 91 eqeq2d 
 |-  ( ( w = x /\ v = y ) -> ( z = <. w , v >. <-> z = <. x , y >. ) )
93 18 19 92 spc2ev 
 |-  ( z = <. x , y >. -> E. w E. v z = <. w , v >. )
94 90 93 syl 
 |-  ( ( ( A = { x } /\ B = { x , y } ) /\ z = { A , B } ) -> E. w E. v z = <. w , v >. )
95 85 94 jaodan 
 |-  ( ( ( A = { x } /\ B = { x , y } ) /\ ( z = { A } \/ z = { A , B } ) ) -> E. w E. v z = <. w , v >. )
96 95 ex 
 |-  ( ( A = { x } /\ B = { x , y } ) -> ( ( z = { A } \/ z = { A , B } ) -> E. w E. v z = <. w , v >. ) )
97 elvv 
 |-  ( z e. ( _V X. _V ) <-> E. w E. v z = <. w , v >. )
98 96 5 97 3imtr4g 
 |-  ( ( A = { x } /\ B = { x , y } ) -> ( z e. <. A , B >. -> z e. ( _V X. _V ) ) )
99 98 ssrdv 
 |-  ( ( A = { x } /\ B = { x , y } ) -> <. A , B >. C_ ( _V X. _V ) )
100 99 exlimivv 
 |-  ( E. x E. y ( A = { x } /\ B = { x , y } ) -> <. A , B >. C_ ( _V X. _V ) )
101 73 100 impbii 
 |-  ( <. A , B >. C_ ( _V X. _V ) <-> E. x E. y ( A = { x } /\ B = { x , y } ) )
102 3 101 bitri 
 |-  ( Rel <. A , B >. <-> E. x E. y ( A = { x } /\ B = { x , y } ) )