Metamath Proof Explorer

Theorem prelrrx2b

Description: An unordered pair of ordered pairs with first components 1 and 2 and real numbers as second components is a point in a real Euclidean space of dimension 2, determined by its coordinates. (Contributed by AV, 7-May-2023)

Ref Expression
Hypotheses prelrrx2.i 
|- I = { 1 , 2 }
prelrrx2.b 
|- P = ( RR ^m I )
Assertion prelrrx2b 
|- ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( Z e. P /\ ( ( ( Z ` 1 ) = A /\ ( Z ` 2 ) = B ) \/ ( ( Z ` 1 ) = X /\ ( Z ` 2 ) = Y ) ) ) <-> Z e. { { <. 1 , A >. , <. 2 , B >. } , { <. 1 , X >. , <. 2 , Y >. } } ) )

Proof

Step Hyp Ref Expression
1 prelrrx2.i 
 |-  I = { 1 , 2 }
2 prelrrx2.b 
 |-  P = ( RR ^m I )
3 2 eleq2i 
 |-  ( Z e. P <-> Z e. ( RR ^m I ) )
4 1 oveq2i 
 |-  ( RR ^m I ) = ( RR ^m { 1 , 2 } )
5 4 eleq2i 
 |-  ( Z e. ( RR ^m I ) <-> Z e. ( RR ^m { 1 , 2 } ) )
6 3 5 bitri 
 |-  ( Z e. P <-> Z e. ( RR ^m { 1 , 2 } ) )
7 elmapi 
 |-  ( Z e. ( RR ^m { 1 , 2 } ) -> Z : { 1 , 2 } --> RR )
8 1ne2 
 |-  1 =/= 2
9 1ex 
 |-  1 e. _V
10 2ex 
 |-  2 e. _V
11 9 10 fprb 
 |-  ( 1 =/= 2 -> ( Z : { 1 , 2 } --> RR <-> E. x e. RR E. y e. RR Z = { <. 1 , x >. , <. 2 , y >. } ) )
12 8 11 ax-mp 
 |-  ( Z : { 1 , 2 } --> RR <-> E. x e. RR E. y e. RR Z = { <. 1 , x >. , <. 2 , y >. } )
13 fveq1 
 |-  ( Z = { <. 1 , x >. , <. 2 , y >. } -> ( Z ` 1 ) = ( { <. 1 , x >. , <. 2 , y >. } ` 1 ) )
14 vex 
 |-  x e. _V
15 9 14 fvpr1 
 |-  ( 1 =/= 2 -> ( { <. 1 , x >. , <. 2 , y >. } ` 1 ) = x )
16 8 15 ax-mp 
 |-  ( { <. 1 , x >. , <. 2 , y >. } ` 1 ) = x
17 13 16 eqtrdi 
 |-  ( Z = { <. 1 , x >. , <. 2 , y >. } -> ( Z ` 1 ) = x )
18 17 eqeq1d 
 |-  ( Z = { <. 1 , x >. , <. 2 , y >. } -> ( ( Z ` 1 ) = A <-> x = A ) )
19 fveq1 
 |-  ( Z = { <. 1 , x >. , <. 2 , y >. } -> ( Z ` 2 ) = ( { <. 1 , x >. , <. 2 , y >. } ` 2 ) )
20 vex 
 |-  y e. _V
21 10 20 fvpr2 
 |-  ( 1 =/= 2 -> ( { <. 1 , x >. , <. 2 , y >. } ` 2 ) = y )
22 8 21 ax-mp 
 |-  ( { <. 1 , x >. , <. 2 , y >. } ` 2 ) = y
23 19 22 eqtrdi 
 |-  ( Z = { <. 1 , x >. , <. 2 , y >. } -> ( Z ` 2 ) = y )
24 23 eqeq1d 
 |-  ( Z = { <. 1 , x >. , <. 2 , y >. } -> ( ( Z ` 2 ) = B <-> y = B ) )
25 18 24 anbi12d 
 |-  ( Z = { <. 1 , x >. , <. 2 , y >. } -> ( ( ( Z ` 1 ) = A /\ ( Z ` 2 ) = B ) <-> ( x = A /\ y = B ) ) )
26 25 adantl 
 |-  ( ( ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) /\ ( x e. RR /\ y e. RR ) ) /\ Z = { <. 1 , x >. , <. 2 , y >. } ) -> ( ( ( Z ` 1 ) = A /\ ( Z ` 2 ) = B ) <-> ( x = A /\ y = B ) ) )
