MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fiint Unicode version

Theorem fiint 7133
Description: Equivalent ways of stating the finite intersection property. We show two ways of saying, "the intersection of elements in every finite non-empty subcollection of 
A is in  A." This theorem is applicable to a topology, which (among other axioms) is closed under finite intersections. Some texts use the left-hand version of this axiom and others the right-hand version, but as our proof here shows, their "intuitively obvious" equivalence can be non-trivial to establish formally. (Contributed by NM, 22-Sep-2002.)
Assertion
Ref Expression
fiint  |-  ( 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 fiint
Dummy variables  z  w  v  f are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isfi 6885 . . . . . . 7  |-  ( x  e.  Fin  <->  E. y  e.  om  x  ~~  y
)
2 ensym 6910 . . . . . . . . 9  |-  ( x 
~~  y  ->  y  ~~  x )
3 breq1 4026 . . . . . . . . . . . . . . . 16  |-  ( y  =  (/)  ->  ( y 
~~  x  <->  (/)  ~~  x
) )
43anbi2d 684 . . . . . . . . . . . . . . 15  |-  ( y  =  (/)  ->  ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  y  ~~  x )  <->  ( (
x  C_  A  /\  x  =/=  (/) )  /\  (/)  ~~  x
) ) )
54imbi1d 308 . . . . . . . . . . . . . 14  |-  ( y  =  (/)  ->  ( ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  y  ~~  x )  ->  |^| x  e.  A
)  <->  ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  (/)  ~~  x
)  ->  |^| x  e.  A ) ) )
65albidv 1611 . . . . . . . . . . . . 13  |-  ( y  =  (/)  ->  ( A. x ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  y  ~~  x )  ->  |^| x  e.  A )  <->  A. x
( ( ( x 
C_  A  /\  x  =/=  (/) )  /\  (/)  ~~  x
)  ->  |^| x  e.  A ) ) )
7 breq1 4026 . . . . . . . . . . . . . . . 16  |-  ( y  =  v  ->  (
y  ~~  x  <->  v  ~~  x ) )
87anbi2d 684 . . . . . . . . . . . . . . 15  |-  ( y  =  v  ->  (
( ( x  C_  A  /\  x  =/=  (/) )  /\  y  ~~  x )  <->  ( (
x  C_  A  /\  x  =/=  (/) )  /\  v  ~~  x ) ) )
98imbi1d 308 . . . . . . . . . . . . . 14  |-  ( y  =  v  ->  (
( ( ( x 
C_  A  /\  x  =/=  (/) )  /\  y  ~~  x )  ->  |^| x  e.  A )  <->  ( (
( x  C_  A  /\  x  =/=  (/) )  /\  v  ~~  x )  ->  |^| x  e.  A
) ) )
109albidv 1611 . . . . . . . . . . . . 13  |-  ( 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 4026 . . . . . . . . . . . . . . . 16  |-  ( y  =  suc  v  -> 
( y  ~~  x  <->  suc  v  ~~  x ) )
1211anbi2d 684 . . . . . . . . . . . . . . 15  |-  ( y  =  suc  v  -> 
( ( ( x 
C_  A  /\  x  =/=  (/) )  /\  y  ~~  x )  <->  ( (
x  C_  A  /\  x  =/=  (/) )  /\  suc  v  ~~  x ) ) )
1312imbi1d 308 . . . . . . . . . . . . . 14  |-  ( y  =  suc  v  -> 
( ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  y  ~~  x )  ->  |^| x  e.  A )  <->  ( (
( x  C_  A  /\  x  =/=  (/) )  /\  suc  v  ~~  x )  ->  |^| x  e.  A
) ) )
1413albidv 1611 . . . . . . . . . . . . 13  |-  ( 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 6910 . . . . . . . . . . . . . . . . . . . 20  |-  ( (/)  ~~  x  ->  x  ~~  (/) )
16 en0 6924 . . . . . . . . . . . . . . . . . . . 20  |-  ( x 
~~  (/)  <->  x  =  (/) )
1715, 16sylib 188 . . . . . . . . . . . . . . . . . . 19  |-  ( (/)  ~~  x  ->  x  =  (/) )
1817anim1i 551 . . . . . . . . . . . . . . . . . 18  |-  ( (
(/)  ~~  x  /\  x  =/=  (/) )  ->  (
x  =  (/)  /\  x  =/=  (/) ) )
1918ancoms 439 . . . . . . . . . . . . . . . . 17  |-  ( ( x  =/=  (/)  /\  (/)  ~~  x
)  ->  ( x  =  (/)  /\  x  =/=  (/) ) )
2019adantll 694 . . . . . . . . . . . . . . . 16  |-  ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  (/)  ~~  x )  ->  (
x  =  (/)  /\  x  =/=  (/) ) )
21 df-ne 2448 . . . . . . . . . . . . . . . . 17  |-  ( x  =/=  (/)  <->  -.  x  =  (/) )
22 pm3.24 852 . . . . . . . . . . . . . . . . . 18  |-  -.  (
x  =  (/)  /\  -.  x  =  (/) )
2322pm2.21i 123 . . . . . . . . . . . . . . . . 17  |-  ( ( x  =  (/)  /\  -.  x  =  (/) )  ->  |^| x  e.  A
)
2421, 23sylan2b 461 . . . . . . . . . . . . . . . 16  |-  ( ( x  =  (/)  /\  x  =/=  (/) )  ->  |^| x  e.  A )
2520, 24syl 15 . . . . . . . . . . . . . . 15  |-  ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  (/)  ~~  x )  ->  |^| x  e.  A )
2625ax-gen 1533 . . . . . . . . . . . . . 14  |-  A. x
( ( ( x 
C_  A  /\  x  =/=  (/) )  /\  (/)  ~~  x
)  ->  |^| x  e.  A )
2726a1i 10 . . . . . . . . . . . . 13  |-  ( 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 1605 . . . . . . . . . . . . . . 15  |-  F/ x A. z  e.  A  A. w  e.  A  ( z  i^i  w
)  e.  A
29 nfa1 1756 . . . . . . . . . . . . . . 15  |-  F/ x A. x ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  v  ~~  x )  ->  |^| x  e.  A )
30 bren 6871 . . . . . . . . . . . . . . . . . . 19  |-  ( suc  v  ~~  x  <->  E. f 
f : suc  v -1-1-onto-> x
)
31 f1of 5472 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( f : suc  v -1-1-onto-> x  -> 
f : suc  v --> x )
32 vex 2791 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  v  e. 
_V
3332sucid 4471 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  v  e. 
suc  v
34 ffvelrn 5663 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( f : suc  v --> x  /\  v  e.  suc  v )  ->  (
f `  v )  e.  x )
3531, 33, 34sylancl 643 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( f : suc  v -1-1-onto-> x  -> 
( f `  v
)  e.  x )
36 ssel 3174 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x 
C_  A  ->  (
( f `  v
)  e.  x  -> 
( f `  v
)  e.  A ) )
3735, 36syl5 28 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x 
C_  A  ->  (
f : suc  v -1-1-onto-> x  ->  ( f `  v
)  e.  A ) )
3837imp 418 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  C_  A  /\  f : suc  v -1-1-onto-> x )  ->  ( f `  v )  e.  A
)
3938adantr 451 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( 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 )
40 df-ne 2448 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( f " v )  =/=  (/)  <->  -.  ( f " v )  =  (/) )
41 imassrn 5025 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( f
" v )  C_  ran  f
42 dff1o2 5477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( f : suc  v -1-1-onto-> x  <->  ( f  Fn  suc  v  /\  Fun  `' f  /\  ran  f  =  x ) )
4342simp3bi 972 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( f : suc  v -1-1-onto-> x  ->  ran  f  =  x
)
4441, 43syl5sseq 3226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( f : suc  v -1-1-onto-> x  -> 
( f " v
)  C_  x )
45 sstr2 3186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( f " v ) 
C_  x  ->  (
x  C_  A  ->  ( f " v ) 
C_  A ) )
4644, 45syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( f : suc  v -1-1-onto-> x  -> 
( x  C_  A  ->  ( f " v
)  C_  A )
)
4746anim1d 547 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( f : suc  v -1-1-onto-> x  -> 
( ( x  C_  A  /\  ( f "
v )  =/=  (/) )  -> 
( ( f "
v )  C_  A  /\  ( f " v
)  =/=  (/) ) ) )
48 f1of1 5471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( f : suc  v -1-1-onto-> x  -> 
f : suc  v -1-1->
x )
49 vex 2791 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  x  e. 
_V
50 sssucid 4469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  v  C_  suc  v
51 f1imaen2g 6922 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( f : suc  v -1-1-> x  /\  x  e.  _V )  /\  (
v  C_  suc  v  /\  v  e.  _V )
)  ->  ( f " v )  ~~  v )
5250, 32, 51mpanr12 666 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( f : suc  v -1-1->
x  /\  x  e.  _V )  ->  ( f
" v )  ~~  v )
5348, 49, 52sylancl 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( f : suc  v -1-1-onto-> x  -> 
( f " v
)  ~~  v )
54 ensym 6910 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( f " v ) 
~~  v  ->  v  ~~  ( f " v
) )
5553, 54syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( f : suc  v -1-1-onto-> x  -> 
v  ~~  ( f " v ) )
5647, 55jctird 528 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( f : suc  v -1-1-onto-> x  -> 
( ( x  C_  A  /\  ( f "
v )  =/=  (/) )  -> 
( ( ( f
" v )  C_  A  /\  ( f "
v )  =/=  (/) )  /\  v  ~~  ( f "
v ) ) ) )
57 vex 2791 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  f  e. 
_V
58 imaexg 5026 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( f  e.  _V  ->  (
f " v )  e.  _V )
5957, 58ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( f
" v )  e. 
_V
60 sseq1 3199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( x  =  ( f "
v )  ->  (
x  C_  A  <->  ( f " v )  C_  A ) )
61 neeq1 2454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( x  =  ( f "
v )  ->  (
x  =/=  (/)  <->  ( f " v )  =/=  (/) ) )
6260, 61anbi12d 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( x  =  ( f "
v )  ->  (
( x  C_  A  /\  x  =/=  (/) )  <->  ( (
f " v ) 
C_  A  /\  (
f " v )  =/=  (/) ) ) )
63 breq2 4027 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( x  =  ( f "
v )  ->  (
v  ~~  x  <->  v  ~~  ( f " v
) ) )
6462, 63anbi12d 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( x  =  ( f "
v )  ->  (
( ( x  C_  A  /\  x  =/=  (/) )  /\  v  ~~  x )  <->  ( (
( f " v
)  C_  A  /\  ( f " v
)  =/=  (/) )  /\  v  ~~  ( f "
v ) ) ) )
65 inteq 3865 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( x  =  ( f "
v )  ->  |^| x  =  |^| ( f "
v ) )
6665eleq1d 2349 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( x  =  ( f "
v )  ->  ( |^| x  e.  A  <->  |^| ( f " v
)  e.  A ) )
6764, 66imbi12d 311 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( 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 ) ) )
6859, 67spcv 2874 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( A. x ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  v  ~~  x )  ->  |^| x  e.  A )  ->  (
( ( ( f
" v )  C_  A  /\  ( f "
v )  =/=  (/) )  /\  v  ~~  ( f "
v ) )  ->  |^| ( f " v
)  e.  A ) )
6956, 68sylan9 638 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( 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 ) )
70 ineq1 3363 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( z  =  |^| ( f
" v )  -> 
( z  i^i  w
)  =  ( |^| ( f " v
)  i^i  w )
)
7170eleq1d 2349 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( z  =  |^| ( f
" v )  -> 
( ( z  i^i  w )  e.  A  <->  (
|^| ( f "
v )  i^i  w
)  e.  A ) )
72 ineq2 3364 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( w  =  ( f `  v )  ->  ( |^| ( f " v
)  i^i  w )  =  ( |^| (
f " v )  i^i  ( f `  v ) ) )
7372eleq1d 2349 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( w  =  ( f `  v )  ->  (
( |^| ( f "
v )  i^i  w
)  e.  A  <->  ( |^| ( f " v
)  i^i  ( f `  v ) )  e.  A ) )
7471, 73rspc2v 2890 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
|^| ( 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
) )
7574ex 423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( |^| ( 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
) ) )
7669, 75syl6 29 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( 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
) ) ) )
7776com4r 80 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 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
) ) ) )
7877exp5c 599 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( 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 ) ) ) ) ) )
7978com14 82 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( 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 ) ) ) ) ) )
8079imp43 578 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( 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 ) ) )
8140, 80syl5bir 209 . . . . . . . . . . . . . . . . . . . . . . . 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 )  =  (/)  ->  ( ( f `
 v )  e.  A  ->  ( |^| ( f " v
)  i^i  ( f `  v ) )  e.  A ) ) )
82 inteq 3865 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( f " v )  =  (/)  ->  |^| (
f " v )  =  |^| (/) )
83 int0 3876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  |^| (/)  =  _V
8482, 83syl6eq 2331 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( f " v )  =  (/)  ->  |^| (
f " v )  =  _V )
8584ineq1d 3369 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( f " v )  =  (/)  ->  ( |^| ( f " v
)  i^i  ( f `  v ) )  =  ( _V  i^i  (
f `  v )
) )
86 ssv 3198 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( f `
 v )  C_  _V
87 sseqin2 3388 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( f `  v ) 
C_  _V  <->  ( _V  i^i  ( f `  v
) )  =  ( f `  v ) )
8886, 87mpbi 199 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( _V 
i^i  ( f `  v ) )  =  ( f `  v
)
8985, 88syl6eq 2331 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( f " v )  =  (/)  ->  ( |^| ( f " v
)  i^i  ( f `  v ) )  =  ( f `  v
) )
9089eleq1d 2349 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( f " v )  =  (/)  ->  ( (
|^| ( f "
v )  i^i  (
f `  v )
)  e.  A  <->  ( f `  v )  e.  A
) )
9190biimprd 214 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( f " v )  =  (/)  ->  ( ( f `  v )  e.  A  ->  ( |^| ( f " v
)  i^i  ( f `  v ) )  e.  A ) )
9281, 91pm2.61d2 152 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( 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
) )
9339, 92mpd 14 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( 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 )
94 fvex 5539 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( f `
 v )  e. 
