Step |
Hyp |
Ref |
Expression |
1 |
|
1z |
|- 1 e. ZZ |
2 |
|
fztp |
|- ( 1 e. ZZ -> ( 1 ... ( 1 + 2 ) ) = { 1 , ( 1 + 1 ) , ( 1 + 2 ) } ) |
3 |
1 2
|
ax-mp |
|- ( 1 ... ( 1 + 2 ) ) = { 1 , ( 1 + 1 ) , ( 1 + 2 ) } |
4 |
|
df-3 |
|- 3 = ( 2 + 1 ) |
5 |
|
2cn |
|- 2 e. CC |
6 |
|
ax-1cn |
|- 1 e. CC |
7 |
5 6
|
addcomi |
|- ( 2 + 1 ) = ( 1 + 2 ) |
8 |
4 7
|
eqtri |
|- 3 = ( 1 + 2 ) |
9 |
8
|
oveq2i |
|- ( 1 ... 3 ) = ( 1 ... ( 1 + 2 ) ) |
10 |
|
tpeq3 |
|- ( 3 = ( 1 + 2 ) -> { 1 , 2 , 3 } = { 1 , 2 , ( 1 + 2 ) } ) |
11 |
8 10
|
ax-mp |
|- { 1 , 2 , 3 } = { 1 , 2 , ( 1 + 2 ) } |
12 |
|
df-2 |
|- 2 = ( 1 + 1 ) |
13 |
|
tpeq2 |
|- ( 2 = ( 1 + 1 ) -> { 1 , 2 , ( 1 + 2 ) } = { 1 , ( 1 + 1 ) , ( 1 + 2 ) } ) |
14 |
12 13
|
ax-mp |
|- { 1 , 2 , ( 1 + 2 ) } = { 1 , ( 1 + 1 ) , ( 1 + 2 ) } |
15 |
11 14
|
eqtri |
|- { 1 , 2 , 3 } = { 1 , ( 1 + 1 ) , ( 1 + 2 ) } |
16 |
3 9 15
|
3eqtr4i |
|- ( 1 ... 3 ) = { 1 , 2 , 3 } |
17 |
16
|
raleqi |
|- ( A. x e. ( 1 ... 3 ) ( F ` x ) = if ( x = 1 , A , if ( x = 2 , B , C ) ) <-> A. x e. { 1 , 2 , 3 } ( F ` x ) = if ( x = 1 , A , if ( x = 2 , B , C ) ) ) |
18 |
|
1ex |
|- 1 e. _V |
19 |
|
2ex |
|- 2 e. _V |
20 |
|
3ex |
|- 3 e. _V |
21 |
|
fveq2 |
|- ( x = 1 -> ( F ` x ) = ( F ` 1 ) ) |
22 |
|
iftrue |
|- ( x = 1 -> if ( x = 1 , A , if ( x = 2 , B , C ) ) = A ) |
23 |
21 22
|
eqeq12d |
|- ( x = 1 -> ( ( F ` x ) = if ( x = 1 , A , if ( x = 2 , B , C ) ) <-> ( F ` 1 ) = A ) ) |
24 |
|
fveq2 |
|- ( x = 2 -> ( F ` x ) = ( F ` 2 ) ) |
25 |
|
1re |
|- 1 e. RR |
26 |
|
1lt2 |
|- 1 < 2 |
27 |
25 26
|
gtneii |
|- 2 =/= 1 |
28 |
|
neeq1 |
|- ( x = 2 -> ( x =/= 1 <-> 2 =/= 1 ) ) |
29 |
27 28
|
mpbiri |
|- ( x = 2 -> x =/= 1 ) |
30 |
|
ifnefalse |
|- ( x =/= 1 -> if ( x = 1 , A , if ( x = 2 , B , C ) ) = if ( x = 2 , B , C ) ) |
31 |
29 30
|
syl |
|- ( x = 2 -> if ( x = 1 , A , if ( x = 2 , B , C ) ) = if ( x = 2 , B , C ) ) |
32 |
|
iftrue |
|- ( x = 2 -> if ( x = 2 , B , C ) = B ) |
33 |
31 32
|
eqtrd |
|- ( x = 2 -> if ( x = 1 , A , if ( x = 2 , B , C ) ) = B ) |
34 |
24 33
|
eqeq12d |
|- ( x = 2 -> ( ( F ` x ) = if ( x = 1 , A , if ( x = 2 , B , C ) ) <-> ( F ` 2 ) = B ) ) |
35 |
|
fveq2 |
|- ( x = 3 -> ( F ` x ) = ( F ` 3 ) ) |
36 |
|
1lt3 |
|- 1 < 3 |
37 |
25 36
|
gtneii |
|- 3 =/= 1 |
38 |
|
neeq1 |
|- ( x = 3 -> ( x =/= 1 <-> 3 =/= 1 ) ) |
39 |
37 38
|
mpbiri |
|- ( x = 3 -> x =/= 1 ) |
40 |
39 30
|
syl |
|- ( x = 3 -> if ( x = 1 , A , if ( x = 2 , B , C ) ) = if ( x = 2 , B , C ) ) |
41 |
|
2re |
|- 2 e. RR |
42 |
|
2lt3 |
|- 2 < 3 |
43 |
41 42
|
gtneii |
|- 3 =/= 2 |
44 |
|
neeq1 |
|- ( x = 3 -> ( x =/= 2 <-> 3 =/= 2 ) ) |
45 |
43 44
|
mpbiri |
|- ( x = 3 -> x =/= 2 ) |
46 |
|
ifnefalse |
|- ( x =/= 2 -> if ( x = 2 , B , C ) = C ) |
47 |
45 46
|
syl |
|- ( x = 3 -> if ( x = 2 , B , C ) = C ) |
48 |
40 47
|
eqtrd |
|- ( x = 3 -> if ( x = 1 , A , if ( x = 2 , B , C ) ) = C ) |
49 |
35 48
|
eqeq12d |
|- ( x = 3 -> ( ( F ` x ) = if ( x = 1 , A , if ( x = 2 , B , C ) ) <-> ( F ` 3 ) = C ) ) |
50 |
18 19 20 23 34 49
|
raltp |
|- ( A. x e. { 1 , 2 , 3 } ( F ` x ) = if ( x = 1 , A , if ( x = 2 , B , C ) ) <-> ( ( F ` 1 ) = A /\ ( F ` 2 ) = B /\ ( F ` 3 ) = C ) ) |
51 |
17 50
|
bitri |
|- ( A. x e. ( 1 ... 3 ) ( F ` x ) = if ( x = 1 , A , if ( x = 2 , B , C ) ) <-> ( ( F ` 1 ) = A /\ ( F ` 2 ) = B /\ ( F ` 3 ) = C ) ) |