27 opeq2 
 |-  ( x = A -> <. 1 , x >. = <. 1 , A >. )
28 27 adantr 
 |-  ( ( x = A /\ y = B ) -> <. 1 , x >. = <. 1 , A >. )
29 opeq2 
 |-  ( y = B -> <. 2 , y >. = <. 2 , B >. )
30 29 adantl 
 |-  ( ( x = A /\ y = B ) -> <. 2 , y >. = <. 2 , B >. )
31 28 30 preq12d 
 |-  ( ( x = A /\ y = B ) -> { <. 1 , x >. , <. 2 , y >. } = { <. 1 , A >. , <. 2 , B >. } )
32 31 eqeq2d 
 |-  ( ( x = A /\ y = B ) -> ( Z = { <. 1 , x >. , <. 2 , y >. } <-> Z = { <. 1 , A >. , <. 2 , B >. } ) )
33 32 biimpcd 
 |-  ( Z = { <. 1 , x >. , <. 2 , y >. } -> ( ( x = A /\ y = B ) -> Z = { <. 1 , A >. , <. 2 , B >. } ) )
34 33 adantl 
 |-  ( ( ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) /\ ( x e. RR /\ y e. RR ) ) /\ Z = { <. 1 , x >. , <. 2 , y >. } ) -> ( ( x = A /\ y = B ) -> Z = { <. 1 , A >. , <. 2 , B >. } ) )
35 26 34 sylbid 
 |-  ( ( ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) /\ ( x e. RR /\ y e. RR ) ) /\ Z = { <. 1 , x >. , <. 2 , y >. } ) -> ( ( ( Z ` 1 ) = A /\ ( Z ` 2 ) = B ) -> Z = { <. 1 , A >. , <. 2 , B >. } ) )
36 35 ex 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) /\ ( x e. RR /\ y e. RR ) ) -> ( Z = { <. 1 , x >. , <. 2 , y >. } -> ( ( ( Z ` 1 ) = A /\ ( Z ` 2 ) = B ) -> Z = { <. 1 , A >. , <. 2 , B >. } ) ) )
37 36 rexlimdvva 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> ( E. x e. RR E. y e. RR Z = { <. 1 , x >. , <. 2 , y >. } -> ( ( ( Z ` 1 ) = A /\ ( Z ` 2 ) = B ) -> Z = { <. 1 , A >. , <. 2 , B >. } ) ) )
38 12 37 syl5bi 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> ( Z : { 1 , 2 } --> RR -> ( ( ( Z ` 1 ) = A /\ ( Z ` 2 ) = B ) -> Z = { <. 1 , A >. , <. 2 , B >. } ) ) )
39 7 38 syl5 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> ( Z e. ( RR ^m { 1 , 2 } ) -> ( ( ( Z ` 1 ) = A /\ ( Z ` 2 ) = B ) -> Z = { <. 1 , A >. , <. 2 , B >. } ) ) )
40 6 39 syl5bi 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> ( Z e. P -> ( ( ( Z ` 1 ) = A /\ ( Z ` 2 ) = B ) -> Z = { <. 1 , A >. , <. 2 , B >. } ) ) )
41 40 imp 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) /\ Z e. P ) -> ( ( ( Z ` 1 ) = A /\ ( Z ` 2 ) = B ) -> Z = { <. 1 , A >. , <. 2 , B >. } ) )
42 17 eqeq1d 
 |-  ( Z = { <. 1 , x >. , <. 2 , y >. } -> ( ( Z ` 1 ) = X <-> x = X ) )
43 23 eqeq1d 
 |-  ( Z = { <. 1 , x >. , <. 2 , y >. } -> ( ( Z ` 2 ) = Y <-> y = Y ) )
44 42 43 anbi12d 
 |-  ( Z = { <. 1 , x >. , <. 2 , y >. } -> ( ( ( Z ` 1 ) = X /\ ( Z ` 2 ) = Y ) <-> ( x = X /\ y = Y ) ) )
45 44 adantl 
 |-  ( ( ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) /\ ( x e. RR /\ y e. RR ) ) /\ Z = { <. 1 , x >. , <. 2 , y >. } ) -> ( ( ( Z ` 1 ) = X /\ ( Z ` 2 ) = Y ) <-> ( x = X /\ y = Y ) ) )
46 opeq2 
 |-  ( x = X -> <. 1 , x >. = <. 1 , X >. )
47 46 adantr 
 |-  ( ( x = X /\ y = Y ) -> <. 1 , x >. = <. 1 , X >. )