_V
9594intunsn 3901 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  |^| (
( f " v
)  u.  { ( f `  v ) } )  =  (
|^| ( f "
v )  i^i  (
f `  v )
)
96 f1ofn 5473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( f : suc  v -1-1-onto-> x  -> 
f  Fn  suc  v
)
97 fnsnfv 5582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( f  Fn  suc  v  /\  v  e.  suc  v )  ->  { ( f `  v ) }  =  ( f
" { v } ) )
9896, 33, 97sylancl 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( f : suc  v -1-1-onto-> x  ->  { ( f `  v ) }  =  ( f " {
v } ) )
9998uneq2d 3329 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( f : suc  v -1-1-onto-> x  -> 
( ( f "
v )  u.  {
( f `  v
) } )  =  ( ( f "
v )  u.  (
f " { v } ) ) )
100 df-suc 4398 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  suc  v  =  ( v  u. 
{ v } )
101100imaeq2i 5010 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( f
" suc  v )  =  ( f "
( v  u.  {
v } ) )
102 imaundi 5093 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( f
" ( v  u. 
{ v } ) )  =  ( ( f " v )  u.  ( f " { v } ) )
103101, 102eqtr2i 2304 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( f " v )  u.  ( f " { v } ) )  =  ( f
" suc  v )
10499, 103syl6eq 2331 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( f : suc  v -1-1-onto-> x  -> 
( ( f "
v )  u.  {
( f `  v
) } )  =  ( f " suc  v ) )
105 f1ofo 5479 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( f : suc  v -1-1-onto-> x  -> 
f : suc  v -onto->
x )
106 foima 5456 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( f : suc  v -onto-> x  ->  ( f " suc  v )  =  x )
107105, 106syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( f : suc  v -1-1-onto-> x  -> 
( f " suc  v )  =  x )
108104, 107eqtrd 2315 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( f : suc  v -1-1-onto-> x  -> 
( ( f "
v )  u.  {
( f `  v
) } )  =  x )
109108inteqd 3867 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( f : suc  v -1-1-onto-> x  ->  |^| ( ( f "
v )  u.  {
( f `  v
) } )  = 
|^| x )
11095, 109syl5eqr 2329 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( f : suc  v -1-1-onto-> x  -> 
( |^| ( f "
v )  i^i  (
f `  v )
)  =  |^| x
)
111110eleq1d 2349 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( f : suc  v -1-1-onto-> x  -> 
( ( |^| (
f " v )  i^i  ( f `  v ) )  e.  A  <->  |^| x  e.  A
) )
112111ad2antlr 707 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( 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
) )
11393, 112mpbid 201 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( 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
)
114113exp43 595 . . . . . . . . . . . . . . . . . . . 20  |-  ( 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 ) ) ) )
115114exlimdv 1664 . . . . . . . . . . . . . . . . . . 19  |-  ( 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
) ) ) )
11630, 115syl5bi 208 . . . . . . . . . . . . . . . . . 18  |-  ( 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 ) ) ) )
117116imp 418 . . . . . . . . . . . . . . . . 17  |-  ( ( 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
) ) )
118117adantlr 695 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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
) ) )
119118com13 74 . . . . . . . . . . . . . . 15  |-  ( 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
) ) )
12028, 29, 119alrimd 1749 . . . . . . . . . . . . . 14  |-  ( 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
) ) )
121120a1i 10 . . . . . . . . . . . . 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
) ) ) )
1226, 10, 14, 27, 121finds2 4684 . . . . . . . . . . . 12  |-  ( 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 ) ) )
123 sp 1716 . . . . . . . . . . . 12  |-  ( A. x ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  y  ~~  x )  ->  |^| x  e.  A )  ->  (
( ( x  C_  A  /\  x  =/=  (/) )  /\  y  ~~  x )  ->  |^| x  e.  A
) )
124122, 123syl6 29 . . . . . . . . . . 11  |-  ( 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 ) ) )
125124exp4a 589 . . . . . . . . . 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
) ) ) )
126125com24 81 . . . . . . . . 9  |-  ( 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
) ) ) )
1272, 126syl5 28 . . . . . . . 8  |-  ( 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
) ) ) )
128127rexlimiv 2661 . . . . . . 7  |-  ( 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
) ) )
1291, 128sylbi 187 . . . . . 6  |-  ( x  e.  Fin  ->  (
( x  C_  A  /\  x  =/=  (/) )  -> 
( A. z  e.  A  A. w  e.  A  ( z  i^i  w )  e.  A  ->  |^| x  e.  A
) ) )
130129com13 74 . . . . 5  |-  ( A. z  e.  A  A. w  e.  A  (
z  i^i  w )  e.  A  ->  ( ( x  C_  A  /\  x  =/=  (/) )  ->  (
x  e.  Fin  ->  |^| x  e.  A ) ) )
131130imp3a 420 . . . 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
) )
132131alrimiv 1617 . . 3  |-  ( 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 ) )
133 zfpair2 4215 . . . . . 6  |-  { z ,  w }  e.  _V
134 sseq1 3199 . . . . . . . . 9  |-  ( x  =  { z ,  w }  ->  (
x  C_  A  <->  { z ,  w }  C_  A
) )
135 neeq1 2454 . . . . . . . . 9  |-  ( x  =  { z ,  w }  ->  (
x  =/=  (/)  <->  { z ,  w }  =/=  (/) ) )
136134, 135anbi12d 691 . . . . . . . 8  |-  ( x  =  { z ,  w }  ->  (
( x  C_  A  /\  x  =/=  (/) )  <->  ( {
z ,  w }  C_  A  /\  { z ,  w }  =/=  (/) ) ) )
137 eleq1 2343 . . . . . . . 8  |-  ( x  =  { z ,  w }  ->  (
x  e.  Fin  <->  { z ,  w }  e.  Fin ) )
138136, 137anbi12d 691 . . . . . . 7  |-  ( x  =  { z ,  w }  ->  (
( ( x  C_  A  /\  x  =/=  (/) )  /\  x  e.  Fin )  <->  ( ( { z ,  w }  C_  A  /\  { z ,  w }  =/=  (/) )  /\  {
z ,  w }  e.  Fin ) ) )
139 inteq 3865 . . . . . . . 8  |-  ( x  =  { z ,  w }  ->  |^| x  =  |^| { z ,  w } )
140139eleq1d 2349 . . . . . . 7  |-  ( x  =  { z ,  w }  ->  ( |^| x  e.  A  <->  |^|
{ z ,  w }  e.  A )
)
141138, 140imbi12d 311 . . . . . 6  |-  ( x  =  { z ,  w }  ->  (
( ( ( x 
C_  A  /\  x  =/=  (/) )  /\  x  e.  Fin )  ->  |^| x  e.  A )  <->  ( (
( { z ,  w }  C_  A  /\  { z ,  w }  =/=  (/) )  /\  {
z ,  w }  e.  Fin )  ->  |^| { z ,  w }  e.  A ) ) )
142133, 141spcv 2874 . . . . 5  |-  ( A. x ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  x  e.  Fin )  ->  |^| x  e.  A )  ->  (
( ( { z ,  w }  C_  A  /\  { z ,  w }  =/=  (/) )  /\  { z ,  w }  e.  Fin )  ->  |^| { z ,  w }  e.  A ) )
143 vex 2791 . . . . . . 7  |-  z  e. 
_V
144 vex 2791 . . . . . . 7  |-  w  e. 
_V
145143, 144prss 3769 . . . . . 6  |-  ( ( z  e.  A  /\  w  e.  A )  <->  { z ,  w }  C_  A )
146143prnz 3745 . . . . . . 7  |-  { z ,  w }  =/=  (/)
147146biantru 491 . . . . . 6  |-  ( { z ,  w }  C_  A  <->  ( { z ,  w }  C_  A  /\  { z ,  w }  =/=  (/) ) )
148 prfi 7131 . . . . . . 7  |-  { z ,  w }  e.  Fin
149148biantru 491 . . . . . 6  |-  ( ( { z ,  w }  C_  A  /\  {
z ,  w }  =/=  (/) )  <->  ( ( { z ,  w }  C_  A  /\  {
z ,  w }  =/=  (/) )  /\  {
z ,  w }  e.  Fin ) )
150145, 147, 1493bitrri 263 . . . . 5  |-  ( ( ( { z ,  w }  C_  A  /\  { z ,  w }  =/=  (/) )  /\  {
z ,  w }  e.  Fin )  <->  ( z  e.  A  /\  w  e.  A ) )
151143, 144intpr 3895 . . . . . 6  |-  |^| { z ,  w }  =  ( z  i^i  w
)
152151eleq1i 2346 . . . . 5  |-  ( |^| { z ,  w }  e.  A  <->  ( z  i^i  w )  e.  A
)
153142, 150, 1523imtr3g 260 . . . 4  |-  ( A. x ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  x  e.  Fin )  ->  |^| x  e.  A )  ->  (
( z  e.  A  /\  w  e.  A
)  ->  ( z  i^i  w )  e.  A
) )
154153ralrimivv 2634 . . 3  |-  ( A. x ( ( ( x  C_  A  /\  x  =/=  (/) )  /\  x  e.  Fin )  ->  |^| x  e.  A )  ->  A. z  e.  A  A. w  e.  A  ( z  i^i  w )  e.  A
)
155132, 154impbii 180 . 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
) )
156 ineq1 3363 . . . 4  |-  ( x  =  z  ->  (
x  i^i  y )  =  ( z  i^i  y ) )
157156eleq1d 2349 . . 3  |-  ( x  =  z  ->  (
( x  i^i  y
)  e.  A  <->  ( z  i^i  y )  e.  A
) )
158 ineq2 3364 . . . 4  |-  ( y  =  w  ->  (
z  i^i  y )  =  ( z  i^i  w ) )
159158eleq1d 2349 . . 3  |-  ( y  =  w  ->  (
( z  i^i  y
)  e.  A  <->  ( z  i^i  w )  e.  A
) )
160157, 159cbvral2v 2772 . 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 )
161 df-3an 936 . . . 4  |-  ( ( x  C_  A  /\  x  =/=  (/)  /\  x  e. 
Fin )  <->  ( (
x  C_  A  /\  x  =/=  (/) )  /\  x  e.  Fin ) )
162161imbi1i 315 . . 3  |-  ( ( ( x  C_  A  /\  x  =/=  (/)  /\  x  e.  Fin )  ->  |^| x  e.  A )  <->  ( (
( x  C_  A  /\  x  =/=  (/) )  /\  x  e.  Fin )  ->  |^| x  e.  A
) )
163162albii 1553 . 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 ) )
164155, 160, 1633bitr4i 268 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    <-> wb 176    /\ wa 358    /\ w3a 934   A.wal 1527   E.wex 1528    = wceq 1623    e. wcel 1684    =/= wne 2446   A.wral 2543   E.wrex 2544   _Vcvv 2788    u. cun 3150    i^i cin 3151    C_ wss 3152   (/)c0 3455   {csn 3640   {cpr 3641   |^|cint 3862   class class class wbr 4023   suc csuc 4394   omcom 4656   `'ccnv 4688   ran crn 4690   "cima 4692   Fun wfun 5249    Fn wfn 5250   -->wf 5251   -1-1->wf1 5252   -onto->wfo 5253   -1-1-onto->wf1o 5254   ` cfv 5255    ~~ cen 6860   Fincfn 6863
This theorem is referenced by:  dffi2  7176  istop2g  16642  istps4OLD  16661  neificl  26467
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-reu 2550  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pss 3168  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-tp 3648  df-op 3649  df-uni 3828  df-int 3863  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-tr 4114  df-eprel 4305  df-id 4309  df-po 4314  df-so 4315  df-fr 4352  df-we 4354  df-ord 4395  df-on 4396  df-lim 4397  df-suc 4398  df-om 4657  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-recs 6388  df-rdg 6423  df-1o 6479  df-oadd 6483  df-er 6660  df-en 6864  df-fin 6867
  Copyright terms: Public domain W3C validator