Step |
Hyp |
Ref |
Expression |
1 |
|
iundisjf.1 |
|- F/_ k A |
2 |
|
iundisjf.2 |
|- F/_ n B |
3 |
|
iundisjf.3 |
|- ( n = k -> A = B ) |
4 |
|
ssrab2 |
|- { n e. NN | x e. A } C_ NN |
5 |
|
nnuz |
|- NN = ( ZZ>= ` 1 ) |
6 |
4 5
|
sseqtri |
|- { n e. NN | x e. A } C_ ( ZZ>= ` 1 ) |
7 |
|
rabn0 |
|- ( { n e. NN | x e. A } =/= (/) <-> E. n e. NN x e. A ) |
8 |
7
|
biimpri |
|- ( E. n e. NN x e. A -> { n e. NN | x e. A } =/= (/) ) |
9 |
|
infssuzcl |
|- ( ( { n e. NN | x e. A } C_ ( ZZ>= ` 1 ) /\ { n e. NN | x e. A } =/= (/) ) -> inf ( { n e. NN | x e. A } , RR , < ) e. { n e. NN | x e. A } ) |
10 |
6 8 9
|
sylancr |
|- ( E. n e. NN x e. A -> inf ( { n e. NN | x e. A } , RR , < ) e. { n e. NN | x e. A } ) |
11 |
|
nfrab1 |
|- F/_ n { n e. NN | x e. A } |
12 |
|
nfcv |
|- F/_ n RR |
13 |
|
nfcv |
|- F/_ n < |
14 |
11 12 13
|
nfinf |
|- F/_ n inf ( { n e. NN | x e. A } , RR , < ) |
15 |
|
nfcv |
|- F/_ n NN |
16 |
14
|
nfcsb1 |
|- F/_ n [_ inf ( { n e. NN | x e. A } , RR , < ) / n ]_ A |
17 |
16
|
nfcri |
|- F/ n x e. [_ inf ( { n e. NN | x e. A } , RR , < ) / n ]_ A |
18 |
|
csbeq1a |
|- ( n = inf ( { n e. NN | x e. A } , RR , < ) -> A = [_ inf ( { n e. NN | x e. A } , RR , < ) / n ]_ A ) |
19 |
18
|
eleq2d |
|- ( n = inf ( { n e. NN | x e. A } , RR , < ) -> ( x e. A <-> x e. [_ inf ( { n e. NN | x e. A } , RR , < ) / n ]_ A ) ) |
20 |
14 15 17 19
|
elrabf |
|- ( inf ( { n e. NN | x e. A } , RR , < ) e. { n e. NN | x e. A } <-> ( inf ( { n e. NN | x e. A } , RR , < ) e. NN /\ x e. [_ inf ( { n e. NN | x e. A } , RR , < ) / n ]_ A ) ) |
21 |
10 20
|
sylib |
|- ( E. n e. NN x e. A -> ( inf ( { n e. NN | x e. A } , RR , < ) e. NN /\ x e. [_ inf ( { n e. NN | x e. A } , RR , < ) / n ]_ A ) ) |
22 |
21
|
simpld |
|- ( E. n e. NN x e. A -> inf ( { n e. NN | x e. A } , RR , < ) e. NN ) |
23 |
21
|
simprd |
|- ( E. n e. NN x e. A -> x e. [_ inf ( { n e. NN | x e. A } , RR , < ) / n ]_ A ) |
24 |
22
|
nnred |
|- ( E. n e. NN x e. A -> inf ( { n e. NN | x e. A } , RR , < ) e. RR ) |
25 |
24
|
ltnrd |
|- ( E. n e. NN x e. A -> -. inf ( { n e. NN | x e. A } , RR , < ) < inf ( { n e. NN | x e. A } , RR , < ) ) |
26 |
|
eliun |
|- ( x e. U_ k e. ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) B <-> E. k e. ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) x e. B ) |
27 |
|
nfcv |
|- F/_ k NN |
28 |
1
|
nfcri |
|- F/ k x e. A |
29 |
27 28
|
nfrex |
|- F/ k E. n e. NN x e. A |
30 |
28 27
|
nfrabw |
|- F/_ k { n e. NN | x e. A } |
31 |
|
nfcv |
|- F/_ k RR |
32 |
|
nfcv |
|- F/_ k < |
33 |
30 31 32
|
nfinf |
|- F/_ k inf ( { n e. NN | x e. A } , RR , < ) |
34 |
33 32 33
|
nfbr |
|- F/ k inf ( { n e. NN | x e. A } , RR , < ) < inf ( { n e. NN | x e. A } , RR , < ) |
35 |
24
|
ad2antrr |
|- ( ( ( E. n e. NN x e. A /\ k e. ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) ) /\ x e. B ) -> inf ( { n e. NN | x e. A } , RR , < ) e. RR ) |
36 |
|
elfzouz |
|- ( k e. ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) -> k e. ( ZZ>= ` 1 ) ) |
37 |
36 5
|
eleqtrrdi |
|- ( k e. ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) -> k e. NN ) |
38 |
37
|
ad2antlr |
|- ( ( ( E. n e. NN x e. A /\ k e. ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) ) /\ x e. B ) -> k e. NN ) |
39 |
38
|
nnred |
|- ( ( ( E. n e. NN x e. A /\ k e. ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) ) /\ x e. B ) -> k e. RR ) |
40 |
|
simpr |
|- ( ( ( E. n e. NN x e. A /\ k e. ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) ) /\ x e. B ) -> x e. B ) |
41 |
|
nfcv |
|- F/_ n k |
42 |
2
|
nfcri |
|- F/ n x e. B |
43 |
3
|
eleq2d |
|- ( n = k -> ( x e. A <-> x e. B ) ) |
44 |
41 15 42 43
|
elrabf |
|- ( k e. { n e. NN | x e. A } <-> ( k e. NN /\ x e. B ) ) |
45 |
38 40 44
|
sylanbrc |
|- ( ( ( E. n e. NN x e. A /\ k e. ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) ) /\ x e. B ) -> k e. { n e. NN | x e. A } ) |
46 |
|
infssuzle |
|- ( ( { n e. NN | x e. A } C_ ( ZZ>= ` 1 ) /\ k e. { n e. NN | x e. A } ) -> inf ( { n e. NN | x e. A } , RR , < ) <_ k ) |
47 |
6 45 46
|
sylancr |
|- ( ( ( E. n e. NN x e. A /\ k e. ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) ) /\ x e. B ) -> inf ( { n e. NN | x e. A } , RR , < ) <_ k ) |
48 |
|
elfzolt2 |
|- ( k e. ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) -> k < inf ( { n e. NN | x e. A } , RR , < ) ) |
49 |
48
|
ad2antlr |
|- ( ( ( E. n e. NN x e. A /\ k e. ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) ) /\ x e. B ) -> k < inf ( { n e. NN | x e. A } , RR , < ) ) |
50 |
35 39 35 47 49
|
lelttrd |
|- ( ( ( E. n e. NN x e. A /\ k e. ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) ) /\ x e. B ) -> inf ( { n e. NN | x e. A } , RR , < ) < inf ( { n e. NN | x e. A } , RR , < ) ) |
51 |
50
|
exp31 |
|- ( E. n e. NN x e. A -> ( k e. ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) -> ( x e. B -> inf ( { n e. NN | x e. A } , RR , < ) < inf ( { n e. NN | x e. A } , RR , < ) ) ) ) |
52 |
29 34 51
|
rexlimd |
|- ( E. n e. NN x e. A -> ( E. k e. ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) x e. B -> inf ( { n e. NN | x e. A } , RR , < ) < inf ( { n e. NN | x e. A } , RR , < ) ) ) |
53 |
26 52
|
syl5bi |
|- ( E. n e. NN x e. A -> ( x e. U_ k e. ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) B -> inf ( { n e. NN | x e. A } , RR , < ) < inf ( { n e. NN | x e. A } , RR , < ) ) ) |
54 |
25 53
|
mtod |
|- ( E. n e. NN x e. A -> -. x e. U_ k e. ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) B ) |
55 |
23 54
|
eldifd |
|- ( E. n e. NN x e. A -> x e. ( [_ inf ( { n e. NN | x e. A } , RR , < ) / n ]_ A \ U_ k e. ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) B ) ) |
56 |
|
csbeq1 |
|- ( m = inf ( { n e. NN | x e. A } , RR , < ) -> [_ m / n ]_ A = [_ inf ( { n e. NN | x e. A } , RR , < ) / n ]_ A ) |
57 |
33
|
nfeq2 |
|- F/ k m = inf ( { n e. NN | x e. A } , RR , < ) |
58 |
|
nfcv |
|- F/_ k ( 1 ..^ m ) |
59 |
|
nfcv |
|- F/_ k 1 |
60 |
|
nfcv |
|- F/_ k ..^ |
61 |
59 60 33
|
nfov |
|- F/_ k ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) |
62 |
|
oveq2 |
|- ( m = inf ( { n e. NN | x e. A } , RR , < ) -> ( 1 ..^ m ) = ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) ) |
63 |
|
eqidd |
|- ( m = inf ( { n e. NN | x e. A } , RR , < ) -> B = B ) |
64 |
57 58 61 62 63
|
iuneq12df |
|- ( m = inf ( { n e. NN | x e. A } , RR , < ) -> U_ k e. ( 1 ..^ m ) B = U_ k e. ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) B ) |
65 |
56 64
|
difeq12d |
|- ( m = inf ( { n e. NN | x e. A } , RR , < ) -> ( [_ m / n ]_ A \ U_ k e. ( 1 ..^ m ) B ) = ( [_ inf ( { n e. NN | x e. A } , RR , < ) / n ]_ A \ U_ k e. ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) B ) ) |
66 |
65
|
eleq2d |
|- ( m = inf ( { n e. NN | x e. A } , RR , < ) -> ( x e. ( [_ m / n ]_ A \ U_ k e. ( 1 ..^ m ) B ) <-> x e. ( [_ inf ( { n e. NN | x e. A } , RR , < ) / n ]_ A \ U_ k e. ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) B ) ) ) |
67 |
66
|
rspcev |
|- ( ( inf ( { n e. NN | x e. A } , RR , < ) e. NN /\ x e. ( [_ inf ( { n e. NN | x e. A } , RR , < ) / n ]_ A \ U_ k e. ( 1 ..^ inf ( { n e. NN | x e. A } , RR , < ) ) B ) ) -> E. m e. NN x e. ( [_ m / n ]_ A \ U_ k e. ( 1 ..^ m ) B ) ) |
68 |
22 55 67
|
syl2anc |
|- ( E. n e. NN x e. A -> E. m e. NN x e. ( [_ m / n ]_ A \ U_ k e. ( 1 ..^ m ) B ) ) |
69 |
|
nfv |
|- F/ m x e. ( A \ U_ k e. ( 1 ..^ n ) B ) |
70 |
|
nfcsb1v |
|- F/_ n [_ m / n ]_ A |
71 |
|
nfcv |
|- F/_ n ( 1 ..^ m ) |
72 |
71 2
|
nfiun |
|- F/_ n U_ k e. ( 1 ..^ m ) B |
73 |
70 72
|
nfdif |
|- F/_ n ( [_ m / n ]_ A \ U_ k e. ( 1 ..^ m ) B ) |
74 |
73
|
nfcri |
|- F/ n x e. ( [_ m / n ]_ A \ U_ k e. ( 1 ..^ m ) B ) |
75 |
|
csbeq1a |
|- ( n = m -> A = [_ m / n ]_ A ) |
76 |
|
oveq2 |
|- ( n = m -> ( 1 ..^ n ) = ( 1 ..^ m ) ) |
77 |
76
|
iuneq1d |
|- ( n = m -> U_ k e. ( 1 ..^ n ) B = U_ k e. ( 1 ..^ m ) B ) |
78 |
75 77
|
difeq12d |
|- ( n = m -> ( A \ U_ k e. ( 1 ..^ n ) B ) = ( [_ m / n ]_ A \ U_ k e. ( 1 ..^ m ) B ) ) |
79 |
78
|
eleq2d |
|- ( n = m -> ( x e. ( A \ U_ k e. ( 1 ..^ n ) B ) <-> x e. ( [_ m / n ]_ A \ U_ k e. ( 1 ..^ m ) B ) ) ) |
80 |
69 74 79
|
cbvrexw |
|- ( E. n e. NN x e. ( A \ U_ k e. ( 1 ..^ n ) B ) <-> E. m e. NN x e. ( [_ m / n ]_ A \ U_ k e. ( 1 ..^ m ) B ) ) |
81 |
68 80
|
sylibr |
|- ( E. n e. NN x e. A -> E. n e. NN x e. ( A \ U_ k e. ( 1 ..^ n ) B ) ) |
82 |
|
eldifi |
|- ( x e. ( A \ U_ k e. ( 1 ..^ n ) B ) -> x e. A ) |
83 |
82
|
reximi |
|- ( E. n e. NN x e. ( A \ U_ k e. ( 1 ..^ n ) B ) -> E. n e. NN x e. A ) |
84 |
81 83
|
impbii |
|- ( E. n e. NN x e. A <-> E. n e. NN x e. ( A \ U_ k e. ( 1 ..^ n ) B ) ) |
85 |
|
eliun |
|- ( x e. U_ n e. NN A <-> E. n e. NN x e. A ) |
86 |
|
eliun |
|- ( x e. U_ n e. NN ( A \ U_ k e. ( 1 ..^ n ) B ) <-> E. n e. NN x e. ( A \ U_ k e. ( 1 ..^ n ) B ) ) |
87 |
84 85 86
|
3bitr4i |
|- ( x e. U_ n e. NN A <-> x e. U_ n e. NN ( A \ U_ k e. ( 1 ..^ n ) B ) ) |
88 |
87
|
eqriv |
|- U_ n e. NN A = U_ n e. NN ( A \ U_ k e. ( 1 ..^ n ) B ) |