48 opeq2 
 |-  ( y = Y -> <. 2 , y >. = <. 2 , Y >. )
49 48 adantl 
 |-  ( ( x = X /\ y = Y ) -> <. 2 , y >. = <. 2 , Y >. )
50 47 49 preq12d 
 |-  ( ( x = X /\ y = Y ) -> { <. 1 , x >. , <. 2 , y >. } = { <. 1 , X >. , <. 2 , Y >. } )
51 50 eqeq2d 
 |-  ( ( x = X /\ y = Y ) -> ( Z = { <. 1 , x >. , <. 2 , y >. } <-> Z = { <. 1 , X >. , <. 2 , Y >. } ) )
52 51 biimpcd 
 |-  ( Z = { <. 1 , x >. , <. 2 , y >. } -> ( ( x = X /\ y = Y ) -> Z = { <. 1 , X >. , <. 2 , Y >. } ) )
53 52 adantl 
 |-  ( ( ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) /\ ( x e. RR /\ y e. RR ) ) /\ Z = { <. 1 , x >. , <. 2 , y >. } ) -> ( ( x = X /\ y = Y ) -> Z = { <. 1 , X >. , <. 2 , Y >. } ) )
54 45 53 sylbid 
 |-  ( ( ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) /\ ( x e. RR /\ y e. RR ) ) /\ Z = { <. 1 , x >. , <. 2 , y >. } ) -> ( ( ( Z ` 1 ) = X /\ ( Z ` 2 ) = Y ) -> Z = { <. 1 , X >. , <. 2 , Y >. } ) )
55 54 ex 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) /\ ( x e. RR /\ y e. RR ) ) -> ( Z = { <. 1 , x >. , <. 2 , y >. } -> ( ( ( Z ` 1 ) = X /\ ( Z ` 2 ) = Y ) -> Z = { <. 1 , X >. , <. 2 , Y >. } ) ) )
56 55 rexlimdvva 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> ( E. x e. RR E. y e. RR Z = { <. 1 , x >. , <. 2 , y >. } -> ( ( ( Z ` 1 ) = X /\ ( Z ` 2 ) = Y ) -> Z = { <. 1 , X >. , <. 2 , Y >. } ) ) )
57 12 56 syl5bi 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> ( Z : { 1 , 2 } --> RR -> ( ( ( Z ` 1 ) = X /\ ( Z ` 2 ) = Y ) -> Z = { <. 1 , X >. , <. 2 , Y >. } ) ) )
58 7 57 syl5 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> ( Z e. ( RR ^m { 1 , 2 } ) -> ( ( ( Z ` 1 ) = X /\ ( Z ` 2 ) = Y ) -> Z = { <. 1 , X >. , <. 2 , Y >. } ) ) )
59 6 58 syl5bi 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> ( Z e. P -> ( ( ( Z ` 1 ) = X /\ ( Z ` 2 ) = Y ) -> Z = { <. 1 , X >. , <. 2 , Y >. } ) ) )
60 59 imp 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) /\ Z e. P ) -> ( ( ( Z ` 1 ) = X /\ ( Z ` 2 ) = Y ) -> Z = { <. 1 , X >. , <. 2 , Y >. } ) )
61 41 60 orim12d 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) /\ Z e. P ) -> ( ( ( ( Z ` 1 ) = A /\ ( Z ` 2 ) = B ) \/ ( ( Z ` 1 ) = X /\ ( Z ` 2 ) = Y ) ) -> ( Z = { <. 1 , A >. , <. 2 , B >. } \/ Z = { <. 1 , X >. , <. 2 , Y >. } ) ) )
62 61 imp 
 |-  ( ( ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) /\ Z e. P ) /\ ( ( ( Z ` 1 ) = A /\ ( Z ` 2 ) = B ) \/ ( ( Z ` 1 ) = X /\ ( Z ` 2 ) = Y ) ) ) -> ( Z = { <. 1 , A >. , <. 2 , B >. } \/ Z = { <. 1 , X >. , <. 2 , Y >. } ) )
63 elprg 
 |-  ( Z e. P -> ( Z e. { { <. 1 , A >. , <. 2 , B >. } , { <. 1 , X >. , <. 2 , Y >. } } <-> ( Z = { <. 1 , A >. , <. 2 , B >. } \/ Z = { <. 1 , X >. , <. 2 , Y >. } ) ) )
