ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  fiintim Unicode version

Theorem fiintim 6783
Description: If a class is closed under pairwise intersections, then it is closed under nonempty finite intersections. The converse would appear to require an additional condition, such as  x and  y not being equal, or  A having decidable equality.

This theorem is applicable to a topology, which (among other axioms) is closed under finite intersections. Some texts use a pairwise intersection and some texts use a finite intersection, but most topology texts assume excluded middle (in which case the two intersection properties would be equivalent). (Contributed by NM, 22-Sep-2002.) (Revised by Jim Kingdon, 14-Jan-2023.)

Assertion
Ref Expression
fiintim  |-  ( A. x  e.  A  A. y  e.  A  (
x  i^i  y )  e.  A  ->  A. x
( ( x  C_  A  /\  x  =/=  (/)  /\  x  e.  Fin )  ->  |^| x  e.  A ) )
Distinct variable group:    x, y, A

Proof of Theorem fiintim
Dummy variables  z  w  v  f are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isfi 6621 . . . . . 6  |-  ( x  e.  Fin  <->  E. y  e.  om  x  ~~  y
)
2 ensym 6641 . . . . . . . 8  |-  ( x 
~~  y  ->  y  ~~  x )
3 breq1 3900 . . . . . . . . . . . . . . 15  |-  ( y  =  (/)  ->  ( y 
~~  x  <->  (/)  ~~  x
) )
43anbi2d 457 . . . . . . . . . . . . . 14  |-  ( y  =  (/)  ->  ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  y  ~~  x )  <->  ( (
x  C_  A  /\  x  =/=  (/) )  /\  (/)  ~~  x
) ) )
54imbi1d 230 . . . . . . . . . . . . 13  |-  ( y  =  (/)  ->  ( ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  y  ~~  x )  ->  |^| x  e.  A
)  <->  ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  (/)  ~~  x
)  ->  |^| x  e.  A ) ) )
65albidv 1778 . . . . . . . . . . . 12  |-  ( y  =  (/)  ->  ( A. x ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  y  ~~  x )  ->  |^| x  e.  A )  <->  A. x
( ( ( x 
C_  A  /\  x  =/=  (/) )  /\  (/)  ~~  x
)  ->  |^| x  e.  A ) ) )
7 breq1 3900 . . . . . . . . . . . . . . 15  |-  ( y  =  v  ->  (
y  ~~  x  <->  v  ~~  x ) )
87anbi2d 457 . . . . . . . . . . . . . 14  |-  ( y  =  v  ->  (
( ( x  C_  A  /\  x  =/=  (/) )  /\  y  ~~  x )  <->  ( (
x  C_  A  /\  x  =/=  (/) )  /\  v  ~~  x ) ) )
98imbi1d 230 . . . . . . . . . . . . 13  |-  ( y  =  v  ->  (
( ( ( x 
C_  A  /\  x  =/=  (/) )  /\  y  ~~  x )  ->  |^| x  e.  A )  <->  ( (
( x  C_  A  /\  x  =/=  (/) )  /\  v  ~~  x )  ->  |^| x  e.  A
) ) )
109albidv 1778 . . . . . . . . . . . 12  |-  ( y  =  v  ->  ( A. x ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  y  ~~  x )  ->  |^| x  e.  A )  <->  A. x
( ( ( x 
C_  A  /\  x  =/=  (/) )  /\  v  ~~  x )  ->  |^| x  e.  A ) ) )
11 breq1 3900 . . . . . . . . . . . . . . 15  |-  ( y  =  suc  v  -> 
( y  ~~  x  <->  suc  v  ~~  x ) )
1211anbi2d 457 . . . . . . . . . . . . . 14  |-  ( y  =  suc  v  -> 
( ( ( x 
C_  A  /\  x  =/=  (/) )  /\  y  ~~  x )  <->  ( (
x  C_  A  /\  x  =/=  (/) )  /\  suc  v  ~~  x ) ) )
1312imbi1d 230 . . . . . . . . . . . . 13  |-  ( y  =  suc  v  -> 
( ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  y  ~~  x )  ->  |^| x  e.  A )  <->  ( (
( x  C_  A  /\  x  =/=  (/) )  /\  suc  v  ~~  x )  ->  |^| x  e.  A
) ) )
1413albidv 1778 . . . . . . . . . . . 12  |-  ( y  =  suc  v  -> 
( A. x ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  y  ~~  x )  ->  |^| x  e.  A
)  <->  A. x ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  suc  v  ~~  x )  ->  |^| x  e.  A
) ) )
15 ensym 6641 . . . . . . . . . . . . . . . . . . 19  |-  ( (/)  ~~  x  ->  x  ~~  (/) )
16 en0 6655 . . . . . . . . . . . . . . . . . . 19  |-  ( x 
~~  (/)  <->  x  =  (/) )
1715, 16sylib 121 . . . . . . . . . . . . . . . . . 18  |-  ( (/)  ~~  x  ->  x  =  (/) )
1817anim1i 336 . . . . . . . . . . . . . . . . 17  |-  ( (
(/)  ~~  x  /\  x  =/=  (/) )  ->  (
x  =  (/)  /\  x  =/=  (/) ) )
1918ancoms 266 . . . . . . . . . . . . . . . 16  |-  ( ( x  =/=  (/)  /\  (/)  ~~  x
)  ->  ( x  =  (/)  /\  x  =/=  (/) ) )
2019adantll 465 . . . . . . . . . . . . . . 15  |-  ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  (/)  ~~  x )  ->  (
x  =  (/)  /\  x  =/=  (/) ) )
21 df-ne 2284 . . . . . . . . . . . . . . . 16  |-  ( x  =/=  (/)  <->  -.  x  =  (/) )
22 pm3.24 665 . . . . . . . . . . . . . . . . 17  |-  -.  (
x  =  (/)  /\  -.  x  =  (/) )
2322pm2.21i 618 . . . . . . . . . . . . . . . 16  |-  ( ( x  =  (/)  /\  -.  x  =  (/) )  ->  |^| x  e.  A
)
2421, 23sylan2b 283 . . . . . . . . . . . . . . 15  |-  ( ( x  =  (/)  /\  x  =/=  (/) )  ->  |^| x  e.  A )
2520, 24syl 14 . . . . . . . . . . . . . 14  |-  ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  (/)  ~~  x )  ->  |^| x  e.  A )
2625ax-gen 1408 . . . . . . . . . . . . 13  |-  A. x
( ( ( x 
C_  A  /\  x  =/=  (/) )  /\  (/)  ~~  x
)  ->  |^| x  e.  A )
2726a1i 9 . . . . . . . . . . . 12  |-  ( A. z  e.  A  A. w  e.  A  (
z  i^i  w )  e.  A  ->  A. x
( ( ( x 
C_  A  /\  x  =/=  (/) )  /\  (/)  ~~  x
)  ->  |^| x  e.  A ) )
28 nfv 1491 . . . . . . . . . . . . . 14  |-  F/ x
( v  e.  om  /\ 
A. z  e.  A  A. w  e.  A  ( z  i^i  w
)  e.  A )
29 nfa1 1504 . . . . . . . . . . . . . 14  |-  F/ x A. x ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  v  ~~  x )  ->  |^| x  e.  A )
30 simpl 108 . . . . . . . . . . . . . . . . 17  |-  ( ( x  C_  A  /\  x  =/=  (/) )  ->  x  C_  A )
31 bren 6607 . . . . . . . . . . . . . . . . . . 19  |-  ( suc  v  ~~  x  <->  E. f 
f : suc  v -1-1-onto-> x
)
32 ssel 3059 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x 
C_  A  ->  (
( f `  v
)  e.  x  -> 
( f `  v
)  e.  A ) )
33 f1of 5333 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( f : suc  v -1-1-onto-> x  -> 
f : suc  v --> x )
34 vex 2661 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  v  e. 
_V
3534sucid 4307 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  v  e. 
suc  v
36 ffvelrn 5519 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( f : suc  v --> x  /\  v  e.  suc  v )  ->  (
f `  v )  e.  x )
3733, 35, 36sylancl 407 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( f : suc  v -1-1-onto-> x  -> 
( f `  v
)  e.  x )
3832, 37impel 276 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( x  C_  A  /\  f : suc  v -1-1-onto-> x )  ->  ( f `  v )  e.  A
)
3938adantr 272 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( x  C_  A  /\  f : suc  v -1-1-onto-> x
)  /\  ( A. x ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  v  ~~  x )  ->  |^| x  e.  A )  /\  A. z  e.  A  A. w  e.  A  (
z  i^i  w )  e.  A ) )  -> 
( f `  v
)  e.  A )
4039adantlll 469 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( v  e. 
om  /\  x  C_  A
)  /\  f : suc  v -1-1-onto-> x )  /\  ( A. x ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  v  ~~  x )  ->  |^| x  e.  A )  /\  A. z  e.  A  A. w  e.  A  (
z  i^i  w )  e.  A ) )  -> 
( f `  v
)  e.  A )
41 imaeq2 4845 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( v  =  (/)  ->  ( f
" v )  =  ( f " (/) ) )
42 ima0 4866 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( f
" (/) )  =  (/)
4341, 42syl6eq 2164 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( v  =  (/)  ->  ( f
" v )  =  (/) )
44 inteq 3742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( f " v )  =  (/)  ->  |^| (
f " v )  =  |^| (/) )
45 int0 3753 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  |^| (/)  =  _V
4644, 45syl6eq 2164 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( f " v )  =  (/)  ->  |^| (
f " v )  =  _V )
4746ineq1d 3244 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( f " v )  =  (/)  ->  ( |^| ( f " v
)  i^i  ( f `  v ) )  =  ( _V  i^i  (
f `  v )
) )
48 ssv 3087 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( f `
 v )  C_  _V
49 sseqin2 3263 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( f `  v ) 
C_  _V  <->  ( _V  i^i  ( f `  v
) )  =  ( f `  v ) )
5048, 49mpbi 144 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( _V 
i^i  ( f `  v ) )  =  ( f `  v
)
5147, 50syl6eq 2164 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( f " v )  =  (/)  ->  ( |^| ( f " v
)  i^i  ( f `  v ) )  =  ( f `  v
) )
5251eleq1d 2184 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( f " v )  =  (/)  ->  ( (
|^| ( f "
v )  i^i  (
f `  v )
)  e.  A  <->  ( f `  v )  e.  A
) )
5352biimprd 157 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( f " v )  =  (/)  ->  ( ( f `  v )  e.  A  ->  ( |^| ( f " v
)  i^i  ( f `  v ) )  e.  A ) )
5443, 53syl 14 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( v  =  (/)  ->  ( ( f `  v )  e.  A  ->  ( |^| ( f " v
)  i^i  ( f `  v ) )  e.  A ) )
5554adantl 273 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( v  e.  om  /\  x  C_  A )  /\  f : suc  v -1-1-onto-> x )  /\  ( A. x ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  v  ~~  x )  ->  |^| x  e.  A )  /\  A. z  e.  A  A. w  e.  A  (
z  i^i  w )  e.  A ) )  /\  v  =  (/) )  -> 
( ( f `  v )  e.  A  ->  ( |^| ( f
" v )  i^i  ( f `  v
) )  e.  A
) )
56 f1ofun 5335 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( f : suc  v -1-1-onto-> x  ->  Fun  f )
5756ad3antlr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( v  e.  om  /\  x  C_  A )  /\  f : suc  v -1-1-onto-> x )  /\  ( A. x ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  v  ~~  x )  ->  |^| x  e.  A )  /\  A. z  e.  A  A. w  e.  A  (
z  i^i  w )  e.  A ) )  /\  (/) 
e.  v )  ->  Fun  f )
58 elelsuc 4299 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (/)  e.  v  ->  (/)  e.  suc  v )
5958adantl 273 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( v  e.  om  /\  x  C_  A )  /\  f : suc  v -1-1-onto-> x )  /\  ( A. x ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  v  ~~  x )  ->  |^| x  e.  A )  /\  A. z  e.  A  A. w  e.  A  (
z  i^i  w )  e.  A ) )  /\  (/) 
e.  v )  ->  (/) 
e.  suc  v )
60 f1odm 5337 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( f : suc  v -1-1-onto-> x  ->  dom  f  =  suc  v )
6160eleq2d 2185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( f : suc  v -1-1-onto-> x  -> 
( (/)  e.  dom  f  <->  (/)  e.  suc  v ) )
6261ad3antlr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( v  e.  om  /\  x  C_  A )  /\  f : suc  v -1-1-onto-> x )  /\  ( A. x ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  v  ~~  x )  ->  |^| x  e.  A )  /\  A. z  e.  A  A. w  e.  A  (
z  i^i  w )  e.  A ) )  /\  (/) 
e.  v )  -> 
( (/)  e.  dom  f  <->  (/)  e.  suc  v ) )
6359, 62mpbird 166 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( v  e.  om  /\  x  C_  A )  /\  f : suc  v -1-1-onto-> x )  /\  ( A. x ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  v  ~~  x )  ->  |^| x  e.  A )  /\  A. z  e.  A  A. w  e.  A  (
z  i^i  w )  e.  A ) )  /\  (/) 
e.  v )  ->  (/) 
e.  dom  f )
6457, 63jca 302 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( v  e.  om  /\  x  C_  A )  /\  f : suc  v -1-1-onto-> x )  /\  ( A. x ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  v  ~~  x )  ->  |^| x  e.  A )  /\  A. z  e.  A  A. w  e.  A  (
z  i^i  w )  e.  A ) )  /\  (/) 
e.  v )  -> 
( Fun  f  /\  (/) 
e.  dom  f )
)
65 simpr 109 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( v  e.  om  /\  x  C_  A )  /\  f : suc  v -1-1-onto-> x )  /\  ( A. x ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  v  ~~  x )  ->  |^| x  e.  A )  /\  A. z  e.  A  A. w  e.  A  (
z  i^i  w )  e.  A ) )  /\  (/) 
e.  v )  ->  (/) 
e.  v )
66 funfvima 5615 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( Fun  f  /\  (/)  e.  dom  f )  ->  ( (/) 
e.  v  ->  (
f `  (/) )  e.  ( f " v
) ) )
6764, 65, 66sylc 62 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( v  e.  om  /\  x  C_  A )  /\  f : suc  v -1-1-onto-> x )  /\  ( A. x ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  v  ~~  x )  ->  |^| x  e.  A )  /\  A. z  e.  A  A. w  e.  A  (
z  i^i  w )  e.  A ) )  /\  (/) 
e.  v )  -> 
( f `  (/) )  e.  ( f " v
) )
68 ne0i 3337 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( f `  (/) )  e.  ( f " v
)  ->  ( f " v )  =/=  (/) )
6967, 68syl 14 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( v  e.  om  /\  x  C_  A )  /\  f : suc  v -1-1-onto-> x )  /\  ( A. x ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  v  ~~  x )  ->  |^| x  e.  A )  /\  A. z  e.  A  A. w  e.  A  (
z  i^i  w )  e.  A ) )  /\  (/) 
e.  v )  -> 
( f " v
)  =/=  (/) )
70 imassrn 4860 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( f
" v )  C_  ran  f
71 dff1o2 5338 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( f : suc  v -1-1-onto-> x  <->  ( f  Fn  suc  v  /\  Fun  `' f  /\  ran  f  =  x ) )
7271simp3bi 981 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( f : suc  v -1-1-onto-> x  ->  ran  f  =  x
)
7370, 72sseqtrid 3115 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( f : suc  v -1-1-onto-> x  -> 
( f " v
)  C_  x )
74 sstr2 3072 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( f " v ) 
C_  x  ->  (
x  C_  A  ->  ( f " v ) 
C_  A ) )
7573, 74syl 14 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( f : suc  v -1-1-onto-> x  -> 
( x  C_  A  ->  ( f " v
)  C_  A )
)
7675anim1d 332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( f : suc  v -1-1-onto-> x  -> 
( ( x  C_  A  /\  ( f "
v )  =/=  (/) )  -> 
( ( f "
v )  C_  A  /\  ( f " v
)  =/=  (/) ) ) )
77 f1of1 5332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( f : suc  v -1-1-onto-> x  -> 
f : suc  v -1-1->
x )
78 vex 2661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  x  e. 
_V
79 sssucid 4305 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  v  C_  suc  v
80 f1imaen2g 6653 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( f : suc  v -1-1-> x  /\  x  e.  _V )  /\  (
v  C_  suc  v  /\  v  e.  _V )
)  ->  ( f " v )  ~~  v )
8179, 34, 80mpanr12 433 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( f : suc  v -1-1->
x  /\  x  e.  _V )  ->  ( f
" v )  ~~  v )
8277, 78, 81sylancl 407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( f : suc  v -1-1-onto-> x  -> 
( f " v
)  ~~  v )
8382ensymd 6643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( f : suc  v -1-1-onto-> x  -> 
v  ~~  ( f " v ) )
8476, 83jctird 313 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( f : suc  v -1-1-onto-> x  -> 
( ( x  C_  A  /\  ( f "
v )  =/=  (/) )  -> 
( ( ( f
" v )  C_  A  /\  ( f "
v )  =/=  (/) )  /\  v  ~~  ( f "
v ) ) ) )
85 vex 2661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  f  e. 
_V
8685imaex 4862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( f
" v )  e. 
_V
87 sseq1 3088 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( x  =  ( f "
v )  ->  (
x  C_  A  <->  ( f " v )  C_  A ) )
88 neeq1 2296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( x  =  ( f "
v )  ->  (
x  =/=  (/)  <->  ( f " v )  =/=  (/) ) )
8987, 88anbi12d 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( x  =  ( f "
v )  ->  (
( x  C_  A  /\  x  =/=  (/) )  <->  ( (
f " v ) 
C_  A  /\  (
f " v )  =/=  (/) ) ) )
90 breq2 3901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( x  =  ( f "
v )  ->  (
v  ~~  x  <->  v  ~~  ( f " v
) ) )
9189, 90anbi12d 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( x  =  ( f "
v )  ->  (
( ( x  C_  A  /\  x  =/=  (/) )  /\  v  ~~  x )  <->  ( (
( f " v
)  C_  A  /\  ( f " v
)  =/=  (/) )  /\  v  ~~  ( f "
v ) ) ) )
92 inteq 3742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( x  =  ( f "
v )  ->  |^| x  =  |^| ( f "
v ) )
9392eleq1d 2184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( x  =  ( f "
v )  ->  ( |^| x  e.  A  <->  |^| ( f " v
)  e.  A ) )
9491, 93imbi12d 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( x  =  ( f "
v )  ->  (
( ( ( x 
C_  A  /\  x  =/=  (/) )  /\  v  ~~  x )  ->  |^| x  e.  A )  <->  ( (
( ( f "
v )  C_  A  /\  ( f " v
)  =/=  (/) )  /\  v  ~~  ( f "
v ) )  ->  |^| ( f " v
)  e.  A ) ) )
9586, 94spcv 2751 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( A. x ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  v  ~~  x )  ->  |^| x  e.  A )  ->  (
( ( ( f
" v )  C_  A  /\  ( f "
v )  =/=  (/) )  /\  v  ~~  ( f "
v ) )  ->  |^| ( f " v
)  e.  A ) )
9684, 95sylan9 404 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( f : suc  v -1-1-onto-> x  /\  A. x ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  v  ~~  x )  ->  |^| x  e.  A
) )  ->  (
( x  C_  A  /\  ( f " v
)  =/=  (/) )  ->  |^| ( f " v
)  e.  A ) )
97 ineq1 3238 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( z  =  |^| ( f
" v )  -> 
( z  i^i  w
)  =  ( |^| ( f " v
)  i^i  w )
)
9897eleq1d 2184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( z  =  |^| ( f
" v )  -> 
( ( z  i^i  w )  e.  A  <->  (
|^| ( f "
v )  i^i  w
)  e.  A ) )
99 ineq2 3239 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( w  =  ( f `  v )  ->  ( |^| ( f " v
)  i^i  w )  =  ( |^| (
f " v )  i^i  ( f `  v ) ) )
10099eleq1d 2184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( w  =  ( f `  v )  ->  (
( |^| ( f "
v )  i^i  w
)  e.  A  <->  ( |^| ( f " v
)  i^i  ( f `  v ) )  e.  A ) )
10198, 100rspc2v 2774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
|^| ( f "
v )  e.  A  /\  ( f `  v
)  e.  A )  ->  ( A. z  e.  A  A. w  e.  A  ( z  i^i  w )  e.  A  ->  ( |^| ( f
" v )  i^i  ( f `  v
) )  e.  A
) )
102101ex 114 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( |^| ( f " v
)  e.  A  -> 
( ( f `  v )  e.  A  ->  ( A. z  e.  A  A. w  e.  A  ( z  i^i  w )  e.  A  ->  ( |^| ( f
" v )  i^i  ( f `  v
) )  e.  A
) ) )
10396, 102syl6 33 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( f : suc  v -1-1-onto-> x  /\  A. x ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  v  ~~  x )  ->  |^| x  e.  A
) )  ->  (
( x  C_  A  /\  ( f " v
)  =/=  (/) )  -> 
( ( f `  v )  e.  A  ->  ( A. z  e.  A  A. w  e.  A  ( z  i^i  w )  e.  A  ->  ( |^| ( f
" v )  i^i  ( f `  v
) )  e.  A
) ) ) )
104103com4r 86 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( A. z  e.  A  A. w  e.  A  (
z  i^i  w )  e.  A  ->  ( ( f : suc  v -1-1-onto-> x  /\  A. x ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  v  ~~  x )  ->  |^| x  e.  A
) )  ->  (
( x  C_  A  /\  ( f " v
)  =/=  (/) )  -> 
( ( f `  v )  e.  A  ->  ( |^| ( f
" v )  i^i  ( f `  v
) )  e.  A
) ) ) )
105104exp5c 371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( A. z  e.  A  A. w  e.  A  (
z  i^i  w )  e.  A  ->  ( f : suc  v -1-1-onto-> x  -> 
( A. x ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  v  ~~  x )  ->  |^| x  e.  A
)  ->  ( x  C_  A  ->  ( (
f " v )  =/=  (/)  ->  ( (
f `  v )  e.  A  ->  ( |^| ( f " v
)  i^i  ( f `  v ) )  e.  A ) ) ) ) ) )
106105com14 88 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x 
C_  A  ->  (
f : suc  v -1-1-onto-> x  ->  ( A. x ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  v  ~~  x )  ->  |^| x  e.  A
)  ->  ( A. z  e.  A  A. w  e.  A  (
z  i^i  w )  e.  A  ->  ( ( f " v )  =/=  (/)  ->  ( (
f `  v )  e.  A  ->  ( |^| ( f " v
)  i^i  ( f `  v ) )  e.  A ) ) ) ) ) )
107106imp43 350 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( x  C_  A  /\  f : suc  v -1-1-onto-> x
)  /\  ( A. x ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  v  ~~  x )  ->  |^| x  e.  A )  /\  A. z  e.  A  A. w  e.  A  (
z  i^i  w )  e.  A ) )  -> 
( ( f "
v )  =/=  (/)  ->  (
( f `  v
)  e.  A  -> 
( |^| ( f "
v )  i^i  (
f `  v )
)  e.  A ) ) )
108107adantlll 469 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( v  e. 
om  /\  x  C_  A
)  /\  f : suc  v -1-1-onto-> x )  /\  ( A. x ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  v  ~~  x )  ->  |^| x  e.  A )  /\  A. z  e.  A  A. w  e.  A  (
z  i^i  w )  e.  A ) )  -> 
( ( f "
v )  =/=  (/)  ->  (
( f `  v
)  e.  A  -> 
( |^| ( f "
v )  i^i  (
f `  v )
)  e.  A ) ) )
109108adantr 272 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( v  e.  om  /\  x  C_  A )  /\  f : suc  v -1-1-onto-> x )  /\  ( A. x ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  v  ~~  x )  ->  |^| x  e.  A )  /\  A. z  e.  A  A. w  e.  A  (
z  i^i  w )  e.  A ) )  /\  (/) 
e.  v )  -> 
( ( f "
v )  =/=  (/)  ->  (
( f `  v
)  e.  A  -> 
( |^| ( f "
v )  i^i  (
f `  v )
)  e.  A ) ) )
11069, 109mpd 13 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( v  e.  om  /\  x  C_  A )  /\  f : suc  v -1-1-onto-> x )  /\  ( A. x ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  v  ~~  x )  ->  |^| x  e.  A )  /\  A. z  e.  A  A. w  e.  A  (
z  i^i  w )  e.  A ) )  /\  (/) 
e.  v )  -> 
( ( f `  v )  e.  A  ->  ( |^| ( f
" v )  i^i  ( f `  v
) )  e.  A
) )
111 0elnn 4500 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( v  e.  om  ->  (
v  =  (/)  \/  (/)  e.  v ) )
112111ad3antrrr 481 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( v  e. 
om  /\  x  C_  A
)  /\  f : suc  v -1-1-onto-> x )  /\  ( A. x ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  v  ~~  x )  ->  |^| x  e.  A )  /\  A. z  e.  A  A. w  e.  A  (
z  i^i  w )  e.  A ) )  -> 
( v  =  (/)  \/  (/)  e.  v ) )
11355, 110, 112mpjaodan 770 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( v  e. 
om  /\  x  C_  A
)  /\  f : suc  v -1-1-onto-> x )  /\  ( A. x ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  v  ~~  x )  ->  |^| x  e.  A )  /\  A. z  e.  A  A. w  e.  A  (
z  i^i  w )  e.  A ) )  -> 
( ( f `  v )  e.  A  ->  ( |^| ( f
" v )  i^i  ( f `  v
) )  e.  A
) )
11440, 113mpd 13 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( v  e. 
om  /\  x  C_  A
)  /\  f : suc  v -1-1-onto-> x )  /\  ( A. x ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  v  ~~  x )  ->  |^| x  e.  A )  /\  A. z  e.  A  A. w  e.  A  (
z  i^i  w )  e.  A ) )  -> 
( |^| ( f "
v )  i^i  (
f `  v )
)  e.  A )
11585, 34fvex 5407 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( f `
 v )  e. 
_V
116115intunsn 3777 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  |^| (
( f " v
)  u.  { ( f `  v ) } )  =  (
|^| ( f "
v )  i^i  (
f `  v )
)
117 f1ofn 5334 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( f : suc  v -1-1-onto-> x  -> 
f  Fn  suc  v
)
118 fnsnfv 5446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( f  Fn  suc  v  /\  v  e.  suc  v )  ->  { ( f `  v ) }  =  ( f
" { v } ) )
119117, 35, 118sylancl 407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( f : suc  v -1-1-onto-> x  ->  { ( f `  v ) }  =  ( f " {
v } ) )
120119uneq2d 3198 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( f : suc  v -1-1-onto-> x  -> 
( ( f "
v )  u.  {
( f `  v
) } )  =  ( ( f "
v )  u.  (
f " { v } ) ) )
121 df-suc 4261 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  suc  v  =  ( v  u. 
{ v } )
122121imaeq2i 4847 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( f
" suc  v )  =  ( f "
( v  u.  {
v } ) )
123 imaundi 4919 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( f
" ( v  u. 
{ v } ) )  =  ( ( f " v )  u.  ( f " { v } ) )
124122, 123eqtr2i 2137 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( f " v )  u.  ( f " { v } ) )  =  ( f
" suc  v )
125120, 124syl6eq 2164 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( f : suc  v -1-1-onto-> x  -> 
( ( f "
v )  u.  {
( f `  v
) } )  =  ( f " suc  v ) )
126 f1ofo 5340 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( f : suc  v -1-1-onto-> x  -> 
f : suc  v -onto->
x )
127 foima 5318 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( f : suc  v -onto-> x  ->  ( f " suc  v )  =  x )
128126, 127syl 14 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( f : suc  v -1-1-onto-> x  -> 
( f " suc  v )  =  x )
129125, 128eqtrd 2148 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( f : suc  v -1-1-onto-> x  -> 
( ( f "
v )  u.  {
( f `  v
) } )  =  x )
130129inteqd 3744 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( f : suc  v -1-1-onto-> x  ->  |^| ( ( f "
v )  u.  {
( f `  v
) } )  = 
|^| x )
131116, 130syl5eqr 2162 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( f : suc  v -1-1-onto-> x  -> 
( |^| ( f "
v )  i^i  (
f `  v )
)  =  |^| x
)
132131eleq1d 2184 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( f : suc  v -1-1-onto-> x  -> 
( ( |^| (
f " v )  i^i  ( f `  v ) )  e.  A  <->  |^| x  e.  A
) )
133132ad2antlr 478 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( v  e. 
om  /\  x  C_  A
)  /\  f : suc  v -1-1-onto-> x )  /\  ( A. x ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  v  ~~  x )  ->  |^| x  e.  A )  /\  A. z  e.  A  A. w  e.  A  (
z  i^i  w )  e.  A ) )  -> 
( ( |^| (
f " v )  i^i  ( f `  v ) )  e.  A  <->  |^| x  e.  A
) )
134114, 133mpbid 146 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( v  e. 
om  /\  x  C_  A
)  /\  f : suc  v -1-1-onto-> x )  /\  ( A. x ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  v  ~~  x )  ->  |^| x  e.  A )  /\  A. z  e.  A  A. w  e.  A  (
z  i^i  w )  e.  A ) )  ->  |^| x  e.  A
)
135134exp43 367 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( v  e.  om  /\  x  C_  A )  -> 
( f : suc  v
-1-1-onto-> x  ->  ( A. x
( ( ( x 
C_  A  /\  x  =/=  (/) )  /\  v  ~~  x )  ->  |^| x  e.  A )  ->  ( A. z  e.  A  A. w  e.  A  ( z  i^i  w
)  e.  A  ->  |^| x  e.  A
) ) ) )
136135exlimdv 1773 . . . . . . . . . . . . . . . . . . 19  |-  ( ( v  e.  om  /\  x  C_  A )  -> 
( E. f  f : suc  v -1-1-onto-> x  -> 
( A. x ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  v  ~~  x )  ->  |^| x  e.  A
)  ->  ( A. z  e.  A  A. w  e.  A  (
z  i^i  w )  e.  A  ->  |^| x  e.  A ) ) ) )
13731, 136syl5bi 151 . . . . . . . . . . . . . . . . . 18  |-  ( ( v  e.  om  /\  x  C_  A )  -> 
( suc  v  ~~  x  ->  ( A. x
( ( ( x 
C_  A  /\  x  =/=  (/) )  /\  v  ~~  x )  ->  |^| x  e.  A )  ->  ( A. z  e.  A  A. w  e.  A  ( z  i^i  w
)  e.  A  ->  |^| x  e.  A
) ) ) )
138137expimpd 358 . . . . . . . . . . . . . . . . 17  |-  ( v  e.  om  ->  (
( x  C_  A  /\  suc  v  ~~  x
)  ->  ( A. x ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  v  ~~  x )  ->  |^| x  e.  A )  ->  ( A. z  e.  A  A. w  e.  A  ( z  i^i  w
)  e.  A  ->  |^| x  e.  A
) ) ) )
13930, 138sylani 401 . . . . . . . . . . . . . . . 16  |-  ( v  e.  om  ->  (
( ( x  C_  A  /\  x  =/=  (/) )  /\  suc  v  ~~  x )  ->  ( A. x
( ( ( x 
C_  A  /\  x  =/=  (/) )  /\  v  ~~  x )  ->  |^| x  e.  A )  ->  ( A. z  e.  A  A. w  e.  A  ( z  i^i  w
)  e.  A  ->  |^| x  e.  A
) ) ) )
140139com24 87 . . . . . . . . . . . . . . 15  |-  ( v  e.  om  ->  ( A. z  e.  A  A. w  e.  A  ( z  i^i  w
)  e.  A  -> 
( A. x ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  v  ~~  x )  ->  |^| x  e.  A
)  ->  ( (
( x  C_  A  /\  x  =/=  (/) )  /\  suc  v  ~~  x )  ->  |^| x  e.  A
) ) ) )
141140imp 123 . . . . . . . . . . . . . 14  |-  ( ( v  e.  om  /\  A. z  e.  A  A. w  e.  A  (
z  i^i  w )  e.  A )  ->  ( A. x ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  v  ~~  x )  ->  |^| x  e.  A )  ->  (
( ( x  C_  A  /\  x  =/=  (/) )  /\  suc  v  ~~  x )  ->  |^| x  e.  A
) ) )
14228, 29, 141alrimd 1572 . . . . . . . . . . . . 13  |-  ( ( v  e.  om  /\  A. z  e.  A  A. w  e.  A  (
z  i^i  w )  e.  A )  ->  ( A. x ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  v  ~~  x )  ->  |^| x  e.  A )  ->  A. x
( ( ( x 
C_  A  /\  x  =/=  (/) )  /\  suc  v  ~~  x )  ->  |^| x  e.  A
) ) )
143142ex 114 . . . . . . . . . . . 12  |-  ( v  e.  om  ->  ( A. z  e.  A  A. w  e.  A  ( z  i^i  w
)  e.  A  -> 
( A. x ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  v  ~~  x )  ->  |^| x  e.  A
)  ->  A. x
( ( ( x 
C_  A  /\  x  =/=  (/) )  /\  suc  v  ~~  x )  ->  |^| x  e.  A
) ) ) )
1446, 10, 14, 27, 143finds2 4483 . . . . . . . . . . 11  |-  ( y  e.  om  ->  ( A. z  e.  A  A. w  e.  A  ( z  i^i  w
)  e.  A  ->  A. x ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  y  ~~  x )  ->  |^| x  e.  A ) ) )
145 sp 1471 . . . . . . . . . . 11  |-  ( A. x ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  y  ~~  x )  ->  |^| x  e.  A )  ->  (
( ( x  C_  A  /\  x  =/=  (/) )  /\  y  ~~  x )  ->  |^| x  e.  A
) )
146144, 145syl6 33 . . . . . . . . . 10  |-  ( y  e.  om  ->  ( A. z  e.  A  A. w  e.  A  ( z  i^i  w
)  e.  A  -> 
( ( ( x 
C_  A  /\  x  =/=  (/) )  /\  y  ~~  x )  ->  |^| x  e.  A ) ) )
147146exp4a 361 . . . . . . . . 9  |-  ( y  e.  om  ->  ( A. z  e.  A  A. w  e.  A  ( z  i^i  w
)  e.  A  -> 
( ( x  C_  A  /\  x  =/=  (/) )  -> 
( y  ~~  x  ->  |^| x  e.  A
) ) ) )
148147com24 87 . . . . . . . 8  |-  ( y  e.  om  ->  (
y  ~~  x  ->  ( ( x  C_  A  /\  x  =/=  (/) )  -> 
( A. z  e.  A  A. w  e.  A  ( z  i^i  w )  e.  A  ->  |^| x  e.  A
) ) ) )
1492, 148syl5 32 . . . . . . 7  |-  ( y  e.  om  ->  (
x  ~~  y  ->  ( ( x  C_  A  /\  x  =/=  (/) )  -> 
( A. z  e.  A  A. w  e.  A  ( z  i^i  w )  e.  A  ->  |^| x  e.  A
) ) ) )
150149rexlimiv 2518 . . . . . 6  |-  ( E. y  e.  om  x  ~~  y  ->  ( ( x  C_  A  /\  x  =/=  (/) )  ->  ( A. z  e.  A  A. w  e.  A  ( z  i^i  w
)  e.  A  ->  |^| x  e.  A
) ) )
1511, 150sylbi 120 . . . . 5  |-  ( x  e.  Fin  ->  (
( x  C_  A  /\  x  =/=  (/) )  -> 
( A. z  e.  A  A. w  e.  A  ( z  i^i  w )  e.  A  ->  |^| x  e.  A
) ) )
152151com13 80 . . . 4  |-  ( A. z  e.  A  A. w  e.  A  (
z  i^i  w )  e.  A  ->  ( ( x  C_  A  /\  x  =/=  (/) )  ->  (
x  e.  Fin  ->  |^| x  e.  A ) ) )
153152impd 252 . . 3  |-  ( A. z  e.  A  A. w  e.  A  (
z  i^i  w )  e.  A  ->  ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  x  e.  Fin )  ->  |^| x  e.  A
) )
154153alrimiv 1828 . 2  |-  ( A. z  e.  A  A. w  e.  A  (
z  i^i  w )  e.  A  ->  A. x
( ( ( x 
C_  A  /\  x  =/=  (/) )  /\  x  e.  Fin )  ->  |^| x  e.  A ) )
155 ineq1 3238 . . . 4  |-  ( x  =  z  ->  (
x  i^i  y )  =  ( z  i^i  y ) )
156155eleq1d 2184 . . 3  |-  ( x  =  z  ->  (
( x  i^i  y
)  e.  A  <->  ( z  i^i  y )  e.  A
) )
157 ineq2 3239 . . . 4  |-  ( y  =  w  ->  (
z  i^i  y )  =  ( z  i^i  w ) )
158157eleq1d 2184 . . 3  |-  ( y  =  w  ->  (
( z  i^i  y
)  e.  A  <->  ( z  i^i  w )  e.  A
) )
159156, 158cbvral2v 2637 . 2  |-  ( A. x  e.  A  A. y  e.  A  (
x  i^i  y )  e.  A  <->  A. z  e.  A  A. w  e.  A  ( z  i^i  w
)  e.  A )
160 df-3an 947 . . . 4  |-  ( ( x  C_  A  /\  x  =/=  (/)  /\  x  e. 
Fin )  <->  ( (
x  C_  A  /\  x  =/=  (/) )  /\  x  e.  Fin ) )
161160imbi1i 237 . . 3  |-  ( ( ( x  C_  A  /\  x  =/=  (/)  /\  x  e.  Fin )  ->  |^| x  e.  A )  <->  ( (
( x  C_  A  /\  x  =/=  (/) )  /\  x  e.  Fin )  ->  |^| x  e.  A
) )
162161albii 1429 . 2  |-  ( A. x ( ( x 
C_  A  /\  x  =/=  (/)  /\  x  e. 
Fin )  ->  |^| x  e.  A )  <->  A. x
( ( ( x 
C_  A  /\  x  =/=  (/) )  /\  x  e.  Fin )  ->  |^| x  e.  A ) )
163154, 159, 1623imtr4i 200 1  |-  ( A. x  e.  A  A. y  e.  A  (
x  i^i  y )  e.  A  ->  A. x
( ( x  C_  A  /\  x  =/=  (/)  /\  x  e.  Fin )  ->  |^| x  e.  A ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 103    <-> wb 104    \/ wo 680    /\ w3a 945   A.wal 1312    = wceq 1314   E.wex 1451    e. wcel 1463    =/= wne 2283   A.wral 2391   E.wrex 2392   _Vcvv 2658    u. cun 3037    i^i cin 3038    C_ wss 3039   (/)c0 3331   {csn 3495   |^|cint 3739   class class class wbr 3897   suc csuc 4255   omcom 4472   `'ccnv 4506   dom cdm 4507   ran crn 4508   "cima 4510   Fun wfun 5085    Fn wfn 5086   -->wf 5087   -1-1->wf1 5088   -onto->wfo 5089   -1-1-onto->wf1o 5090   ` cfv 5091    ~~ cen 6598   Fincfn 6600
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-13 1474  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-sep 4014  ax-nul 4022  ax-pow 4066  ax-pr 4099  ax-un 4323  ax-iinf 4470
This theorem depends on definitions:  df-bi 116  df-3an 947  df-tru 1317  df-fal 1320  df-nf 1420  df-sb 1719  df-eu 1978  df-mo 1979  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-ne 2284  df-ral 2396  df-rex 2397  df-v 2660  df-sbc 2881  df-dif 3041  df-un 3043  df-in 3045  df-ss 3052  df-nul 3332  df-pw 3480  df-sn 3501  df-pr 3502  df-op 3504  df-uni 3705  df-int 3740  df-br 3898  df-opab 3958  df-id 4183  df-suc 4261  df-iom 4473  df-xp 4513  df-rel 4514  df-cnv 4515  df-co 4516  df-dm 4517  df-rn 4518  df-res 4519  df-ima 4520  df-iota 5056  df-fun 5093  df-fn 5094  df-f 5095  df-f1 5096  df-fo 5097  df-f1o 5098  df-fv 5099  df-er 6395  df-en 6601  df-fin 6603
This theorem is referenced by:  istopfin  12073
  Copyright terms: Public domain W3C validator