64 63 ad2antlr 
 |-  ( ( ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) /\ Z e. P ) /\ ( ( ( Z ` 1 ) = A /\ ( Z ` 2 ) = B ) \/ ( ( Z ` 1 ) = X /\ ( Z ` 2 ) = Y ) ) ) -> ( Z e. { { <. 1 , A >. , <. 2 , B >. } , { <. 1 , X >. , <. 2 , Y >. } } <-> ( Z = { <. 1 , A >. , <. 2 , B >. } \/ Z = { <. 1 , X >. , <. 2 , Y >. } ) ) )
65 62 64 mpbird 
 |-  ( ( ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) /\ Z e. P ) /\ ( ( ( Z ` 1 ) = A /\ ( Z ` 2 ) = B ) \/ ( ( Z ` 1 ) = X /\ ( Z ` 2 ) = Y ) ) ) -> Z e. { { <. 1 , A >. , <. 2 , B >. } , { <. 1 , X >. , <. 2 , Y >. } } )
66 65 expl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( Z e. P /\ ( ( ( Z ` 1 ) = A /\ ( Z ` 2 ) = B ) \/ ( ( Z ` 1 ) = X /\ ( Z ` 2 ) = Y ) ) ) -> Z e. { { <. 1 , A >. , <. 2 , B >. } , { <. 1 , X >. , <. 2 , Y >. } } ) )
67 elpri 
 |-  ( Z e. { { <. 1 , A >. , <. 2 , B >. } , { <. 1 , X >. , <. 2 , Y >. } } -> ( Z = { <. 1 , A >. , <. 2 , B >. } \/ Z = { <. 1 , X >. , <. 2 , Y >. } ) )
68 1 2 prelrrx2 
 |-  ( ( A e. RR /\ B e. RR ) -> { <. 1 , A >. , <. 2 , B >. } e. P )
69 68 ad2antrr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) /\ Z = { <. 1 , A >. , <. 2 , B >. } ) -> { <. 1 , A >. , <. 2 , B >. } e. P )
70 eleq1 
 |-  ( Z = { <. 1 , A >. , <. 2 , B >. } -> ( Z e. P <-> { <. 1 , A >. , <. 2 , B >. } e. P ) )
71 70 adantl 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) /\ Z = { <. 1 , A >. , <. 2 , B >. } ) -> ( Z e. P <-> { <. 1 , A >. , <. 2 , B >. } e. P ) )
72 69 71 mpbird 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) /\ Z = { <. 1 , A >. , <. 2 , B >. } ) -> Z e. P )
73 simpl 
 |-  ( ( A e. RR /\ B e. RR ) -> A e. RR )
74 8 a1i 
 |-  ( ( A e. RR /\ B e. RR ) -> 1 =/= 2 )
75 fvpr1g 
 |-  ( ( 1 e. _V /\ A e. RR /\ 1 =/= 2 ) -> ( { <. 1 , A >. , <. 2 , B >. } ` 1 ) = A )
76 9 73 74 75 mp3an2i 
 |-  ( ( A e. RR /\ B e. RR ) -> ( { <. 1 , A >. , <. 2 , B >. } ` 1 ) = A )
77 simpr 
 |-  ( ( A e. RR /\ B e. RR ) -> B e. RR )
78 fvpr2g 
 |-  ( ( 2 e. _V /\ B e. RR /\ 1 =/= 2 ) -> ( { <. 1 , A >. , <. 2 , B >. } ` 2 ) = B )
79 10 77 74 78 mp3an2i 
 |-  ( ( A e. RR /\ B e. RR ) -> ( { <. 1 , A >. , <. 2 , B >. } ` 2 ) = B )
80 76 79 jca 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( { <. 1 , A >. , <. 2 , B >. } ` 1 ) = A /\ ( { <. 1 , A >. , <. 2 , B >. } ` 2 ) = B ) )
81 80 ad2antrr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) /\ Z = { <. 1 , A >. , <. 2 , B >. } ) -> ( ( { <. 1 , A >. , <. 2 , B >. } ` 1 ) = A /\ ( { <. 1 , A >. , <. 2 , B >. } ` 2 ) = B ) )
82 fveq1 
 |-  ( Z = { <. 1 , A >. , <. 2 , B >. } -> ( Z ` 1 ) = ( { <. 1 , A >. , <. 2 , B >. } ` 1 ) )
83 82 eqeq1d 
 |-  ( Z = { <. 1 , A >. , <. 2 , B >. } -> ( ( Z ` 1 ) = A <-> ( { <. 1 , A >. , <. 2 , B >. } ` 1 ) = A ) )
84 fveq1 
 |-  ( Z = { <. 1 , A >. , <. 2 , B >. } -> ( Z ` 2 ) = ( { <. 1 , A >. , <. 2 , B >. } ` 2 ) )
85 84 eqeq1d 
 |-  ( Z = { <. 1 , A >. , <. 2 , B >. } -> ( ( Z ` 2 ) = B <-> ( { <. 1 , A >. , <. 2 , B >. } ` 2 ) = B ) )
86 83 85 anbi12d 
 |-  ( Z = { <. 1 , A >. , <. 2 , B >. } -> ( ( ( Z ` 1 ) = A /\ ( Z ` 2 ) = B ) <-> ( ( { <. 1 , A >. , <. 2 , B >. } ` 1 ) = A /\ ( { <. 1 , A >. , <. 2 , B >. } ` 2 ) = B ) ) )
87 86 adantl 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) /\ Z = { <. 1 , A >. , <. 2 , B >. } ) -> ( ( ( Z ` 1 ) = A /\ ( Z ` 2 ) = B ) <-> ( ( { <. 1 , A >. , <. 2 , B >. } ` 1 ) = A /\ ( { <. 1 , A >. , <. 2 , B >. } ` 2 ) = B ) ) )
88 81 87 mpbird 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) /\ Z = { <. 1 , A >. , <. 2 , B >. } ) -> ( ( Z ` 1 ) = A /\ ( Z ` 2 ) = B ) )
89 88 orcd 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) /\ Z = { <. 1 , A >. , <. 2 , B >. } ) -> ( ( ( Z ` 1 ) = A /\ ( Z ` 2 ) = B ) \/ ( ( Z ` 1 ) = X /\ ( Z ` 2 ) = Y ) ) )
90 72 89 jca 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) /\ Z = { <. 1 , A >. , <. 2 , B >. } ) -> ( Z e. P /\ ( ( ( Z ` 1 ) = A /\ ( Z ` 2 ) = B ) \/ ( ( Z ` 1 ) = X /\ ( Z ` 2 ) = Y ) ) ) )
91 90 ex 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> ( Z = { <. 1 , A >. , <. 2 , B >. } -> ( Z e. P /\ ( ( ( Z ` 1 ) = A /\ ( Z ` 2 ) = B ) \/ ( ( Z ` 1 ) = X /\ ( Z ` 2 ) = Y ) ) ) ) )
92 1 2 prelrrx2 
 |-  ( ( X e. RR /\ Y e. RR ) -> { <. 1 , X >. , <. 2 , Y >. } e. P )
93 92 ad2antlr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) /\ Z = { <. 1 , X >. , <. 2 , Y >. } ) -> { <. 1 , X >. , <. 2 , Y >. } e. P )
94 eleq1 
 |-  ( Z = { <. 1 , X >. , <. 2 , Y >. } -> ( Z e. P <-> { <. 1 , X >. , <. 2 , Y >. } e. P ) )
95 94 adantl 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) /\ Z = { <. 1 , X >. , <. 2 , Y >. } ) -> ( Z e. P <-> { <. 1 , X >. , <. 2 , Y >. } e. P ) )
96 93 95 mpbird 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) /\ Z = { <. 1 , X >. , <. 2 , Y >. } ) -> Z e. P )
97 simpl 
 |-  ( ( X e. RR /\ Y e. RR ) -> X e. RR )
98 8 a1i 
 |-  ( ( X e. RR /\ Y e. RR ) -> 1 =/= 2 )
99 fvpr1g 
 |-  ( ( 1 e. _V /\ X e. RR /\ 1 =/= 2 ) -> ( { <. 1 , X >. , <. 2 , Y >. } ` 1 ) = X )
100 9 97 98 99 mp3an2i 
 |-  ( ( X e. RR /\ Y e. RR ) -> ( { <. 1 , X >. , <. 2 , Y >. } ` 1 ) = X )
101 simpr 
 |-  ( ( X e. RR /\ Y e. RR ) -> Y e. RR )
102 fvpr2g 
 |-  ( ( 2 e. _V /\ Y e. RR /\ 1 =/= 2 ) -> ( { <. 1 , X >. , <. 2 , Y >. } ` 2 ) = Y )
103 10 101 98 102 mp3an2i 
 |-  ( ( X e. RR /\ Y e. RR ) -> ( { <. 1 , X >. , <. 2 , Y >. } ` 2 ) = Y )
104 100 103 jca 
 |-  ( ( X e. RR /\ Y e. RR ) -> ( ( { <. 1 , X >. , <. 2 , Y >. } ` 1 ) = X /\ ( { <. 1 , X >. , <. 2 , Y >. } ` 2 ) = Y ) )
105 104 ad2antlr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) /\ Z = { <. 1 , X >. , <. 2 , Y >. } ) -> ( ( { <. 1 , X >. , <. 2 , Y >. } ` 1 ) = X /\ ( { <. 1 , X >. , <. 2 , Y >. } ` 2 ) = Y ) )
106 fveq1 
 |-  ( Z = { <. 1 , X >. , <. 2 , Y >. } -> ( Z ` 1 ) = ( { <. 1 , X >. , <. 2 , Y >. } ` 1 ) )
107 106 eqeq1d 
 |-  ( Z = { <. 1 , X >. , <. 2 , Y >. } -> ( ( Z ` 1 ) = X <-> ( { <. 1 , X >. , <. 2 , Y >. } ` 1 ) = X ) )
108 fveq1 
 |-  ( Z = { <. 1 , X >. , <. 2 , Y >. } -> ( Z ` 2 ) = ( { <. 1 , X >. , <. 2 , Y >. } ` 2 ) )
109 108 eqeq1d 
 |-  ( Z = { <. 1 , X >. , <. 2 , Y >. } -> ( ( Z ` 2 ) = Y <-> ( { <. 1 , X >. , <. 2 , Y >. } ` 2 ) = Y ) )
110 107 109 anbi12d 
 |-  ( Z = { <. 1 , X >. , <. 2 , Y >. } -> ( ( ( Z ` 1 ) = X /\ ( Z ` 2 ) = Y ) <-> ( ( { <. 1 , X >. , <. 2 , Y >. } ` 1 ) = X /\ ( { <. 1 , X >. , <. 2 , Y >. } ` 2 ) = Y ) ) )
111 110 adantl 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) /\ Z = { <. 1 , X >. , <. 2 , Y >. } ) -> ( ( ( Z ` 1 ) = X /\ ( Z ` 2 ) = Y ) <-> ( ( { <. 1 , X >. , <. 2 , Y >. } ` 1 ) = X /\ ( { <. 1 , X >. , <. 2 , Y >. } ` 2 ) = Y ) ) )
112 105 111 mpbird 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) /\ Z = { <. 1 , X >. , <. 2 , Y >. } ) -> ( ( Z ` 1 ) = X /\ ( Z ` 2 ) = Y ) )
113 112 olcd 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) /\ Z = { <. 1 , X >. , <. 2 , Y >. } ) -> ( ( ( Z ` 1 ) = A /\ ( Z ` 2 ) = B ) \/ ( ( Z ` 1 ) = X /\ ( Z ` 2 ) = Y ) ) )
114 96 113 jca 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) /\ Z = { <. 1 , X >. , <. 2 , Y >. } ) -> ( Z e. P /\ ( ( ( Z ` 1 ) = A /\ ( Z ` 2 ) = B ) \/ ( ( Z ` 1 ) = X /\ ( Z ` 2 ) = Y ) ) ) )
115 114 ex 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> ( Z = { <. 1 , X >. , <. 2 , Y >. } -> ( Z e. P /\ ( ( ( Z ` 1 ) = A /\ ( Z ` 2 ) = B ) \/ ( ( Z ` 1 ) = X /\ ( Z ` 2 ) = Y ) ) ) ) )
116 91 115 jaod 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( Z = { <. 1 , A >. , <. 2 , B >. } \/ Z = { <. 1 , X >. , <. 2 , Y >. } ) -> ( Z e. P /\ ( ( ( Z ` 1 ) = A /\ ( Z ` 2 ) = B ) \/ ( ( Z ` 1 ) = X /\ ( Z ` 2 ) = Y ) ) ) ) )
117 67 116 syl5 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> ( Z e. { { <. 1 , A >. , <. 2 , B >. } , { <. 1 , X >. , <. 2 , Y >. } } -> ( Z e. P /\ ( ( ( Z ` 1 ) = A /\ ( Z ` 2 ) = B ) \/ ( ( Z ` 1 ) = X /\ ( Z ` 2 ) = Y ) ) ) ) )
118 66 117 impbid 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( Z e. P /\ ( ( ( Z ` 1 ) = A /\ ( Z ` 2 ) = B ) \/ ( ( Z ` 1 ) = X /\ ( Z ` 2 ) = Y ) ) ) <-> Z e. { { <. 1 , A >. , <. 2 , B >. } , { <. 1 , X >. , <. 2 , Y >. } } ) )